set_option linter.style.longLine false

PSD Integrability and Fubini Symmetrization for Coulomb

Inner and outer integrability of the PSD integrand, and the Fubini symmetrization needed for the H-theorem entropy dissipation identity. Depends on continuity and pointwise bounds from CoulombPSDHelpers.

theorem VML.psd_inner_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) {Cg : ℝ} {Kg : ℕ} (hGrad : ∀ (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ f v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f v) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (PSDIntegrand coulombKernel f v) MeasureTheory.volume

PSD integrand is integrable for Coulomb kernel (inner integral, fixing v). Uses element-wise Coulomb matrix bound |A_{ij}| ≤ ‖z‖⁻¹ combined with polynomial score bound and Newtonian potential of Schwartz functions.

theorem VML.psd_outer_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) {Cg : ℝ} {Kg : ℕ} (hGrad : ∀ (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ f v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f v) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => ∫ (w : Fin 3 → ℝ), PSDIntegrand coulombKernel f v w) MeasureTheory.volume

PSD integrand is integrable for Coulomb kernel (outer integral). Uses pointwise bound + Newtonian uniform bounds + Schwartz decay.

theorem VML.fubini_double_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) {Cg : ℝ} {Kg : ℕ} (hGrad : ∀ (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ f v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f v) : MeasureTheory.Integrable (fun (p : (Fin 3 → ℝ) × (Fin 3 → ℝ)) => vGrad (Real.log ∘ f) p.1 ⬝ᵥ (landauMatrix coulombKernel (p.1 - p.2)).mulVec (f p.2 • vGrad f p.1 - f p.1 • vGrad f p.2)) MeasureTheory.volume

The Fubini integrand (score · flux) is jointly integrable on the product space for the Coulomb kernel. Uses integrable_prod_iff with:

• Joint measurability from measurability of each factor
• Inner integrability from landau_flux_integrable_coulomb
• Norm integral bound from PSD pointwise bound + Newtonian uniform bounds