Gleason's theorem, finite-dimensional: bounded frame functions attain their extremal values

Category: 1-Mathlib (CSD-free; staged for upstream). specs/gleason-feasibility.md, stage 57(d): Cooke–Keane–Moran §6 — the second of the two risk points of the core lemma. A bounded frame function on S² ⊂ ℝ³ attains its supremum (★ IsFrameFunction.exists_forall_le) and its infimum (IsFrameFunction.exists_forall_ge).

The argument, in the paper's four steps, with the Lean shape of each:

• A maximising sequence and its limit. u n with f (u n) → sup f; a convergent subsequence by compactness of the sphere (IsCompact.tendsto_subseq), limit p. Suppose f p < sup f; then eventually u n ≠ p and ⟪p, u n⟫ > 0.
• Step 1, changing coordinates. For each q near p, a rigid motion motion p e₀ e₁ q with motion p = q and motion c_q = p, where c_q lies on the meridian of e₀ at parameter meridianParam p q = √(1 − ⟪p,q⟫²)/⟪p,q⟫ (exists_motion: the linear isometry sending the orthonormal basis (c_q, d_q, e₁) to (p, d'_q, p × d'_q), OrthonormalBasis.equiv). g_q = f ∘ motion is again a frame function (IsFrameFunction.comp_inner).
• Step 2, symmetrisation. rot p s = ⟪p, s⟫ p + p × s is the 90° rotation about p (inner_rot_rot); symmetrise p g s = g s + g (rot p s) is a frame function of weight 2W, bounded by 2m and 2M, with symmetrise p g p = 2 g p, and constant on the equator (symmetrise_equator: the four-point identity for the orthonormal pairs (e, p × e)).
• Step 3, the limit. The functions H n = symmetrise p g_{u n} restricted to the sphere lie in the compact box [2m, 2M]^{S²} (Tychonoff, isCompact_univ_pi); a cluster point h₀ (IsCompact.exists_clusterPt) is a frame function, is at most 2M, is constant on the equator (closed conditions, mem_of_clusterPt), and has h₀ p = 2 sup f (eq_of_clusterPt_of_tendsto). By the simple-frame-function theorem (IsFrameFunction.eq_add_mul_latitude) it is m' + (2 sup f − m') ⟪p, ·⟫².
• Step 4. A fixed point c⋆ on the meridian of e₀ close to p has h₀ c⋆ > 2 sup f − ε, and frequently H n c⋆ is within ε of it (clusterPt_iff_frequently); for such an n large enough, c_{u n} is higher than c⋆ on the same meridian, so c⋆ is reached from c_{u n} in two descents (descent_step_ray), and the approximate basic lemma (IsFrameFunction.descent_lt_add) gives H n c_{u n} > H n c⋆ − 6ε; but H n c_{u n} = f p + f (…) ≤ f p + sup f. Hence f p > sup f − 8ε for every ε, the contradiction.

Source

Cooke, Keane, Moran 1985, Math. Proc. Cambridge Philos. Soc. 98, 117–128, §6.

The 90° rotation about the pole

noncomputable def Gleason.rot (p s : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

The right-hand rotation by 90° about p: s ↦ ⟪p, s⟫ p + p × s.

Equations

• Gleason.rot p s = inner ℝ p s • p + Gleason.cross p s

theorem Gleason.cross_self' (v : EuclideanSpace ℝ (Fin 3)) : cross v v = 0

theorem Gleason.norm_eq_one_of_real_inner_self {v : EuclideanSpace ℝ (Fin 3)} (h : inner ℝ v v = 1) : ‖v‖ = 1

A vector with ⟪v, v⟫ = 1 is a unit vector.

theorem Gleason.inner_rot_rot {p : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (x y : EuclideanSpace ℝ (Fin 3)) : inner ℝ (rot p x) (rot p y) = inner ℝ x y

The rotation preserves inner products (Lagrange's identity).

theorem Gleason.norm_rot {p : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : ‖rot p s‖ = 1

theorem Gleason.rot_pole {p : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) : rot p p = p

theorem Gleason.rot_mem_equator {p : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) {e : EuclideanSpace ℝ (Fin 3)} (he : e ∈ equator p) : rot p e ∈ equator p

theorem Gleason.inner_rot_of_equator {p e : EuclideanSpace ℝ (Fin 3)} (he : e ∈ equator p) : inner ℝ e (rot p e) = 0

Frame functions composed with inner-product-preserving maps; symmetrisation

theorem Gleason.IsFrameFunction.comp_inner {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {T : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} (hT : ∀ (x y : EuclideanSpace ℝ (Fin 3)), inner ℝ (T x) (T y) = inner ℝ x y) : IsFrameFunction ℝ (fun (s : EuclideanSpace ℝ (Fin 3)) => f (T s)) W

A frame function composed with an inner-product-preserving map is a frame function of the same weight.

noncomputable def Gleason.symmetrise (p : EuclideanSpace ℝ (Fin 3)) (g : EuclideanSpace ℝ (Fin 3) → ℝ) (s : EuclideanSpace ℝ (Fin 3)) : ℝ

Symmetrisation about the pole: g s + g (rot p s).

Equations

• Gleason.symmetrise p g s = g s + g (Gleason.rot p s)

theorem Gleason.IsFrameFunction.symmetrise {p : EuclideanSpace ℝ (Fin 3)} {g : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hg : IsFrameFunction ℝ g W) (hp : ‖p‖ = 1) : IsFrameFunction ℝ (Gleason.symmetrise p g) (W + W)

theorem Gleason.symmetrise_pole {p : EuclideanSpace ℝ (Fin 3)} {g : EuclideanSpace ℝ (Fin 3) → ℝ} (hp : ‖p‖ = 1) : symmetrise p g p = 2 * g p

theorem Gleason.symmetrise_le {p : EuclideanSpace ℝ (Fin 3)} {g : EuclideanSpace ℝ (Fin 3) → ℝ} {M : ℝ} (hp : ‖p‖ = 1) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → g u ≤ M) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : symmetrise p g s ≤ 2 * M

theorem Gleason.le_symmetrise {p : EuclideanSpace ℝ (Fin 3)} {g : EuclideanSpace ℝ (Fin 3) → ℝ} {m : ℝ} (hp : ‖p‖ = 1) (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → m ≤ g u) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : 2 * m ≤ symmetrise p g s

theorem Gleason.symmetrise_equator {p : EuclideanSpace ℝ (Fin 3)} {g : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hg : IsFrameFunction ℝ g W) (hp : ‖p‖ = 1) {e e' : EuclideanSpace ℝ (Fin 3)} (he : e ∈ equator p) (he' : e' ∈ equator p) : symmetrise p g e = symmetrise p g e'

The symmetrisation is constant on the equator (the four-point identity for the orthonormal pairs (e, p × e)).

The rigid motion taking the pole to a nearby point

noncomputable def Gleason.meridianParam (p q : EuclideanSpace ℝ (Fin 3)) : ℝ

The meridian parameter of q: the tangent coordinate √(1 − ⟪p,q⟫²)/⟪p,q⟫ of the point of the meridian of e₀ at the latitude of q.

Equations

• Gleason.meridianParam p q = √(1 - inner ℝ p q ^ 2) / inner ℝ p q

theorem Gleason.tangent_ofReal (e₁ e₂ : EuclideanSpace ℝ (Fin 3)) (r : ℝ) : tangent e₁ e₂ ↑r = r • e₁

The tangent vector with a real coordinate.

theorem Gleason.inner_lt_one_of_ne {p q : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hq : q ∈ northern p) (hqp : q ≠ p) : inner ℝ p q < 1

The strict form of latitude_le_one: off the pole, ⟪p, q⟫ < 1 on the northern hemisphere.

theorem Gleason.exists_motion {p e₀ e₁ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₀, e₁]) {q : EuclideanSpace ℝ (Fin 3)} (hq : ‖q‖ = 1) (hpq : 0 < inner ℝ p q) (hqp : q ≠ p) : ∃ (T : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)), (∀ (x y : EuclideanSpace ℝ (Fin 3)), inner ℝ (T x) (T y) = inner ℝ x y) ∧ T p = q ∧ T (lift p (tangent e₀ e₁ ↑(meridianParam p q))) = p

The rigid motion (CKM §6, Step 1). For a unit q ≠ p in the open northern hemisphere there is an inner-product-preserving T with T p = q and T c_q = p, where c_q is the point of the meridian of e₀ with tangent coordinate meridianParam p q.

noncomputable def Gleason.motion (p e₀ e₁ q : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)

The rigid motion, as a total function: the choice of exists_motion where its hypotheses hold, the identity elsewhere.

Equations

• Gleason.motion p e₀ e₁ q = if h : Orthonormal ℝ ![p, e₀, e₁] ∧ ‖q‖ = 1 ∧ 0 < inner ℝ p q ∧ q ≠ p then Classical.choose ⋯ else id

theorem Gleason.motion_inner (p e₀ e₁ q x y : EuclideanSpace ℝ (Fin 3)) : inner ℝ (motion p e₀ e₁ q x) (motion p e₀ e₁ q y) = inner ℝ x y

The motion always preserves inner products.

theorem Gleason.norm_motion (p e₀ e₁ q : EuclideanSpace ℝ (Fin 3)) {x : EuclideanSpace ℝ (Fin 3)} (hx : ‖x‖ = 1) : ‖motion p e₀ e₁ q x‖ = 1

theorem Gleason.motion_pole {p e₀ e₁ q : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₀, e₁]) (hq : ‖q‖ = 1) (hpq : 0 < inner ℝ p q) (hqp : q ≠ p) : motion p e₀ e₁ q p = q

theorem Gleason.motion_meridian {p e₀ e₁ q : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₀, e₁]) (hq : ‖q‖ = 1) (hpq : 0 < inner ℝ p q) (hqp : q ≠ p) : motion p e₀ e₁ q (lift p (tangent e₀ e₁ ↑(meridianParam p q))) = p

Cluster points

theorem Gleason.mem_of_clusterPt {X : Type u_1} [TopologicalSpace X] {F : Filter X} {x : X} {K : Set X} (hx : ClusterPt x F) (hK : IsClosed K) (hF : F ≤ Filter.principal K) : x ∈ K

A cluster point of a filter supported in a closed set lies in it.

theorem Gleason.eq_of_clusterPt_of_tendsto {X : Type u_1} [TopologicalSpace X] [T2Space X] {ι : Type u_2} {l : Filter ι} {u : ι → X} {x y : X} (hx : ClusterPt x (Filter.map u l)) (hy : Filter.Tendsto u l (nhds y)) : x = y

In a Hausdorff space, a cluster point of a convergent filter is its limit.

Bounded frame functions attain their extremal values

theorem Gleason.IsFrameFunction.exists_forall_le {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {M m : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → m ≤ f u) : ∃ (p : EuclideanSpace ℝ (Fin 3)), ‖p‖ = 1 ∧ ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ f p

★ Bounded frame functions attain their supremum (CKM §6, Theorem).

theorem Gleason.IsFrameFunction.exists_forall_ge {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {M m : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → m ≤ f u) : ∃ (p : EuclideanSpace ℝ (Fin 3)), ‖p‖ = 1 ∧ ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f p ≤ f u

Bounded frame functions attain their infimum.

theorem Gleason.IsFrameFunction.exists_eq_sphereSup {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {M m : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → m ≤ f u) : ∃ (p : EuclideanSpace ℝ (Fin 3)), ‖p‖ = 1 ∧ f p = sphereSup f

A bounded frame function attains sphereSup.