Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Rokhlin's lemma

Lax606786.RokhlinLemma · concepts/Lax606786/RokhlinLemma.lean · lax-606786

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let σ\sigma be an invertible ergodic measure-preserving transformation of a Lebesgue probability space (Ω,μ)(\Omega, \mu) (a standard Borel space with a probability measure giving points measure zero). For every n≥1n \ge 1 and ε>0\varepsilon > 0 there is a measurable set B⊆ΩB \subseteq \Omega such that B,σB,…,σn−1BB, \sigma B, \ldots, \sigma^{n-1} B are pairwise disjoint and

    μ(⋃i=0n−1σiB)>1−ε.\mu\Big(\bigcup_{i=0}^{n-1} \sigma^i B\Big) > 1 - \varepsilon.
    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitLab

    1import Mathlib.Dynamics.Ergodic.Ergodic
    2import Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
    3import Mathlib.MeasureTheory.Constructions.Polish.Basic
    4
    5/-!
    6---
    7title: Rokhlin's lemma
    8type: theorem
    9---
    10Let σ\sigma be an invertible ergodic measure-preserving transformation of a Lebesgue
    11probability space (Ω,μ)(\Omega, \mu) (a standard Borel space with a probability measure giving
    12points measure zero). For every n≥1n \ge 1 and ε>0\varepsilon > 0 there is a measurable set
    13B⊆ΩB \subseteq \Omega such that B,σB,…,σn−1BB, \sigma B, \ldots, \sigma^{n-1} B are pairwise disjoint and
    14μ(⋃i=0n−1σiB)>1−ε.\mu\Big(\bigcup_{i=0}^{n-1} \sigma^i B\Big) > 1 - \varepsilon.
    15-/
    16
    17namespace Lax606786.RokhlinLemma
    18
    19open MeasureTheory
    20
    21/-- A Rokhlin tower of height `n` covering all but `ε` of the space. -/
    22axiom rokhlin_lemma {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    23 (μ : Measure Ω) [IsProbabilityMeasure μ] [NullSingletonClass μ]
    24 (σ : Ω ≃ᵐ Ω) (hσ : Ergodic σ μ) (n : ℕ) (hn : 1 ≤ n) (ε : ℝ) (hε : 0 < ε) :
    25 ∃ B : Set Ω, MeasurableSet B ∧
    26 (∀ i < n, ∀ j < n, i ≠ j → Disjoint (σ^[i] '' B) (σ^[j] '' B)) ∧
    27 ENNReal.ofReal (1 - ε) < μ (⋃ i ∈ Finset.range n, σ^[i] '' B)
    28
    29end Lax606786.RokhlinLemma
    30
    Show Proof
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…