The pointwise (Birkhoff) ergodic theorem

The individual (pointwise) ergodic theorem: for a measure-preserving map T of a finite measure space and an integrable g, the Birkhoff averages birkhoffAverage ℝ T g n x converge almost everywhere to the conditional expectation of g onto the σ-algebra of T-invariant sets. The proof combines the maximal ergodic inequality (Oseledets.Ergodic.MaximalErgodic), a Borel–Cantelli tail estimate for the orbital values of an integrable function, and the conditional-expectation API.

This file also proves the supporting commutation lemma (condExp commutes with a measure-preserving composition) and the ergodic corollary (the limit is the space average ∫ g ∂μ).

Main results

• Oseledets.condExp_invariants_comp: the conditional expectation onto the invariant σ-algebra commutes with composition by the measure-preserving map.
• Oseledets.ae_tendsto_orbit_div_atTop_zero: for integrable g, the orbital tail n⁻¹ · g (T^[n] x) tends to 0 almost everywhere.
• Oseledets.tendsto_birkhoffAverage_ae: the pointwise ergodic theorem over a finite measure. The finiteness hypothesis is necessary (see the theorem docstring).
• Oseledets.tendsto_birkhoffAverage_ae_integral: the ergodic case over a probability measure, where the a.e. limit is the space average ∫ g ∂μ.

References

• G. D. Birkhoff, Proof of the ergodic theorem, Proc. Natl. Acad. Sci. USA 17 (1931).
• Y. Katznelson, B. Weiss, A simple proof of some ergodic theorems, Israel J. Math. 42 (1982).

theorem Oseledets.condExp_invariants_comp {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) (hTm : Measurable T) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) : μ[g ∘ T | MeasurableSpace.invariants T] =ᵐ[μ] μ[g | MeasurableSpace.invariants T] ∘ T

condExp commutes with a measure-preserving composition: μ[g ∘ T | invariants T] =ᵐ[μ] (μ[g | invariants T]) ∘ T.

The tail estimate n⁻¹ · g (T^[n] x) → 0 a.e.

For an integrable g and a measure-preserving T, the orbital values g (T^[n] x) grow slower than linearly, almost everywhere. This is the analytic input that makes the Birkhoff limsup/liminf T-invariant. The proof is a Borel–Cantelli argument: for a fixed threshold δ > 0 the series ∑ₙ μ {x | (n+1)·δ ≤ |g x|} is finite (its terms integrate the pointwise count, bounded by |g|/δ), and measure-preservation transfers this to g ∘ T^[n].

theorem Oseledets.ae_tendsto_orbit_div_atTop_zero {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * g (T^[n] x)) Filter.atTop (nhds 0)

For integrable g and measure-preserving T, the orbital tail n⁻¹ · g (T^[n] x) tends to 0 almost everywhere. Proved by Borel–Cantelli: for each threshold δ = 1/(k+1) the series ∑ₙ μ {x | (n+1)δ ≤ |g (T^[n] x)|} is finite (measure-preservation transfers tsum_measure_threshold_ne_top), so a.e. only finitely many n cross the threshold. This estimate is what makes the one-step log-norm factor of a cocycle subexponential.

Almost-everywhere T-invariance facts

theorem Oseledets.ae_forall_orbit_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {h : X → ℝ} (hh : h ∘ T =ᵐ[μ] h) : ∀ᵐ (x : X) ∂μ, ∀ (j : ℕ), h (T^[j] x) = h x

If h ∘ T =ᵐ[μ] h then a.e. h is constant along the whole forward orbit: ∀ j, h (T^[j] x) = h x. Each step transfers h ∘ T =ᵐ h along the measure-preserving iterate T^[j], and a countable family of a.e. statements holds a.e.

theorem Oseledets.condExp_invariants_comp_self {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) (hTm : Measurable T) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) : μ[g | MeasurableSpace.invariants T] ∘ T =ᵐ[μ] μ[g | MeasurableSpace.invariants T]

The conditional expectation μ[g | invariants T] is a.e. T-invariant: (μ[g | invariants T]) ∘ T =ᵐ[μ] μ[g | invariants T]. Combines condExp_invariants_comp with condExp_comp_invariants_eq.

Maximal-set algebra and birkhoffAverage

theorem Oseledets.ae_bddAbove_birkhoffAverage {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) : ∀ᵐ (x : X) ∂μ, BddAbove (Set.range fun (n : ℕ) => birkhoffAverage ℝ T g (n + 1) x)

Almost every orbit has Birkhoff averages bounded above: the exceptional set where birkhoffAverage ℝ T g (·+1) x is unbounded above is contained in ⋂ₖ Bₖ, whose measure is ≤ ∫|g| / k → 0.

A real-analysis helper: limsup is insensitive to a vanishing perturbation

theorem Oseledets.limsup_eq_of_sub_tendsto_zero {u v : ℕ → ℝ} (hau : BddAbove (Set.range u)) (hbu : BddBelow (Set.range u)) (hav : BddAbove (Set.range v)) (hbv : BddBelow (Set.range v)) (h : Filter.Tendsto (fun (n : ℕ) => u n - v n) Filter.atTop (nhds 0)) : Filter.limsup u Filter.atTop = Filter.limsup v Filter.atTop

If two bounded real sequences differ by a sequence tending to 0, their limsups (along atTop) coincide. Bound u ≤ v + δ eventually and use limsup_add_const.

theorem Oseledets.ae_bddBelow_birkhoffAverage {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) : ∀ᵐ (x : X) ∂μ, BddBelow (Set.range fun (n : ℕ) => birkhoffAverage ℝ T g (n + 1) x)

Almost every orbit has Birkhoff averages bounded below (apply ae_bddAbove to -g).

limsup of the Birkhoff averages is a.e. T-invariant

The core one-sided bound limsup ≤ μ[g | I]

theorem Oseledets.measure_setOf_lt_limsup_eq_zero {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) {ε : ℝ} (hε : 0 < ε) : μ {x : X | μ[g | MeasurableSpace.invariants T] x + ε < Filter.limsup (fun (n : ℕ) => birkhoffAverage ℝ T g n x) Filter.atTop} = 0

Core maximal-inequality step. For ε > 0, the invariant superlevel set where the limsup of the Birkhoff averages strictly exceeds μ[g | I] + ε is null.

The set E = {x | L x + ε < Ls x} (with L = μ[g|I], Ls = limsup A_·(g)) is a.e. T-invariant, so a.e. equal to a genuinely invariant I-measurable set E' (exists_preimage_eq_of_preimage_ae). Applying the maximal ergodic inequality to φ = E'.indicator (g - L - ε) and showing the maximal set equals E', one gets 0 ≤ ∫_{E'} (g - L - ε) = -ε · μ E' (using ∫_{E'} g = ∫_{E'} L), forcing μ E' = 0.

theorem Oseledets.tendsto_birkhoffAverage_ae {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ T g n x) Filter.atTop (nhds (μ[g | MeasurableSpace.invariants T] x))

Pointwise (Birkhoff) ergodic theorem: for a finite measure, a measure-preserving T, and integrable g, the Birkhoff averages converge μ-a.e. to the conditional expectation of g onto the σ-algebra of T-invariant sets. Sandwiches the a.e. bounds limsup ≤ μ[g|I] and μ[g|I] ≤ liminf via tendsto_of_le_liminf_of_limsup_le.

The [IsFiniteMeasure μ] hypothesis is necessary: without it (e.g. when the trim of μ to invariants T is not σ-finite) μ[g | invariants T] = 0 while the Birkhoff averages need not converge to 0. The Oseledets MET only ever uses this for probability measures, where it applies directly.

theorem Oseledets.tendsto_birkhoffAverage_ae_integral {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {g : X → ℝ} (hg : MeasureTheory.Integrable g μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ T g n x) Filter.atTop (nhds (∫ (y : X), g y ∂μ))

Birkhoff ergodic theorem, ergodic case: when T is ergodic for a probability measure, the Birkhoff averages converge μ-a.e. to the space average ∫ g dμ.