Rokhlin lemma

DefinitionFree \(\mathbb{Z}^d\)-action#✓fully proved

Let \(d\) be a natural number, let \(\mu\) be a measure on a measurable space \(\Omega\), and let \(T\) assign to each \(v \in \mathbb{Z}^d\) a map \(T_v \colon \Omega \to \Omega\). Then \(T\) is free (in the Ornstein–Weiss sense) with respect to \(\mu\) if, for every nonzero \(v \in \mathbb{Z}^d\), the set of points \(x \in \Omega\) with \(T_v(x) = x\) has \(\mu\)-measure zero.

def IsFreeAction {Ω : Type*} [MeasurableSpace Ω] {d : ℕ}
    (μ : Measure Ω) (T : (Fin d → ℤ) → Ω → Ω) : Prop :=
  ∀ v : Fin d → ℤ, v ≠ 0 → μ {x | T v x = x} = 0

Used by 1

Used byOrnstein–Weiss Rokhlin lemma for \(\mathbb{Z}^d\)-actions

DefinitionInteger box#✓fully proved

For natural numbers \(d\) and \(N\), the integer box \([0, N)^d\) is the finite set of vectors \(v \in \mathbb{Z}^d\) with \(0 \le v_i < N\) for every coordinate \(i\).

noncomputable def boxShape (d N : ℕ) : Finset (Fin d → ℤ) :=
  Fintype.piFinset (fun _ : Fin d => Finset.Ico (0 : ℤ) (N : ℤ))

Used by 1

Used byOrnstein–Weiss Rokhlin lemma for \(\mathbb{Z}^d\)-actions

TheoremOrnstein–Weiss Rokhlin lemma for \(\mathbb{Z}^d\)-actions#●ready to prove

Let \(d \ge 1\), let \(\Omega\) be a standard Borel space with a probability measure \(\mu\), and let \(T\) assign to each \(v \in \mathbb{Z}^d\) a map \(T_v \colon \Omega \to \Omega\) such that \(T_0\) is the identity, \(T_{u + v} = T_u \circ T_v\) for all \(u, v \in \mathbb{Z}^d\), every \(T_v\) is measure preserving for \(\mu\), and the action is free (for every \(v \ne 0\) the set of fixed points of \(T_v\) has \(\mu\)-measure zero). Then for every integer \(N \ge 1\) and every \(\varepsilon \in (0, \infty]\) there is a measurable set \(B \subseteq \Omega\) such that the images \(T_v(B)\), for \(v\) in the integer box \([0, N)^d\), are pairwise disjoint and their union has measure at least \(1 - \varepsilon\).

public theorem_wanted 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 : 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 - ε

Sources

• 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. Problem ornstein_weiss_rokhlin of the lean-eval benchmark.

Uses 2

Statement usesFree \(\mathbb{Z}^d\)-action · Integer box

DefinitionAperiodic transformation#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\). A map \(T : \Omega \to \Omega\) is aperiodic with respect to \(\mu\) if the set of periodic points of \(T\), the points \(x\) with \(T^k(x) = x\) for some \(k \ge 1\), where \(T^k\) is the \(k\)-fold iterate of \(T\), has (outer) \(\mu\)-measure zero. Equivalently, for \(\mu\)-almost every \(x\), no positive iterate of \(T\) fixes \(x\).

def IsAperiodic {Ω : Type*} [MeasurableSpace Ω]
    (T : Ω → Ω) (μ : Measure Ω) : Prop :=
  μ (Function.periodicPts T) = 0

Used by 1

Used byRokhlin lemma for non-invertible maps

DefinitionFloor of a Rokhlin tower#✓fully proved

For a map \(T : \Omega \to \Omega\), a set \(B \subseteq \Omega\) and \(k \in \mathbb{N}\), the level-\(k\) floor with base \(B\) is the image \(T^k(B)\) of \(B\) under the \(k\)-fold iterate \(T^k\) of \(T\); the level-\(0\) floor is \(B\).

def towerFloor {Ω : Type*} (T : Ω → Ω) (B : Set Ω) (k : ℕ) : Set Ω :=
  T^[k] '' B

Used by 2

Used byRokhlin tower · Union of a Rokhlin tower

DefinitionUnion of a Rokhlin tower#✓fully proved

For a map \(T : \Omega \to \Omega\), a set \(B \subseteq \Omega\) and \(n \in \mathbb{N}\), the union of the tower with base \(B\) and height \(n\) is the set \(\bigcup_{k=0}^{n-1} T^k(B)\) of its floors \(B, T(B), \dots, T^{n-1}(B)\), where \(T^k(B)\) is the image of \(B\) under the \(k\)-fold iterate of \(T\). It is empty when \(n = 0\), and no disjointness of the floors is required.

def towerUnion {Ω : Type*} (T : Ω → Ω) (B : Set Ω) (n : ℕ) : Set Ω :=
  ⋃ k ∈ Finset.range n, towerFloor T B k

Uses 1 · Used by 1

Statement usesFloor of a Rokhlin tower

Used byRokhlin lemma for non-invertible maps

DefinitionRokhlin tower#✓fully proved

Let \(\Omega\) be a measurable space, \(T : \Omega \to \Omega\) a map and \(n \in \mathbb{N}\). A set \(B \subseteq \Omega\) is the base of a Rokhlin tower of height \(n\) for \(T\) if \(B\) is measurable and the floors \(B, T(B), \dots, T^{n-1}(B)\) are pairwise disjoint, that is, \(T^i(B) \cap T^j(B) = \emptyset\) for all \(i \ne j\) with \(i, j < n\); here \(T^k(B)\) is the image of \(B\) under the \(k\)-fold iterate of \(T\).

Only the base is required to be measurable. For a non-invertible \(T\), the floors need not be measurable, so evaluating a measure on their union uses its outer measure.

def IsRokhlinTower {Ω : Type*} [MeasurableSpace Ω]
    (T : Ω → Ω) (B : Set Ω) (n : ℕ) : Prop :=
  MeasurableSet B ∧
    (Finset.range n : Set ℕ).PairwiseDisjoint (towerFloor T B)

Uses 1 · Used by 1

Statement usesFloor of a Rokhlin tower

Used byRokhlin lemma for non-invertible maps

TheoremRokhlin lemma for non-invertible maps#●ready to prove

Let \(\Omega\) be a standard Borel space with a probability measure \(\mu\), and let \(T : \Omega \to \Omega\) be a measure-preserving map that is aperiodic with respect to \(\mu\). Then for every integer \(n \ge 1\) and every \(\varepsilon \in (0, \infty]\) there is a measurable set \(B \subseteq \Omega\) such that the floors \(B, T(B), \dots, T^{n-1}(B)\) are pairwise disjoint, where \(T^k(B)\) is the image of \(B\) under the \(k\)-fold iterate of \(T\), and their union \(\bigcup_{k=0}^{n-1} T^k(B)\) has outer \(\mu\)-measure at least \(1 - \varepsilon\) (truncated subtraction, so the bound is \(0\) when \(\varepsilon \ge 1\)). No invertibility of \(T\) is assumed.

public theorem_wanted 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 - ε

Sources

• 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). Problem rokhlin_lemma of the lean-eval benchmark.

Uses 3

Statement usesAperiodic transformation · Rokhlin tower · Union of a Rokhlin tower

6 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.