Subadditive cocycles: Fekete's lemma and the EReal envelope setup #
The definition of a subadditive cocycle and the first layer of Kingman's subadditive ergodic
theorem: Fekete's lemma giving the limit γ of the normalized integrals, the EReal-valued
limsup/liminf envelopes of the normalized cocycle, their a.e. measurability and boundedness,
and the Fatou step bounding the limsup envelope and the integrability of its positive part.
The public statement of the theorem lives in Oseledets.Ergodic.Kingman.Core; the intermediate
constructions are internal infrastructure and live in the Oseledets.Kingman namespace.
Main definitions #
Oseledets.IsSubadditiveCocycle— a sequenceg : ℕ → X → ℝwithg (m + n) x ≤ g m x + g n (T^[m] x).
A sequence g : ℕ → X → ℝ is a subadditive cocycle over T when
g (m + n) x ≤ g m x + g n (T^[m] x) for all m, n, x. (For gₙ = log‖A⁽ⁿ⁾‖ this
follows from submultiplicativity of the operator norm and the cocycle identity.)
Instances For
Singleton partition subadditivity. For n ≥ 1, a subadditive cocycle is
dominated by the Birkhoff sum of its first level: g (n+1) x ≤ birkhoffSum T (g 1) (n+1) x.
(The statement fails at n = 0: subadditivity only forces 0 ≤ g 0 x, not g 0 x ≤ 0.)
Block subadditivity. For a subadditive cocycle and any consecutive block
decomposition of [0, n) into k+1 blocks of lengths ℓ 0, …, ℓ k (with
n = ∑_{i ≤ k} ℓ i), the cocycle is dominated by the sum of the block cocycle values along
the orbit, evaluated at the partial-sum frontiers T^[∑_{j < i} ℓ j] x. (Used by the
Tᴹ-subsequence cocycle algebra; stated for k+1 blocks since the empty decomposition
would force the false g 0 x ≤ 0.)
Reindexing the normalized sequence #
Reindexing. The Kingman sequence (n : ℝ)⁻¹ * g n x converges to L iff the
shifted sequence g (n+1) x / (n+1) converges to L. The n = 0 term of the original
sequence is 0⁻¹ * g 0 x = 0, so dropping it is harmless.
Integral of a measure-preserving composition #
The integral of a measure-preserving composition equals the integral:
∫ g n (T^[m] x) ∂μ = ∫ g n x ∂μ.
Integral subadditivity. The integral sequence aₙ = ∫ gₙ is subadditive
in Mathlib's sense (a (m+n) ≤ a m + a n), the Fekete input.
Fekete: the limit γ of the normalized integrals #
Fekete. The normalized integral sequence (∫ g (n+1)) / (n+1) converges to
the Fekete constant γ := (integral_subadditive …).lim. The n+1-indexed bounded-below
hypothesis is bridged to the n-indexed Fekete input by hand (the n = 0 term is
(∫ g 0)/0 = 0).
A.e. T-invariance from monotonicity under T #
Invariance from F ≤ F ∘ T. If F is a.e. measurable, T is
measure-preserving on a finite measure, and F x ≤ F (T x) for a.e. x, then
F ∘ T =ᵐ[μ] F. The upper level sets {c ≤ F} satisfy {c ≤ F} ⊆ᵐ T⁻¹ {c ≤ F} with
equal (finite) measure, hence agree a.e.; ranging over rational c gives invariance.
Notation for the normalized cocycle and its envelopes #
cdiv g n x := g (n+1) x / (n+1) is the normalized sequence whose limit Kingman's theorem
identifies; f₊ = limsup, f₋ = liminf.
cdiv g n x is dominated by the Birkhoff average of g 1: an immediate rephrasing of
le_birkhoffSum_one.
A.e. measurability of the limsup/liminf envelopes #
The pointwise limsup of cdiv g · x is a.e. measurable: it agrees a.e.
with the limsup of measurable representatives of each level g (n+1).
The pointwise liminf of cdiv g · x is a.e. measurable.
Boundedness of the normalized cocycle #
A.e., the range of cdiv g · x is bounded above (immediate from le_birkhoffSum_one and
a.e. boundedness of
the Birkhoff averages of g 1). The bounded-below direction is the subtle one: subadditivity
gives only upper bounds, so a.e. finiteness of the liminf holds only once a.e. convergence is
known. Accordingly it is derived from the core lemma ae_tendsto_cdiv (a convergent sequence
is bounded), defined below.
A.e. the range of cdiv g · x is bounded above (le_birkhoffSum_one +
ae_bddAbove_birkhoffAverage).
EReal envelopes (avoiding the ℝ junk value at −∞) #
The normalized cocycle may a priori tend to −∞ on a positive-measure set, where the
ℝ-valued Filter.liminf/limsup return the junk value 0. To control the relevant
extrema before finiteness is established we coerce the sequence into EReal, a
CompleteLinearOrder where Filter.limsup/liminf are total and liminf ≤ limsup is
unconditional. The two facts produced here — limsup < ⊤ (envelope, from
le_birkhoffSum_one and Birkhoff convergence) and
limsup > ⊥ (Fatou) — together with the hard limsup ≤ liminf (ae_ereal_limsup_le_liminf)
pin the EReal limsup/liminf to a common finite value, from which the ℝ convergence
follows.
The EReal-coerced normalized cocycle.
Equations
- Oseledets.Kingman.ecdiv g n x = ↑(Oseledets.Kingman.cdiv g n x)
Instances For
Envelope. A.e. the EReal limsup of the normalized cocycle is bounded above by the
(finite) conditional expectation μ[g 1 | invariants T], hence is < ⊤. From
cdiv_le_birkhoffAverage and the Birkhoff convergence birkhoffAverage g₁ (n+1) → μ[g₁|I].
The Fatou step: finiteness of the limsup and integrability of f₊ #
The normalized cocycle satisfies cdiv g n x ≤ birkhoffAverage ℝ T (g 1) (n+1) x
(le_birkhoffSum_one), so the
nonnegative defect d n x := birkhoffAverage ℝ T (g 1) (n+1) x − cdiv g n x ≥ 0 controls how
far cdiv can drop. A single ℝ≥0∞ Fatou pass (lintegral_liminf_le) on ENNReal.ofReal (d n)
shows liminf_n (d n x) < ∞ a.e., which (since the Birkhoff average converges) is exactly
limsup_n (cdiv g n x) > −∞ a.e. (i.e. ⊥ < EReal limsup), and also yields that the limsup
envelope f₊ is integrable.
The nonnegative Fatou defect birkhoffAverage ℝ T (g 1) (n+1) x − cdiv g n x ≥ 0.
Equations
- Oseledets.Kingman.fdefect g n x = birkhoffAverage ℝ T (g 1) (n + 1) x - Oseledets.Kingman.cdiv g n x
Instances For
The Fatou defect is nonnegative, by cdiv_le_birkhoffAverage.
The integral of birkhoffAverage ℝ T (g 1) (n+1) is ∫ g 1: the Birkhoff average is an
average of measure-preserving compositions of g 1, each with integral ∫ g 1.
cdiv g n is integrable (g (n+1) divided by a constant).
birkhoffAverage ℝ T (g 1) (n+1) is integrable.
The Fatou defect d n is integrable.
The integral of the Fatou defect: ∫ d n = ∫ g 1 − a_{n+1}/(n+1).
Fatou core. A.e. the ℝ≥0∞-liminf of ENNReal.ofReal (d n x) is finite. From this
finiteness both ⊥ < limsup (ecdiv) and Integrable f₊ follow.
A.e. measurability of the ℝ≥0∞-liminf of the Fatou defect (for ae_lt_top').
Fatou step, pointwise. A.e. the ℝ≥0∞-liminf of the Fatou defect is finite.
A.e. the EReal limsup of the normalized cocycle is bounded below by
⊥: the Fatou defect cannot tend to +∞, so the cocycle cannot tend to −∞.
The ℝ-valued limsup envelope f₊ is integrable, by the Fatou step.
Set B := μ[g 1 | invariants T] (integrable) and Δ := B − f₊. Then a.e. 0 ≤ Δ (the
envelope f₊ ≤ B) and Δ ≤ liminf_n (d n) =: D (by le_liminf_add applied to
A_{n+1} + (−cdiv), using only that cdiv is bounded above). Since d n ≥ 0,
ENNReal.ofReal D = liminf_n (ENNReal.ofReal (d n)) (Monotone.map_liminf_of_continuousAt),
so ∫⁻ ofReal Δ ≤ ∫⁻ liminf (ofReal d_n) < ∞ (the Fatou core
ae_liminf_ofReal_fdefect_lt_top). Hence Δ is integrable and f₊ = B − Δ is integrable.
This is a direct Fatou proof, independent of ae_tendsto_cdiv (no circularity), and — crucially
— it never assumes cdiv is bounded below (which only follows after the stopping-time lemma).