Integrability for the three-dimensional fundamental solution

The real inverse-norm kernel is integrable on every ball about its pole.

The inverse-norm singularity is locally integrable in three dimensions.

theorem LiebThirring.integrableOn_inv_norm_sub_ball (y : Position) (R : ℝ) : MeasureTheory.IntegrableOn (fun (x : Position) => ‖x - y‖⁻¹) (Metric.ball y R) MeasureTheory.volume

The real inverse-norm kernel is integrable on every ball about its pole.

theorem LiebThirring.locallyIntegrable_inv_norm_sub (y : Position) : MeasureTheory.LocallyIntegrable (fun (x : Position) => ‖x - y‖⁻¹) MeasureTheory.volume

The inverse-norm singularity is locally integrable in three dimensions.

theorem LiebThirring.continuous_laplacian_position {f : Position → ℝ} (hf : ContDiff ℝ 2 f) : Continuous (Laplacian.laplacian f)

A C² function has continuous Mathlib Laplacian on Position.

theorem LiebThirring.hasCompactSupport_laplacian_position {f : Position → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (Laplacian.laplacian f)

Taking the Laplacian preserves compact support.

theorem LiebThirring.integrable_inv_norm_sub_mul_laplacian {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (y : Position) : MeasureTheory.Integrable (fun (x : Position) => ‖x - y‖⁻¹ * Laplacian.laplacian f x) MeasureTheory.volume

Absolute integrability in the fundamental solution, before the distributional identity.

theorem LiebThirring.measurable_coulombPotential (β : MeasureTheory.Measure Position) [MeasureTheory.SFinite β] : Measurable (coulombPotential β)

The shared extended potential is measurable for an s-finite charge.

theorem LiebThirring.locallyIntegrable_coulombPotential_toReal (β : MeasureTheory.Measure Position) [MeasureTheory.SFinite β] {C : ENNReal} (hC : C ≠ ⊤) (hβ : ∀ (x : Position), coulombPotential β x ≤ C) : MeasureTheory.LocallyIntegrable (fun (x : Position) => (coulombPotential β x).toReal) MeasureTheory.volume

Bounded extended Coulomb potentials are locally integrable after toReal. The bound is on the extended potential, so it also asserts finiteness everywhere.

theorem LiebThirring.integrable_coulombPotential_toReal_mul_laplacian (β : MeasureTheory.Measure Position) [MeasureTheory.SFinite β] {C : ENNReal} (hC : C ≠ ⊤) (hβ : ∀ (x : Position), coulombPotential β x ≤ C) {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : MeasureTheory.Integrable (fun (x : Position) => (coulombPotential β x).toReal * Laplacian.laplacian f x) MeasureTheory.volume

The left-hand test-function pairing in the fundamental solution is absolutely integrable.