The distributional Laplacian of the screened potential

Equation with the explicit unordered genuine-face integrals.

Equation, stated directly with the face measure ν.

theorem LiebThirring.integral_eq_sum_voronoiCells {M : ℕ} (hM : 1 ≤ M) (R : Fin M → Position) (hR : Function.Injective R) (g : Position → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (x : Position), g x = ∑ k : Fin M, ∫ (x : Position) in voronoiCell R k, g x

theorem LiebThirring.integral_screenedPotentialReal_mul_laplacian_faces {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (f : Position → ℝ) (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : ∫ (x : Position), screenedPotentialReal Z R x * Laplacian.laplacian f x = -4 * Real.pi * ∑ p : NuclearPair M, ∫ (x : Position) in voronoiFace R (↑p).1 (↑p).2, nuclearFaceDensity R (↑Z) (↑p).1 (↑p).2 x * f x ∂bisectorSurfaceMeasure R hR (↑p).1 (↑p).2 ⋯

Equation (8.2) with the explicit unordered genuine-face integrals.

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

Equation (8.2), stated directly with the face measure ν.