Reduction to the non-positive companion cocycle #
Karlsson's §3.3 reduction running the argument on the non-positive companion cocycle: the
T^[M]-subsequence cocycle algebra and the EReal-envelope T-invariance in the non-positive
case.
Internal infrastructure for Kingman's theorem (the Oseledets.Kingman namespace); the public
statement is in Oseledets.Ergodic.Kingman.Core.
Reduction to the non-positive companion cocycle #
Karlsson's §3.3 argument is run on the non-positive companion
vcoc g n := g n − birkhoffSum T (g 1) n. Since birkhoffSum (g 1) is an additive cocycle,
vcoc g is again subadditive, and le_birkhoffSum_one gives vcoc g (n+1) ≤ 0.
The normalized gap is unchanged: cdiv g − cdiv (vcoc g) = birkhoffAverage (g 1) (·+1), which
converges a.e. (Birkhoff) to the finite μ[g 1 | invariants T], so liminf = limsup for
ecdiv g
follows from the same statement for ecdiv (vcoc g).
The non-positive companion cocycle vcoc g n x := g n x − birkhoffSum T (g 1) n x.
Equations
- Oseledets.Kingman.vcoc g n x = g n x - birkhoffSum T (g 1) n x
Instances For
vcoc g is a subadditive cocycle: subtracting the additive cocycle birkhoffSum (g 1)
from the subadditive g preserves subadditivity.
Each level of vcoc g is integrable (a difference of integrable g n and birkhoffSum).
The integral of vcoc g (n+1) is (∫ g (n+1)) − (n+1)·(∫ g 1): the additive cocycle
birkhoffSum (g 1) integrates to (n+1)·∫ g 1 by measure preservation.
The normalized integrals of vcoc g are bounded below: (∫ vcoc(n+1))/(n+1) = (∫ g(n+1))/(n+1) − ∫ g 1, a shift of the bounded-below sequence hbdd.
Gap-transfer identity. Pointwise in EReal, the normalized g-cocycle is the
normalized companion plus the Birkhoff average of g 1:
ecdiv g n x = ecdiv (vcoc g) n x + ↑(birkhoffAverage ℝ T (g 1) (n+1) x).
The Tᴹ-subsequence cocycle algebra #
For a non-positive subadditive cocycle g over T and a block length M, the
Tᴹ-subsequence cocycle vM g M n x := g (n*M) x − ∑_{i<n} g M (T^[i*M] x) is a non-positive
subadditive cocycle for T^[M]. This is a pure-algebra layer; no measure theory is used.
vM g M is a subadditive cocycle for T^[M]. Block subadditivity of g over the split
(n+p)·M = n·M + p·M gives the g-term bound; the sum splits as range (n+p) = range n ∪ tail,
and reindexing the tail i = n+j lines up T^[i*M] = (T^[M])^[n] (T^[j*M]).
vM g M n ≤ 0 for n ≥ 1 when g is non-positive subadditive: block subadditivity
(le_sum_blocks with all n blocks equal to M) gives g (n*M) ≤ ∑_{i<n} g M (T^[i*M]).
Each level vM g M n is integrable for measure-preserving T (a finite difference of
integrable terms; each g M (T^[i*M] ·) is integrable since T^[i*M] is measure-preserving).
T^[M] is measure-preserving for measure-preserving T (stated for downstream use).
The integral of vM g M n is (∫ g (n*M)) − n·(∫ g M): the orbit-sum integrates to
n·∫ g M by measure preservation.
Block sandwich (non-positive case). For a non-positive subadditive cocycle and a block
length M, when k*M ≤ m ≤ (k+1)*M the cocycle value g m x is sandwiched:
g ((k+1)*M) x ≤ g m x ≤ g (k*M) x. (Upper bound: g m = g (kM + (m−kM)) ≤ g (kM) + g (m−kM)(…) ≤ g (kM) since g (m−kM) ≤ 0; the offset 0 case is equality. Lower bound symmetric using
(k+1)M = m + ((k+1)M − m).)
EReal-envelope T-invariance (non-positive case) #
The ℝ-valued envelope invariance (liminf_div_comp_ae) requires the normalized cocycle to be
bounded below a.e. — a fact available only after ae_tendsto_cdiv. For the non-positive case
we need the envelope invariance before convergence, so we work directly in EReal, where the
liminf/limsup are total and no boundedness is needed.
EReal liminf of a finite shift. Liminf analogue of ereal_limsup_add_coe.
EReal perturbation (liminf), one-sided. If a n − b n → 0 then
liminf ↑b ≤ liminf ↑a in EReal. Via EReal.le_liminf_add with the vanishing perturbation
↑(a − b), whose liminf is 0. No boundedness is required (EReal is a complete lattice).
EReal perturbation (liminf). If two real sequences differ by a sequence tending to 0,
their EReal-coerced liminfs coincide.
EReal perturbation (limsup). If two real sequences differ by a sequence tending to 0,
their EReal-coerced limsups coincide. Via limsup_neg and ereal_liminf_eq_of_sub_tendsto_zero
on the negated sequences.
EReal ratio squeeze (liminf), one-sided. If z n ≤ 0, c n → 1, 1 ≤ c n, then the
nonpositive EReal-coerced products ↑(c n · z n) (which are ≤ ↑(z n)) have liminf no smaller
than that of ↑z: liminf ↑z ≤ liminf ↑(c · z). (The reverse is monotonicity.) For each ε > 0,
eventually (1+ε)·z n ≤ c n · z n (as z ≤ 0), and
liminf ↑((1+ε)·z) = (1+ε)·liminf ↑z → liminf ↑z
as ε → 0; the EReal scalar law EReal.liminf_const_mul_of_nonneg_of_ne_top handles the −∞
case uniformly.
EReal ratio squeeze (limsup), one-sided. Dual of ereal_liminf_le_ratio:
limsup ↑z ≤ limsup ↑(c · z) when z n ≤ 0, c n → 1, 1 ≤ c n.
EReal ratio squeeze (limsup), c ≤ 1 companion. If z n ≤ 0, 0 ≤ c n ≤ 1, c n → 1,
then limsup ↑(c · z) ≤ limsup ↑z. (The reverse is monotonicity, since c ≤ 1, z ≤ 0 ⟹ z ≤ c·z.)
For each ε ∈ (0,1), eventually 1 − ε ≤ c n, so c n · z n ≤ (1−ε)·z n (as z ≤ 0), and
limsup ↑((1−ε)·z) = (1−ε)·limsup ↑z → limsup ↑z as ε → 0.
EReal ratio squeeze (liminf), c ≤ 1 companion. Dual of ereal_ratio_le_limsup:
liminf ↑(c · z) ≤ liminf ↑z when z n ≤ 0, 0 ≤ c n ≤ 1, c n → 1.
EReal limsup with a convergent real shift. If s n → σ then
limsup ↑(b n + s n) = limsup ↑(b n) + ↑σ.
EReal liminf with a convergent real shift. If s n → σ then
liminf ↑(b n + s n) = liminf ↑(b n) + ↑σ.
EReal limsup under positive real scaling. For 0 ≤ r,
limsup ↑(r * b n) = ↑r * limsup ↑(b n).
EReal liminf under positive real scaling. For 0 ≤ r,
liminf ↑(r * b n) = ↑r * liminf ↑(b n).
The EReal liminf envelope x ↦ liminf (ecdiv g · x) is a.e. measurable: it agrees a.e.
with the EReal liminf of measurable representatives of each level.
The EReal limsup envelope x ↦ limsup (ecdiv g · x) is a.e. measurable.
The shift-and-ratio lower bound on the cocycle at T x (non-positive case): for every k,
cdiv g k (T x) ≥ c k · z k − g 1 x/(k+1), where z k := cdiv g (k+1) x ≤ 0 and
c k := (k+2)/(k+1) ≥ 1. From g (k+2) x ≤ g 1 x + g (k+1) (T x) (subadditivity, first block of
length 1), so g (k+1) (T x) ≥ g (k+2) x − g 1 x; dividing by k+1 and rewriting
g (k+2) x/(k+1) = (k+2)/(k+1) · cdiv g (k+1) x.
The ratio sequence c k := (k+2)/(k+1) is ≥ 1 and tends to 1.
EReal liminf comparison (non-positive case). For every x,
liminf (ecdiv g · x) ≤ liminf (ecdiv g · (T x)). From the shift-and-ratio lower bound
cdiv_comp_ge_ratio, the ratio squeeze ereal_liminf_le_ratio (using cdiv g (k+1) x ≤ 0), the
vanishing perturbation g 1 x/(k+1) → 0, and the index shift liminf (cdiv g · x) = liminf (cdiv g (·+1) x).
EReal limsup comparison (non-positive case). For every x,
limsup (ecdiv g · x) ≤ limsup (ecdiv g · (T x)). Same route as ereal_liminf_le_comp with
ereal_limsup_le_ratio and ereal_limsup_eq_of_sub_tendsto_zero.
EReal version of ae_eq_comp_of_le_comp. For an a.e.-measurable EReal-valued F
with F x ≤ F (T x) a.e., F ∘ T =ᵐ[μ] F. Verbatim adaptation of the ℝ proof, with rational
levels ↑(c : ℚ) : EReal and EReal.exists_rat_btwn_of_lt for the separation step.
EReal liminf-envelope T-invariance (non-positive case).
(fun x => liminf (ecdiv g · x)) ∘ T =ᵐ[μ] ….
EReal limsup-envelope T-invariance (non-positive case).
(fun x => limsup (ecdiv g · x)) ∘ T =ᵐ[μ] ….