Gleason's theorem, finite-dimensional: the basic lemma and the simple frame functions

Category: 1-Mathlib (CSD-free; staged for upstream). specs/gleason-feasibility.md, stage 57(c): Cooke–Keane–Moran §4 (the basic lemma) and the theorem of §5 — Gleason's theorem for the simple frame functions, those attaining their supremum at a point p and constant on the equator of p. Bell's and Piron's elementary proofs of the extreme case end here.

For a frame function f on S² ⊂ ℝ³ and a unit pole p:

• IsFrameFunction.equator_le — if f p = sup f and f = m on the equator then m = inf f (P4 at the pole); IsFrameFunction.equator_lt_add is the approximate version;
• the basic lemma IsFrameFunction.descent_le — under the same hypotheses, f s' ≤ f s for every s' on the descent through s (the four-point identity on the great circle D_s, whose point orthogonal to s lies on the equator); IsFrameFunction.descent_lt_add is the approximate version (f p > sup f − ξ gives f s' − ξ < f s);
• IsFrameFunction.le_of_latitude_lt — f is monotone in latitude on the northern hemisphere, by Piron's geometric lemma (exists_descent_chain) and the basic lemma along the chain;
• exists_frame_of_latitudes — for a + b + c = 1 there is a frame in the northern hemisphere with latitudes a, b, c (transport a unit vector of square roots through an orthonormal basis of p^⊥);
• the suprema and infima of f over the parallels (parallelSup, parallelInf), which are interlaced by monotonicity, so that the set of latitudes where they differ is a family of disjoint open intervals, hence countable (Set.PairwiseDisjoint.countable_of_isOpen);
• ★ the simple-frame-function theorem IsFrameFunction.eq_add_mul_latitude — if f p = sup f and f = m on the equator of p, then f s = m + (f p − m) ⟪p, s⟫² for every unit s: Warmup Theorem II (eq_self_of_monotone_sum_eq_one) applied to the common value of parallelSup and parallelInf off the countable exceptional set, then a squeeze that shows the exceptional set is empty. IsFrameFunction.eq_latitude_of_normalised is the normalised form (f p = 1, f = 0 on the equator: f s = latitude p s).

Source

Cooke, Keane, Moran 1985, Math. Proc. Cambridge Philos. Soc. 98, 117–128, §4 and the Theorem of §5; Piron, Foundations of Quantum Physics (1976); Bell 1966, Rev. Mod. Phys. 38, 447 (the extreme case).

More about latitudes and the coldest vector

theorem Gleason.latitude_nonneg (p s : EuclideanSpace ℝ (Fin 3)) : 0 ≤ latitude p s

theorem Gleason.latitude_le_one {p s : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hs : ‖s‖ = 1) : latitude p s ≤ 1

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

theorem Gleason.latitude_neg (p s : EuclideanSpace ℝ (Fin 3)) : latitude p (-s) = latitude p s

theorem Gleason.pole_mem_northern {p : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) : p ∈ northern p

theorem Gleason.eq_pole_of_latitude_eq_one {p s : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hs : s ∈ northern p) (hl : latitude p s = 1) : s = p

The only point of the northern hemisphere at latitude 1 is the pole.

theorem Gleason.mem_equator_of_latitude_eq_zero {p s : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) (hl : latitude p s = 0) : s ∈ equator p

A point of the northern hemisphere at latitude 0 is on the equator.

theorem Gleason.sub_inner_smul_ne_zero {p s : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hs : s ∈ northern p) (hsp : s ≠ p) : p - inner ℝ p s • s ≠ 0

Off the pole, p − ⟪p, s⟫ s is nonzero.

theorem Gleason.norm_coldest {p s : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hs : s ∈ northern p) (hsp : s ≠ p) : ‖coldest p s‖ = 1

theorem Gleason.inner_pole_cross_coldest (p s : EuclideanSpace ℝ (Fin 3)) : inner ℝ p (cross s (coldest p s)) = 0

The point of the descent orthogonal to s lies on the equator: ⟪p, s × s^⊥⟫ = 0.

The equator is the minimum; the basic lemma

theorem Gleason.IsFrameFunction.equator_le {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W m : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ f p) (hE : ∀ e ∈ equator p, f e = m) {u : EuclideanSpace ℝ (Fin 3)} (hu : ‖u‖ = 1) : m ≤ f u

The equator value is the minimum (CKM §4, from P4 at the pole): if f p = sup f and f = m on the equator of p, then m ≤ f u for every unit u.

theorem Gleason.IsFrameFunction.equator_lt_add {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W m : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) {M ξ : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) (hpξ : M - ξ < f p) (hE : ∀ e ∈ equator p, f e = m) {u : EuclideanSpace ℝ (Fin 3)} (hu : ‖u‖ = 1) : m - ξ < f u

The approximate form: if f p > M − ξ with M an upper bound and f = m on the equator, then m − ξ < f u for every unit u.

theorem Gleason.IsFrameFunction.descent_le {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W m : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ f p) (hE : ∀ e ∈ equator p, f e = m) {s s' : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) (hsp : s ≠ p) (hs' : s' ∈ descent p s) : f s' ≤ f s

The basic lemma (CKM §4). If f p = sup f and f is constant on the equator of p, then f s' ≤ f s for every s ≠ p in the northern hemisphere and every s' on the descent through s.

theorem Gleason.IsFrameFunction.descent_lt_add {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W m : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) {M ξ : ℝ} (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ M) (hpξ : M - ξ < f p) (hE : ∀ e ∈ equator p, f e = m) {s s' : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) (hsp : s ≠ p) (hs' : s' ∈ descent p s) : f s' - ξ < f s

The approximate basic lemma (CKM §4). If f p > sup f − ξ and f is constant on the equator of p, then f s' − ξ < f s for s' on the descent through s ≠ p.

theorem Gleason.IsFrameFunction.le_of_latitude_lt {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W m : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ f p) (hE : ∀ e ∈ equator p, f e = m) {s t : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) (ht : t ∈ northern p) (hl : latitude p s < latitude p t) : f s ≤ f t

Monotonicity in latitude (CKM §5). Under the hypotheses of the basic lemma, f is monotone in latitude on the northern hemisphere: latitude p s < latitude p t → f s ≤ f t.

Frames with prescribed latitudes

theorem Gleason.exists_frame_of_latitudes {p : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) {a b c : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (habc : a + b + c = 1) : ∃ (q : Fin 3 → EuclideanSpace ℝ (Fin 3)), Orthonormal ℝ q ∧ (∀ (j : Fin 3), q j ∈ northern p) ∧ latitude p (q 0) = a ∧ latitude p (q 1) = b ∧ latitude p (q 2) = c

A frame with prescribed latitudes. For a + b + c = 1, a, b, c ≥ 0, there is a frame (q₀, q₁, q₂) in the northern hemisphere of p with latitudes a, b, c: transport the unit vector (√a, √b, √c), completed to an orthonormal basis, through an orthonormal basis (p, e₁, e₂).

Suprema and infima over the parallels

def Gleason.parallelValues (p : EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ) (l : ℝ) : Set ℝ

The values of f on the l-th parallel of the northern hemisphere.

Equations

• Gleason.parallelValues p f l = f '' {s : EuclideanSpace ℝ (Fin 3) | s ∈ Gleason.northern p ∧ Gleason.latitude p s = l}

noncomputable def Gleason.parallelSup (p : EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ) (l : ℝ) : ℝ

The supremum of f over the l-th parallel.

Equations

• Gleason.parallelSup p f l = sSup (Gleason.parallelValues p f l)

noncomputable def Gleason.parallelInf (p : EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ) (l : ℝ) : ℝ

The infimum of f over the l-th parallel.

Equations

• Gleason.parallelInf p f l = sInf (Gleason.parallelValues p f l)

theorem Gleason.mem_parallelValues {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {s : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) : f s ∈ parallelValues p f (latitude p s)

theorem Gleason.parallelValues_nonempty {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {l : ℝ} (hp : ‖p‖ = 1) (hl : l ∈ Set.Icc 0 1) : (parallelValues p f l).Nonempty

theorem Gleason.bddAbove_parallelValues {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {l : ℝ} (h1 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ 1) : BddAbove (parallelValues p f l)

theorem Gleason.bddBelow_parallelValues {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {l : ℝ} (h0 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → 0 ≤ f u) : BddBelow (parallelValues p f l)

theorem Gleason.le_parallelSup {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (h1 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ 1) {s : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) : f s ≤ parallelSup p f (latitude p s)

theorem Gleason.parallelInf_le {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (h0 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → 0 ≤ f u) {s : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) : parallelInf p f (latitude p s) ≤ f s

theorem Gleason.parallelSup_le_one {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {l : ℝ} (hp : ‖p‖ = 1) (h1 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ 1) (hl : l ∈ Set.Icc 0 1) : parallelSup p f l ≤ 1

theorem Gleason.parallelInf_nonneg {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {l : ℝ} (hp : ‖p‖ = 1) (h0 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → 0 ≤ f u) (hl : l ∈ Set.Icc 0 1) : 0 ≤ parallelInf p f l

theorem Gleason.parallelInf_le_parallelSup {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {l : ℝ} (hp : ‖p‖ = 1) (h0 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → 0 ≤ f u) (h1 : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ 1) (hl : l ∈ Set.Icc 0 1) : parallelInf p f l ≤ parallelSup p f l

theorem Gleason.parallelSup_le_parallelInf {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} {l : ℝ} (hp : ‖p‖ = 1) (hmono : ∀ (s t : EuclideanSpace ℝ (Fin 3)), s ∈ northern p → t ∈ northern p → latitude p s < latitude p t → f s ≤ f t) {l' : ℝ} (hl : 0 ≤ l) (hl' : l' ≤ 1) (hll' : l < l') : parallelSup p f l ≤ parallelInf p f l'

The parallels are interlaced: for l < l', every value on the l-th parallel is at most every value on the l'-th.

theorem Gleason.parallelValues_zero {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (hE : ∀ e ∈ equator p, f e = 0) : parallelValues p f 0 = {0}

theorem Gleason.parallelValues_one {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (hp : ‖p‖ = 1) : parallelValues p f 1 = {f p}

theorem Gleason.parallelSup_zero {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (hE : ∀ e ∈ equator p, f e = 0) : parallelSup p f 0 = 0

theorem Gleason.parallelInf_zero {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (hE : ∀ e ∈ equator p, f e = 0) : parallelInf p f 0 = 0

theorem Gleason.parallelSup_one {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (hp : ‖p‖ = 1) : parallelSup p f 1 = f p

theorem Gleason.parallelInf_one {p : EuclideanSpace ℝ (Fin 3)} {f : EuclideanSpace ℝ (Fin 3) → ℝ} (hp : ‖p‖ = 1) : parallelInf p f 1 = f p

The simple frame functions

theorem Gleason.IsFrameFunction.eq_latitude_of_normalised {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) (hfp : f p = 1) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ 1) (hE : ∀ e ∈ equator p, f e = 0) (s : EuclideanSpace ℝ (Fin 3)) : ‖s‖ = 1 → f s = latitude p s

The simple-frame-function theorem, normalised (CKM §5). A frame function with f p = 1 = sup f and f = 0 on the equator of p is the latitude: f s = ⟪p, s⟫².

theorem Gleason.IsFrameFunction.eq_add_mul_latitude {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W m : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ f p) (hE : ∀ e ∈ equator p, f e = m) (s : EuclideanSpace ℝ (Fin 3)) : ‖s‖ = 1 → f s = m + (f p - m) * latitude p s

★ The simple-frame-function theorem (CKM §5, Theorem). If a frame function attains its supremum at p and takes the constant value m on the equator of p, then f s = m + (f p − m) ⟪p, s⟫² for every unit s.