Exact energy bookkeeping conditional on the potential identity

An off-diagonal symmetric finite sum counts its upper triangle twice.

At a nucleus the screened potential omits that nucleus.

theorem LiebThirring.sum_erase_eq_two_sum_upper {M : ℕ} (f : Fin M → Fin M → ENNReal) (hf : ∀ (k l : Fin M), f k l = f l k) : ∑ k : Fin M, ∑ l ∈ Finset.univ.erase k, f k l = 2 * ∑ k : Fin M, ∑ l : Fin M with k < l, f k l

An off-diagonal symmetric finite sum counts its upper triangle twice.

theorem LiebThirring.screenedPotential_at_nucleus_eq_sum {M : ℕ} (Z : NNReal) (R : Fin M → Position) (k : Fin M) : screenedPotential Z R (R k) = ∑ l ∈ Finset.univ.erase k, ↑Z * coulombKernel (R k) (R l)

At a nucleus the screened potential omits that nucleus.

theorem LiebThirring.lintegral_nuclear_attraction_of_potential_eq {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) (k : Fin M) : ∫⁻ (y : Position), ↑Z * coulombKernel y (R k) ∂voronoiFaceMeasure R hR ↑Z = ∑ l ∈ Finset.univ.erase k, ↑Z ^ 2 * coulombKernel (R k) (R l)

Testing the face charge against one nuclear kernel uses exactly the potential identity.

theorem LiebThirring.energy_add_nearestIntegral_eq_two_repulsion_of_potential_eq {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) + ∫⁻ (y : Position), ↑Z * (nearestNucleusDistance R y)⁻¹ ∂voronoiFaceMeasure R hR ↑Z = 2 * nuclearRepulsion (fun (x : Fin M) => Z) R

Additive exact deficit identity, avoiding subtraction of extended quantities.

theorem LiebThirring.half_energy_add_half_nearestIntegral_eq_repulsion_of_potential_eq {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) / 2 + (∫⁻ (y : Position), ↑Z * (nearestNucleusDistance R y)⁻¹ ∂voronoiFaceMeasure R hR ↑Z) / 2 = nuclearRepulsion (fun (x : Fin M) => Z) R

The normalized first equality in the energy deficit, with its the potential identity premise explicit.