Kingman means identification

For an integrable subadditive cocycle g over an ergodic measure-preserving system, Kingman's theorem (Oseledets.tendsto_kingman_ergodic) provides a constant c to which (n : ℝ)⁻¹ • gₙ converges μ-a.e.; the file Oseledets.Ergodic.Kingman deliberately leaves the value of c unidentified.

This module identifies that constant with the limit of the normalized integral means (∫ g (n+1)) / (n+1), which exists by Fekete's lemma applied to the subadditive sequence n ↦ ∫ gₙ.

Main statements

• Oseledets.tendsto_kingman_ergodic_means: there is a single constant c that is both the limit of the integral means (∫ g (n+1)) / (n+1) and the μ-a.e. limit of the normalized cocycle (n : ℝ)⁻¹ • gₙ.

Implementation notes

The two halves c ≤ L and c ≥ L of the identification c = L := lim (∫ gₙ)/n are proved separately.

• c ≤ L: iterate subadditivity in blocks of length n, dividing by m·n and letting m → ∞. The left-hand side converges along the multiples of n to the a.e. Kingman limit c, while the right-hand side is the T^[n]-Birkhoff average of (1/n) gₙ whose pointwise limit integrates to (1/n) ∫ gₙ. Integrating the pointwise inequality and letting n → ∞ gives c ≤ L.

• c ≥ L: a single Fatou pass on the nonnegative defect birkhoffAverage T (g 1) (n+1) − cdiv g n (nonnegative by singleton subadditivity). Its a.e. limit is the constant ∫ g 1 − c, while its integral tends to ∫ g 1 − L; Fatou yields ∫ g 1 − c ≤ ∫ g 1 − L, i.e. c ≥ L.

Fekete: convergence of the integral means

The lower bound c ≤ L via block subadditivity

The upper bound c ≥ L via Fatou on the nonnegative defect

The means identification

theorem Oseledets.tendsto_kingman_ergodic_means {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {g : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T g) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (hbdd : BddBelow (Set.range fun (n : ℕ) => (∫ (x : X), g (n + 1) x ∂μ) / (↑n + 1))) : ∃ (c : ℝ), Filter.Tendsto (fun (n : ℕ) => (∫ (x : X), g (n + 1) x ∂μ) / (↑n + 1)) Filter.atTop (nhds c) ∧ ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * g n x) Filter.atTop (nhds c)

Kingman means identification. Under the hypotheses of tendsto_kingman_ergodic, there is a single constant c that is both the limit of the integral means (∫ g (n+1)) / (n+1) and the μ-a.e. limit of the normalized cocycle (n : ℝ)⁻¹ • gₙ.