The three-dimensional Coulomb fundamental solution

The Coulomb fundamental-solution identity, the fundamental solution. Together with integrable_inv_norm_sub_mul_laplacian, this asserts absolute integrability and the value of the pairing. C² suffices, so in particular the identity holds for every smooth compactly supported test.

A finite positive charge with bounded extended potential satisfies the test-function identity the fundamental solution. Local integrability is supplied by locallyIntegrable_coulombPotential_toReal, and absolute test-pairing integrability by integrable_coulombPotential_toReal_mul_laplacian.

theorem LiebThirring.integral_inv_norm_sub_mul_laplacian {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (y : Position) : ∫ (x : Position), ‖x - y‖⁻¹ * Laplacian.laplacian f x = -4 * Real.pi * f y

The Coulomb fundamental-solution identity, the fundamental solution. Together with integrable_inv_norm_sub_mul_laplacian, this asserts absolute integrability and the value of the pairing. C² suffices, so in particular the identity holds for every smooth compactly supported test.

theorem LiebThirring.integral_coulombPotential_toReal_mul_laplacian (β : MeasureTheory.Measure Position) [MeasureTheory.IsFiniteMeasure β] {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 = -4 * Real.pi * ∫ (y : Position), f y ∂β

A finite positive charge with bounded extended potential satisfies the test-function identity the fundamental solution. Local integrability is supplied by locallyIntegrable_coulombPotential_toReal, and absolute test-pairing integrability by integrable_coulombPotential_toReal_mul_laplacian.