Gleason's theorem, finite-dimensional: the projection package and its frame function

Category: 1-Mathlib (CSD-free; staged for upstream). The statement side of the finite-dimensional Gleason theorem, and the reductions of its "Layer A" that are pure linear algebra (specs/gleason-feasibility.md).

A projection package on ℂᴺ assigns to every orthogonal projection P (an IsStarProjection matrix — self-adjoint idempotent) a number p P with 0 ≤ p P, p 1 = 1, and p (P + Q) = p P + p Q whenever P * Q = 0. Gleason's theorem says that for N ≥ 3 such a p is P ↦ Tr(ρ P) for a unique density matrix ρ; the theorem is Gleason/Core.lean (and its real counterpart Gleason/Real.lean), and this file sets up:

• rankOne v = |v⟩⟨v|, a star projection for ‖v‖ = 1 (isStarProjection_rankOne), phase invariant (rankOne_smul_of_norm_one), with ∑ᵢ rankOne (bᵢ) = 1 over every orthonormal basis (sum_rankOne_orthonormalBasis) and pairwise-orthogonal products over orthonormal families;
• ProjectionPackage.p_sum — additivity over any finite family of pairwise-orthogonal projections (induction on IsStarProjection.add), p_zero, p_le_one;
• A1, the frame function frame v = p (rankOne v): nonnegative, at most 1, constant on phases (frame_smul), summing to 1 over every orthonormal basis (sum_frame_orthonormalBasis), i.e. IsFrameFunction ℂ OP.frame 1;
• A2, restriction: for a complex-orthonormal family e : Fin k → ℂᴺ, the function realRestrict OP e x = frame (∑ᵢ xᵢ eᵢ) on ℝᵏ is a real frame function with weight p (∑ᵢ rankOne (eᵢ)) (isFrameFunction_realRestrict) — for k = 3 a frame function on the real sphere S², the input of Gleason's core lemma.

Design

Projections are matrices with IsStarProjection (Mathlib's self-adjoint idempotents), and p is a total function on matrices whose values off the projections are never constrained: this keeps every statement free of subtypes, and Mathlib's IsStarProjection.add is exactly the closure property the additivity axiom needs. Vectors live in EuclideanSpace ℂ (Fin N) and rank-one projections are vecMulVec v (star v), so Matrix.posSemidef_vecMulVec_self_star and the vecMulVec calculus apply verbatim.

Source

Gleason 1957, J. Math. Mech. 6, 885 (§1 frame functions, §3 the complex reduction); Cooke–Keane–Moran 1985, Math. Proc. Cambridge Philos. Soc. 98, 117 (the elementary proof of the core lemma).

Column matrices and Gram identities, over any RCLike field

def Gleason.colMatrix {𝕜 : Type u_1} {N k : ℕ} (e : Fin k → EuclideanSpace 𝕜 (Fin N)) : Matrix (Fin N) (Fin k) 𝕜

The matrix whose i-th column is e i.

Equations

• Gleason.colMatrix e = Matrix.of fun (a : Fin N) (i : Fin k) => (e i).ofLp a

@[simp]

theorem Gleason.colMatrix_apply {𝕜 : Type u_1} {N k : ℕ} (e : Fin k → EuclideanSpace 𝕜 (Fin N)) (a : Fin N) (i : Fin k) : colMatrix e a i = (e i).ofLp a

theorem Gleason.conjTranspose_mul_colMatrix_apply {𝕜 : Type u_1} [RCLike 𝕜] {N k : ℕ} (e : Fin k → EuclideanSpace 𝕜 (Fin N)) (i j : Fin k) : ((colMatrix e).conjTranspose * colMatrix e) i j = inner 𝕜 (e i) (e j)

The Gram matrix of a family: (Eᴴ E) i j = ⟪e i, e j⟫.

theorem Gleason.conjTranspose_mul_colMatrix_of_orthonormal {𝕜 : Type u_1} [RCLike 𝕜] {N k : ℕ} {e : Fin k → EuclideanSpace 𝕜 (Fin N)} (he : Orthonormal 𝕜 e) : (colMatrix e).conjTranspose * colMatrix e = 1

An orthonormal family has Gram matrix 1.

theorem Gleason.colMatrix_mul_conjTranspose_of_orthonormalBasis {𝕜 : Type u_1} [RCLike 𝕜] {N : ℕ} (b : OrthonormalBasis (Fin N) 𝕜 (EuclideanSpace 𝕜 (Fin N))) : colMatrix ⇑b * (colMatrix ⇑b).conjTranspose = 1

An orthonormal basis has E Eᴴ = 1 as well (square matrices).

theorem Gleason.colMatrix_mulVec {𝕜 : Type u_1} [RCLike 𝕜] {N k : ℕ} (e : Fin k → EuclideanSpace 𝕜 (Fin N)) (c : Fin k → 𝕜) : (colMatrix e).mulVec c = (∑ i : Fin k, c i • e i).ofLp

E *ᵥ c = ∑ᵢ cᵢ • eᵢ.

theorem Gleason.sum_vecMulVec_eq_colMatrix_mul {𝕜 : Type u_1} [RCLike 𝕜] {N k : ℕ} (e : Fin k → EuclideanSpace 𝕜 (Fin N)) : ∑ i : Fin k, Matrix.vecMulVec (e i).ofLp (star (e i).ofLp) = colMatrix e * (colMatrix e).conjTranspose

∑ᵢ |eᵢ⟩⟨eᵢ| = E Eᴴ.

Rank-one projections

def Gleason.rankOne {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) : Matrix (Fin N) (Fin N) ℂ

The rank-one projection |v⟩⟨v| onto v (a projection when ‖v‖ = 1).

Equations

• Gleason.rankOne v = Matrix.vecMulVec v.ofLp (star v.ofLp)

theorem Gleason.rankOne_apply {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) (a c : Fin N) : rankOne v a c = v.ofLp a * (starRingEnd ((fun (x : Fin N) => ℂ) c)) (v.ofLp c)

theorem Gleason.rankOne_posSemidef {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) : (rankOne v).PosSemidef

theorem Gleason.rankOne_isHermitian {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) : (rankOne v).IsHermitian

theorem Gleason.rankOne_mul_rankOne {N : ℕ} (v w : EuclideanSpace ℂ (Fin N)) : rankOne v * rankOne w = inner ℂ v w • Matrix.vecMulVec v.ofLp (star w.ofLp)

|v⟩⟨v| |w⟩⟨w| = ⟪v, w⟫ |v⟩⟨w|.

theorem Gleason.rankOne_mul_self {N : ℕ} {v : EuclideanSpace ℂ (Fin N)} (hv : ‖v‖ = 1) : rankOne v * rankOne v = rankOne v

theorem Gleason.rankOne_mul_rankOne_of_inner_eq_zero {N : ℕ} {v w : EuclideanSpace ℂ (Fin N)} (h : inner ℂ v w = 0) : rankOne v * rankOne w = 0

theorem Gleason.isStarProjection_rankOne {N : ℕ} {v : EuclideanSpace ℂ (Fin N)} (hv : ‖v‖ = 1) : IsStarProjection (rankOne v)

|v⟩⟨v| is an orthogonal projection for every unit vector v.

theorem Gleason.rankOne_smul_of_norm_one {N : ℕ} {c : ℂ} (hc : ‖c‖ = 1) (v : EuclideanSpace ℂ (Fin N)) : rankOne (c • v) = rankOne v

Phase invariance: |c v⟩⟨c v| = |v⟩⟨v| for ‖c‖ = 1.

theorem Gleason.rankOne_mul_rankOne_of_orthonormal {N k : ℕ} {e : Fin k → EuclideanSpace ℂ (Fin N)} (he : Orthonormal ℂ e) {i j : Fin k} (hij : i ≠ j) : rankOne (e i) * rankOne (e j) = 0

The rank-one projections of an orthonormal family are pairwise orthogonal.

theorem Gleason.sum_rankOne_eq {N : ℕ} (e : Fin N → EuclideanSpace ℂ (Fin N)) : ∑ i : Fin N, rankOne (e i) = colMatrix e * (colMatrix e).conjTranspose

∑ᵢ |eᵢ⟩⟨eᵢ| = E Eᴴ for the column matrix E of the family.

theorem Gleason.sum_rankOne_orthonormalBasis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : ∑ i : Fin N, rankOne (b i) = 1

Resolution of the identity: ∑ᵢ |bᵢ⟩⟨bᵢ| = 1 over an orthonormal basis.

Frame functions

def Gleason.IsFrameFunction (𝕜 : Type u_1) [RCLike 𝕜] {n : ℕ} (f : EuclideanSpace 𝕜 (Fin n) → ℝ) (W : ℝ) : Prop

A frame function on 𝕜ⁿ with weight W: ∑ᵢ f (bᵢ) = W over every orthonormal basis (Gleason 1957, §1).

Equations

• Gleason.IsFrameFunction 𝕜 f W = ∀ (b : OrthonormalBasis (Fin n) 𝕜 (EuclideanSpace 𝕜 (Fin n))), ∑ i : Fin n, f (b i) = W

The projection package

structure Gleason.ProjectionPackage (N : ℕ) : Type

A projection package on ℂᴺ: a nonnegative, normalised, orthogonally additive assignment on the orthogonal projections. The values of p off the projections are unconstrained and never used.

• p : Matrix (Fin N) (Fin N) ℂ → ℝ

  The assignment.

• nonneg (P : Matrix (Fin N) (Fin N) ℂ) : IsStarProjection P → 0 ≤ self.p P

  0 ≤ p P for every projection.

• total_one : self.p 1 = 1

  p 1 = 1.

• additive (P Q : Matrix (Fin N) (Fin N) ℂ) : IsStarProjection P → IsStarProjection Q → P * Q = 0 → self.p (P + Q) = self.p P + self.p Q

  p (P + Q) = p P + p Q for orthogonal projections (P * Q = 0).

theorem Gleason.ProjectionPackage.p_zero {N : ℕ} (OP : ProjectionPackage N) : OP.p 0 = 0

p 0 = 0: 0 = 0 + 0 with 0 * 0 = 0.

theorem Gleason.ProjectionPackage.p_le_one {N : ℕ} (OP : ProjectionPackage N) {P : Matrix (Fin N) (Fin N) ℂ} (hP : IsStarProjection P) : OP.p P ≤ 1

p P ≤ 1: P + (1 − P) = 1 and p (1 − P) ≥ 0.

theorem Gleason.ProjectionPackage.isStarProjection_sum {N : ℕ} {ι : Type u_1} (P : ι → Matrix (Fin N) (Fin N) ℂ) (hP : ∀ (i : ι), IsStarProjection (P i)) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) (s : Finset ι) : IsStarProjection (∑ i ∈ s, P i)

A finite sum of pairwise-orthogonal projections is a projection.

theorem Gleason.ProjectionPackage.p_sum {N : ℕ} (OP : ProjectionPackage N) {ι : Type u_1} (P : ι → Matrix (Fin N) (Fin N) ℂ) (hP : ∀ (i : ι), IsStarProjection (P i)) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) (s : Finset ι) : OP.p (∑ i ∈ s, P i) = ∑ i ∈ s, OP.p (P i)

Additivity over any finite family of pairwise-orthogonal projections.

def Gleason.ProjectionPackage.frame {N : ℕ} (OP : ProjectionPackage N) (v : EuclideanSpace ℂ (Fin N)) : ℝ

The frame function of the package: frame v = p |v⟩⟨v|.

Equations

• OP.frame v = OP.p (Gleason.rankOne v)

theorem Gleason.ProjectionPackage.frame_nonneg {N : ℕ} (OP : ProjectionPackage N) {v : EuclideanSpace ℂ (Fin N)} (hv : ‖v‖ = 1) : 0 ≤ OP.frame v

theorem Gleason.ProjectionPackage.frame_le_one {N : ℕ} (OP : ProjectionPackage N) {v : EuclideanSpace ℂ (Fin N)} (hv : ‖v‖ = 1) : OP.frame v ≤ 1

theorem Gleason.ProjectionPackage.frame_smul {N : ℕ} (OP : ProjectionPackage N) {c : ℂ} (hc : ‖c‖ = 1) (v : EuclideanSpace ℂ (Fin N)) : OP.frame (c • v) = OP.frame v

The frame function is constant on phases.

theorem Gleason.ProjectionPackage.p_sum_rankOne {N : ℕ} (OP : ProjectionPackage N) {k : ℕ} {e : Fin k → EuclideanSpace ℂ (Fin N)} (he : Orthonormal ℂ e) : OP.p (∑ i : Fin k, rankOne (e i)) = ∑ i : Fin k, OP.frame (e i)

Additivity over the rank-one projections of an orthonormal family.

theorem Gleason.ProjectionPackage.sum_frame_orthonormalBasis {N : ℕ} (OP : ProjectionPackage N) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : ∑ i : Fin N, OP.frame (b i) = 1

A1. The frame function sums to 1 over every orthonormal basis.

theorem Gleason.ProjectionPackage.isFrameFunction_frame {N : ℕ} (OP : ProjectionPackage N) : IsFrameFunction ℂ OP.frame 1

A1, packaged: frame is a complex frame function of weight 1.

A2 — restriction to a completely real subspace

def Gleason.ProjectionPackage.realCombination {N k : ℕ} (e : Fin k → EuclideanSpace ℂ (Fin N)) (x : EuclideanSpace ℝ (Fin k)) : EuclideanSpace ℂ (Fin N)

The vectors of ℂᴺ with real coordinates in a complex-orthonormal family e: the completely real subspace span_ℝ {e₁, …, eₖ}, parametrised by ℝᵏ.

Equations

• Gleason.ProjectionPackage.realCombination e x = ∑ i : Fin k, ↑(x.ofLp i) • e i

theorem Gleason.ProjectionPackage.colMatrix_map_ofReal {k : ℕ} (b : Fin k → EuclideanSpace ℝ (Fin k)) : (colMatrix fun (j : Fin k) => WithLp.toLp 2 fun (i : Fin k) => ↑((b j).ofLp i)) = (colMatrix b).map Complex.ofReal

The complex column matrix of a real vector family.

theorem Gleason.ProjectionPackage.orthonormal_realCombination {N k : ℕ} {e : Fin k → EuclideanSpace ℂ (Fin N)} (he : Orthonormal ℂ e) {b : Fin k → EuclideanSpace ℝ (Fin k)} (hb : Orthonormal ℝ b) : Orthonormal ℂ fun (j : Fin k) => realCombination e (b j)

Transporting a real orthonormal family through a complex-orthonormal e gives a complex-orthonormal family: Gram = Bᴴ (Eᴴ E) B = Bᴴ B = 1.

theorem Gleason.ProjectionPackage.sum_rankOne_realCombination {N k : ℕ} (e : Fin k → EuclideanSpace ℂ (Fin N)) (b : OrthonormalBasis (Fin k) ℝ (EuclideanSpace ℝ (Fin k))) : ∑ j : Fin k, rankOne (realCombination e (b j)) = ∑ i : Fin k, rankOne (e i)

The rank-one projections of a transported orthonormal basis sum to those of e: ∑ⱼ |wⱼ⟩⟨wⱼ| = E (B Bᴴ) Eᴴ = E Eᴴ = ∑ᵢ |eᵢ⟩⟨eᵢ|.

theorem Gleason.ProjectionPackage.norm_realCombination {N k : ℕ} {e : Fin k → EuclideanSpace ℂ (Fin N)} (he : Orthonormal ℂ e) {x : EuclideanSpace ℝ (Fin k)} (hx : ‖x‖ = 1) : ‖realCombination e x‖ = 1

A real unit vector transports to a complex unit vector.

def Gleason.ProjectionPackage.realRestrict {N : ℕ} (OP : ProjectionPackage N) {k : ℕ} (e : Fin k → EuclideanSpace ℂ (Fin N)) (x : EuclideanSpace ℝ (Fin k)) : ℝ

The restriction of the frame function to a completely real subspace, as a function on ℝᵏ: realRestrict OP e x = frame (∑ᵢ xᵢ eᵢ).

Equations

• OP.realRestrict e x = OP.frame (Gleason.ProjectionPackage.realCombination e x)

theorem Gleason.ProjectionPackage.isFrameFunction_realRestrict {N : ℕ} (OP : ProjectionPackage N) {k : ℕ} {e : Fin k → EuclideanSpace ℂ (Fin N)} (he : Orthonormal ℂ e) : IsFrameFunction ℝ (OP.realRestrict e) (OP.p (∑ i : Fin k, rankOne (e i)))

A2. For a complex-orthonormal e : Fin k → ℂᴺ, the restriction is a real frame function on ℝᵏ with weight p (∑ᵢ |eᵢ⟩⟨eᵢ|) — for k = 3, a frame function on the sphere S².

theorem Gleason.ProjectionPackage.realRestrict_nonneg {N : ℕ} (OP : ProjectionPackage N) {k : ℕ} {e : Fin k → EuclideanSpace ℂ (Fin N)} (he : Orthonormal ℂ e) {x : EuclideanSpace ℝ (Fin k)} (hx : ‖x‖ = 1) : 0 ≤ OP.realRestrict e x

The restriction is nonnegative on the real unit sphere.