Rokhlin lemma

rokhlin_lemma

Submitter: Kim Morrison.

Notes: §109 of Knill's 'Some Fundamental Theorems in Mathematics' gives the classical automorphism form. This problem strengthens it by dropping invertibility. The conclusion uses forward images: every aperiodic measure-preserving transformation of a standard Borel probability space admits, for every height n and every ε > 0, a measurable base B such that B, T B, …, T^{n-1} B are pairwise disjoint with union of outer measure ≥ 1 - ε. Only the base B is required measurable by IsRokhlinTower; the forward-image floors need not be measurable. 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); S.-M. Heinemann and O. Schmitt, *Rokhlin's lemma for non-invertible maps*, Dynam. Systems Appl. 10 (2001), no. 2, 201-213. The classical form is listed as §109 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Apply the non-invertible Rokhlin lemma in its usual preimage form to obtain a measurable high-measure tower `V = ⋃ j < n, T^{-j} C`. Put `B = T^{-(n-1)} C`, which is measurable. For `k < n`, the forward floor satisfies `T^k B = T^k(Ω) ∩ T^{-(n-1-k)} C`, so the floors are pairwise disjoint and their union contains `T^{n-1}(Ω) ∩ V`. Every measurable superset of `T^{n-1}(Ω)` pulls back to `Ω`, so `T^{n-1}(Ω)` has full outer measure; subadditivity with the small complement of `V` gives the required lower bound.

theorem declaration uses `sorry`rokhlin_lemma {Ω : Type*} [MeasurableSpace Ω]
    [StandardBorelSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (T : Ω → Ω)
    (_hT : MeasurePreserving T μ μ) (_hap : LeanEval.Dynamics.IsAperiodic T μ)
    (n : ℕ) (_hn : 1 ≤ n) {ε : ENNReal} (_hε : 0 < ε) :
    ∃ B : Set Ω, LeanEval.Dynamics.IsRokhlinTower T B n ∧
      μ (LeanEval.Dynamics.towerUnion T B n) ≥ 1 - ε := byΩ:Type u_1inst✝²:MeasurableSpace Ωinst✝¹:StandardBorelSpace Ωμ:Measure Ωinst✝:IsProbabilityMeasure μT:Ω → Ω_hT:MeasurePreserving T μ μ_hap:IsAperiodic T μn:ℕ_hn:1 ≤ nε:ENNReal_hε:0 < ε⊢ ∃ B, IsRokhlinTower T B n ∧ μ (towerUnion T B n) ≥ 1 - ε
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 27, 2026

• @parabamoghv with Aristotle (Harmonic) on Jun 9, 2026

• @lukerj00 with Tau (caj.al) on Jun 18, 2026

• @rishistyping with Stealth Model on Jul 1, 2026

• @Morgan-Griffiths with GPT-5.6 on Jul 13, 2026

• @ZhengyangZhang06 with Humanifa + GPT 5.6 sol on Jul 28, 2026