Rumin integration of the high Fourier field

The exact scalar integral and the kinetic layer cake turn the pointwise low-momentum estimate into the kinetic Lieb--Thirring bound.

theorem LiebThirring.rumin_bound_of_lowMomentumBound (q : ℕ) (hq : 1 ≤ q) {N : ℕ} (i : Fin N) (ψ : State N q) (hanti : antisymmetric ψ) (hLow : ∀ (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 the Rumin bound: the exact pointwise low-momentum bound implies the kinetic Lieb--Thirring inequality. the low-momentum bound supplies the sole conditional input.