Baxter's additive inequality at collisions and empty configurations

Meeting a nucleus makes the nearest-nucleus distance zero.

An electron-nucleus collision makes the control infinite, including at zero charge.

theorem LiebThirring.nearestNucleusDistance_eq_zero_of_eq {M : ℕ} (R : Fin M → Position) (a : Position) (k : Fin M) (ha : a = R k) : nearestNucleusDistance R a = 0

Meeting a nucleus makes the nearest-nucleus distance zero.

theorem LiebThirring.nearestNucleusControl_eq_top_of_collision {N M : ℕ} (Z : NNReal) (R : Fin M → Position) (x : Configuration N) (i : Fin N) (k : Fin M) (hx : particlePosition x i = R k) : nearestNucleusControl Z R x = ⊤

An electron-nucleus collision makes the control infinite, including at zero charge.

theorem LiebThirring.nuclearRepulsion_eq_top_of_collision {M : ℕ} (Z : NNReal) (hZ : Z ≠ 0) (R : Fin M → Position) (k l : Fin M) (hkl : k < l) (hR : R k = R l) : nuclearRepulsion (fun (x : Fin M) => Z) R = ⊤

A collision of two positive equally charged nuclei makes nuclear repulsion infinite.

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

Zero charge annihilates attraction and correction even at collisions.

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

With no nuclei, attraction and correction are empty sums.

theorem LiebThirring.baxter_of_basicElectrostaticInequality (hB12 : ∀ (M : ℕ) (Z : NNReal) (R : Fin M → Position), 1 ≤ M → Function.Injective R → BasicElectrostaticInequality Z R) (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

The exact Baxter conclusion from the basic electrostatic inequality, for every endpoint and collision case.