@[reducible]

def invariantMeasurableSpace {α : Type u_1} (m₀ : MeasurableSpace α) (T : α → α) : MeasurableSpace α

The sub-σ-algebra of T-invariant measurable sets on (α, m₀): those s ∈ m₀ satisfying T⁻¹(s) = s. This is the invariant σ-algebra 𝓘 appearing on the right-hand side of Birkhoff's ergodic theorem.

theorem birkhoff_ergodic_theorem {α : Type u_2} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : α → α) (g : α → ℝ) (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.IsProbabilityMeasure μ] (hg : MeasureTheory.Integrable g μ) : ∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ T g n ω) Filter.atTop (nhds (μ[g | invariantMeasurableSpace m₀ T] ω))

Birkhoff's ergodic theorem (a.s. form). Let T be a measure-preserving transformation of the probability space (α, m₀, μ) and let g ∈ L¹(μ). Then the time averages (1/n) ∑_{m=0}^{n-1} g(T^m ω) converge μ-almost surely to the conditional expectation E(g | 𝓘), where 𝓘 = invariantMeasurableSpace m₀ T is the σ-algebra of T-invariant measurable sets (Durrett, Lecture 33).

theorem birkhoff_ergodic_theorem_L1 {α : Type u_2} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : α → α) (g : α → ℝ) (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.IsProbabilityMeasure μ] (hg : MeasureTheory.Integrable g μ) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : α), ‖birkhoffAverage ℝ T g n ω - μ[g | invariantMeasurableSpace m₀ T] ω‖ ∂μ) Filter.atTop (nhds 0)

Birkhoff's ergodic theorem (L¹ form). Under the same hypotheses as birkhoff_ergodic_theorem, the Birkhoff averages converge to E(g | 𝓘) in L¹(μ): the L¹ distance ∫ ‖A_n g - E(g | 𝓘)‖ dμ tends to 0 as n → ∞.

theorem birkhoff_ergodic_theorem_full {α : Type u_2} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : α → α) (g : α → ℝ) (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.IsProbabilityMeasure μ] (hg : MeasureTheory.Integrable g μ) : (∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ T g n ω) Filter.atTop (nhds (μ[g | invariantMeasurableSpace m₀ T] ω))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (ω : α), ‖birkhoffAverage ℝ T g n ω - μ[g | invariantMeasurableSpace m₀ T] ω‖ ∂μ) Filter.atTop (nhds 0)

Birkhoff's ergodic theorem (combined). Combines birkhoff_ergodic_theorem and birkhoff_ergodic_theorem_L1: the Birkhoff averages of g ∈ L¹(μ) under a measure-preserving T converge to E(g | 𝓘) both μ-almost surely and in L¹(μ).