Flux Integrability and Measurability Helpers for Coulomb

Proves integrability of the Landau collision flux, Schwartz partial decay, and AEStronglyMeasurability of flux components for the Coulomb kernel.

theorem VML.landau_flux_integrable_coulomb (f : (Fin 3 → ℝ) → ℝ) (_hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) (hf_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 2 → ∃ C > 0, ∀ (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k f v‖ * (1 + ‖v‖) ^ N ≤ C) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => (landauMatrix coulombKernel (v - w)).mulVec (f w • vGrad f v - f v • vGrad f w)) MeasureTheory.volume

The Landau collision flux is integrable for the Coulomb kernel.

theorem VML.schwartz_partial_decay {f : Torus3 → (Fin 3 → ℝ) → ℝ} (hSchwartz : UniformSchwartzDecay f) (x : Torus3) (j : Fin 3) (N : ℕ) : ∃ C > 0, ∀ (w : Fin 3 → ℝ), |(fderiv ℝ (f x) w) (Pi.single j 1)| * (1 + ‖w‖) ^ N ≤ C

Schwartz decay of partial derivatives: |∂_j f(x,w)| * (1+‖w‖)^N ≤ C. Follows from ‖iteratedFDeriv 1 f w‖ bounds and |∂_jf| ≤ ‖fderiv f w‖ ≤ ‖iteratedFDeriv 1 f w‖.

theorem VML.flux_component_aestronglyMeasurable (φ : (Fin 3 → ℝ) → ℝ) (hφ_smooth : ContDiff ℝ 3 φ) (hFlux : ∀ (v : Fin 3 → ℝ), MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => (landauMatrix coulombKernel (v - w)).mulVec (φ w • vGrad φ v - φ v • vGrad φ w)) MeasureTheory.volume) (i : Fin 3) : MeasureTheory.AEStronglyMeasurable (fun (v : Fin 3 → ℝ) => (∫ (w : Fin 3 → ℝ), (landauMatrix coulombKernel (v - w)).mulVec (φ w • vGrad φ v - φ v • vGrad φ w)) i) MeasureTheory.volume

The Landau flux component is AEStronglyMeasurable as a parametric integral. Uses joint measurability on the product space + integral_prod_right'.