set_option linter.style.longLine false

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'.