Baxter shell assembly from the basic electrostatic inequality

The inverse half-distance is twice the inverse distance, in the extended reals.

Shell assembly for nonempty nuclei and electrons away from nuclear singularities. No electron separation is needed in this additive extended proof.

theorem LiebThirring.inv_ofReal_half (d : ℝ) : (ENNReal.ofReal (d / 2))⁻¹ = 2 * (ENNReal.ofReal d)⁻¹

The inverse half-distance is twice the inverse distance, in the extended reals.

theorem LiebThirring.baxter_of_basicElectrostaticInequality_of_separated {N M : ℕ} (Z : NNReal) (R : Fin M → Position) (x : Configuration N) (hM : 1 ≤ M) (hB12 : BasicElectrostaticInequality Z R) (hx : ∀ (i : Fin N) (k : Fin M), particlePosition x i ≠ R k) : attraction (fun (x : Fin M) => Z) R x + baxterCorrection Z R ≤ electronRepulsion x + nuclearRepulsion (fun (x : Fin M) => Z) R + nearestNucleusControl Z R x

Shell assembly for nonempty nuclei and electrons away from nuclear singularities. No electron separation is needed in this additive extended proof.