Lax Lean Archive

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

Birkhoff's pointwise ergodic theorem

Lax606786.BirkhoffErgodicTheorem · concepts/Lax606786/BirkhoffErgodicTheorem.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 ergodic measure-preserving transformation of a probability space (Ω,μ)(\Omega, \mu) and let f:Ω→Rf : \Omega \to \mathbb{R} be measurable and integrable. Then the Birkhoff averages converge to the space average almost everywhere:

    1n∑k=0n−1f(σkω)→∫f dμfor μ-a.e. ω.\frac1n \sum_{k=0}^{n-1} f(\sigma^k \omega) \to \int f \, d\mu \quad \text{for } \mu\text{-a.e. } \omega.

    The theorem is due to Birkhoff (1931).

    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.BirkhoffSum.Average
    2import Mathlib.Dynamics.Ergodic.Ergodic
    3import Mathlib.MeasureTheory.Integral.Bochner.Basic
    4
    5/-!
    6---
    7title: Birkhoff's pointwise ergodic theorem
    8type: theorem
    9---
    10Let σ\sigma be an ergodic measure-preserving transformation of a probability space
    11(Ω,μ)(\Omega, \mu) and let f:Ω→Rf : \Omega \to \mathbb{R} be measurable and integrable. Then the
    12Birkhoff averages converge to the space average almost everywhere:
    131n∑k=0n−1f(σkω)→∫f dμfor μ-a.e. ω.\frac1n \sum_{k=0}^{n-1} f(\sigma^k \omega) \to \int f \, d\mu \quad \text{for } \mu\text{-a.e. } \omega.
    14
    15The theorem is due to Birkhoff (1931).
    16-/
    17
    18namespace Lax606786.BirkhoffErgodicTheorem
    19
    20open MeasureTheory Filter Topology
    21
    22/-- The Birkhoff averages of an integrable function converge almost everywhere to its integral. -/
    23axiom birkhoff {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    24 (σ : Ω → Ω) (hσ : Ergodic σ μ) (f : Ω → ℝ) (hfm : Measurable f) (hf : Integrable f μ) :
    25 ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => birkhoffAverage ℝ σ f n ω) atTop (𝓝 (∫ x, f x ∂μ))
    26
    27end Lax606786.BirkhoffErgodicTheorem
    28
    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…