Baxter

Baxter’s electrostatic inequality, including collisions and empty configurations, from the Voronoi boundary measure argument.

theorem LiebThirring.baxter (N M : ℕ) (Z : NNReal) (R : Fin M → Position) (x : Configuration N) : attraction (fun (x : Fin M) => Z) R x + baxterCorrection Z R ≤ electronRepulsion x + nuclearRepulsion (fun (x : Fin M) => Z) R + nearestNucleusControl Z R x