The basic electrostatic inequality from the Voronoi face charge #
Finite face-charge self-energy, the potential identity, and the energy deficit give the basic electrostatic inequality for distinct nuclei by square completion.
theorem
LiebThirring.basicElectrostaticInequality_of_injective
{M : ℕ}
(hM : 1 ≤ M)
(Z : NNReal)
(R : Fin M → Position)
(hR : Function.Injective R)
:
the basic electrostatic inequality with no analytic premises: the Voronoi charge supplies square completion.