Gleason's theorem, finite-dimensional: the descent from a quadratic form to the density matrix

Category: 1-Mathlib (CSD-free; staged for upstream). "Layer C" of specs/gleason-feasibility.md: everything that follows once the frame function is known to be the quadratic form of a Hermitian matrix on the unit sphere. Shared by Busch's effect theorem (LF2/EffectGleason.lean, whose state conditions and uniqueness are re-routed through quadraticForm_on_sphere_to_density) and the projection theorem.

• posSemidef_of_sphere_nonneg — a Hermitian matrix whose quadratic form is nonnegative on the unit sphere is positive semidefinite;
• trace_eq_sum_sphere — its trace is the sum of the quadratic form over the standard basis;
• eq_of_sphere_quadForm_eq — two Hermitian matrices with the same quadratic form on the unit sphere are equal (scale off the sphere, then matrix_eq_zero_of_quadForm_zero);
• ★ quadraticForm_on_sphere_to_density — the three packaged: if f v = Re ⟪v, A v⟫ on the sphere with f ≥ 0 and ∑ᵢ f eᵢ = 1, then A is a density matrix and is the only Hermitian matrix with that quadratic form on the sphere;
• ProjectionPackage.p_eq_re_trace — the projection descent: a package whose frame function is the quadratic form of A on the sphere satisfies p P = Re Tr(A P) for every projection P (spectral resolution P = ∑ λᵢ |bᵢ⟩⟨bᵢ| with λᵢ ∈ {0, 1}, additivity over the pairwise-orthogonal rank-ones);
• ★★ ProjectionPackage.existsUnique_density_of_frame_quadratic — Gleason's conclusion from the quadratic-form hypothesis: a unique density matrix ρ with p P = Re Tr(ρ P) for every projection. What Gleason's theorem adds is that the hypothesis holds whenever N ≥ 3 (specs/gleason-feasibility.md, the core lemma).

Source

Gleason 1957, J. Math. Mech. 6, 885, §1 (frame functions and their weights) and the end of §3.

The quadratic form of a Hermitian matrix

theorem Gleason.star_smul_dotProduct_mulVec_smul {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (c : ℂ) (x : Fin N → ℂ) : star (c • x) ⬝ᵥ A.mulVec (c • x) = (starRingEnd ℂ) c * c * star x ⬝ᵥ A.mulVec x

Scaling the argument of a quadratic form: ⟨c x, A (c x)⟩ = conj c · c · ⟨x, A x⟩.

theorem Gleason.conj_star_dotProduct_mulVec {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (x : Fin N → ℂ) : (starRingEnd ℂ) (star x ⬝ᵥ A.mulVec x) = star x ⬝ᵥ A.mulVec x

The quadratic form of a Hermitian matrix is conjugation invariant (real).

theorem Gleason.ofReal_re_star_dotProduct_mulVec {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (x : Fin N → ℂ) : ↑(star x ⬝ᵥ A.mulVec x).re = star x ⬝ᵥ A.mulVec x

The quadratic form of a Hermitian matrix is its real part.

theorem Gleason.exists_norm_one_smul_eq {N : ℕ} {x : Fin N → ℂ} (hx : x ≠ 0) : ∃ (r : ℝ) (v : EuclideanSpace ℂ (Fin N)), 0 < r ∧ ‖v‖ = 1 ∧ x = ↑r • v.ofLp

Every nonzero vector is a positive multiple of a unit vector of EuclideanSpace.

theorem Gleason.posSemidef_of_sphere_nonneg {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (h : ∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → 0 ≤ (star v.ofLp ⬝ᵥ A.mulVec v.ofLp).re) : A.PosSemidef

A Hermitian matrix with nonnegative quadratic form on the unit sphere is positive semidefinite.

theorem Gleason.star_single_dotProduct_mulVec_single {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (i : Fin N) : star (EuclideanSpace.single i 1).ofLp ⬝ᵥ A.mulVec (EuclideanSpace.single i 1).ofLp = A i i

The quadratic form at a standard basis vector is the diagonal entry.

theorem Gleason.trace_eq_sum_sphere {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) : A.trace = ∑ i : Fin N, star (EuclideanSpace.single i 1).ofLp ⬝ᵥ A.mulVec (EuclideanSpace.single i 1).ofLp

The trace is the sum of the quadratic form over the standard basis.

theorem Gleason.ofReal_re_trace {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) : ↑A.trace.re = A.trace

The trace of a Hermitian matrix is real.

theorem Gleason.eq_of_sphere_quadForm_eq {N : ℕ} {A B : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (h : ∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → (star v.ofLp ⬝ᵥ A.mulVec v.ofLp).re = (star v.ofLp ⬝ᵥ B.mulVec v.ofLp).re) : A = B

Two Hermitian matrices with the same quadratic form on the unit sphere are equal.

theorem Gleason.quadraticForm_on_sphere_to_density {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) {f : EuclideanSpace ℂ (Fin N) → ℝ} (hf : ∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → f v = (star v.ofLp ⬝ᵥ A.mulVec v.ofLp).re) (h0 : ∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) (h1 : ∑ i : Fin N, f (EuclideanSpace.single i 1) = 1) : A.PosSemidef ∧ A.trace = 1 ∧ ∀ (B : Matrix (Fin N) (Fin N) ℂ), B.IsHermitian → (∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → f v = (star v.ofLp ⬝ᵥ B.mulVec v.ofLp).re) → B = A

★ From a quadratic form on the sphere to a density matrix. If f v = Re ⟪v, A v⟫ for every unit v, with A Hermitian, f ≥ 0 on the sphere and ∑ᵢ f eᵢ = 1 over the standard basis, then A is positive semidefinite with unit trace, and it is the only Hermitian matrix whose quadratic form on the sphere is f.

The projection descent

theorem Matrix.IsHermitian.eq_sum_eigenvalues_smul_rankOne {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) : A = ∑ i : Fin N, hA.eigenvalues i • Gleason.rankOne (hA.eigenvectorBasis i)

Spectral resolution as a sum of rank-ones: A = ∑ᵢ λᵢ |bᵢ⟩⟨bᵢ| over the eigenvector basis of a Hermitian matrix.

theorem Gleason.eigenvalues_eq_zero_or_one {N : ℕ} {P : Matrix (Fin N) (Fin N) ℂ} (hP : IsStarProjection P) (hPh : P.IsHermitian) (i : Fin N) : hPh.eigenvalues i = 0 ∨ hPh.eigenvalues i = 1

The eigenvalues of an orthogonal projection are 0 or 1.

theorem Gleason.ProjectionPackage.isStarProjection_smul_rankOne {N : ℕ} {l : ℝ} (hl : l = 0 ∨ l = 1) {b : EuclideanSpace ℂ (Fin N)} (hb : ‖b‖ = 1) : IsStarProjection (l • rankOne b)

The weighted rank-one λ • |b⟩⟨b| with λ ∈ {0, 1} is a projection.

theorem Gleason.ProjectionPackage.p_smul_rankOne {N : ℕ} (OP : ProjectionPackage N) {l : ℝ} (hl : l = 0 ∨ l = 1) (b : EuclideanSpace ℂ (Fin N)) : OP.p (l • rankOne b) = l * OP.frame b

p (λ • |b⟩⟨b|) = λ · frame b for λ ∈ {0, 1}.

theorem Gleason.ProjectionPackage.p_eq_re_trace {N : ℕ} (OP : ProjectionPackage N) {A : Matrix (Fin N) (Fin N) ℂ} (hf : ∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → OP.frame v = (star v.ofLp ⬝ᵥ A.mulVec v.ofLp).re) {P : Matrix (Fin N) (Fin N) ℂ} (hP : IsStarProjection P) : OP.p P = (A * P).trace.re

The projection descent. If the frame function is the quadratic form of a matrix A on the unit sphere, then p P = Re Tr(A P) for every orthogonal projection P.

theorem Gleason.ProjectionPackage.existsUnique_density_of_frame_quadratic {N : ℕ} (OP : ProjectionPackage N) {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (hf : ∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → OP.frame v = (star v.ofLp ⬝ᵥ A.mulVec v.ofLp).re) : ∃! ρ : Matrix (Fin N) (Fin N) ℂ, ρ.PosSemidef ∧ ρ.trace = 1 ∧ ∀ (P : Matrix (Fin N) (Fin N) ℂ), IsStarProjection P → OP.p P = (ρ * P).trace.re

★★ Gleason's conclusion from the quadratic-form hypothesis. If the frame function of a projection package is the quadratic form of a Hermitian matrix on the unit sphere, then there is a unique density matrix ρ with p P = Re Tr(ρ P) for every orthogonal projection P.