Lax Lean Archive

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

Kingman's theorem along shifted and backward orbits

Lax606786.KingmanVariants · concepts/Lax606786/KingmanVariants.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 (fn)(f_n) a subadditive family over σ\sigma with f1+f_1^+ integrable, and let CC be the constant of Kingman's theorem (the concept KingmanTheoremKingmanTheorem). Then, for μ\mu-a.e. ω\omega,

    1nfn(σnω)→C,\tfrac1n f_n(\sigma^n \omega) \to C,

    and, if σ\sigma is invertible, also 1nfn(σ−nω)→C\tfrac1n f_n(\sigma^{-n}\omega) \to C. Limits are taken in the extended reals. For the shifted averages see Ferrando (1995); both forms are used in Lee (2024, Lemma 22 and Corollary 21).

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

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 kingman_backward proven

    2 kingman_shifted proven

    Lean source view on GitLab

    1import Lax606786.SubadditiveFamilies
    2import Lax606786.LowerIntegrals
    3import Lax606786.KingmanTheorem
    4import Mathlib.Dynamics.Ergodic.Ergodic
    5import Mathlib.MeasureTheory.Function.L1Space.Integrable
    6
    7/-!
    8---
    9title: Kingman's theorem along shifted and backward orbits
    10type: theorem
    11---
    12Let σ\sigma be an ergodic measure-preserving transformation of a probability space
    13(Ω,μ)(\Omega, \mu) and (fn)(f_n) a subadditive family over σ\sigma with f1+f_1^+ integrable, and let
    14CC be the constant of Kingman's theorem (the concept `KingmanTheorem`). Then, for μ\mu-a.e.
    15ω\omega,
    161nfn(σnω)→C,\tfrac1n f_n(\sigma^n \omega) \to C,
    17and, if σ\sigma is invertible, also 1nfn(σ−nω)→C\tfrac1n f_n(\sigma^{-n}\omega) \to C. Limits are taken in
    18the extended reals. For the shifted averages see Ferrando (1995); both forms are used in Lee (2024,
    19Lemma 22 and Corollary 21).
    20-/
    21
    22namespace Lax606786.KingmanVariants
    23
    24open MeasureTheory Filter Topology
    25open Lax606786.SubadditiveFamilies Lax606786.LowerIntegrals
    26
    27variable {Ω : Type*} [MeasurableSpace Ω]
    28
    29/-- Kingman's theorem along the shifted orbit, `f_n(σⁿω)/n → C`. -/
    30axiom kingman_shifted (μ : Measure Ω) [IsProbabilityMeasure μ] (σ : Ω → Ω) (hσ : Ergodic σ μ)
    31 (f : ℕ → Ω → ℝ) (hf : IsSubadditiveFamily σ f)
    32 (h1 : Integrable (fun ω => max (f 1 ω) 0) μ) :
    33 ∃ C : EReal, C < ⊤ ∧
    34 (∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (f n (σ^[n] ω) / n : EReal)) atTop (𝓝 C)) ∧
    35 Tendsto (fun n : ℕ => lowerIntegral μ (fun ω => f n ω / n)) atTop (𝓝 C)
    36
    37/-- Kingman's theorem along the backward orbit, `f_n(σ⁻ⁿω)/n → C`. -/
    38axiom kingman_backward (μ : Measure Ω) [IsProbabilityMeasure μ] (σ : Ω ≃ᵐ Ω)
    39 (hσ : Ergodic σ μ) (f : ℕ → Ω → ℝ) (hf : IsSubadditiveFamily σ f)
    40 (h1 : Integrable (fun ω => max (f 1 ω) 0) μ) :
    41 ∃ C : EReal, C < ⊤ ∧
    42 (∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (f n ((σ.symm : Ω → Ω)^[n] ω) / n : EReal)) atTop (𝓝 C)) ∧
    43 Tendsto (fun n : ℕ => lowerIntegral μ (fun ω => f n ω / n)) atTop (𝓝 C)
    44
    45end Lax606786.KingmanVariants
    46
    Show ProofShow 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…