Real-form stability conditional on the one-body Hardy bound

The one-body Hardy bound gives finite Coulomb expectations and a real quadratic-form inequality with the same constant as extended stability.

theorem LiebThirring.Assembly.stability_of_matter_real_of_one_body_bound (q : ℕ) (hq : 1 ≤ q) (Z : NNReal) (hHardy : ∀ (N : ℕ) (c : Position) (u : ↥(MeasureTheory.Lp (SpinAmplitudes N q) 2 MeasureTheory.volume)), ∫⁻ (x : Position), coulombKernel x c * ↑‖↑↑u x‖₊ ^ 2 ≤ ↑‖u‖₊ ^ 2 + 4 * ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position (SpinAmplitudes N q)) u) ξ‖₊ ^ 2) : ∃ (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

Real-form stability from additive stability and the one-body Fourier Coulomb bound.