Gleason's theorem, finite-dimensional: frame functions on the sphere S² ⊂ ℝ³

Category: 1-Mathlib (CSD-free; staged for upstream). specs/gleason-feasibility.md, stage 57(a), first half: Cooke–Keane–Moran §2 — the elementary properties of frame functions on the unit sphere of ℝ³ that every later stage of the core lemma uses.

A frame is an orthonormal triple (p, q, r); a frame function has f p + f q + f r = W on every frame (IsFrameFunction ℝ f W, Gleason/ProjectionPackage.lean). This file:

• the tools of ℝ³: cross x y (the cross product, as a vector of EuclideanSpace ℝ (Fin 3)), orthonormal_triple_iff, orthonormal_cross (an orthonormal pair extends to a frame by its cross product), exists_unit_orthogonal_pair (a unit vector orthogonal to any two vectors — the orthogonal complement of a plane is nontrivial in ℝ³), and IsFrameFunction.sum_triple — the frame identity for any orthonormal triple, because an orthonormal triple of ℝ³ is an orthonormal basis (orthonormalBasisOfTriple);
• P1 IsFrameFunction.add/smul/const/neg/sub — frame functions form a vector space with additive weights;
• P2 IsFrameFunction.neg_apply — f (−s) = f s;
• P3 IsFrameFunction.four_point — if s ⟂ t and s' ⟂ t' lie on one great circle (all four orthogonal to a unit w) then f s + f t = f s' + f t';
• P4 IsFrameFunction.exists_orthogonal_lt — if f s > M − ξ (with M an upper bound and m an approximate lower bound) there is t ⟂ s with f t < m + ξ; and the sphereSup / sphereInf form exists_orthogonal_lt_sphereInf_add;
• boundedness: a nonnegative frame function takes values in [0, W] (IsFrameFunction.le_weight_of_nonneg, weight_nonneg);
• the examples: constants, s ↦ ⟪p₀, s⟫² (weight 1, Parseval), and every quadratic form s ↦ s ⬝ᵥ A s (weight Tr A, isFrameFunction_quadForm) — the regular frame functions. Gleason's core lemma proves that every nonnegative frame function is regular.

Source

Cooke, Keane, Moran 1985, Math. Proc. Cambridge Philos. Soc. 98, 117–128, §2 (P1–P4 and the examples); Gleason 1957, §1.

ℝ³: inner products, the cross product, orthonormal triples

theorem Gleason.real_inner_eq_dotProduct (x y : EuclideanSpace ℝ (Fin 3)) : inner ℝ x y = x.ofLp ⬝ᵥ y.ofLp

The real inner product of EuclideanSpace ℝ (Fin 3) is the dot product.

def Gleason.cross (x y : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

The cross product of two vectors of ℝ³.

Equations

• Gleason.cross x y = WithLp.toLp 2 ((crossProduct x.ofLp) y.ofLp)

@[simp]

theorem Gleason.coe_cross (x y : EuclideanSpace ℝ (Fin 3)) : (cross x y).ofLp = (crossProduct x.ofLp) y.ofLp

theorem Gleason.inner_cross_left (x y : EuclideanSpace ℝ (Fin 3)) : inner ℝ x (cross x y) = 0

theorem Gleason.inner_cross_right (x y : EuclideanSpace ℝ (Fin 3)) : inner ℝ y (cross x y) = 0

theorem Gleason.inner_cross_cross (u v w x : EuclideanSpace ℝ (Fin 3)) : inner ℝ (cross u v) (cross w x) = inner ℝ u w * inner ℝ v x - inner ℝ u x * inner ℝ v w

Lagrange's identity ⟪u × v, w × x⟫ = ⟪u, w⟫⟪v, x⟫ − ⟪u, x⟫⟪v, w⟫.

theorem Gleason.norm_cross_of_orthonormal {x y : EuclideanSpace ℝ (Fin 3)} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (hxy : inner ℝ x y = 0) : ‖cross x y‖ = 1

The cross product of an orthonormal pair is a unit vector.

theorem Gleason.orthonormal_triple_iff {x y z : EuclideanSpace ℝ (Fin 3)} : Orthonormal ℝ ![x, y, z] ↔ ‖x‖ = 1 ∧ ‖y‖ = 1 ∧ ‖z‖ = 1 ∧ inner ℝ x y = 0 ∧ inner ℝ x z = 0 ∧ inner ℝ y z = 0

An orthonormal triple of ℝ³, unpacked.

theorem Gleason.orthonormal_cross {x y : EuclideanSpace ℝ (Fin 3)} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (hxy : inner ℝ x y = 0) : Orthonormal ℝ ![x, y, cross x y]

An orthonormal pair extends to a frame by its cross product.

theorem Gleason.exists_unit_orthogonal_pair (s t : EuclideanSpace ℝ (Fin 3)) : ∃ (w : EuclideanSpace ℝ (Fin 3)), ‖w‖ = 1 ∧ inner ℝ s w = 0 ∧ inner ℝ t w = 0

In ℝ³ there is a unit vector orthogonal to any two given vectors.

theorem Gleason.exists_unit_orthogonal (s : EuclideanSpace ℝ (Fin 3)) : ∃ (t : EuclideanSpace ℝ (Fin 3)), ‖t‖ = 1 ∧ inner ℝ s t = 0

A unit vector of ℝ³ has a unit orthogonal vector.

noncomputable def Gleason.orthonormalBasisOfTriple {v : Fin 3 → EuclideanSpace ℝ (Fin 3)} (hv : Orthonormal ℝ v) : OrthonormalBasis (Fin 3) ℝ (EuclideanSpace ℝ (Fin 3))

An orthonormal triple of ℝ³ is an orthonormal basis.

Equations

• Gleason.orthonormalBasisOfTriple hv = OrthonormalBasis.mk hv ⋯

@[simp]

theorem Gleason.coe_orthonormalBasisOfTriple {v : Fin 3 → EuclideanSpace ℝ (Fin 3)} (hv : Orthonormal ℝ v) : ⇑(orthonormalBasisOfTriple hv) = v

Frame functions: P1 (a vector space), the frame identity for triples

theorem Gleason.IsFrameFunction.const {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} (c : ℝ) : IsFrameFunction 𝕜 (fun (x : EuclideanSpace 𝕜 (Fin n)) => c) (↑n * c)

P1. Constants are frame functions, with weight n · c.

theorem Gleason.IsFrameFunction.add {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} {f g : EuclideanSpace 𝕜 (Fin n) → ℝ} {W W' : ℝ} (hf : IsFrameFunction 𝕜 f W) (hg : IsFrameFunction 𝕜 g W') : IsFrameFunction 𝕜 (fun (s : EuclideanSpace 𝕜 (Fin n)) => f s + g s) (W + W')

theorem Gleason.IsFrameFunction.smul {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} {f : EuclideanSpace 𝕜 (Fin n) → ℝ} {W : ℝ} (hf : IsFrameFunction 𝕜 f W) (c : ℝ) : IsFrameFunction 𝕜 (fun (s : EuclideanSpace 𝕜 (Fin n)) => c * f s) (c * W)

theorem Gleason.IsFrameFunction.neg {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} {f : EuclideanSpace 𝕜 (Fin n) → ℝ} {W : ℝ} (hf : IsFrameFunction 𝕜 f W) : IsFrameFunction 𝕜 (fun (s : EuclideanSpace 𝕜 (Fin n)) => -f s) (-W)

theorem Gleason.IsFrameFunction.sub {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} {f g : EuclideanSpace 𝕜 (Fin n) → ℝ} {W W' : ℝ} (hf : IsFrameFunction 𝕜 f W) (hg : IsFrameFunction 𝕜 g W') : IsFrameFunction 𝕜 (fun (s : EuclideanSpace 𝕜 (Fin n)) => f s - g s) (W - W')

theorem Gleason.IsFrameFunction.sum_triple {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {v : Fin 3 → EuclideanSpace ℝ (Fin 3)} (hv : Orthonormal ℝ v) : ∑ i : Fin 3, f (v i) = W

The frame identity for any orthonormal triple (not only for OrthonormalBasis values).

theorem Gleason.IsFrameFunction.eq_of_triple {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {p q r : EuclideanSpace ℝ (Fin 3)} (h : Orthonormal ℝ ![p, q, r]) : f p + f q + f r = W

The frame identity, unfolded: f p + f q + f r = W.

P2, P3, P4

theorem Gleason.IsFrameFunction.neg_apply {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : f (-s) = f s

P2. f (−s) = f s on the sphere.

theorem Gleason.IsFrameFunction.four_point {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {w s t s' t' : EuclideanSpace ℝ (Fin 3)} (hw : ‖w‖ = 1) (hs : ‖s‖ = 1) (ht : ‖t‖ = 1) (hs' : ‖s'‖ = 1) (ht' : ‖t'‖ = 1) (hsw : inner ℝ s w = 0) (htw : inner ℝ t w = 0) (hs'w : inner ℝ s' w = 0) (ht'w : inner ℝ t' w = 0) (hst : inner ℝ s t = 0) (hs't' : inner ℝ s' t' = 0) : f s + f t = f s' + f t'

P3, the four-point identity. If s ⟂ t and s' ⟂ t' are two orthonormal pairs on one great circle — all four orthogonal to a unit vector w — then f s + f t = f s' + f t'.

theorem Gleason.IsFrameFunction.exists_orthogonal_lt {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {M m : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) (hm : ∀ (δ : ℝ), 0 < δ → ∃ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 ∧ f u < m + δ) {ξ : ℝ} {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) (hfs : M - ξ < f s) : ∃ (t : EuclideanSpace ℝ (Fin 3)), ‖t‖ = 1 ∧ inner ℝ s t = 0 ∧ f t < m + ξ

P4. Let M bound f above on the sphere and let m be approached from above by values of f (for instance M = sup f, m = inf f). If f s > M − ξ, then some unit t ⟂ s has f t < m + ξ.

Boundedness

theorem Gleason.IsFrameFunction.le_weight_of_nonneg {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) (h0 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → 0 ≤ f u) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : f s ≤ W

A nonnegative frame function is at most its weight on the sphere.

theorem Gleason.IsFrameFunction.weight_nonneg {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) (h0 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → 0 ≤ f u) : 0 ≤ W

The weight of a nonnegative frame function is nonnegative.

Supremum and infimum over the sphere

noncomputable def Gleason.sphereSup (f : EuclideanSpace ℝ (Fin 3) → ℝ) : ℝ

The supremum of f over the unit sphere.

Equations

• Gleason.sphereSup f = sSup (f '' Metric.sphere 0 1)

noncomputable def Gleason.sphereInf (f : EuclideanSpace ℝ (Fin 3) → ℝ) : ℝ

The infimum of f over the unit sphere.

Equations

• Gleason.sphereInf f = sInf (f '' Metric.sphere 0 1)

theorem Gleason.sphere_nonempty {f : EuclideanSpace ℝ (Fin 3) → ℝ} : (f '' Metric.sphere 0 1).Nonempty

theorem Gleason.bddAbove_sphere {f : EuclideanSpace ℝ (Fin 3) → ℝ} {M : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) : BddAbove (f '' Metric.sphere 0 1)

theorem Gleason.bddBelow_sphere {f : EuclideanSpace ℝ (Fin 3) → ℝ} {m : ℝ} (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → m ≤ f u) : BddBelow (f '' Metric.sphere 0 1)

theorem Gleason.le_sphereSup {f : EuclideanSpace ℝ (Fin 3) → ℝ} {M : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : f s ≤ sphereSup f

theorem Gleason.sphereSup_le {f : EuclideanSpace ℝ (Fin 3) → ℝ} {M : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) : sphereSup f ≤ M

theorem Gleason.sphereInf_le {f : EuclideanSpace ℝ (Fin 3) → ℝ} {m : ℝ} (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → m ≤ f u) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : sphereInf f ≤ f s

theorem Gleason.le_sphereInf {f : EuclideanSpace ℝ (Fin 3) → ℝ} {m : ℝ} (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → m ≤ f u) : m ≤ sphereInf f

theorem Gleason.exists_sphereSup_sub_lt {f : EuclideanSpace ℝ (Fin 3) → ℝ} {δ : ℝ} (hδ : 0 < δ) : ∃ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 ∧ sphereSup f - δ < f u

Values of f come within any δ > 0 of sphereSup f.

theorem Gleason.exists_lt_sphereInf_add {f : EuclideanSpace ℝ (Fin 3) → ℝ} {δ : ℝ} (hδ : 0 < δ) : ∃ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 ∧ f u < sphereInf f + δ

Values of f come within any δ > 0 of sphereInf f.

theorem Gleason.IsFrameFunction.exists_orthogonal_lt_sphereInf_add {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W M : ℝ} (hf : IsFrameFunction ℝ f W) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) {ξ : ℝ} {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) (hfs : sphereSup f - ξ < f s) : ∃ (t : EuclideanSpace ℝ (Fin 3)), ‖t‖ = 1 ∧ inner ℝ s t = 0 ∧ f t < sphereInf f + ξ

P4 in sup/inf form. For a bounded frame function, f s > sup f − ξ gives a unit t ⟂ s with f t < inf f + ξ.

The regular frame functions

theorem Gleason.isFrameFunction_inner_sq {p₀ : EuclideanSpace ℝ (Fin 3)} (hp₀ : ‖p₀‖ = 1) : IsFrameFunction ℝ (fun (s : EuclideanSpace ℝ (Fin 3)) => inner ℝ p₀ s ^ 2) 1

s ↦ ⟪p₀, s⟫² is a frame function of weight 1 (Parseval).

theorem Gleason.dotProduct_mulVec_eq_trace (A : Matrix (Fin 3) (Fin 3) ℝ) (s : Fin 3 → ℝ) : s ⬝ᵥ A.mulVec s = (A * Matrix.vecMulVec s s).trace

s ⬝ᵥ A s = Tr(A · s sᵀ).

theorem Gleason.isFrameFunction_quadForm (A : Matrix (Fin 3) (Fin 3) ℝ) : IsFrameFunction ℝ (fun (s : EuclideanSpace ℝ (Fin 3)) => s.ofLp ⬝ᵥ A.mulVec s.ofLp) A.trace

Every quadratic form is a frame function, with weight the trace of its matrix (CKM §2, Proposition).