Gleason's theorem (separable Hilbert space)

gleason_theorem_separable

Submitter: Kim Morrison.

Notes: Gleason's theorem for a separable complex Hilbert space H of dimension at least 3, in Gleason's original `frame function on the unit sphere' formulation: any non-negative function on the unit sphere whose values sum to 1 along every Hilbert basis is given by x ↦ re ⟨x, ρ x⟩ for some positive bounded operator ρ. The Lean conclusion does not assert that ρ is trace-class with Tr(ρ) = 1; stating that would require trace-class infrastructure not yet at this Mathlib pin. This side-steps the absence of Schatten 1 / trace-class infrastructure in Mathlib at the time of writing.

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

Informal solution: Reduce to the real 3-dimensional case via restriction to real subspaces of H, where Gleason's continuity argument plus an analysis of regular frame functions on S^2 gives a positive quadratic form. Patch these forms together using rotation-invariance and the assumed basis-sum normalization to obtain a globally defined positive bounded operator ρ on H reproducing the frame function on every unit vector.

theorem declaration uses `sorry`gleason_theorem_separable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
    (hdim : 3 ≤ Module.rank ℂ H)
    (f : LeanEval.Analysis.SphereFrameFunction H) :
    ∃ ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      ∀ x : Metric.sphere (0 : H) 1,
        f.f x = (inner ℂ (x : H) (ρ (x : H))).re := byH:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ Hinst✝¹:CompleteSpace Hinst✝:TopologicalSpace.SeparableSpace Hhdim:3 ≤ Module.rank ℂ Hf:SphereFrameFunction H⊢ ∃ ρ, ρ.IsPositive ∧ ∀ (x : ↑(Metric.sphere 0 1)), f.f x = (inner ℂ (↑x) (ρ ↑x)).re
  sorryAll goals completed! 🐙

Solved by

Not yet solved.