Lax Lean Archive

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

Kingman's subadditive ergodic theorem

Lax606786.KingmanTheorem · concepts/Lax606786/KingmanTheorem.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 (fn)(f_n) be a subadditive family of integrable functions over σ\sigma. Then there is a constant C∈[−∞,∞)C \in [-\infty, \infty) such that

    C=lim⁡n→∞1n∫fn dμand1nfn(ω)→Cfor μ-a.e. ω.C = \lim_{n \to \infty} \tfrac1n \int f_n \, d\mu \qquad \text{and} \qquad \tfrac1n f_n(\omega) \to C \quad \text{for } \mu\text{-a.e. } \omega.

    Limits are taken in the extended reals [−∞,∞][-\infty, \infty]. The theorem is due to Kingman (1968).

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.SubadditiveFamilies
    2import Mathlib.Dynamics.Ergodic.Ergodic
    3import Mathlib.MeasureTheory.Integral.Bochner.Basic
    4import Mathlib.Data.EReal.Operations
    5
    6/-!
    7---
    8title: Kingman's subadditive ergodic theorem
    9type: theorem
    10---
    11Let σ\sigma be an ergodic measure-preserving transformation of a probability space
    12(Ω,μ)(\Omega, \mu), and let (fn)(f_n) be a subadditive family of integrable functions over σ\sigma.
    13Then there is a constant C∈[−∞,∞)C \in [-\infty, \infty) such that
    14C=lim⁡n→∞1n∫fn dμand1nfn(ω)→Cfor μ-a.e. ω.C = \lim_{n \to \infty} \tfrac1n \int f_n \, d\mu \qquad \text{and} \qquad \tfrac1n f_n(\omega) \to C \quad \text{for } \mu\text{-a.e. } \omega.
    15
    16Limits are taken in the extended reals [−∞,∞][-\infty, \infty]. The theorem is due to Kingman
    17(1968).
    18-/
    19
    20namespace Lax606786.KingmanTheorem
    21
    22open MeasureTheory Filter Topology
    23open Lax606786.SubadditiveFamilies
    24
    25/-- Kingman's theorem: `f_n / n` converges almost everywhere to the constant
    26`C = lim (1/n) ∫ f_n ∈ [-∞, ∞)`. -/
    27axiom kingman {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    28 (σ : Ω → Ω) (hσ : Ergodic σ μ) (f : ℕ → Ω → ℝ) (hf : IsSubadditiveFamily σ f)
    29 (hint : ∀ n, Integrable (f n) μ) :
    30 ∃ C : EReal, C ≠ ⊤ ∧
    31 Tendsto (fun n : ℕ => (((∫ ω, f n ω ∂μ) / n : ℝ) : EReal)) atTop (𝓝 C) ∧
    32 ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (f n ω / n : EReal)) atTop (𝓝 C)
    33
    34end Lax606786.KingmanTheorem
    35
    Show Proof
    Builds on
    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…