Gleason's theorem for real frame functions

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #87, the last generality gap of the Gleason development: #58 proved the real theorem for a projection package, and this file proves it for a bare frame function, which is the object Gleason's paper is about.

★★★ existsUnique_density_of_frameFunction: for N ≥ 3, a nonnegative frame function of weight W on ℝᴺ — a map on the unit sphere with ∑ᵢ f(bᵢ) = W over every orthonormal basis — is the quadratic form of a unique positive semidefinite matrix of trace W.

What the package gave for free, and what a frame function has to earn

The core lemma of #57 is about ℝ³, so every route to ℝᴺ needs the restriction of f to the span of an orthonormal triple to be a frame function there — that is, the weight of a 3-space must not depend on which orthonormal basis of it is used. A projection package reads that weight off p (∑ᵢ |eᵢ⟩⟨eᵢ|), which is manifestly basis independent (#58's isFrameFunction_restrictR). A bare frame function has no p, so the fact has to be earned by completing the triple:

• orthonormalBasisOfCardR — an orthonormal family indexed by a type of cardinality N is an orthonormal basis (basisOfOrthonormalOfCardEqFinrank), so no span argument is needed;
• orthonormal_sum_elim — two orthonormal families that are mutually orthogonal glue along ⊕;
• ★ IsFrameFunction.sum_eq_of_basis — the frame sum is the weight over an orthonormal basis indexed by any finite type (reindex to Fin N), and ★ IsFrameFunction.sum_elim_eq splits it along a completion;
• exists_orthonormal_complement — the orthogonal complement carries an orthonormal family of the complementary size (stdOrthonormalBasis of Sᴿ, finrank_add_finrank_orthogonal);
• hence ★★ IsFrameFunction.exists_weight_restrict: the weight of a 3-space is basis independent, because a fixed complement family completes every triple of that space and the frame sums add to W.

Two more consequences of the same completion, both needed by the middle layer of Gleason/Real.lean and neither available for a bare f before now: ★ IsFrameFunction.le_weight (f ≤ W on the sphere in any dimension — Gleason/Sphere.lean proves it for ℝ³ through the cross product) and ★ IsFrameFunction.neg_eq (f is even on the sphere: flipping one vector of a basis gives another basis with the same tail).

With those three, exists_isSymm_sphere_of_quad — the layer #58 was refactored to state for any function quadratic on triples — gives ★★ exists_isSymm_sphere_of_frameFunction_one at weight 1, and the theorem follows after normalising by W and running the descent (quadraticForm_on_sphere_to_densityR).

Honest scope

⚠️ N ≥ 3 and finite dimensions, as in #57 and #58. N = 2 is false for Gleason's theorem, and N ≤ 1 is only the trivial statement. ⚠️ The weight-W statement is reduced to the weight-1 one by dividing, which needs W > 0; the W = 0 case is handled separately (f vanishes on the sphere, the matrix is 0). ⚠️ Nothing in the corpus consumes this file: LF2 and the CSD layers use the complex theorem, and #58's package form is what a real application would use. It exists because it is the statement Gleason wrote, and because an upstream PR would be asked for it.

Source

A. Gleason, Measures on the closed subspaces of a Hilbert space, J. Math. Mech. 6 (1957) 885, §1 (frame functions; the real theorem); Gleason/Core.lean (#57, the core lemma), Gleason/Real.lean (#58, the real reduction and the descent); specs/gleason-feasibility.md §2; specs/BACKLOG.md #87; specs/future-work.md.

An orthonormal family of the right size is an orthonormal basis

noncomputable def Gleason.orthonormalBasisOfCardR {N : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {v : ι → EuclideanSpace ℝ (Fin N)} (hv : Orthonormal ℝ v) (hcard : Fintype.card ι = N) : OrthonormalBasis ι ℝ (EuclideanSpace ℝ (Fin N))

An orthonormal family indexed by a type of the right cardinality is an orthonormal basis.

Equations

• Gleason.orthonormalBasisOfCardR hv hcard = (basisOfOrthonormalOfCardEqFinrank hv ⋯).toOrthonormalBasis ⋯

@[simp]

theorem Gleason.coe_orthonormalBasisOfCardR {N : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] {v : ι → EuclideanSpace ℝ (Fin N)} (hv : Orthonormal ℝ v) (hcard : Fintype.card ι = N) : ⇑(orthonormalBasisOfCardR hv hcard) = v

theorem Gleason.orthonormal_sum_elim {N k m : ℕ} {v : Fin k → EuclideanSpace ℝ (Fin N)} {g : Fin m → EuclideanSpace ℝ (Fin N)} (hv : Orthonormal ℝ v) (hg : Orthonormal ℝ g) (hvg : ∀ (j : Fin k) (i : Fin m), inner ℝ (v j) (g i) = 0) : Orthonormal ℝ (Sum.elim v g)

Two families glued along a sum type are orthonormal when each is and they are orthogonal.

The frame sum over any orthonormal basis

theorem Gleason.IsFrameFunction.sum_eq_of_basis {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {ι : Type u_1} [Fintype ι] (b : OrthonormalBasis ι ℝ (EuclideanSpace ℝ (Fin N))) : ∑ i : ι, f (b i) = W

The frame sum is the weight over every orthonormal basis, whatever it is indexed by: reindex along an equivalence to Fin N.

theorem Gleason.IsFrameFunction.sum_elim_eq {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {k m : ℕ} [Nonempty (Fin k ⊕ Fin m)] {v : Fin k → EuclideanSpace ℝ (Fin N)} {g : Fin m → EuclideanSpace ℝ (Fin N)} (h : Orthonormal ℝ (Sum.elim v g)) (hcard : k + m = N) : ∑ j : Fin k, f (v j) + ∑ i : Fin m, f (g i) = W

The frame sum splits along a completion: an orthonormal family and an orthogonal family of the complementary size form an orthonormal basis, so the two frame sums add to the weight.

Completing an orthonormal family

theorem Gleason.exists_orthonormal_complement {N : ℕ} (S : Submodule ℝ (EuclideanSpace ℝ (Fin N))) : ∃ (m : ℕ) (g : Fin m → EuclideanSpace ℝ (Fin N)), Orthonormal ℝ g ∧ (∀ (i : Fin m), g i ∈ Sᗮ) ∧ Module.finrank ℝ ↥S + m = N

The orthogonal complement carries an orthonormal family of the complementary size.

What a bare frame function inherits from the completion

theorem Gleason.IsFrameFunction.exists_tail {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : ∃ (m : ℕ) (g : Fin m → EuclideanSpace ℝ (Fin N)), Orthonormal ℝ g ∧ (∀ (i : Fin m), inner ℝ v (g i) = 0) ∧ 1 + m = N ∧ f v + ∑ i : Fin m, f (g i) = W

A unit vector, completed: the frame sum splits as f v plus a tail orthogonal to v.

theorem Gleason.IsFrameFunction.le_weight {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) (h0 : ∀ (u : EuclideanSpace ℝ (Fin N)), ‖u‖ = 1 → 0 ≤ f u) {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : f v ≤ W

A nonnegative frame function is bounded by its weight, in any dimension (the Fin 3 proof in Gleason/Sphere.lean goes through the cross product).

theorem Gleason.IsFrameFunction.neg_eq {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : f (-v) = f v

A frame function is even on the sphere: flipping one vector of a basis gives another basis, with the same tail.

The restriction to the span of an orthonormal triple

theorem Gleason.IsFrameFunction.exists_weight_restrict {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {e : Fin 3 → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) : ∃ (W' : ℝ), IsFrameFunction ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => f (combR e x)) W'

★★ The step #58 got from the projection package and a bare frame function has to earn. The weight of a 3-space is basis independent: complete an orthonormal triple of that space by a fixed orthonormal family of the orthogonal complement, and the frame sum of the triple is the total weight minus the tail's — the same for every triple of the space. So the restriction to the span is a frame function on ℝ³, which is what Gleason's core lemma consumes.

Gleason's theorem for real frame functions

theorem Gleason.exists_isSymm_sphere_of_frameFunction_one {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hf : IsFrameFunction ℝ f 1) (hN : 3 ≤ N) (h0 : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) : ∃ (A : Matrix (Fin N) (Fin N) ℝ), A.IsSymm ∧ ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v = v.ofLp ⬝ᵥ A.mulVec v.ofLp

★★ A nonnegative frame function of weight 1 is a symmetric quadratic form on the sphere.

theorem Gleason.IsFrameFunction.zero_le_weight {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) (h0 : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) : 0 ≤ W

The weight of a nonnegative frame function is nonnegative.

theorem Gleason.existsUnique_density_of_frameFunction {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) (hN : 3 ≤ N) (h0 : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) : ∃! A : Matrix (Fin N) (Fin N) ℝ, A.PosSemidef ∧ A.trace = W ∧ ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v = v.ofLp ⬝ᵥ A.mulVec v.ofLp

★★★ Gleason's theorem for real frame functions, N ≥ 3 — the statement Gleason wrote. A nonnegative frame function of weight W on ℝᴺ is the quadratic form of a unique positive semidefinite matrix of trace W. #58 proved this for a projection package, whose p on the projections makes the weight of a 3-space manifestly basis independent; here that step is earned by completing the triple (exists_weight_restrict).