Exterior half-space lower bound for the Baxter correction

Exact normalization of one half-space contribution.

Each exterior contributes the required nearest-other inverse distance.

theorem LiebThirring.inverse_fourth_halfSpace_coefficient (Z : NNReal) (d : ℝ) (hd : 0 < d) : ENNReal.ofReal (↑Z ^ 2 / (8 * Real.pi)) * ENNReal.ofReal (Real.pi / (d / 2)) = ↑Z ^ 2 / 4 * (ENNReal.ofReal d)⁻¹

Exact normalization of one half-space contribution.

theorem LiebThirring.baxterCorrection_summand_le_exterior_integral {M : ℕ} (hM : 2 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) : ↑Z ^ 2 / 4 * (nearestOtherNucleusDistance R k)⁻¹ ≤ ENNReal.ofReal (↑Z ^ 2 / (8 * Real.pi)) * ∫⁻ (x : Position) in (voronoiCell R k)ᶜ, ENNReal.ofReal (‖x - R k‖ ^ 4)⁻¹

Each exterior contributes the required nearest-other inverse distance.

theorem LiebThirring.baxterCorrection_le_exterior_integrals {M : ℕ} (hM : 2 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) : baxterCorrection Z R ≤ ENNReal.ofReal (↑Z ^ 2 / (8 * Real.pi)) * ∑ k : Fin M, ∫⁻ (x : Position) in (voronoiCell R k)ᶜ, ENNReal.ofReal (‖x - R k‖ ^ 4)⁻¹

The entire nearest-nucleus correction is bounded by the exterior integral sum.