Conditional specialization of the projection argument to State

For unit one-particle vectors, the Pauli estimate follows from the two concrete lift relations supplied as explicit hypotheses.

The complete occupation estimate conditional on the global contraction double-exchange identity. Covariance, norm equality, and nonunit scaling are discharged by proved lemmas on the actual State carrier.

theorem LiebThirring.oneParticleContraction_pauli_unit_of_lift_relations {N q : ℕ} (i : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (hf : ‖f‖ = 1) (ψ : State N q) (hψ : antisymmetric ψ) (hdouble : ∀ (k l : Fin N), k ≠ l → ∀ (φ : State N q), (oneParticleProjection k f) ((oneParticleProjection l f) (simultaneousPermutation (Equiv.swap k l) φ)) = (oneParticleProjection k f) ((oneParticleProjection l f) φ)) (hequal : ∀ (j : Fin N), ‖(oneParticleProjection j f) ψ‖ = ‖(oneParticleProjection i f) ψ‖) : ↑N * ‖(oneParticleContraction i f) ψ‖ ^ 2 ≤ ‖ψ‖ ^ 2

For unit one-particle vectors, the Pauli estimate follows from the two concrete lift relations supplied as explicit hypotheses.

theorem LiebThirring.oneParticleContraction_pauli_of_double_exchange {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) (hdouble : ∀ (g : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)), ‖g‖ = 1 → ∀ (k l : Fin N), k ≠ l → ∀ (φ : State N q), (oneParticleProjection k g) ((oneParticleProjection l g) (simultaneousPermutation (Equiv.swap k l) φ)) = (oneParticleProjection k g) ((oneParticleProjection l g) φ)) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) : ↑N * ‖(oneParticleContraction i f) ψ‖ ^ 2 ≤ ‖f‖ ^ 2 * ‖ψ‖ ^ 2

The complete occupation estimate conditional on the global contraction double-exchange identity. Covariance, norm equality, and nonunit scaling are discharged by proved lemmas on the actual State carrier.