Coulomb Kernel Definition and Schwartz Helpers

Defines coulombKernel (Psi(r) = r^{-3} for r > 0) and proves basic properties: strict positivity, Schwartz uniform bounds, and inv_norm_schwartz_integrable.

def VML.coulombKernel (r : ℝ) : ℝ

The Coulomb collision kernel: Ψ(r) = r⁻³ for r > 0, extended to 1 for r ≤ 0. The value at r ≤ 0 is irrelevant since landauMatrix Ψ 0 = 0 always (the projection |z|²I - zz^T vanishes at z = 0). Setting it to 1 ensures ∀ r, 0 < Ψ r, which the abstract theorem requires.

Equations

• VML.coulombKernel r = if r ≤ 0 then 1 else r ^ (-3)

theorem VML.coulombKernel_pos (r : ℝ) : 0 < coulombKernel r

theorem VML.schwartz_log_bound {f : Torus3 → (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hSchwartz : UniformSchwartzDecay f) (hExpDecay : ∃ (C : ℝ) (K : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), Real.exp (-C * (1 + ‖v‖) ^ K) ≤ f x v) : ∃ (C_log : ℝ) (K_log : ℕ), ∀ (x : Torus3) (v : Fin 3 → ℝ), |Real.log (f x v)| ≤ C_log * (1 + ‖v‖) ^ K_log

Log bound from Schwartz upper bound + stretched-exponential lower bound. From Schwartz N=0, k=0: |f x v| ≤ C_upper (uniform in x, v). From ExpDecay: f x v ≥ exp(-C_exp * (1+‖v‖)^K_exp). Together: |log(f x v)| ≤ max(|log C_upper|, C_exp * (1+‖v‖)^K_exp).

theorem VML.schwartz_norm_pow_integrable {f : Torus3 → (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (x : Torus3) (v : Fin 3 → ℝ), 0 < f x v) (hf_smooth : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (hSchwartz : UniformSchwartzDecay f) (x : Torus3) (k : ℕ) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ‖v‖ ^ k * |f x v|) MeasureTheory.volume

Schwartz decay implies moment integrability with norm powers.