Nullspace of the Landau Operator (Section 3)

H-theorem for the Landau operator (D(f) <= 0), characterization of D(f) = 0 as f being a Maxwellian, and Corollary 1: if entropy dissipation vanishes then f is a local Maxwellian at each spatial point.

theorem VML.H_theorem (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (hΨ : ∀ (r : ℝ), 0 ≤ Ψ r) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) (hSWF : ∫ (v : Fin 3 → ℝ), LandauOperator Ψ f v * (Real.log ∘ f) v = -(1 / 2) * ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w) ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) : entropyDissipation Ψ f ≤ 0

Theorem 3 (H-theorem for the Landau operator). Reference: thm:H_theorem

D(f) = ∫ Q(f,f)(v) log f(v) dv ≤ 0.

Proof: By Lemma 5, D(f) is the negative of a double integral of the quadratic form Yᵀ A(z) Y weighted by f(v)f(w) > 0. By Lemma 2 (PSD), the integrand is non-negative, so D(f) ≤ 0.

theorem VML.log_f_quadratic (f : (Fin 3 → ℝ) → ℝ) (b : Fin 3 → ℝ) (c₀ : ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) (hgrad : ∀ (v : Fin 3 → ℝ), vGrad (Real.log ∘ f) v = b + (2 * c₀) • v) : ∃ (a₀ : ℝ), ∀ (v : Fin 3 → ℝ), Real.log (f v) = a₀ + b ⬝ᵥ v + c₀ * normSq v

Lemma 8 (Integration: log f is a polynomial of degree ≤ 2). Reference: lem:log_f_quadratic

If ∇log f(v) = b + 2c₀ v, then log f(v) = a₀ + b · v + c₀|v|².

Proof: Direct integration of each component ∂ᵢ log f = bᵢ + 2c₀ vᵢ.

theorem VML.nullspace_necessity (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (hΨ : ∀ (r : ℝ), 0 < Ψ r) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (_hf_smooth : ContDiff ℝ 3 f) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hQ : ∀ (v : Fin 3 → ℝ), LandauOperator Ψ f v = 0) (hScoreForm : entropyDissipation Ψ f = -(1 / 2) * ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), PSDIntegrand Ψ f v w) (hPSD_cont : Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => PSDIntegrand Ψ f p.1 p.2) (hPSD_inner : ∀ (v : Fin 3 → ℝ), MeasureTheory.Integrable (PSDIntegrand Ψ f v) MeasureTheory.volume) (hPSD_outer : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), PSDIntegrand Ψ f v w) MeasureTheory.volume) : IsMaxwellian f

Theorem 4 (Nullspace of the Landau operator — necessity). Reference: thm:nullspace_necessity

If Q(f,f) = 0 and f ∈ L¹(ℝ³), then f is a Maxwellian.

Proof chains: Q=0 → D=0 (Lemma 5) → parallelism (Lemma 6) → ∇log f affine (Lemma 7) → log f quadratic (Lemma 8) → f Maxwellian.

theorem VML.nullspace_sufficiency (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (a₀ : ℝ) (b : Fin 3 → ℝ) (c₀ : ℝ) (_hc₀ : c₀ < 0) (hf : ∀ (v : Fin 3 → ℝ), f v = Real.exp (a₀ + b ⬝ᵥ v + c₀ * normSq v)) (v : Fin 3 → ℝ) : LandauOperator Ψ f v = 0

Theorem 5 (Nullspace of the Landau operator — sufficiency). Reference: thm:nullspace_sufficiency

If log f(v) = a₀ + b · v + c₀|v|², then Q(f,f) = 0.

Proof: ∇log f(v) - ∇log f(w) = 2c₀(v - w), so the integrand in Q contains A(v-w)(v-w) = 0 by Lemma 3 (projection annihilation).

theorem VML.density_positive_of_integral (f : (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) : 0 < ∫ (v : Fin 3 → ℝ), f v

Density is positive when f > 0 and integrable. Proof: ∫ f > 0 for continuous positive integrable f on ℝ³ (positive measure). Reference: Used in VMLInput construction.

theorem VML.landauMatrix_sub_comm (Ψ : ℝ → ℝ) (v w : Fin 3 → ℝ) : landauMatrix Ψ (w - v) = landauMatrix Ψ (v - w)

landauMatrix is symmetric under swapping arguments of subtraction.

theorem VML.fubini_symmetrization_logf (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (_hf_smooth : ContDiff ℝ 3 f) (h_int_double : MeasureTheory.Integrable (fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => vGrad (Real.log ∘ f) p.1 ⬝ᵥ (landauMatrix Ψ (p.1 - p.2)).mulVec (f p.2 • vGrad f p.1 - f p.1 • vGrad f p.2)) MeasureTheory.volume) : (∀ (v : Fin 3 → ℝ), MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => vGrad (Real.log ∘ f) v ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) MeasureTheory.volume) → MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), vGrad (Real.log ∘ f) v ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) MeasureTheory.volume → ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w) ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w) = 2 * ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), vGrad (Real.log ∘ f) v ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)

Fubini symmetrization for the Landau weak form specialized to φ = log ∘ f. ∫∫ ⟨∇log f(v) - ∇log f(w), A(v-w) · flux⟩ = 2 · ∫∫ ⟨∇log f(v), A(v-w) · flux⟩ Proved by Aristotle (project 85302568).