Lax Lean Archive

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

The maximal ergodic theorem

Lax606786.MaximalErgodicTheorem · concepts/Lax606786/MaximalErgodicTheorem.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), let f:Ω→Rf : \Omega \to \mathbb{R} be measurable and integrable, and write Sjf=∑i<jf∘σiS_j f = \sum_{i < j} f \circ \sigma^i for its Birkhoff sums. For every nn,

    ∫{x : Sjf(x)>0 for some 1≤j≤n}f dμ ≥ 0.\int_{\{x \,:\, S_j f(x) > 0 \text{ for some } 1 \le j \le n\}} f \, d\mu \ \ge\ 0.

    If moreover μ\mu is finite then, for every ε>0\varepsilon > 0 and every nn, the weak-type maximal inequality holds:

    ε μ{x:Sjf(x)>εj for some 1≤j≤n}≤∫∣f∣ dμ.\varepsilon\, \mu\{x : S_j f(x) > \varepsilon j \text{ for some } 1 \le j \le n\} \le \int |f| \, d\mu.

    The first statement is Garsia's form of the maximal ergodic theorem (Garsia 1965; see also Rudolph 1990, Lemma 3.2).

    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 maximal_ergodic proven

    2 maximal_inequality proven

    Lean source view on GitLab

    1import Mathlib.Dynamics.BirkhoffSum.Basic
    2import Mathlib.Dynamics.Ergodic.MeasurePreserving
    3import Mathlib.MeasureTheory.Integral.Bochner.Set
    4
    5/-!
    6---
    7title: The maximal ergodic theorem
    8type: theorem
    9---
    10Let σ\sigma be a measure-preserving map of a measure space (Ω,μ)(\Omega, \mu), let
    11f:Ω→Rf : \Omega \to \mathbb{R} be measurable and integrable, and write
    12Sjf=∑i<jf∘σiS_j f = \sum_{i < j} f \circ \sigma^i for its Birkhoff sums. For every nn,
    13∫{x : Sjf(x)>0 for some 1≤j≤n}f dμ ≥ 0.\int_{\{x \,:\, S_j f(x) > 0 \text{ for some } 1 \le j \le n\}} f \, d\mu \ \ge\ 0.
    14If moreover μ\mu is finite then, for every ε>0\varepsilon > 0 and every nn, the weak-type
    15maximal inequality holds:
    16ε μ{x:Sjf(x)>εj for some 1≤j≤n}≤∫∣f∣ dμ.\varepsilon\, \mu\{x : S_j f(x) > \varepsilon j \text{ for some } 1 \le j \le n\} \le \int |f| \, d\mu.
    17
    18The first statement is Garsia's form of the maximal ergodic theorem (Garsia 1965; see also Rudolph 1990, Lemma 3.2).
    19-/
    20
    21namespace Lax606786.MaximalErgodicTheorem
    22
    23open MeasureTheory
    24
    25variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {σ : Ω → Ω} {f : Ω → ℝ}
    26
    27/-- Garsia's maximal ergodic theorem. -/
    28axiom maximal_ergodic (hmp : MeasurePreserving σ μ μ) (hf : Integrable f μ)
    29 (hfm : Measurable f) (n : ℕ) :
    30 0 ≤ ∫ x in {x | ∃ j, 1 ≤ j ∧ j ≤ n ∧ 0 < birkhoffSum σ f j x}, f x ∂μ
    31
    32/-- The weak-type `(1,1)` maximal inequality. -/
    33axiom maximal_inequality [IsFiniteMeasure μ] (hmp : MeasurePreserving σ μ μ)
    34 (hf : Integrable f μ) (hfm : Measurable f) {ε : ℝ} (hε : 0 < ε) (n : ℕ) :
    35 ε * μ.real {x | ∃ j, 1 ≤ j ∧ j ≤ n ∧ ε * j < birkhoffSum σ f j x} ≤ ∫ x, |f x| ∂μ
    36
    37end Lax606786.MaximalErgodicTheorem
    38
    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…