Abstract square completion for the basic electrostatic inequality #
Coulomb positivity gives the basic electrostatic inequality from a finite-energy screening measure with the prescribed potential and nuclear-energy deficit.
theorem
LiebThirring.basicElectrostaticInequality_of_potential
{M : ℕ}
(Z : NNReal)
(R : Fin M → Position)
(ν : MeasureTheory.Measure Position)
[MeasureTheory.IsFiniteMeasure ν]
(hνE : coulombEnergy ν ν ≠ ⊤)
(hΦ : ∀ (x : Position), screenedPotential Z R x = coulombPotential ν x)
(hdef : coulombEnergy ν ν / 2 + baxterCorrection Z R ≤ nuclearRepulsion (fun (x : Fin M) => Z) R)
:
the basic electrostatic inequality from a finite-energy screening measure with the prescribed potential and nuclear-energy deficit.