Equality of the screened and face-charge potentials

The screened and face-charge potentials have a weakly harmonic difference. Continuity and decay force that difference to vanish everywhere.

theorem LiebThirring.tendsto_screenedPotentialReal_zero {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) : Filter.Tendsto (screenedPotentialReal Z R) (Bornology.cobounded Position) (nhds 0)

The screened real potential tends uniformly to zero outside large balls.

theorem LiebThirring.screenedPotential_eq_coulombPotential_of_laplacian_identity {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hLap : ∀ (f : Position → ℝ), ContDiff ℝ (↑⊤) f → HasCompactSupport f → ∫ (x : Position), screenedPotentialReal Z R x * Laplacian.laplacian f x = -4 * Real.pi * ∫ (x : Position), f x ∂voronoiFaceMeasure R hR ↑Z) (x : Position) : screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x

the potential identity from the screened-potential test-function identity for smooth compactly supported tests. This is the expansion of the former ScreenedLaplacianIdentity premise.

theorem LiebThirring.screenedPotential_eq_coulombPotential_voronoiFaceMeasure {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (x : Position) : screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x

the potential identity: the actual face-charge measure represents the screened potential everywhere.