Lax Lean Archive

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

Kingman's theorem for balanced intervals

Lax606786.BalancedKingman · concepts/Lax606786/BalancedKingman.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 invertible ergodic measure-preserving transformation of a Lebesgue probability space (Ω,μ)(\Omega, \mu) (a standard Borel space with a probability measure giving points measure zero), and let (fn)(f_n) be a subadditive family of integrable functions over σ\sigma. Then the averages over the balanced time intervals [−n,n)[-n, n) converge to the same constant as in Kingman's theorem:

    12nf2n(σ−nω)→C=lim⁡n→∞1n∫fn dμfor μ-a.e. ω,\tfrac{1}{2n} f_{2n}(\sigma^{-n}\omega) \to C = \lim_{n \to \infty} \tfrac1n \int f_n \, d\mu \quad \text{for } \mu\text{-a.e. } \omega,

    with C∈[−∞,∞)C \in [-\infty, \infty) and limits taken in the extended reals. This is the balanced subadditive ergodic theorem of Lee (2024).

    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 7 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.MeasureTheory.Measure.Typeclasses.NoAtoms
    5import Mathlib.MeasureTheory.Constructions.Polish.Basic
    6import Mathlib.Data.EReal.Operations
    7
    8/-!
    9---
    10title: Kingman's theorem for balanced intervals
    11type: theorem
    12---
    13Let σ\sigma be an invertible ergodic measure-preserving transformation of a Lebesgue
    14probability space (Ω,μ)(\Omega, \mu) (a standard Borel space with a probability measure giving
    15points measure zero), and let (fn)(f_n) be a subadditive family of integrable functions over
    16σ\sigma. Then the averages over the balanced time intervals [−n,n)[-n, n) converge to the same
    17constant as in Kingman's theorem:
    1812nf2n(σ−nω)→C=lim⁡n→∞1n∫fn dμfor μ-a.e. ω,\tfrac{1}{2n} f_{2n}(\sigma^{-n}\omega) \to C = \lim_{n \to \infty} \tfrac1n \int f_n \, d\mu \quad \text{for } \mu\text{-a.e. } \omega,
    19
    20with C∈[−∞,∞)C \in [-\infty, \infty) and limits taken in the extended reals. This is the balanced
    21subadditive ergodic theorem of Lee (2024).
    22-/
    23
    24namespace Lax606786.BalancedKingman
    25
    26open MeasureTheory Filter Topology
    27open Lax606786.SubadditiveFamilies
    28
    29/-- `f_{2n}(σ^{-n} ω) / 2n` converges almost everywhere to `C = lim (1/n) ∫ f_n`. -/
    30axiom balancedKingman {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    31 (μ : Measure Ω) [IsProbabilityMeasure μ] [NullSingletonClass μ]
    32 (σ : Ω ≃ᵐ Ω) (hσ : Ergodic σ μ) (f : ℕ → Ω → ℝ) (hf : IsSubadditiveFamily σ f)
    33 (hint : ∀ n, Integrable (f n) μ) :
    34 ∃ C : EReal, C ≠ ⊤ ∧
    35 Tendsto (fun n : ℕ => (((∫ ω, f n ω ∂μ) / n : ℝ) : EReal)) atTop (𝓝 C) ∧
    36 ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (f (2 * n) ((σ.symm : Ω → Ω)^[n] ω) / (2 * n) : EReal))
    37 atTop (𝓝 C)
    38
    39end Lax606786.BalancedKingman
    40
    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…