POVM Outcome Lower Bound

Abstract

A normalized finite effect family needs at least d squared outcomes for completeness.

Theorem 1.1 (An informationally complete POVM has at least d squared outcomes).

$$\begin{array}{c}\forall d,m:\mathrm{Nat},\mathrm{NeZero}\left(d\right),\\ E:\mathrm{Fin}\left(m\right)\to \mathrm{HermitianSpace}\left(d\right),\\ \sum _{a\in \mathrm{Fin}\left(m\right)}{E}_a=\mathrm{identityHermitian}\left(d\right)\Rightarrow \\ C_a:=\mathrm{centeredHermitianMap}\left(d,E_a\right),\\ \sum _{a\in \mathrm{Fin}\left(m\right)}{C}_a=0\wedge \\ \mathrm{finrank}\left(\mathbb{R},\mathrm{span}\left(\mathbb{R},\{C_a:a\in \mathrm{Fin}\left(m\right)\}\right)\right)\le m-1\wedge \\ (\mathrm{span}\left(\mathbb{R},\{C_a:a\in \mathrm{Fin}\left(m\right)\}\right)=\mathrm{traceZeroHermitian}\left(d\right)\Rightarrow d^2\le m).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/PovmOutcomeLowerBound.povm_outcome_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The effects are a finite family on the canonical real Hermitian carrier whose sum is the identity. The displayed centered family is constructed by the repository’s canonical trace-removal map.

Normalization gives a nonzero all-ones coefficient relation among the centered effects. Their real span therefore has dimension at most one less than the number of outcomes.

When that span is the whole real trace-zero Hermitian carrier, its dimension is d squared minus one, so the outcome count is at least d squared.

References

• Truth anchor: D5/S3/Quantum/Measurement/PovmOutcomeLowerBound.povm_outcome_lower_bound
• Dependency: D5/S3/Quantum/PredictionDepth/FiniteSequentialWordCertificate
• Dependency: D5/S3/Quantum/Tomography/InformationalCompletenessEquivalence