The unconditional low-momentum density bound

Each low-field spin component is bounded by the phase-space volume.

Summing the spin components gives q times the low-region volume.

theorem LiebThirring.lowFourierField_density_component_bound {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) (hnorm : ‖ψ‖ = 1) (E : ℝ) (hE : 0 ≤ E) (x : Position) (s : Fin q) : ‖(lowFourierField (densityField i ψ) E x).ofLp s‖ ^ 2 ≤ (MeasureTheory.volume (lowMomentumRegion E)).toReal

Each low-field spin component is bounded by the phase-space volume.

theorem LiebThirring.lowFourierField_density_bound_volume {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) (hnorm : ‖ψ‖ = 1) (E : ℝ) (hE : 0 ≤ E) (x : Position) : ‖lowFourierField (densityField i ψ) E x‖ ^ 2 ≤ ↑q * (MeasureTheory.volume (lowMomentumRegion E)).toReal

Summing the spin components gives q times the low-region volume.

theorem LiebThirring.lowFourierField_density_bound {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) (hnorm : ‖ψ‖ = 1) (E : ℝ) (hE : 0 ≤ E) (x : Position) : ‖lowFourierField (densityField i ψ) E x‖ ^ 2 ≤ ↑q * (1 / (6 * Real.pi ^ 2)) * E ^ (3 / 2)

the low-momentum bound: the scaled density field has the exact three-dimensional low-momentum bound at every spatial point, with no finite-energy or positive-spin premise.