Kinetic Lieb--Thirring inequality on the state carrier

The non-vacuum Rumin estimate and the vacuum density identity give the kinetic Lieb–Thirring inequality.

theorem LiebThirring.Kinetic.kinetic_lieb_thirring_of_lowMomentumBound (q : ℕ) (hq : 1 ≤ q) (N : ℕ) (ψ : State N q) (hanti : antisymmetric ψ) (hLow : ∀ (i : Fin N) (E : ℝ), 0 ≤ E → ∀ (x : Position), ‖lowFourierField (densityField i ψ) E x‖ ^ 2 ≤ ↑q * (1 / (6 * Real.pi ^ 2)) * E ^ (3 / 2)) : ↑ruminConstant * ↑q ^ (-2 / 3) * ∫⁻ (x : Position), density ψ x ^ (5 / 3) ≤ kineticEnergy ψ

Conditional assembly with exactly the pointwise low-momentum estimate as its sole extra premise. The final theorem supplies it from the unconditional low-momentum theorem.

theorem LiebThirring.Kinetic.kinetic_lieb_thirring (q : ℕ) (hq : 1 ≤ q) (N : ℕ) (ψ : State N q) (hanti : antisymmetric ψ) (hnorm : ‖ψ‖ = 1) : ↑ruminConstant * ↑q ^ (-2 / 3) * ∫⁻ (x : Position), density ψ x ^ (5 / 3) ≤ kineticEnergy ψ

Proof of the kinetic Lieb--Thirring theorem.