Real quadratic-form stability

Finiteness of Coulomb expectations and real quadratic-form stability, using the Fourier Hardy bound and extended stability with the same constant.

theorem LiebThirring.stability_of_matter_real (q : ℕ) (hq : 1 ≤ q) (Z : NNReal) : ∃ (C : NNReal), 0 < C ∧ ∀ (N M : ℕ) (z : Fin M → NNReal) (R : Fin M → Position) (ψ : State N q), (∀ (k : Fin M), z k ≤ Z) → Function.Injective R → antisymmetric ψ → ‖ψ‖ = 1 → kineticEnergy ψ < ⊤ → ∫⁻ (x : Configuration N), attraction z R x * ↑‖↑↑ψ x‖₊ ^ 2 < ⊤ ∧ ∫⁻ (x : Configuration N), electronRepulsion x * ↑‖↑↑ψ x‖₊ ^ 2 < ⊤ ∧ nuclearRepulsion z R < ⊤ ∧ -↑C * ↑(N + M) ≤ (kineticEnergy ψ).toReal + (∫⁻ (x : Configuration N), electronRepulsion x * ↑‖↑↑ψ x‖₊ ^ 2).toReal + (nuclearRepulsion z R).toReal - (∫⁻ (x : Configuration N), attraction z R x * ↑‖↑↑ψ x‖₊ ^ 2).toReal