From 48ffad49c57962eed79f7ee8a486d3d1201537ad Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 24 May 2026 07:45:48 +0000 Subject: [PATCH] feat: add Rokhlin lemma eval problem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §109 of Knill's "Some Fundamental Theorems in Mathematics" (Rokhlin 1947, independently Kakutani 1943). Every aperiodic measure-preserving automorphism of a standard Borel probability space admits, for every height n and every ε > 0, a measurable tower base B such that B, T B, …, T^{n-1} B are pairwise disjoint with total measure ≥ 1 - ε. The [StandardBorelSpace Ω] hypothesis is essential — the countable- cocountable σ-algebra on ℝ has MeasurableSingletonClass but admits no nontrivial Rokhlin towers for the integer-shift map. Mathlib has MeasurePreserving, periodic-point infrastructure, and StandardBorelSpace but no Rokhlin lemma. Co-Authored-By: Claude Opus 4.7 --- LeanEval/Dynamics/RokhlinLemma.lean | 75 +++++++++++++++++++++++++++ manifests/problems/rokhlin_lemma.toml | 9 ++++ 2 files changed, 84 insertions(+) create mode 100644 LeanEval/Dynamics/RokhlinLemma.lean create mode 100644 manifests/problems/rokhlin_lemma.toml diff --git a/LeanEval/Dynamics/RokhlinLemma.lean b/LeanEval/Dynamics/RokhlinLemma.lean new file mode 100644 index 0000000..3c6a9e0 --- /dev/null +++ b/LeanEval/Dynamics/RokhlinLemma.lean @@ -0,0 +1,75 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace Dynamics + +/-! +# Rokhlin lemma (Rokhlin 1947; independently Kakutani 1943) + +§109 of Knill's *Some Fundamental Theorems in Mathematics*. Every +aperiodic measure-preserving automorphism of a standard Borel +probability space admits, for every height `n` and every `ε > 0`, a +measurable tower base `B` such that `B, T B, …, T^{n−1} B` are pairwise +disjoint and their union has measure at least `1 − ε`. + +Mathlib has `MeasurePreserving`, `IsProbabilityMeasure`, periodic-point +infrastructure (`Function.periodicPts`), `Set.PairwiseDisjoint`, and +`StandardBorelSpace`, but no Rokhlin lemma (`grep -ri 'rokhlin' +Mathlib/Dynamics/` finds nothing; the only `tower` hits are +`IsScalarTower`). The Challenge ships four small helper definitions +(`IsAperiodic`, `towerFloor`, `towerUnion`, `IsRokhlinTower`). + +The `[StandardBorelSpace Ω]` hypothesis is essential: the +countable-cocountable σ-algebra on `ℝ` with the integer-shift map +`x ↦ x + 1` is aperiodic and measure-preserving (for the 0/1 measure +that sends countable sets to 0 and cocountable sets to 1), but admits +no nontrivial Rokhlin towers — every cocountable base intersects its +own shift, and every countable base has zero-measure tower. The +countable-cocountable σ-algebra has `MeasurableSingletonClass` but is +strictly coarser than the Borel σ-algebra of any Polish topology on +`ℝ`, hence not standard Borel. +-/ + +open MeasureTheory Set + +/-- `T : Ω → Ω` is **aperiodic** w.r.t. `μ` if the set of periodic +points has measure zero, i.e. for a.e. `x`, no positive iterate of `T` +fixes `x`. -/ +def IsAperiodic {Ω : Type*} [MeasurableSpace Ω] + (T : Ω → Ω) (μ : Measure Ω) : Prop := + μ (Function.periodicPts T) = 0 + +/-- The level-`k` floor of a Rokhlin tower of base `B`: the image +`T^[k] '' B`. -/ +def towerFloor {Ω : Type*} (T : Ω → Ω) (B : Set Ω) (k : ℕ) : Set Ω := + T^[k] '' B + +/-- The set-theoretic union of a Rokhlin tower of base `B` and height +`n`. -/ +def towerUnion {Ω : Type*} (T : Ω → Ω) (B : Set Ω) (n : ℕ) : Set Ω := + ⋃ k ∈ Finset.range n, towerFloor T B k + +/-- The base `B` is a **Rokhlin tower of height `n`** for `T` if the +floors `B, T B, …, T^{n−1} B` are measurable and pairwise disjoint. -/ +def IsRokhlinTower {Ω : Type*} [MeasurableSpace Ω] + (T : Ω → Ω) (B : Set Ω) (n : ℕ) : Prop := + MeasurableSet B ∧ + (Finset.range n : Set ℕ).PairwiseDisjoint (towerFloor T B) + +/-- **Rokhlin lemma.** For every aperiodic measure-preserving +automorphism `T` of a standard Borel probability space `(Ω, μ)`, every +height `n ≥ 1`, and every `ε > 0`, there is a Rokhlin tower of height +`n` whose union has measure at least `1 − ε`. -/ +@[eval_problem] +theorem rokhlin_lemma {Ω : Type*} [MeasurableSpace Ω] + [StandardBorelSpace Ω] + (μ : Measure Ω) [IsProbabilityMeasure μ] (T : Ω → Ω) + (_hT : MeasurePreserving T μ μ) (_hap : IsAperiodic T μ) + (n : ℕ) (_hn : 1 ≤ n) {ε : ENNReal} (_hε : 0 < ε) : + ∃ B : Set Ω, IsRokhlinTower T B n ∧ + μ (towerUnion T B n) ≥ 1 - ε := by + sorry + +end Dynamics +end LeanEval diff --git a/manifests/problems/rokhlin_lemma.toml b/manifests/problems/rokhlin_lemma.toml new file mode 100644 index 0000000..a92dece --- /dev/null +++ b/manifests/problems/rokhlin_lemma.toml @@ -0,0 +1,9 @@ +id = "rokhlin_lemma" +title = "Rokhlin lemma" +test = false +module = "LeanEval.Dynamics.RokhlinLemma" +holes = ["rokhlin_lemma"] +submitter = "Kim Morrison" +notes = "§109 of Knill's 'Some Fundamental Theorems in Mathematics'. Every aperiodic measure-preserving automorphism of a standard Borel probability space admits, for every height n and every ε > 0, a measurable tower base B such that B, T B, …, T^{n-1} B are pairwise disjoint with total measure ≥ 1 - ε. The [StandardBorelSpace Ω] hypothesis is essential: the countable-cocountable σ-algebra on ℝ with the integer-shift map x ↦ x + 1 is aperiodic and measure-preserving but admits no nontrivial Rokhlin towers (every cocountable base intersects its own shift; every countable base has zero-measure tower). Mathlib has MeasurePreserving, IsProbabilityMeasure, Function.periodicPts, Set.PairwiseDisjoint, and StandardBorelSpace, but no Rokhlin lemma. The Challenge ships four small helper defs (IsAperiodic, towerFloor, towerUnion, IsRokhlinTower)." +source = "V. A. Rokhlin, *A general measure-preserving transformation is not mixing*, Doklady Akademii Nauk SSSR 60 (1948), 349-351 (original Russian; English translation later); S. Kakutani, *Induced measure-preserving transformations*, Proc. Imp. Acad. Tokyo 19 (1943), 635-641 (independent discovery). Listed as §109 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover." +informal_solution = "Standard proof: pick a measurable set A of small measure ε/n with positive density relative to T's orbit structure (the Halmos–Kakutani skyscraper). The first-return time r : A → ℕ is a.e. finite by aperiodicity; partition A by level sets {r = k}. Reassemble disjoint level-k floors T^j ({r = k}) for j < k into a height-n tower by horizontal cuts; the remaining 'roof' has measure at most ε."