Lax Lean Archive

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

Recurrence, and invariance along orbits

Lax606786.RecurrenceAndInvariance · concepts/Lax606786/RecurrenceAndInvariance.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 a measure-preserving map of a measure space (Ω,μ)(\Omega, \mu).

    • An almost-everywhere property holds almost everywhere at every point of the forward orbit: if pp holds a.e., then a.e. ω\omega has p(σiω)p(\sigma^i\omega) for every ii.
    • ∫g∘σk dμ=∫g dμ\int g \circ \sigma^k \, d\mu = \int g \, d\mu for integrable gg.
    • (Recurrence.) If μ\mu is a probability measure, σ\sigma is ergodic and μ(Λ)>0\mu(\Lambda) > 0, then almost every orbit visits Λ\Lambda.
    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

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

    1 ae_exists_mem_iterate proven

    2 ae_forall_iterate proven

    3 integral_comp_iterate proven

    Lean source view on GitLab

    1import Mathlib.Dynamics.Ergodic.Ergodic
    2import Mathlib.MeasureTheory.Integral.Bochner.Basic
    3
    4/-!
    5---
    6title: Recurrence, and invariance along orbits
    7type: theorem
    8---
    9Let σ\sigma be a measure-preserving map of a measure space (Ω,μ)(\Omega, \mu).
    10
    11- An almost-everywhere property holds almost everywhere at every point of the forward orbit: if
    12 pp holds a.e., then a.e. ω\omega has p(σiω)p(\sigma^i\omega) for every ii.
    13- ∫g∘σk dμ=∫g dμ\int g \circ \sigma^k \, d\mu = \int g \, d\mu for integrable gg.
    14- (Recurrence.) If μ\mu is a probability measure, σ\sigma is ergodic and μ(Λ)>0\mu(\Lambda) > 0, then
    15 almost every orbit visits Λ\Lambda.
    16-/
    17
    18namespace Lax606786.RecurrenceAndInvariance
    19
    20open MeasureTheory
    21
    22variable {Ω : Type*} [MeasurableSpace Ω]
    23
    24/-- An a.e. property holds a.e. along whole forward orbits. -/
    25axiom ae_forall_iterate {μ : Measure Ω} {σ : Ω → Ω} (hσ : MeasurePreserving σ μ μ)
    26 {p : Ω → Prop} (h : ∀ᵐ ω ∂μ, p ω) : ∀ᵐ ω ∂μ, ∀ i : ℕ, p (σ^[i] ω)
    27
    28/-- Integrals are invariant under iterates of a measure-preserving map. -/
    29axiom integral_comp_iterate {μ : Measure Ω} {σ : Ω → Ω} (hmp : MeasurePreserving σ μ μ)
    30 {g : Ω → ℝ} (hg : Integrable g μ) (k : ℕ) :
    31 ∫ ω, g (σ^[k] ω) ∂μ = ∫ ω, g ω ∂μ
    32
    33/-- Almost every orbit of an ergodic map visits a set of positive measure. -/
    34axiom ae_exists_mem_iterate {μ : Measure Ω} [IsProbabilityMeasure μ] {σ : Ω → Ω}
    35 (hσ : Ergodic σ μ) {Λ : Set Ω} (hΛm : MeasurableSet Λ) (hΛ : μ Λ ≠ 0) :
    36 ∀ᵐ ω ∂μ, ∃ n : ℕ, σ^[n] ω ∈ Λ
    37
    38end Lax606786.RecurrenceAndInvariance
    39
    Show ProofShow 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…