The Pauli occupation bound

The double coordinate projection is unchanged by exchanging its input coordinates. This holds on every state and for every one-particle vector.

Pauli occupation: the occupation of any spatial-and-spin one-particle vector is at most one in an antisymmetric state, with the state norm kept explicit.

theorem LiebThirring.oneParticleProjection_double_exchange {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (φ : State N q) : (oneParticleProjection i f) ((oneParticleProjection j f) (simultaneousPermutation (Equiv.swap i j) φ)) = (oneParticleProjection i f) ((oneParticleProjection j f) φ)

The double coordinate projection is unchanged by exchanging its input coordinates. This holds on every state and for every one-particle vector.

theorem LiebThirring.oneParticleContraction_pauli {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) : ↑N * ‖(oneParticleContraction i f) ψ‖ ^ 2 ≤ ‖f‖ ^ 2 * ‖ψ‖ ^ 2

Pauli occupation: the occupation of any spatial-and-spin one-particle vector is at most one in an antisymmetric state, with the state norm kept explicit.

theorem LiebThirring.oneParticleContraction_pauli_of_norm_eq_one {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) (hnorm : ‖ψ‖ = 1) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) : ↑N * ‖(oneParticleContraction i f) ψ‖ ^ 2 ≤ ‖f‖ ^ 2

The normalized Pauli occupation estimate consumed by the low-momentum bound.