Entropy Dissipation Identity (Section 2)

Properties of the Landau collision matrix: evenness, positive semidefiniteness, the symmetrized weak form, and the entropy dissipation identity D(f) as a double integral.

theorem VML.landauMatrix_even (Ψ : ℝ → ℝ) (z : Fin 3 → ℝ) : landauMatrix Ψ (-z) = landauMatrix Ψ z

Lemma 1(b): A(-z) = A(z). Reference: lem:A_symmetric

theorem VML.innerLandauMatrix_quadForm (z Y : Fin 3 → ℝ) : Y ⬝ᵥ (innerLandauMatrix z).mulVec Y = normSq z * normSq Y - (z ⬝ᵥ Y) ^ 2

The quadratic form of the inner Landau matrix: Yᵀ B(z) Y = |z|²|Y|² - (z·Y)². Reference: lem:A_psd

theorem VML.dotProduct_sq_le_normSq (z Y : Fin 3 → ℝ) : (z ⬝ᵥ Y) ^ 2 ≤ normSq z * normSq Y

Cauchy–Schwarz for dotProduct: (z·Y)² ≤ |z|²·|Y|². This follows from the Cauchy–Schwarz inequality.

theorem VML.landauMatrix_posSemidef {Ψ : ℝ → ℝ} {z : Fin 3 → ℝ} (hΨ : 0 ≤ Ψ (eucNorm z)) (Y : Fin 3 → ℝ) : 0 ≤ Y ⬝ᵥ (landauMatrix Ψ z).mulVec Y

Lemma 2: Yᵀ A(z) Y ≥ 0 when Ψ(|z|) ≥ 0. Reference: lem:A_psd

theorem VML.landauMatrix_quadForm_eq_zero_iff {Ψ : ℝ → ℝ} {z : Fin 3 → ℝ} (hΨ : 0 < Ψ (eucNorm z)) (hz : z ≠ 0) (Y : Fin 3 → ℝ) (h : Y ⬝ᵥ (landauMatrix Ψ z).mulVec Y = 0) : ∃ (l : ℝ), Y = l • z

Lemma 2 (equality case): If Ψ(|z|) > 0, z ≠ 0, and the quadratic form vanishes, then Y is parallel to z. Reference: lem:A_psd

theorem VML.innerLandauMatrix_mulVec_self (z : Fin 3 → ℝ) : (innerLandauMatrix z).mulVec z = 0

B(z) z = 0 (the inner matrix annihilates z).

theorem VML.landauMatrix_mulVec_self (Ψ : ℝ → ℝ) (z : Fin 3 → ℝ) : (landauMatrix Ψ z).mulVec z = 0

Lemma 3: A(z) z = 0. Reference: lem:zA_zero