The finite projection argument underlying the Pauli bound

Finite families of symmetric idempotent lifts with zero double occupancy satisfy a projection-sum bound. The operator relations are explicit hypotheses.

theorem LiebThirring.sum_norm_sq_le_of_projection_relations {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ι : Type u_2} [Fintype ι] (P : ι → E →L[ℂ] E) (ψ : E) (hsym : ∀ (i : ι) (x y : E), inner ℂ ((P i) x) y = inner ℂ x ((P i) y)) (hid : ∀ (i : ι), (P i) ((P i) ψ) = (P i) ψ) (hzero : ∀ (i j : ι), i ≠ j → (P i) ((P j) ψ) = 0) : ∑ i : ι, ‖(P i) ψ‖ ^ 2 ≤ ‖ψ‖ ^ 2

Symmetric idempotent lifts with zero double occupancy have a bounded sum of squared projected norms. All operator relations are explicit inputs to this abstract lemma.

theorem LiebThirring.card_mul_norm_sq_le_of_projection_relations {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ι : Type u_2} [Fintype ι] (P : ι → E →L[ℂ] E) (ψ : E) (hsym : ∀ (i : ι) (x y : E), inner ℂ ((P i) x) y = inner ℂ x ((P i) y)) (hid : ∀ (i : ι), (P i) ((P i) ψ) = (P i) ψ) (hzero : ∀ (i j : ι), i ≠ j → (P i) ((P j) ψ) = 0) (i : ι) (hequal : ∀ (j : ι), ‖(P j) ψ‖ = ‖(P i) ψ‖) : ↑(Fintype.card ι) * ‖(P i) ψ‖ ^ 2 ≤ ‖ψ‖ ^ 2

Equal projection norms turn the projection sum estimate into an occupation estimate. This is abstract infrastructure, not Pauli occupation on the state space.