set_option linter.style.longLine false

Polynomial Matching (Section 5)

Temperature is spatially constant, Lorentz force expansion, and polynomial identity matching that constrains the Maxwellian parameters (a, b, c) from the Vlasov transport equation.

theorem VML.lorentz_force_expansion (E b B v : Fin 3 → ℝ) (c : ℝ) : (E + cross v B) ⬝ᵥ (b + (2 * c) • v) = E ⬝ᵥ b + v ⬝ᵥ ((2 * c) • E + cross B b)

Expansion of (E + v×B)·(b + 2cv) = E·b + v·(2cE + B×b). Uses (v×B)·v = 0 and (v×B)·b = v·(B×b). Proved by Aristotle (Harmonic).

theorem VML.temperature_constant (X : Type u_1) (c : X → ℝ) (gradX : (X → ℝ) → X → Fin 3 → ℝ) (hcubic : ∀ (x : X) (v : Fin 3 → ℝ), v ⬝ᵥ gradX c x * normSq v = 0) (x : X) : gradX c x = 0

Lemma 14 (Temperature is spatially constant). Reference: lem:T_constant

Under the conditions of Lemma 13, ∇ₓc = 0, i.e., T(x) ≡ T∞ is a global constant.

Proof: The O(|v|³) terms give (v · ∇c)|v|² = 0 for all v. Choosing v = t eᵢ for t → ∞ shows ∂ₓᵢ c = 0 for each i. Since c = -1/(2T), T is constant.

theorem VML.polynomial_identity_from_vlasov {X : Type u_1} [FlatTorus3 X] (f : X → (Fin 3 → ℝ) → ℝ) (E B : X → Fin 3 → ℝ) (Ψ : ℝ → ℝ) (ν : ℝ) (_hf_pos : ∀ (x : X) (v : Fin 3 → ℝ), 0 < f x v) (_hf_smooth : ∀ (x : X), ContDiff ℝ 3 (f x)) (_hf_int : ∀ (x : X), MeasureTheory.Integrable (f x) MeasureTheory.volume) (_hΨ : ∀ (r : ℝ), 0 < Ψ r) (_hVlasov : ∀ (x : X) (v : Fin 3 → ℝ), v ⬝ᵥ FlatTorus3.gradX (fun (y : X) => f y v) x + (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v = ν * LandauOperator Ψ (f x) v) (a : X → ℝ) (b : X → Fin 3 → ℝ) (c : X → ℝ) : FlatTorus3.IsSpatiallySmooth 2 a → (∀ (j : Fin 3), FlatTorus3.IsSpatiallySmooth 2 fun (y : X) => b y j) → FlatTorus3.IsSpatiallySmooth 2 c → (∀ (x : X) (v : Fin 3 → ℝ), f x v = Real.exp (a x + b x ⬝ᵥ v + c x * normSq v)) → ∀ (x : X) (v : Fin 3 → ℝ), v ⬝ᵥ FlatTorus3.gradX c x * normSq v + ∑ i : Fin 3, ∑ j : Fin 3, v i * v j * FlatTorus3.gradX (fun (y : X) => b y j) x i + v ⬝ᵥ FlatTorus3.gradX a x + E x ⬝ᵥ b x + v ⬝ᵥ ((2 * c x) • E x + cross (B x) (b x)) = 0

Polynomial identity from the Vlasov equation. When f has Maxwellian form exp(a + b·v + c|v|²), the Landau operator vanishes (nullspace sufficiency), so the Vlasov equation reduces to collisionless transport. Expanding and dividing by f > 0 gives a polynomial in v. Reference: Lemma 13 (lem:polynomial_identity) in H-theorem-formal.tex.