Kinetic Lieb–Thirring inequality

The kinetic Lieb–Thirring inequality for normalized antisymmetric L² states, from the Pauli occupation estimate and Rumin integration.

theorem LiebThirring.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 ψ