set_option linter.style.longLine false

Transport Constraints (Section 4)

Derives that steady states are local Maxwellians: from the transport equation and D(f) = 0 at each spatial point, applies Corollary 1 to conclude f(x, .) is Maxwellian for each x.

theorem VML.steady_state_is_local_maxwellian (X : Type u_1) (f : X → (Fin 3 → ℝ) → ℝ) (Ψ : ℝ → ℝ) (hΨ : ∀ (r : ℝ), 0 < Ψ r) (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) (hD_zero : ∀ (x : X), entropyDissipation Ψ (f x) = 0) (hScoreForm : ∀ (x : X), entropyDissipation Ψ (f x) = -(1 / 2) * ∫ (v : Fin 3 → ℝ) (w : Fin 3 → ℝ), PSDIntegrand Ψ (f x) v w) (hPSD_cont : ∀ (x : X), Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => PSDIntegrand Ψ (f x) p.1 p.2) (hPSD_inner : ∀ (x : X) (v : Fin 3 → ℝ), MeasureTheory.Integrable (PSDIntegrand Ψ (f x) v) MeasureTheory.volume) (hPSD_outer : ∀ (x : X), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), PSDIntegrand Ψ (f x) v w) MeasureTheory.volume) (x : X) : IsMaxwellian (f x)

Corollary 2 (Steady state is a local Maxwellian). Reference: cor:local_maxwellian

At any steady state of the VML system with ν > 0, f(x,·) is a Maxwellian for each x ∈ T³.

Proof: By Lemma 11, Dₓ(f) = 0 for all x. By Corollary 1, f(x,·) is Maxwellian.

theorem VML.lorentz_force_div_zero (E_val B_val v : Fin 3 → ℝ) : vDiv (fun (w : Fin 3 → ℝ) => E_val + cross w B_val) v = 0

Velocity divergence of the Lorentz force vanishes: div_v(E + v×B) = 0. E is constant in v, and the cross product v×B has zero trace.

theorem VML.force_transport_zero (g : (Fin 3 → ℝ) → ℝ) (E_val B_val : Fin 3 → ℝ) (hg_pos : ∀ (v : Fin 3 → ℝ), 0 < g v) (hg_smooth : ContDiff ℝ 3 g) (_hg_int : MeasureTheory.Integrable g MeasureTheory.volume) (h_int_f_dg : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E_val + cross v B_val) i * (fderiv ℝ (fun (w : Fin 3 → ℝ) => g w * Real.log (g w) - g w) v) (Pi.single i 1)) MeasureTheory.volume) (h_int_fg : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E_val + cross v B_val) i * (g v * Real.log (g v) - g v)) MeasureTheory.volume) : ∫ (v : Fin 3 → ℝ), (E_val + cross v B_val) ⬝ᵥ vGrad g v * Real.log (g v) = 0

Force transport vanishes: ∫_v (E + v×B) · ∇_v f · log f dv = 0. Uses: div_v(E + v×B) = 0 + velocity-space IBP (velocity_ibp).

theorem VML.transport_entropy_from_vlasov {X : Type u_1} [FlatTorus3 X] (f : X → (Fin 3 → ℝ) → ℝ) (E B : X → Fin 3 → ℝ) (Ψ : ℝ → ℝ) (ν : ℝ) (hν : 0 < ν) (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) (hDiff_fv : ∀ (v : Fin 3 → ℝ), FlatTorus3.IsSpatiallySmooth 2 fun (x : X) => f x v) (hDiff_logfv : ∀ (v : Fin 3 → ℝ), FlatTorus3.IsSpatiallySmooth 2 fun (x : X) => Real.log (f x v)) (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) (hSpatialTransport_int : ∀ (x : X), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => v ⬝ᵥ FlatTorus3.gradX (fun (y : X) => f y v) x * Real.log (f x v)) MeasureTheory.volume) (hForceTransport_int : ∀ (x : X), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E x + cross v (B x)) ⬝ᵥ vGrad (f x) v * Real.log (f x v)) MeasureTheory.volume) (hForceIBP_f_dg : ∀ (x : X) (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E x + cross v (B x)) i * (fderiv ℝ (fun (w : Fin 3 → ℝ) => f x w * Real.log (f x w) - f x w) v) (Pi.single i 1)) MeasureTheory.volume) (hForceIBP_fg : ∀ (x : X) (i : Fin 3), MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (E x + cross v (B x)) i * (f x v * Real.log (f x v) - f x v)) MeasureTheory.volume) (hSpatialTransport_joint : MeasureTheory.Integrable (Function.uncurry fun (x : X) (v : Fin 3 → ℝ) => v ⬝ᵥ FlatTorus3.gradX (fun (y : X) => f y v) x * Real.log (f x v)) (MeasureTheory.volume.prod MeasureTheory.volume)) (hSpatTransComp : ∀ (v : Fin 3 → ℝ) (i : Fin 3), MeasureTheory.Integrable (fun (x : X) => FlatTorus3.gradX (fun (y : X) => f y v) x i * Real.log (f x v)) MeasureTheory.volume) : ∫ (x : X), entropyDissipation Ψ (f x) = 0

Transport entropy vanishes at steady state on T³. Proof: Multiply Vlasov by log f, integrate over v and X. Spatial transport vanishes by hIBP_spatial (spatial_transport_log_zero), force transport vanishes by velocity-space IBP (force_transport_zero). Reference: Lemma 11 (lem:global_entropy_zero) in H-theorem-formal.tex.