set_option linter.style.longLine false

Abstract Theorem 4.2: Steady State Implies Maxwellian

States and proves the main abstract result: any smooth steady state of the Vlasov-Maxwell-Landau system satisfying VelocityDecayConditions is a global Maxwellian with E = 0 and B = const.

Physical Context (Non-Relativistic Limit): Note that this formalization assumes a strictly non-relativistic framework where velocities $v \in \mathbb{R}^3$ are unbounded. This admits superluminal particles, but is the standard mathematical setting for the classical Landau equation.

structure VML.VelocityDecayConditions {X : Type u_1} [FlatTorus3 X] (Ψ : ℝ → ℝ) (f : X → (Fin 3 → ℝ) → ℝ) (E B : X → Fin 3 → ℝ) : Prop

Velocity-space decay / integrability conditions for the VML steady state theorem.

These conditions hold for distribution functions with sufficient velocity-space decay (e.g., Schwartz class or sub-Gaussian tails). They ensure that:

• The H-theorem chain (IBP + Fubini symmetrization) goes through
• The transport entropy equation can be decomposed
• The Landau flux is differentiable and integrable

Bundled into a single structure for readability of the main theorem.

• hPSD_inner_int (x : X) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (PSDIntegrand Ψ (f x) v) MeasureTheory.volume
• hPSD_outer_int (x : X) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), PSDIntegrand Ψ (f x) v w) MeasureTheory.volume
• hFubini_double (x : X) : MeasureTheory.Integrable (fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => vGrad (Real.log ∘ f x) p.1 ⬝ᵥ (landauMatrix Ψ (p.1 - p.2)).mulVec (f x p.2 • vGrad (f x) p.1 - f x p.1 • vGrad (f x) p.2)) MeasureTheory.volume
• hFubini_inner (x : X) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => vGrad (Real.log ∘ f x) v ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (f x w • vGrad (f x) v - f x v • vGrad (f x) w)) MeasureTheory.volume
• hFubini_outer (x : X) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), vGrad (Real.log ∘ f x) v ⬝ᵥ (landauMatrix Ψ (v - w)).mulVec (f x w • vGrad (f x) v - f x v • vGrad (f x) w)) MeasureTheory.volume
• 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
• hLandauFluxDiff (x : X) (i : Fin 3) : Differentiable ℝ fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v - w)).mulVec (f x w • vGrad (f x) v - f x v • vGrad (f x) w)) i
• hLandauIBP_df_g (x : X) (i : Fin 3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (fderiv ℝ (fun (v' : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v' - w)).mulVec (f x w • vGrad (f x) v' - f x v' • vGrad (f x) w)) i) v) (Pi.single i 1) * (Real.log ∘ f x) v) MeasureTheory.volume
• hLandauIBP_f_dg (x : X) (i : Fin 3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v - w)).mulVec (f x w • vGrad (f x) v - f x v • vGrad (f x) w)) i * (fderiv ℝ (Real.log ∘ f x) v) (Pi.single i 1)) MeasureTheory.volume
• hLandauIBP_fg (x : X) (i : Fin 3) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix Ψ (v - w)).mulVec (f x w • vGrad (f x) v - f x v • vGrad (f x) w)) i * (Real.log ∘ f x) v) MeasureTheory.volume
• hLandauFluxInt (x : X) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => (landauMatrix Ψ (v - w)).mulVec (f x w • vGrad (f x) v - f x v • vGrad (f x) w)) 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
• hf_velocity_dominated : ∃ (g : (Fin 3 → ℝ) → ℝ), MeasureTheory.Integrable g MeasureTheory.volume ∧ ∀ (x : X) (v : Fin 3 → ℝ), f x v ≤ g v
• hPSD_cont (x : X) : Continuous fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => PSDIntegrand Ψ (f x) p.1 p.2
• hD_cont : Continuous fun (x : X) => entropyDissipation Ψ (f x)

theorem VML.Theorem42 {X : Type u_1} [FlatTorus3 X] (f : X → (Fin 3 → ℝ) → ℝ) (E B : X → Fin 3 → ℝ) (Ψ : ℝ → ℝ) (ν ρ_ion : ℝ) (hν : 0 < ν) (hρ_ion : 0 < ρ_ion) (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) (hAmpere : ∀ (x : X), FlatTorus3.curlX B x = fun (i : Fin 3) => ∫ (v : Fin 3 → ℝ), v i * f x v) (hGauss : ∀ (x : X), FlatTorus3.divX E x = (∫ (v : Fin 3 → ℝ), f x v) - ρ_ion) (hDivB : ∀ (x : X), FlatTorus3.divX B x = 0) (hDiff_B : ∀ (i : Fin 3), FlatTorus3.IsSpatiallySmooth 2 fun (y : X) => B y i) (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) (hDiff_fv : ∀ (v : Fin 3 → ℝ), FlatTorus3.IsSpatiallySmooth 2 fun (x : X) => f x v) (hDecay : VelocityDecayConditions Ψ f E B) : ∃ (T_eq : ℝ) (B₀ : Fin 3 → ℝ), 0 < T_eq ∧ (∀ (x : X) (v : Fin 3 → ℝ), f x v = equilibriumMaxwellian ρ_ion T_eq v) ∧ (∀ (x : X), E x = 0) ∧ ∀ (x : X), B x = B₀

Theorem 42 (Global steady state of the VML system).

Consider the Vlasov-Maxwell-Landau system on a periodic spatial domain (modeled by a FlatTorus3) with collision frequency ν > 0, interaction potential Ψ > 0, and uniform neutralizing ion background density ρ_ion > 0.

Let (f, E, B) be a sufficiently smooth steady-state solution with f > 0 and f(x, ·) ∈ L¹(ℝ³) for each x. Then:

(i) f is a spatially uniform, zero-drift Maxwellian: f(v) = ρ_ion / (2πT)^(3/2) · exp(-|v|²/(2T))

(ii) The electric field vanishes: E = 0.

(iii) The magnetic field is spatially constant.

The velocity-space decay conditions (bundled in VelocityDecayConditions) require not only sufficient upper-bound velocity-space decay (e.g., Schwartz class), but importantly also a matching LOWER bound. The polynomial score bound (hGradBound) actively excludes functions with faster-than-exponential decay (like $e^{-e^{\|v\|}}$), even though they are Schwartz class. The conditions effectively restrict the domain to near-Maxwellian or stretched-exponential states.

Note on Physical Rigor: This theorem addresses the classic non-relativistic formulation over $v \in \mathbb{R}^3$. As with all non-relativistic kinetic theory over an unbounded velocity space, this formally admits unphysical superluminal velocities ($|v| > c$). A strictly correct physical model would require replacing $v$ with momentum $p$.

Reference: H-theorem-formal.pdf, Theorem 42.