Kingman's subadditive ergodic theorem #
The core a.e.-existence of an integrable limit, the a.e. T-invariance and integrability of the
envelopes, the hard direction limsup ≤ liminf a.e., and the final assembly of Kingman's
subadditive ergodic theorem: for a measure-preserving T and an integrable subadditive cocycle
whose normalized integrals are bounded below, gₙ / n converges μ-a.e. to a T-invariant
integrable limit; under ergodicity the limit is a.e. constant.
The supporting constructions live in the Oseledets.Kingman namespace across the sibling files
Fekete, Derriennic, Companion, BlockSqueeze.
Main statements #
Oseledets.tendsto_kingman— a.e. convergence to aT-invariant integrable limit.Oseledets.tendsto_kingman_ergodic— the ergodic case: an a.e.-constant limit.
References #
- J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30 (1968), 499–510.
- Y. Katznelson, B. Weiss, A simple proof of some ergodic theorems, Israel J. Math. 42 (1982), 291–296.
The Kingman core: a.e. existence of an integrable limit #
Kingman core. The normalized cocycle g (n+1) x / (n+1)
converges, for μ-a.e. x, to the value G x of some integrable G. This packages the
entire analytic content of Kingman's theorem that is not generic measure theory:
- a.e. convergence (the stopping-time / greedy block partition, Katznelson–Weiss); and
- integrability of the limit (the Fatou step).
Everything else in this file — a.e. boundedness (ae_bddBelow_cdiv), limsup ≤ liminf
(ae_limsup_le_liminf_div), integrability of the envelope (int_limsup_div_integrable),
T-invariance, and the ergodic collapse — is derived from this one lemma by soft arguments.
The proof works with the EReal-valued limsup/liminf to avoid the ℝ junk value at
−∞: the ℝ≥0∞ Fatou step (ae_bot_lt_ereal_limsup, int_limsup_div_integrable_aux)
gives limsup > ⊥ a.e. and the integrability; the stopping-time lemma
ae_ereal_limsup_le_liminf gives liminf = limsup; together with the envelope
limsup ≤ ↑B < ⊤ they force a finite a.e. limit e.toReal.
A.e. the range of cdiv g · x is bounded below: a convergent sequence is bounded
(derived from ae_tendsto_cdiv).
A.e. T-invariance of the limsup/liminf envelopes #
Key limsup comparison. For a fixed x at which the normalized cocycle is bounded
(at x and at T x), limsup (cdiv g · x) ≤ limsup (cdiv g · (T x)). Combines the
subadditivity bound with the vanishing-perturbation lemma limsup_eq_of_sub_tendsto_zero.
The envelope f₊ x = limsup_n cdiv g n x is a.e. T-invariant.
The pointwise inequality f₊ x ≤ f₊ (T x) (limsup_cdiv_le_comp) feeds the level-set
invariance argument ae_eq_comp_of_le_comp.
Depends on ae_bddBelow_cdiv (a.e. boundedness below of the normalized cocycle) for the
cobounded side-conditions, which is the single boundedness fact entangled with the hard
direction ae_limsup_le_liminf_div.
liminf vanishing-perturbation. If two bounded real sequences differ by a sequence
tending to 0, their liminfs coincide. Mirrors limsup_eq_of_sub_tendsto_zero with the
order reversed, using liminf_add_const.
Liminf comparison. Mirror of limsup_cdiv_le_comp for the liminf envelope:
for a fixed x at which the normalized cocycle is bounded (at x and at T x),
liminf (cdiv g · x) ≤ liminf (cdiv g · (T x)).
The envelope f₋ x = liminf_n cdiv g n x is a.e. T-invariant. Mirrors
limsup_div_comp_ae, using liminf_cdiv_le_comp and ae_eq_comp_of_le_comp.
Integrability of the limsup envelope #
Integrable f₊. The limsup envelope f₊ x = limsup_n cdiv g n x is integrable:
on the a.e. set where cdiv g · x converges to G x (ae_tendsto_cdiv), the limsup equals
G x, and G is integrable.
The hard direction: limsup ≤ liminf almost everywhere #
limsup ≤ liminf a.e. For a.e. x the limsup of the normalized cocycle is dominated
by its liminf. Derived from ae_tendsto_cdiv: where the sequence converges, both equal the
limit. (The deep content is in ae_tendsto_cdiv; this is a soft corollary.)
Assembly #
Kingman's subadditive ergodic theorem. For a measure-preserving T and
an integrable subadditive cocycle g whose normalized integrals are bounded below,
gₙ / n converges μ-a.e. to a T-invariant integrable limit G.
Kingman, ergodic case: under ergodicity the a.e. limit is a single constant.
(That constant is the Fekete infimum ⨅ n, (∫ g_{n+1})/(n+1); the statement here asserts
only a.e.-constancy, which is what the multiplicative ergodic theorem consumes.)