Gleason's theorem

DefinitionOrthogonal projection#✓fully proved

A continuous linear operator \(P\) on a complex Hilbert space \(H\) is an orthogonal projection if it is idempotent, \(P^2 = P\), and self-adjoint, \(P^* = P\).

def IsOrthProj (P : H →L[ℂ] H) : Prop :=
  IsIdempotentElem P ∧ IsSelfAdjoint P

Used by 2

Used byFrame function on projections · Gleason's theorem in finite dimensions

StructureFrame function on projections#✓fully proved

Let \(H\) be a complex Hilbert space. A frame function on the projection lattice of \(H\) is a function \(\mu\) from the continuous linear operators on \(H\) to \(\mathbb{R}\) such that \(\mu(P) \ge 0\) for every orthogonal projection \(P\) on \(H\), \(\mu(P + Q) = \mu(P) + \mu(Q)\) for all orthogonal projections \(P\) and \(Q\) on \(H\) with \(PQ = 0\), and \(\mu(I) = 1\) for the identity operator \(I\) on \(H\).

Only the values of \(\mu\) on orthogonal projections are constrained. In finite dimensions every orthogonal family of nonzero projections is finite, so additivity on orthogonal pairs already yields countable additivity.

structure FrameFunction (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] where
  μ : (H →L[ℂ] H) → ℝ
  nonneg : ∀ P : H →L[ℂ] H, IsOrthProj P → 0 ≤ μ P
  additive : ∀ P Q : H →L[ℂ] H, IsOrthProj P → IsOrthProj Q → P * Q = 0 →
    μ (P + Q) = μ P + μ Q
  normalized : μ (1 : H →L[ℂ] H) = 1

Uses 1 · Used by 1

Statement usesOrthogonal projection

Used byGleason's theorem in finite dimensions

DefinitionReal part of the trace#✓fully proved

For a continuous linear operator \(A\) on a finite-dimensional complex Hilbert space \(H\), let \(\operatorname{tr}(A) \in \mathbb{C}\) be the trace of \(A\) as a \(\mathbb{C}\)-linear map on \(H\). The real part of the trace of \(A\) is the real number \(\operatorname{Re} \operatorname{tr}(A)\).

noncomputable def reTr [FiniteDimensional ℂ H] (A : H →L[ℂ] H) : ℝ :=
  (LinearMap.trace ℂ H A.toLinearMap).re

Used by 1

Used byGleason's theorem in finite dimensions

TheoremGleason's theorem in finite dimensions#●ready to prove

Let \(H\) be a finite-dimensional complex Hilbert space of dimension at least \(3\), write \(\operatorname{tr}\) for the trace of a \(\mathbb{C}\)-linear map on \(H\), and let \(\mu\) be a frame function on the projection lattice of \(H\). Then there is a unique continuous linear operator \(\rho\) on \(H\) such that \(\rho\) is positive, \(\operatorname{Re} \operatorname{tr}(\rho) = 1\), and \(\mu(P) = \operatorname{Re} \operatorname{tr}(\rho P)\) for every orthogonal projection \(P\) on \(H\).

public theorem_wanted gleason_theorem_finite
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [FiniteDimensional ℂ H]
    (hdim : 3 ≤ Module.finrank ℂ H)
    (f : FrameFunction H) :
    ∃! ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      reTr ρ = 1 ∧
      ∀ P : H →L[ℂ] H, IsOrthProj P → f.μ P = reTr (ρ * P)

Sources

• A. M. Gleason, Measures on the closed subspaces of a Hilbert space, J. Math. Mech. 6 (1957), 885-893. Problem gleason_theorem_finite of the lean-eval benchmark.

Uses 3

Statement usesFrame function on projections · Orthogonal projection · Real part of the trace

StructureFrame function on the unit sphere#✓fully proved

Let \(H\) be a complex Hilbert space. A frame function on the unit sphere of \(H\) is a function \(f\) from the unit vectors of \(H\) to \(\mathbb{R}\) such that \(f(x) \ge 0\) for every unit vector \(x\) in \(H\) and, for every Hilbert basis \((b_i)_{i \in \iota}\) of \(H\), the family \((f(b_i))_{i \in \iota}\) is unconditionally summable with sum \(1\).

This is Gleason's 1957 notion of a frame function, normalized to weight \(1\) and required to be non-negative.

structure SphereFrameFunction (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] where
  f : Metric.sphere (0 : H) 1 → ℝ
  nonneg : ∀ x : Metric.sphere (0 : H) 1, 0 ≤ f x
  basis_sum : ∀ {ι : Type*} (b : HilbertBasis ι ℂ H),
    HasSum
      (fun i : ι => f ⟨b i, mem_sphere_zero_iff_norm.mpr (b.orthonormal.norm_eq_one i)⟩)
      1

Used by 1

Used byGleason's theorem for separable Hilbert spaces

TheoremGleason's theorem for separable Hilbert spaces#●ready to prove

Let \(H\) be a separable complex Hilbert space whose dimension over \(\mathbb{C}\) is at least \(3\), and let \(f\) be a frame function on the unit sphere of \(H\). Then there is a positive continuous linear operator \(\rho\) on \(H\) such that \(f(x) = \operatorname{Re} \langle x, \rho x \rangle\) for every unit vector \(x\) in \(H\).

The statement does not assert that \(\rho\) is trace class with trace \(1\), nor that \(\rho\) is unique.

public theorem_wanted gleason_theorem_separable
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
    (hdim : 3 ≤ Module.rank ℂ H)
    (f : SphereFrameFunction H) :
    ∃ ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      ∀ x : Metric.sphere (0 : H) 1,
        f.f x = (inner ℂ (x : H) (ρ (x : H))).re

Sources

• A. M. Gleason, Measures on the closed subspaces of a Hilbert space, J. Math. Mech. 6 (1957), 885-893. Problem gleason_theorem_separable of the lean-eval benchmark.

Uses 1

Statement usesFrame function on the unit sphere

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.