Ornstein–Weiss ℤᵈ Rokhlin lemma

ornstein_weiss_rokhlin

Submitter: Kim Morrison.

Notes: §109 of Knill's 'Some Fundamental Theorems in Mathematics' (additional statement; the boxed main theorem is the classical Rokhlin lemma). The multidimensional generalization: for every free measure-preserving ℤᵈ-action T on a standard Borel probability space, every box size N ≥ 1, and every ε > 0, there is a measurable base B such that the translates T v '' B for v ∈ [0, N)ᵈ are pairwise disjoint with measure ≥ 1 - ε. Three hypotheses beyond the classical lemma: 1 ≤ d (rules out d = 0 degeneracy); the identity axiom T 0 = id (homomorphism alone only forces T 0 idempotent); [StandardBorelSpace Ω] (rules out the countable-cocountable σ-algebra defect). Mathlib has MeasurePreserving, IsProbabilityMeasure, Set.PairwiseDisjoint, Fintype.piFinset, Finset.Ico, StandardBorelSpace, but no Ornstein–Weiss lemma, no free measure-preserving ℤᵈ-actions, no multidimensional Rokhlin towers. The Challenge ships two small helper defs (IsFreeAction, boxShape).

Source: D. S. Ornstein and B. Weiss, *Entropy and isomorphism theorems for actions of amenable groups*, J. Anal. Math. 48 (1987), 1-141 — Theorem 5.2 establishes the multidimensional (and amenable-group) Rokhlin lemma. 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 reduces to the one-dimensional Rokhlin lemma by induction on d using the quasi-tiling lemma of Ornstein–Weiss: every Følner set in ℤᵈ can be ε-quasi-tiled by finitely many translates of cubes [0, N)ᵈ, so a one-dimensional skyscraper over a transversal of one direction can be folded into a d-dimensional Rokhlin tower with arbitrarily small remainder.

theorem declaration uses `sorry`ornstein_weiss_rokhlin {Ω : Type*} [MeasurableSpace Ω]
    [StandardBorelSpace Ω]
    {d : ℕ} (_hd : 1 ≤ d) (μ : Measure Ω) [IsProbabilityMeasure μ]
    (T : (Fin d → ℤ) → Ω → Ω)
    (_hid : ∀ x, T 0 x = x)
    (_hT : ∀ v, MeasurePreserving (T v) μ μ)
    (_hgrp : ∀ u v x, T (u + v) x = T u (T v x))
    (_hfree : LeanEval.Dynamics.IsFreeAction μ T)
    (N : ℕ) (_hN : 1 ≤ N) {ε : ENNReal} (_hε : 0 < ε) :
    ∃ B : Set Ω,
      MeasurableSet B ∧
      ((boxShape d N : Finset (Fin d → ℤ)) : Set (Fin d → ℤ)).PairwiseDisjoint
        (fun v => T v '' B) ∧
      μ (⋃ v ∈ boxShape d N, T v '' B) ≥ 1 - ε := byΩ:Type u_1inst✝²:MeasurableSpace Ωinst✝¹:StandardBorelSpace Ωd:ℕ_hd:1 ≤ dμ:Measure Ωinst✝:IsProbabilityMeasure μT:(Fin d → ℤ) → Ω → Ω_hid:∀ (x : Ω), T 0 x = x_hT:∀ (v : Fin d → ℤ), MeasurePreserving (T v) μ μ_hgrp:∀ (u v : Fin d → ℤ) (x : Ω), T (u + v) x = T u (T v x)_hfree:IsFreeAction μ TN:ℕ_hN:1 ≤ Nε:ENNReal_hε:0 < ε⊢ ∃ B, MeasurableSet B ∧ ((↑(boxShape d N)).PairwiseDisjoint fun v => T v '' B) ∧ μ (⋃ v ∈ boxShape d N, T v '' B) ≥ 1 - ε
  sorryAll goals completed! 🐙

Solved by

Not yet solved.