Helper Lemmas for Section 3

Gaussian normalization, gradient of exponential-quadratic functions, Maxwellian characterization, and derivative bounds used in the nullspace analysis of the Landau operator.

theorem VML.analysis_fluxFactor (f : (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (v w : Fin 3 → ℝ) : f w • vGrad f v - f v • vGrad f w = (f v * f w) • (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w)

Flux factoring: f(w)∇f(v) - f(v)∇f(w) = f(v)f(w)(∇logf(v) - ∇logf(w)).

theorem VML.analysis_scalarFactor (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (v w : Fin 3 → ℝ) : (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w) ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec ((f v * f w) • (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w)) = f v * f w * (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w) ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w)

Scalar factors through mulVec and dotProduct: y ⬝ (A *ᵥ (c • y)) = c * (y ⬝ (A *ᵥ y)).

theorem VML.analysis_nonneg_dbl_zero (g : (Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ) (hnn : ∀ (v w : Fin 3 → ℝ), 0 ≤ g v w) (hcont : Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => g p.1 p.2) (hint_inner : ∀ (v : Fin 3 → ℝ), MeasureTheory.Integrable (g v) MeasureTheory.volume) (hint_outer : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), g v w) MeasureTheory.volume) (hint : ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), g v w = 0) (v w : Fin 3 → ℝ) : g v w = 0

Nonneg double integral zero → pointwise zero.

theorem VML.poly_cubic_extraction (d_c : Fin 3 → ℝ) (K : Fin 3 → Fin 3 → ℝ) (d_lin : Fin 3 → ℝ) (C : ℝ) (h : ∀ (v : Fin 3 → ℝ), v ⬝ᵥ d_c * normSq v + ∑ i : Fin 3, ∑ j : Fin 3, v i * v j * K i j + v ⬝ᵥ d_lin + C = 0) (v : Fin 3 → ℝ) : v ⬝ᵥ d_c * normSq v = 0

Polynomial cubic extraction: cubic part of a vanishing polynomial vanishes. Proved by Aristotle (Harmonic).

theorem VML.poly_killing_extraction (K : Fin 3 → Fin 3 → ℝ) (h : ∀ (v : Fin 3 → ℝ), ∑ i : Fin 3, ∑ j : Fin 3, v i * v j * K i j = 0) (i j : Fin 3) : K i j + K j i = 0

Polynomial quadratic extraction: Killing equation from vanishing quadratic form. Proved by Aristotle (Harmonic).

theorem VML.poly_linear_extraction (d : Fin 3 → ℝ) (C : ℝ) (h : ∀ (v : Fin 3 → ℝ), v ⬝ᵥ d + C = 0) : d = 0 ∧ C = 0

Polynomial linear extraction: coefficients of vanishing linear polynomial vanish. Proved by Aristotle (Harmonic).

theorem VML.entropy_score_form (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (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 = -(1 / 2) * ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), PSDIntegrand Ψ f v w

Gap 1-3 combined: Score function identity for the entropy dissipation formula. D(f) = -(1/2) ∫∫ f(v)f(w) ⟨Δ, A(v-w) Δ⟩ where Δ = ∇log f(v) - ∇log f(w). Derived from: IBP (Gap 1) + Fubini+symmetrization (Gap 2) + score substitution (Gap 3). Reference: Proof of Lemma 5 (lem:entropy_dissipation).

theorem VML.psd_weighted_integral_nonneg (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (hΨ : ∀ (r : ℝ), 0 ≤ Ψ r) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) : 0 ≤ ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), f v * f w * (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w) ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w)

Gap 4: Non-negativity of the PSD-weighted double integral. Since f > 0, Ψ ≥ 0, and Yᵀ A(z) Y ≥ 0 (Lemma 2), the integrand is non-negative, so the double integral is non-negative. Reference: Step in the proof of Theorem 3 (thm:H_theorem).

theorem VML.entropy_zero_quadform_zero (Ψ : ℝ → ℝ) (f : (Fin 3 → ℝ) → ℝ) (hΨ : ∀ (r : ℝ), 0 < Ψ r) (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) (hD : entropyDissipation Ψ f = 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) (v w : Fin 3 → ℝ) : (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w) ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (vGrad (Real.log ∘ f) v - vGrad (Real.log ∘ f) w) = 0

Gap 5: D(f) = 0 forces the PSD quadratic form integrand to vanish pointwise. From D(f) = 0, the entropy dissipation formula, f > 0, and continuity: the non-negative integrand integrates to zero, hence vanishes pointwise. Reference: Step in the proof of Lemma 6 (lem:D_zero_functional_eq).

theorem VML.parallel_curl_free_affine (g : (Fin 3 → ℝ) → Fin 3 → ℝ) (hg_smooth : ContDiff ℝ 2 g) (hparallel : ∀ (v w : Fin 3 → ℝ), v ≠ w → ∃ (l : ℝ), g v - g w = l • (v - w)) : ∃ (b : Fin 3 → ℝ) (c₀ : ℝ), ∀ (v : Fin 3 → ℝ), g v = b + (2 * c₀) • v

Gap 6: Solution of the functional equation: parallel + curl-free → affine. If g(v) - g(w) ∥ (v - w) for all v ≠ w and g is smooth (hence curl-free), then g(v) = b + 2c₀ v for constants b, c₀. Reference: Proof of Lemma 7 (lem:functional_eq_solution).

theorem VML.affine_gradient_antiderivative (h : (Fin 3 → ℝ) → ℝ) (b : Fin 3 → ℝ) (c₀ : ℝ) (hh_smooth : ContDiff ℝ 3 h) (hgrad : ∀ (v : Fin 3 → ℝ), vGrad h v = b + (2 * c₀) • v) (v : Fin 3 → ℝ) : h v = h 0 + b ⬝ᵥ v + c₀ * normSq v

Gap 7: Antiderivative of an affine gradient. If ∇h(v) = b + 2c₀ v, then h(v) = h(0) + b · v + c₀|v|². Reference: Proof of Lemma 8 (lem:log_f_quadratic).