The Rokhlin (Kakutani) tower lemma (issue #15)

This file assembles the Rokhlin tower lemma: for an ergodic, measure-preserving automorphism e of a standard Borel probability space with a non-atomic measure, and for any height N ≥ 1 and any ε > 0, there is a measurable base set B whose first N iterates eⁱ '' B are pairwise disjoint and whose union covers all but ε of the space:

1 - ENNReal.ofReal ε < μ (⋃ i : Fin N, eⁱ '' B).

This is the key input to Krieger's generator theorem.

Proof outline

Fix a small positive base set A with μ A < ε / N (exists_small_pos_measurableSet). The base is the tower base B := towerBase e A N, the complete-block starts of the skyscraper over A.

• The N levels eⁱ '' B are pairwise disjoint (pairwise_disjoint_levels).
• Their union C := coveredSet e A N covers all but ε: the skyscraper covers a.e. point (skyscraper_ae_univ), the uncovered part of the skyscraper lies in the top incomplete floors (compl_inter_skyscraper_subset_topFloors), and those have measure ≤ ∑ k, ((k+1) mod N) · μ (returnLevel e A (k+1)) ≤ N · μ A < ε (measure_topFloors_le, tsum_returnLevel_eq, residual_lt_eps).

Main results

• rokhlin_tower_aux — the inner statement, carrying the benign working hypothesis ε ≤ 1.
• rokhlin_tower — the headline lemma; a WLOG wrapper reducing ε to min ε 1.

theorem Oseledets.Krieger.rokhlin_tower_aux {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NoAtoms μ] (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) (herg : Ergodic (⇑e) μ) (N : ℕ) (hN : 1 ≤ N) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) : ∃ (B : Set α), MeasurableSet B ∧ Pairwise (Function.onFun Disjoint fun (i : Fin N) => (⇑e)^[↑i] '' B) ∧ 1 - ENNReal.ofReal ε < μ (⋃ (i : Fin N), (⇑e)^[↑i] '' B)

Inner form of the Rokhlin tower lemma, carrying the benign working hypothesis ε ≤ 1: there is a measurable base whose first N iterates are pairwise disjoint and cover all but ε.

theorem Oseledets.Krieger.rokhlin_tower {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NoAtoms μ] (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) (herg : Ergodic (⇑e) μ) (N : ℕ) (hN : 1 ≤ N) (ε : ℝ) (hε : 0 < ε) : ∃ (B : Set α), MeasurableSet B ∧ Pairwise (Function.onFun Disjoint fun (i : Fin N) => (⇑e)^[↑i] '' B) ∧ 1 - ENNReal.ofReal ε < μ (⋃ (i : Fin N), (⇑e)^[↑i] '' B)

The Rokhlin (Kakutani) tower lemma. For an ergodic, measure-preserving automorphism e of a standard Borel probability space with non-atomic μ, any height N ≥ 1, and any ε > 0, there is a measurable base B whose first N iterates eⁱ '' B are pairwise disjoint and whose union covers all but ε of the space.

The proof reduces ε to min ε 1 ≤ 1 and applies rokhlin_tower_aux; since min ε 1 ≤ ε, the stronger small-ε bound implies the target.