feat: add Rokhlin lemma eval problem

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

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 ε."