Extending a unit-vector occupation bound by scaling

A unit-vector Pauli bound extends to every one-particle vector, including zero. This is a conditional scaling helper, not the unconditional Pauli occupation result.

theorem LiebThirring.oneParticleContraction_pauli_of_unit_bound {N q : ℕ} (i : Fin N) (ψ : State N q) (hunit : ∀ (g : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)), ‖g‖ = 1 → ↑N * ‖(oneParticleContraction i g) ψ‖ ^ 2 ≤ ‖ψ‖ ^ 2) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) : ↑N * ‖(oneParticleContraction i f) ψ‖ ^ 2 ≤ ‖f‖ ^ 2 * ‖ψ‖ ^ 2

A unit-vector Pauli bound extends to every one-particle vector, including zero. This is a conditional scaling helper, not the unconditional Pauli occupation result.