Lax Lean Archive

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

Periodic points of an ergodic system on a Lebesgue space are null

Lax606786.PeriodicPointsNull · concepts/Lax606786/PeriodicPointsNull.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 nonatomic standard probability space (Ω,μ)(\Omega, \mu). Then for every N≥1N \ge 1 the set {ω:σNω=ω}\{\omega : \sigma^N \omega = \omega\} is null.

    Consequently, inside any set of positive measure there is a set of positive measure whose first NN iterates are pairwise disjoint.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 exists_subset_disjoint_iterates proven

    2 measure_periodicPts_eq_zero proven

    Lean source view on GitLab

    1import Mathlib.Dynamics.Ergodic.Ergodic
    2import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
    3import Mathlib.MeasureTheory.Constructions.Polish.Basic
    4
    5/-!
    6---
    7title: Periodic points of an ergodic system on a Lebesgue space are null
    8type: theorem
    9---
    10Let σ\sigma be an invertible ergodic measure-preserving transformation of a nonatomic standard
    11probability space (Ω,μ)(\Omega, \mu). Then for every N≥1N \ge 1 the set {ω:σNω=ω}\{\omega : \sigma^N \omega = \omega\}
    12 is null.
    13
    14Consequently, inside any set of positive measure there is a set of positive measure whose first NN
    15iterates are pairwise disjoint.
    16-/
    17
    18namespace Lax606786.PeriodicPointsNull
    19
    20open MeasureTheory
    21
    22/-- The points of period `N` form a null set. -/
    23axiom measure_periodicPts_eq_zero {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    24 (μ : Measure Ω) [IsProbabilityMeasure μ] [NullSingletonClass μ] (σ : Ω ≃ᵐ Ω)
    25 (hσ : Ergodic σ μ) {N : ℕ} (hN : 1 ≤ N) :
    26 μ {x | σ^[N] x = x} = 0
    27
    28/-- Inside a set of positive measure there is a set of positive measure whose first `N`
    29iterates are pairwise disjoint. -/
    30axiom exists_subset_disjoint_iterates {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    31 (μ : Measure Ω) [IsProbabilityMeasure μ] [NullSingletonClass μ] (σ : Ω ≃ᵐ Ω)
    32 (hσ : Ergodic (⇑σ) μ) (N : ℕ) {A : Set Ω} (hA : MeasurableSet A) (hApos : 0 < μ A) :
    33 ∃ A' ⊆ A, MeasurableSet A' ∧ 0 < μ A' ∧
    34 ∀ i < N, ∀ k < N, i ≠ k → Disjoint ((⇑σ)^[i] '' A') ((⇑σ)^[k] '' A')
    35
    36end Lax606786.PeriodicPointsNull
    37
    Show ProofShow 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…