Screening paid for by kinetic energy

The nearest-nucleus cutoff, extended Young inequality, and kinetic Lieb–Thirring bound pay for screening. The positive cutoff radius is κ / (2Z + 1).

theorem LiebThirring.Assembly.kinetic_coefficient_pos (q : ℕ) (hq : 1 ≤ q) : 0 < ↑ruminConstant * ↑q ^ (-2 / 3)

Positivity of the real kinetic coefficient for a nonzero spin multiplicity.

theorem LiebThirring.Assembly.kinetic_coefficient_eq (q : ℕ) (hq : 1 ≤ q) : ENNReal.ofReal (↑ruminConstant * ↑q ^ (-2 / 3)) = ↑ruminConstant * ↑q ^ (-2 / 3)

The real kinetic coefficient embeds as the exact extended coefficient.

theorem LiebThirring.Assembly.screening_of_lt (hLT : ∀ (q : ℕ), 1 ≤ q → ∀ (N : ℕ) (ψ : State N q), antisymmetric ψ → ‖ψ‖ = 1 → ↑ruminConstant * ↑q ^ (-2 / 3) * ∫⁻ (x : Position), density ψ x ^ (5 / 3) ≤ kineticEnergy ψ) (q : ℕ) (hq : 1 ≤ q) (Z : NNReal) (N M : ℕ) (R : Fin M → Position) (ψ : State N q) (hanti : antisymmetric ψ) (hnorm : ‖ψ‖ = 1) : ENNReal.ofReal (2 * ↑Z + 1) * ∫⁻ (x : Position), (nearestNucleusDistance R x)⁻¹ * density ψ x ≤ kineticEnergy ψ + ENNReal.ofReal ((2 * ↑Z + 1) ^ 2 / (↑ruminConstant * ↑q ^ (-2 / 3)) * (↑N + 8 * Real.pi * (2 / 5 * (3 / 5) ^ (3 / 2)) * ↑M))

Screening is paid for by the exact kinetic LT hypothesis and the screening cost.