Gleason's theorem (finite-dimensional)

gleason_theorem_finite

Submitter: Kim Morrison.

Notes: Gleason's theorem in finite dimensions: every frame function on the orthogonal projections of a complex Hilbert space of dimension at least 3 is given by P ↦ Tr(ρ P) for the unique density operator ρ. Stated using a bespoke `FrameFunction` structure (non-negative, additive on orthogonal projection pairs, normalized at the identity) and the standard Mathlib trace `LinearMap.trace`. Finite additivity on orthogonal pairs already implies countable additivity in finite dimensions, so the hypothesis matches Gleason's original σ-additive frame functions.

Source: A. M. Gleason, Measures on the closed subspaces of a Hilbert space, J. Math. Mech. 6 (1957), 885-893.

Informal solution: Gleason's original proof analyses regular frame functions on the unit sphere of R^3 by showing they are continuous and then quadratic, then promotes the resulting positive quadratic form on every 3-dimensional real subspace of H to a positive operator ρ on H whose diagonal in any orthonormal basis recovers the frame function, with Tr(ρ) = μ(I) = 1 ensuring ρ is a density operator.

theorem declaration uses `sorry`gleason_theorem_finite {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [FiniteDimensional ℂ H]
    (hdim : 3 ≤ Module.finrank ℂ H)
    (f : LeanEval.Analysis.FrameFunction H) :
    ∃! ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      reTr ρ = 1 ∧
      ∀ P : H →L[ℂ] H, LeanEval.Analysis.IsOrthProj P → f.μ P = reTr (ρ * P) := byH:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ Hinst✝¹:CompleteSpace Hinst✝:FiniteDimensional ℂ Hhdim:3 ≤ Module.finrank ℂ Hf:FrameFunction H⊢ ∃! ρ, ρ.IsPositive ∧ reTr ρ = 1 ∧ ∀ (P : H →L[ℂ] H), IsOrthProj P → f.μ P = reTr (ρ * P)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.