Core Definitions for the Vlasov-Maxwell-Landau System

Defines the Landau collision operator, velocity decay conditions, the VMLSteadyState structure, and the FlatTorus3 typeclass. Also provides @[simp] unfolding lemmas and small auxiliary lemmas about the definitions. Derived FlatTorus3 lemmas are in FlatTorus3Lemmas.lean.

def VML.normSq (z : Fin 3 → ℝ) : ℝ

Squared Euclidean norm: ‖z‖² = z · z = ∑ᵢ zᵢ²

Equations

• VML.normSq z = z ⬝ᵥ z

@[simp]

theorem VML.normSq_zero : normSq 0 = 0

theorem VML.normSq_nonneg (z : Fin 3 → ℝ) : 0 ≤ normSq z

theorem VML.normSq_eq_zero {z : Fin 3 → ℝ} : normSq z = 0 ↔ z = 0

theorem VML.normSq_pos {z : Fin 3 → ℝ} (hz : z ≠ 0) : 0 < normSq z

theorem VML.normSq_neg (z : Fin 3 → ℝ) : normSq (-z) = normSq z

def VML.eucNorm (z : Fin 3 → ℝ) : ℝ

Euclidean norm: |z| = √(z · z)

Equations

• VML.eucNorm z = √(VML.normSq z)

theorem VML.eucNorm_nonneg (z : Fin 3 → ℝ) : 0 ≤ eucNorm z

theorem VML.eucNorm_neg (z : Fin 3 → ℝ) : eucNorm (-z) = eucNorm z

theorem VML.eucNorm_sq (z : Fin 3 → ℝ) : eucNorm z ^ 2 = normSq z

def VML.innerLandauMatrix (z : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The inner part of the Landau matrix: B(z) = |z|² I₃ - z zᵀ. This is the matrix that appears inside the scalar factor Ψ(|z|).

Equations

• VML.innerLandauMatrix z = VML.normSq z • 1 - Matrix.vecMulVec z z

def VML.landauMatrix (Ψ : ℝ → ℝ) (z : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The Landau collision matrix: A(z) = Ψ(|z|) · (|z|² I₃ - z zᵀ). Reference: Definition 2 (def:landau_matrix)

Equations

• VML.landauMatrix Ψ z = Ψ (VML.eucNorm z) • VML.innerLandauMatrix z

theorem VML.innerLandauMatrix_apply (z : Fin 3 → ℝ) (i j : Fin 3) : innerLandauMatrix z i j = (if i = j then normSq z else 0) - z i * z j

def VML.IsMaxwellian (f : (Fin 3 → ℝ) → ℝ) : Prop

A Maxwellian distribution: log-quadratic with c₀ < 0 (ensuring integrability). Specifically: ∃ a₀ b c₀, c₀ < 0 ∧ f(v) = exp(a₀ + b · v + c₀ |v|²)

Equations

• VML.IsMaxwellian f = ∃ (a₀ : ℝ) (b : Fin 3 → ℝ), ∃ c₀ < 0, ∀ (v : Fin 3 → ℝ), f v = Real.exp (a₀ + b ⬝ᵥ v + c₀ * VML.normSq v)

theorem VML.IsMaxwellian_params_injective (a₀ a₀' : ℝ) (b b' : Fin 3 → ℝ) (c₀ c₀' : ℝ) (h : ∀ (v : Fin 3 → ℝ), a₀ + b ⬝ᵥ v + c₀ * normSq v = a₀' + b' ⬝ᵥ v + c₀' * normSq v) : a₀ = a₀' ∧ b = b' ∧ c₀ = c₀'

The Maxwellian parameters (a₀, b, c₀) are injective: if exp(a₀ + b·v + c₀|v|²) = exp(a₀' + b'·v + c₀'|v|²) for all v, then a₀ = a₀', b = b', c₀ = c₀'.

theorem VML.IsMaxwellian.pos {f : (Fin 3 → ℝ) → ℝ} (hM : IsMaxwellian f) (v : Fin 3 → ℝ) : 0 < f v

A Maxwellian distribution is strictly positive everywhere.

theorem VML.IsMaxwellian.contDiff {f : (Fin 3 → ℝ) → ℝ} (hM : IsMaxwellian f) : ContDiff ℝ ⊤ f

A Maxwellian distribution is smooth (C^∞).

def VML.equilibriumMaxwellian (ρ_ion T : ℝ) (v : Fin 3 → ℝ) : ℝ

The equilibrium Maxwellian (zero drift, density = ρ_ion): f∞(v) = ρ_ion/(2πT∞)^(3/2) · exp(-|v|²/(2T∞))

Equations

• VML.equilibriumMaxwellian ρ_ion T v = ρ_ion / (2 * Real.pi * T) ^ (3 / 2) * Real.exp (-VML.normSq v / (2 * T))

theorem VML.equilibriumMaxwellian_isMaxwellian (ρ T : ℝ) (hρ : 0 < ρ) (hT : 0 < T) : IsMaxwellian (equilibriumMaxwellian ρ T)

The equilibrium Maxwellian is a Maxwellian (i.e., satisfies IsMaxwellian). Rewrites ρ/(2πT)^{3/2} · exp(-|v|²/(2T)) = exp(log(ρ/(2πT)^{3/2}) + 0·v + (-1/(2T))|v|²).

theorem VML.equilibriumMaxwellian_T_injective (ρ T₁ T₂ : ℝ) (hρ : 0 < ρ) (hT₁ : 0 < T₁) (hT₂ : 0 < T₂) (h : ∀ (v : Fin 3 → ℝ), equilibriumMaxwellian ρ T₁ v = equilibriumMaxwellian ρ T₂ v) : T₁ = T₂

The equilibrium temperature T is an injective parameter: if two Maxwellians with the same density agree as functions, their temperatures must be equal.

theorem VML.equilibriumMaxwellian_pos (ρ T : ℝ) (hρ : 0 < ρ) (hT : 0 < T) (v : Fin 3 → ℝ) : 0 < equilibriumMaxwellian ρ T v

The equilibrium Maxwellian is strictly positive for ρ > 0, T > 0.

def VML.vGrad (f : (Fin 3 → ℝ) → ℝ) (v : Fin 3 → ℝ) : Fin 3 → ℝ

Velocity gradient: ∇ᵥf(v), the vector of partial derivatives of f at v. Uses Fréchet derivative from Mathlib.

Equations

• VML.vGrad f v i = (fderiv ℝ f v) (Pi.single i 1)

def VML.vDiv (F : (Fin 3 → ℝ) → Fin 3 → ℝ) (v : Fin 3 → ℝ) : ℝ

Velocity divergence: ∇ᵥ · F(v) = ∑ᵢ ∂Fᵢ/∂vᵢ

Equations

• VML.vDiv F v = ∑ i : Fin 3, (fderiv ℝ (fun (w : Fin 3 → ℝ) => F w i) v) (Pi.single i 1)

def VML.cross (a b : Fin 3 → ℝ) : Fin 3 → ℝ

Cross product in ℝ³: a × b

Equations

• VML.cross a b = ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]

theorem VML.velocity_ibp (F : (Fin 3 → ℝ) → Fin 3 → ℝ) (g : (Fin 3 → ℝ) → ℝ) (hF_diff : ∀ (i : Fin 3), Differentiable ℝ fun (v : Fin 3 → ℝ) => F v i) (hg_diff : Differentiable ℝ g) (h_int_df_g : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (fderiv ℝ (fun (w : Fin 3 → ℝ) => F w i) v) (Pi.single i 1) * g v) MeasureTheory.volume) (h_int_f_dg : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => F v i * (fderiv ℝ g v) (Pi.single i 1)) MeasureTheory.volume) (h_int_fg : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => F v i * g v) MeasureTheory.volume) : ∫ (v : Fin 3 → ℝ), vDiv F v * g v = -∫ (v : Fin 3 → ℝ), F v ⬝ᵥ vGrad g v

Velocity-space integration by parts on ℝ³. ∫ (∇ᵥ · F)(v) · g(v) dv = -∫ F(v) · (∇ᵥg)(v) dv.

Uses Mathlib's integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable (n-dimensional IBP for Fréchet derivatives) applied per component.

The three per-component integrability hypotheses (derivative·g, f·derivative, and f·g) are the natural conditions for Bochner-integral IBP.

def VML.LandauOperator (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (v : Fin 3 → ℝ) : ℝ

The Landau collision operator Q(f,f)(v). Reference: Definition 3 (def:landau_operator)

Q(f,f)(v) = ∇ᵥ · ∫_{ℝ³} A(v-w) [f(w)∇ᵥf(v) - f(v)∇_wf(w)] dw

Equations

• VML.LandauOperator Ψ f v = VML.vDiv (fun (v' : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), (VML.landauMatrix Ψ (v' - w)).mulVec (f w • VML.vGrad f v' - f v' • VML.vGrad f w)) v

def VML.entropyDissipation (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) : ℝ

The entropy dissipation functional: D(f) = ∫ Q(f,f)(v) log f(v) dv. Reference: Definition in Lemma 5 (lem:entropy_dissipation)

Equations

• VML.entropyDissipation Ψ f = ∫ (v : Fin 3 → ℝ), VML.LandauOperator Ψ f v * Real.log (f v)

theorem VML.landau_ibp (Ψ : ℝ → ℝ) (g : (Fin 3 → ℝ) → ℝ) (hg_pos : ∀ (v : Fin 3 → ℝ), 0 < g v) (hg_smooth : ContDiff ℝ 3 g) (_hg_int : MeasureTheory.Integrable g MeasureTheory.volume) (hFlux_diff : ∀ (i : Fin 3), Differentiable ℝ fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v - w)).mulVec (g w • vGrad g v - g v • vGrad g w)) i) (h_int_df_g : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (fderiv ℝ (fun (v' : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v' - w)).mulVec (g w • vGrad g v' - g v' • vGrad g w)) i) v) (Pi.single i 1) * (Real.log ∘ g) v) MeasureTheory.volume) (h_int_f_dg : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v - w)).mulVec (g w • vGrad g v - g v • vGrad g w)) i * (fderiv ℝ (Real.log ∘ g) v) (Pi.single i 1)) MeasureTheory.volume) (h_int_fg : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v - w)).mulVec (g w • vGrad g v - g v • vGrad g w)) i * (Real.log ∘ g) v) MeasureTheory.volume) (hFlux_int : ∀ (v : Fin 3 → ℝ), MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => (landauMatrix Ψ (v - w)).mulVec (g w • vGrad g v - g v • vGrad g w)) MeasureTheory.volume) : ∫ (v : Fin 3 → ℝ), LandauOperator Ψ g v * (Real.log ∘ g) v = -∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), vGrad (Real.log ∘ g) v ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (g w • vGrad g v - g v • vGrad g w)

IBP for the Landau collision operator: ∫ Q(g,g)(v) · log g(v) dv equals the symmetrized weak form. Combines velocity-space IBP (∫ div F · g = -∫ F · ∇g) with dotProduct_integral_comm (pulling the w-integral through the dot product).

The integrability hypotheses on the Landau flux are the natural conditions for Bochner-integral IBP. They require the flux F(v) = ∫_w A(v-w)[...] dw and its derivatives to be integrable against log g — this holds for distributions with sufficient velocity-space decay (e.g., sub-Gaussian tails).

def VML.PSDIntegrand (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (v w : Fin 3 → ℝ) : ℝ

The PSD integrand: g(v,w) = f(v)·f(w)·⟨Δ(v,w), A(v-w) Δ(v,w)⟩ where Δ(v,w) = ∇log f(v) - ∇log f(w). This appears in the entropy dissipation formula (Lemma 5).

Equations

• One or more equations did not get rendered due to their size.

theorem VML.neg_cross (a b : Fin 3 → ℝ) : -cross a b = cross b a

Cross product antisymmetry: -cross a b = cross b a.

theorem VML.cross_smul_left (c : ℝ) (a b : Fin 3 → ℝ) : cross (c • a) b = c • cross a b

theorem VML.cross_zero_left (b : Fin 3 → ℝ) : cross 0 b = 0

Helper: cross product with zero first argument

theorem VML.vecMulVec_self_mulVec (z w : Fin 3 → ℝ) : (Matrix.vecMulVec z z).mulVec w = (z ⬝ᵥ w) • z

Helper: (vecMulVec z z) *ᵥ w = (z · w) • z

class VML.FlatTorus3 (X : Type u_1) extends MeasureTheory.MeasureSpace X, TopologicalSpace X : Type u_1

Abstract characterization of a flat 3-torus with differential operators.

The spatial domain X is a compact nonempty space equipped with a MeasureSpace instance (providing a canonical measure for integration via Mathlib's ∫) and abstract differential operators (grad, div, curl).

These axioms are satisfied by any flat compact Riemannian 3-manifold without boundary (e.g. T³ = ℝ³/ℤ³) equipped with its standard differential operators and Riemannian volume form. See TorusInstance.lean for a concrete instance on Fin 3 → AddCircle 1.

Axiom design note: The linear operator axioms (hGradAdd, hGradScalarMul, hDivLinear) are stated universally (for all functions X → ℝ) because linearity of fderiv genuinely holds for all functions: fderiv(c * f) = c * fderiv(f) is true even for non-differentiable f (both sides are 0 by definition).

The chain rule axiom (hGradChainExp) requires IsSpatiallySmooth ⊤ φ: without it, on the concrete torus both sides collapse to 0 via fderiv's junk value, making the axiom vacuously true rather than expressing a genuine chain rule.

hSpatialVelocityFubini requires joint integrability of uncurried F; the concrete instance (TorusInstance) provides it via Mathlib's integral_integral_swap. hSpatialAdd requires integrability of both summands (honest: Mathlib's integral_add). hGradIntegrable provides integrability of gradient components for spatially differentiable functions (on torus: C¹ → continuous → integrable on compact).

Integration uses Mathlib's ∫ x, f x (Bochner integral over volume).

Property fields (23):

• Operator properties (5): hDivLinear, hGradConst, hGradAdd, hGradScalarMul, hGradChainExp
• Closed manifold integration (2): hCurlIntZero, hIBP_spatial
• Analysis on compact manifold (4): hHarmonic_const, hLaplacianMaxNonpos, hSpatialPos, hSpatialNonnegZero
• Flat geometry (2): hKillingToHarmonic, hCurlZeroDivZeroHarmonic
• Abstract measure (3): hSpatialVelocityFubini, hSpatialAdd, hGradIntegrable
• Differentiability predicate + closure (7): IsSpatiallySmooth ⊤, hDiff_const ⊤, hDiff_add ⊤, hDiff_smul ⊤, hDiff_log ⊤, hDiff_continuous ⊤, hDiff_grad ⊤

Derived lemmas (in FlatTorus3Lemmas.lean):

• hGradChainLog, hGradIntZero, hLaplacianMinNonneg, hSpatialMul, etc.

• MeasurableSet' : Set X → Prop
• measurableSet_empty : MeasurableSet' self.toMeasurableSpace ∅
• measurableSet_compl (s : Set X) : MeasurableSet' self.toMeasurableSpace s → MeasurableSet' self.toMeasurableSpace sᶜ
• measurableSet_iUnion (f : ℕ → Set X) : (∀ (i : ℕ), MeasurableSet' self.toMeasurableSpace (f i)) → MeasurableSet' self.toMeasurableSpace (⋃ (i : ℕ), f i)
• volume : Measure X
• IsOpen : Set X → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set X) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set X)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• instCompact : CompactSpace X
• instNonempty : Nonempty X
• instFirstCountable : FirstCountableTopology X
• gradX : (X → ℝ) → X → Fin 3 → ℝ
• divX : (X → Fin 3 → ℝ) → X → ℝ
• curlX : (X → Fin 3 → ℝ) → X → Fin 3 → ℝ
• hDivLinear (α : ℝ) (G : X → Fin 3 → ℝ) (x : X) : divX (fun (y : X) => α • G y) x = α * divX G x
• hGradConst (φ : X → ℝ) : (∀ (x y : X), φ x = φ y) → ∀ (x : X), gradX φ x = 0
• hSpatialPos (g : X → ℝ) : Continuous g → (∀ (x : X), 0 < g x) → 0 < ∫ (x : X), g x
• hSpatialNonnegZero (g : X → ℝ) : Continuous g → (∀ (x : X), 0 ≤ g x) → ∫ (x : X), g x = 0 → ∀ (x : X), g x = 0
• IsSpatiallySmooth : ℕ∞ → (X → ℝ) → Prop
• hDiff_of_le {n m : ℕ∞} (f : X → ℝ) : m ≤ n → IsSpatiallySmooth n f → IsSpatiallySmooth m f
• hDiff_const (n : ℕ∞) (c : ℝ) : IsSpatiallySmooth n fun (x : X) => c
• hDiff_add (n : ℕ∞) (f g : X → ℝ) : IsSpatiallySmooth n f → IsSpatiallySmooth n g → IsSpatiallySmooth n fun (x : X) => f x + g x
• hDiff_smul (n : ℕ∞) (c : ℝ) (f : X → ℝ) : IsSpatiallySmooth n f → IsSpatiallySmooth n fun (x : X) => c * f x
• hDiff_log (n : ℕ∞) (f : X → ℝ) : IsSpatiallySmooth n f → (∀ (x : X), 0 < f x) → IsSpatiallySmooth n (Real.log ∘ f)
• hDiff_continuous (n : ℕ∞) (f : X → ℝ) : IsSpatiallySmooth (n + 1) f → Continuous f
• hDiff_grad (n : ℕ∞) (f : X → ℝ) (i : Fin 3) : IsSpatiallySmooth (n + 1) f → IsSpatiallySmooth n fun (x : X) => gradX f x i
• hCurlIntZero (F : X → Fin 3 → ℝ) (u : Fin 3 → ℝ) : (∀ (j : Fin 3), IsSpatiallySmooth 1 fun (x : X) => F x j) → ∫ (x : X), u ⬝ᵥ curlX F x = 0
• hHarmonic_const (φ : X → ℝ) : IsSpatiallySmooth 2 φ → (∀ (x : X), divX (gradX φ) x = 0) → ∀ (x y : X), φ x = φ y
• hLaplacianMaxNonpos (φ : X → ℝ) (x₀ : X) : IsSpatiallySmooth 2 φ → (∀ (x : X), φ x ≤ φ x₀) → divX (gradX φ) x₀ ≤ 0
• hGradAdd (f g : X → ℝ) : IsSpatiallySmooth 1 f → IsSpatiallySmooth 1 g → ∀ (x : X), gradX (fun (y : X) => f y + g y) x = gradX f x + gradX g x
• hGradScalarMul (c : ℝ) (f : X → ℝ) (x : X) : gradX (fun (y : X) => c * f y) x = c • gradX f x
• hGradChainExp (φ : X → ℝ) : IsSpatiallySmooth 1 φ → ∀ (x : X) (i : Fin 3), gradX (fun (y : X) => Real.exp (φ y)) x i = Real.exp (φ x) * gradX φ x i
• hKillingToHarmonic (b : X → Fin 3 → ℝ) : (∀ (j : Fin 3), IsSpatiallySmooth 1 fun (y : X) => b y j) → (∀ (j i : Fin 3), IsSpatiallySmooth 1 fun (x : X) => gradX (fun (y : X) => b y j) x i) → (∀ (x : X) (i j : Fin 3), gradX (fun (y : X) => b y j) x i + gradX (fun (y : X) => b y i) x j = 0) → ∀ (j : Fin 3) (x : X), divX (gradX fun (y : X) => b y j) x = 0
• hCurlZeroDivZeroHarmonic (F : X → Fin 3 → ℝ) : (∀ (i : Fin 3), IsSpatiallySmooth 1 fun (y : X) => F y i) → (∀ (i j : Fin 3), IsSpatiallySmooth 1 fun (x : X) => gradX (fun (y : X) => F y i) x j) → (∀ (x : X), curlX F x = 0) → (∀ (x : X), divX F x = 0) → ∀ (i : Fin 3) (x : X), divX (gradX fun (y : X) => F y i) x = 0
• hIBP_spatial (φ ψ : X → ℝ) (i : Fin 3) : IsSpatiallySmooth 1 φ → IsSpatiallySmooth 1 ψ → ∫ (x : X), φ x * gradX ψ x i = -∫ (x : X), ψ x * gradX φ x i
• hSpatialVelocityFubini (F : X → (Fin 3 → ℝ) → ℝ) : MeasureTheory.Integrable (Function.uncurry F) (MeasureTheory.volume.prod MeasureTheory.volume) → ∫ (x : X) (v : Fin 3 → ℝ), F x v = ∫ (v : Fin 3 → ℝ) (x : X), F x v
• hSpatialAdd (g₁ g₂ : X → ℝ) : MeasureTheory.Integrable g₁ MeasureTheory.volume → MeasureTheory.Integrable g₂ MeasureTheory.volume → ∫ (x : X), g₁ x + g₂ x = (∫ (x : X), g₁ x) + ∫ (x : X), g₂ x
• hGradIntegrable (g : X → ℝ) : IsSpatiallySmooth 1 g → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (x : X) => gradX g x i) MeasureTheory.volume

@[instance 100]

instance VML.FlatTorus3.instCompactSpace {X : Type u_1} [FlatTorus3 X] : CompactSpace X

@[instance 100]

instance VML.FlatTorus3.instNonemptySpace {X : Type u_1} [FlatTorus3 X] : Nonempty X

@[instance 100]

instance VML.FlatTorus3.instFirstCountableTopology {X : Type u_1} [FlatTorus3 X] : FirstCountableTopology X

@[reducible, inline]

noncomputable abbrev VML.FlatTorus3.spatialIntegral {X : Type u_1} [FlatTorus3 X] (g : X → ℝ) : ℝ

Compatibility wrapper: spatial integral as Mathlib's Bochner integral. Defined as abbrev so it unfolds transparently in rewrites.

Equations

• VML.FlatTorus3.spatialIntegral g = ∫ (x : X), g x