Finite Coulomb forms and extended-to-real arithmetic

Elementary finite-sum and arithmetic steps for the real quadratic-form corollary. The electron estimate is supplied by RealFormPairs.

theorem LiebThirring.Assembly.nuclearRepulsion_lt_top {M : ℕ} (z : Fin M → NNReal) (R : Fin M → Position) (hR : Function.Injective R) : nuclearRepulsion z R < ⊤

Distinct nuclear positions give finite nuclear repulsion.

theorem LiebThirring.Assembly.real_form_of_extended_bound {A T B U : ENNReal} (C : NNReal) (K : ℕ) (hT : T < ⊤) (hB : B < ⊤) (hU : U < ⊤) (hA : A ≤ T + B + U + ↑C * ↑K) : A < ⊤ ∧ -↑C * ↑K ≤ T.toReal + B.toReal + U.toReal - A.toReal

An extended additive estimate with finite positive terms gives attraction finiteness and the corresponding real energy lower bound.