Fubini for bounded Coulomb potentials

The real value of the extended kernel is the real inverse norm, including value zero on the diagonal.

A finite pointwise potential is the Bochner integral of the real kernel.

theorem LiebThirring.coulombKernel_toReal_eq_inv_norm (x y : Position) : (coulombKernel x y).toReal = ‖x - y‖⁻¹

The real value of the extended kernel is the real inverse norm, including value zero on the diagonal.

theorem LiebThirring.coulombPotential_toReal_eq_integral (β : MeasureTheory.Measure Position) (x : Position) (hx : coulombPotential β x ≠ ⊤) : (coulombPotential β x).toReal = ∫ (y : Position), ‖x - y‖⁻¹ ∂β

A finite pointwise potential is the Bochner integral of the real kernel.

theorem LiebThirring.lintegral_abs_mul_coulombKernel_ne_top (β : MeasureTheory.Measure Position) [MeasureTheory.SFinite β] {C : ENNReal} (hC : C ≠ ⊤) (hβ : ∀ (x : Position), coulombPotential β x ≤ C) {g : Position → ℝ} (hg : Continuous g) (hgc : HasCompactSupport g) : ∫⁻ (p : Position × Position), ENNReal.ofReal ‖g p.1‖ * coulombKernel p.1 p.2 ∂MeasureTheory.volume.prod β ≠ ⊤

Absolute Tonelli bound for a compactly supported continuous multiplier.

theorem LiebThirring.integrable_inv_norm_sub_mul_prod (β : MeasureTheory.Measure Position) [MeasureTheory.SFinite β] {C : ENNReal} (hC : C ≠ ⊤) (hβ : ∀ (x : Position), coulombPotential β x ≤ C) {g : Position → ℝ} (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (fun (p : Position × Position) => ‖p.1 - p.2‖⁻¹ * g p.1) (MeasureTheory.volume.prod β)

Absolute product integrability licenses the ordinary Fubini exchange in the fundamental solution.

theorem LiebThirring.integral_coulombPotential_toReal_mul_eq_integral_integral (β : MeasureTheory.Measure Position) [MeasureTheory.SFinite β] {C : ENNReal} (hC : C ≠ ⊤) (hβ : ∀ (x : Position), coulombPotential β x ≤ C) {g : Position → ℝ} (hg : Continuous g) (hgc : HasCompactSupport g) : ∫ (x : Position), (coulombPotential β x).toReal * g x = ∫ (y : Position), ∫ (x : Position), ‖x - y‖⁻¹ * g x ∂β

Unconditional Fubini reduction of bounded-potential pairings to point-charge pairings.

theorem LiebThirring.integral_coulombPotential_toReal_mul_laplacian_eq_integral_integral (β : MeasureTheory.Measure Position) [MeasureTheory.SFinite β] {C : ENNReal} (hC : C ≠ ⊤) (hβ : ∀ (x : Position), coulombPotential β x ≤ C) {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : ∫ (x : Position), (coulombPotential β x).toReal * Laplacian.laplacian f x = ∫ (y : Position), ∫ (x : Position), ‖x - y‖⁻¹ * Laplacian.laplacian f x ∂β

the fundamental solution's Fubini reduction, with the weak-harmonic Laplacian.