Gleason's theorem, finite-dimensional: the two "warmup" theorems on [0, 1]

Category: 1-Mathlib (CSD-free; staged for upstream). specs/gleason-feasibility.md, stage 57(a), second half: Cooke–Keane–Moran §3 — the one-dimensional "abelianised" versions of Gleason's theorem, which the core lemma's proof (§5) applies along the latitudes of the sphere.

• Warmup Theorem I (affine_of_sum_eq_const): a bounded f : [0, 1] → ℝ with f a + f b + f c constant whenever a + b + c = 1 is affine, f a = (w − 3 f 0) a + f 0. The engine is linear_of_add_on_Icc: an additive function on [0, 1] that is bounded there is linear — additivity is extended to ℝ by x ↦ g (fract x) + ⌊x⌋ g 1 and Gleason.additive_bounded_linear (Cauchy's equation with a local bound) finishes.
• Warmup Theorem II (eq_self_of_monotone_sum_eq_one): let C ⊆ (0, 1) be countable and f be defined off C with f 0 = 0, monotone on [0, 1] \ C, and f a + f b + f c = 1 whenever a + b + c = 1 off C. Then f a = a off C. The proof picks a₀ ∈ (0, 1) outside the countable set of rational multiples of C and 1 − C, so that every rational multiple r a₀ and its complement 1 − r a₀ avoid C; additivity on those gives f (r a₀) = r f a₀, monotonicity squeezes every other point between rational multiples, and the frame identity at one triple pins the slope to 1.

Source

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

Warmup Theorem I

theorem Gleason.linear_of_add_on_Icc {g : ℝ → ℝ} (hg0 : g 0 = 0) (hadd : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → a + b ≤ 1 → g (a + b) = g a + g b) {K : ℝ} (hK : ∀ a ∈ Set.Icc 0 1, |g a| ≤ K) (a : ℝ) : a ∈ Set.Icc 0 1 → g a = a * g 1

An additive function on [0, 1] that is bounded there is linear: g a = a · g 1. The additivity is extended to all of ℝ by x ↦ g (fract x) + ⌊x⌋ g 1.

theorem Gleason.affine_of_sum_eq_const {f : ℝ → ℝ} {w K : ℝ} (hK : ∀ a ∈ Set.Icc 0 1, |f a| ≤ K) (h : ∀ (a b c : ℝ), a ∈ Set.Icc 0 1 → b ∈ Set.Icc 0 1 → c ∈ Set.Icc 0 1 → a + b + c = 1 → f a + f b + f c = w) (a : ℝ) : a ∈ Set.Icc 0 1 → f a = (w - 3 * f 0) * a + f 0

Warmup Theorem I (CKM §3). A bounded f : [0, 1] → ℝ such that f a + f b + f c has the same value w whenever a + b + c = 1 is affine: f a = (w − 3 f 0) a + f 0.

Warmup Theorem II

theorem Gleason.eq_self_of_monotone_sum_eq_one {C : Set ℝ} (hC : C.Countable) (hC1 : C ⊆ Set.Ioo 0 1) {f : ℝ → ℝ} (hf0 : f 0 = 0) (hmono : ∀ (a b : ℝ), a ∈ Set.Icc 0 1 → b ∈ Set.Icc 0 1 → a ∉ C → b ∉ C → a < b → f a ≤ f b) (hsum : ∀ (a b c : ℝ), a ∈ Set.Icc 0 1 → b ∈ Set.Icc 0 1 → c ∈ Set.Icc 0 1 → a ∉ C → b ∉ C → c ∉ C → a + b + c = 1 → f a + f b + f c = 1) (a : ℝ) : a ∈ Set.Icc 0 1 → a ∉ C → f a = a

Warmup Theorem II (CKM §3). Let C ⊆ (0, 1) be countable and f : ℝ → ℝ satisfy, on [0, 1] \ C: f 0 = 0, f is monotone, and f a + f b + f c = 1 whenever a + b + c = 1. Then f a = a on [0, 1] \ C.