Newtonian Potential Bounds and Inverse-Norm Integrability

Proves coulomb_landauMatrix_entry_le (|A(z)_{ij}| <= ||z||^{-1}) and local integrability of ||z||^{-1} against Schwartz functions, the key estimates for handling the Coulomb singularity in collision integrals.

theorem VML.coulomb_landauMatrix_entry_le (z : Fin 3 → ℝ) (i j : Fin 3) : |landauMatrix coulombKernel z i j| ≤ if z = 0 then 0 else (eucNorm z)⁻¹

Coulomb Landau matrix entry bound: |A(z)_{ij}| ≤ (eucNorm z)⁻¹ for z ≠ 0, and A(0) = 0. This is the key bound enabling integrability of collision integrands despite the singular kernel Ψ(r) = r⁻³.

theorem VML.pi_norm_le_eucNorm (z : Fin 3 → ℝ) : ‖z‖ ≤ eucNorm z

Pi norm ≤ Euclidean norm in ℝ³: ‖z‖_∞ ≤ √(z·z).

theorem VML.coulomb_landauMatrix_entry_le_pi (z : Fin 3 → ℝ) (i j : Fin 3) (hz : z ≠ 0) : |landauMatrix coulombKernel z i j| ≤ ‖z‖⁻¹

Coulomb matrix entry bound in Pi norm: |A(z)_{ij}| ≤ ‖z‖⁻¹ for z ≠ 0.

theorem VML.inv_norm_summable_series (R : ℝ) (hR : 0 < R) : Summable fun (k : ℕ) => (2 ^ (-↑k - 1) * R)⁻¹ * (2 ^ (-↑k) * R) ^ 3

theorem VML.inv_norm_ball_volume (R : ℝ) (hR : 0 < R) (k : ℕ) : (MeasureTheory.volume (Metric.closedBall 0 (2 ^ (-↑k) * R))).toReal = (2 ^ (-↑k) * R) ^ 3 * (MeasureTheory.volume (Metric.closedBall 0 1)).toReal

theorem VML.inv_norm_lintegral_bounded (R : ℝ) (hR : 0 < R) (k : ℕ) : ∫⁻ (z : Fin 3 → ℝ) in Metric.closedBall 0 (2 ^ (-↑k) * R) \ Metric.closedBall 0 (2 ^ (-↑k - 1) * R), ENNReal.ofReal ‖z‖⁻¹ ≤ ENNReal.ofReal ((2 ^ (-↑k - 1) * R)⁻¹ * (MeasureTheory.volume (Metric.closedBall 0 (2 ^ (-↑k) * R))).toReal)

theorem VML.inv_norm_local_integrable (R : ℝ) (hR : 0 < R) : MeasureTheory.IntegrableOn (fun (z : Fin 3 → ℝ) => ‖z‖⁻¹) (Metric.closedBall 0 R) MeasureTheory.volume

‖·‖⁻¹ is locally integrable in ℝ³. Proved by Aristotle (job 3dc1b4dc). Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

theorem VML.convolution_local_int_schwartz (g : (Fin 3 → ℝ) → ℝ) (hg_decay : ∀ (N : ℕ), ∃ C > 0, ∀ (w : Fin 3 → ℝ), |g w| * (1 + ‖w‖) ^ N ≤ C) (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hK_local : MeasureTheory.IntegrableOn (fun (z : Fin 3 → ℝ) => ‖z‖⁻¹) (Metric.closedBall 0 1) MeasureTheory.volume) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => ‖v - w‖⁻¹ * g w) MeasureTheory.volume

Convolution of a locally integrable kernel with a Schwartz function is integrable. Proved by Aristotle (job 1ba752be). Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

theorem VML.inv_norm_schwartz_integrable (g : (Fin 3 → ℝ) → ℝ) (hg_decay : ∀ (N : ℕ), ∃ C > 0, ∀ (w : Fin 3 → ℝ), |g w| * (1 + ‖w‖) ^ N ≤ C) (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (v : Fin 3 → ℝ) : MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => ‖v - w‖⁻¹ * g w) MeasureTheory.volume

Key integrability fact for Coulomb kernel: ‖·‖⁻¹ × Schwartz is integrable in ℝ³. Combines inv_norm_local_integrable and convolution_local_int_schwartz.

theorem VML.newtonian_near_bound (g : (Fin 3 → ℝ) → ℝ) (C₀ : ℝ) (hg_sup : ∀ (w : Fin 3 → ℝ), |g w| ≤ C₀) (v : Fin 3 → ℝ) (h_int_translated : MeasureTheory.Integrable (fun (z : Fin 3 → ℝ) => ‖z‖⁻¹ * |g (v - z)|) MeasureTheory.volume) (h_inv_loc : MeasureTheory.IntegrableOn (fun (z : Fin 3 → ℝ) => ‖z‖⁻¹) (Metric.closedBall 0 1) MeasureTheory.volume) : ∫ (z : Fin 3 → ℝ) in Metric.closedBall 0 1, ‖z‖⁻¹ * |g (v - z)| ≤ C₀ * ∫ (z : Fin 3 → ℝ) in Metric.closedBall 0 1, ‖z‖⁻¹

theorem VML.newtonian_far_bound (g : (Fin 3 → ℝ) → ℝ) (hg_abs_int : MeasureTheory.Integrable (fun (w : Fin 3 → ℝ) => |g w|) MeasureTheory.volume) (v : Fin 3 → ℝ) (h_int_translated : MeasureTheory.Integrable (fun (z : Fin 3 → ℝ) => ‖z‖⁻¹ * |g (v - z)|) MeasureTheory.volume) : ∫ (z : Fin 3 → ℝ) in (Metric.closedBall 0 1)ᶜ, ‖z‖⁻¹ * |g (v - z)| ≤ ∫ (w : Fin 3 → ℝ), |g w|

theorem VML.newtonian_schwartz_uniform_bound (g : (Fin 3 → ℝ) → ℝ) (hg_decay : ∀ (N : ℕ), ∃ C > 0, ∀ (w : Fin 3 → ℝ), |g w| * (1 + ‖w‖) ^ N ≤ C) (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) : ∃ M > 0, ∀ (v : Fin 3 → ℝ), ∫ (w : Fin 3 → ℝ), ‖v - w‖⁻¹ * |g w| ≤ M

The Newtonian potential (convolution with ‖·‖⁻¹) of a Schwartz function is uniformly bounded in ℝ³. Proof: split into near (B(v,1)) and far parts near is bounded by sup|g| × ∫_{B(0,1)} ‖z‖⁻¹, far by ∫|g|.