The M-block subsequence squeeze and additive assembly

The M-block subsequence squeeze of the EReal limsup/liminf envelopes and the additive assembly via the T^[M]-Birkhoff average, combining the non-positive companion estimates back into a statement about the original cocycle.

Internal infrastructure for Kingman's theorem (the Oseledets.Kingman namespace); the public statement is in Oseledets.Ergodic.Kingman.Core.

The M-block subsequence squeeze

For a non-positive subadditive cocycle and M ≥ 1, the full EReal limsup/liminf of the normalized cocycle equal the limsup/liminf along the M-subsequence k ↦ g (k*M) x / (k*M). The hard direction (full ≤ subseq) combines the pointwise block_sandwich with the c ≤ 1 ratio squeeze (ereal_ratio_le_limsup/_liminf); the easy direction is Tendsto.limsup_comp_le_limsup along Tendsto (·*M) atTop atTop.

noncomputable def Oseledets.Kingman.usub {X : Type u_1} (g : ℕ → X → ℝ) (x : X) (j : ℕ) : EReal

The raw normalized cocycle ↑(g j x / j) (with g 0 x / 0 = 0), indexed so that ecdiv g n x = usub g x (n+1).

Equations

• Oseledets.Kingman.usub g x j = ↑(g j x / ↑j)

theorem Oseledets.Kingman.ecdiv_eq_usub_succ {X : Type u_1} (g : ℕ → X → ℝ) (x : X) : (fun (n : ℕ) => ecdiv g n x) = fun (n : ℕ) => usub g x (n + 1)

(fun n => ecdiv g n x) = fun n => usub g x (n+1).

theorem Oseledets.Kingman.limsup_ecdiv_eq_usub {X : Type u_1} (g : ℕ → X → ℝ) (x : X) : Filter.limsup (fun (n : ℕ) => ecdiv g n x) Filter.atTop = Filter.limsup (fun (j : ℕ) => usub g x j) Filter.atTop

limsup_n (ecdiv g n x) = limsup_j (usub g x j).

theorem Oseledets.Kingman.liminf_ecdiv_eq_usub {X : Type u_1} (g : ℕ → X → ℝ) (x : X) : Filter.liminf (fun (n : ℕ) => ecdiv g n x) Filter.atTop = Filter.liminf (fun (j : ℕ) => usub g x j) Filter.atTop

liminf_n (ecdiv g n x) = liminf_j (usub g x j).

theorem Oseledets.Kingman.tendsto_mul_const_atTop_nat {M : ℕ} (hM : 1 ≤ M) : Filter.Tendsto (fun (k : ℕ) => k * M) Filter.atTop Filter.atTop

Tendsto (·*M) atTop atTop for M ≥ 1.

theorem Oseledets.Kingman.tendsto_div_const_atTop_nat {M : ℕ} (hM : 1 ≤ M) : Filter.Tendsto (fun (j : ℕ) => j / M) Filter.atTop Filter.atTop

Tendsto (·/M) atTop atTop for M ≥ 1.

theorem Oseledets.Kingman.lt_div_add_one_mul {M : ℕ} (hM : 1 ≤ M) (j : ℕ) : j < (j / M + 1) * M

Strict block upper bound: j < (j/M + 1) * M for M ≥ 1.

theorem Oseledets.Kingman.limsup_ecdiv_eq_block {X : Type u_1} {T : X → X} {g : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T g) (hnonpos : ∀ (n : ℕ) (x : X), g (n + 1) x ≤ 0) {M : ℕ} (hM : 1 ≤ M) (x : X) : Filter.limsup (fun (n : ℕ) => ecdiv g n x) Filter.atTop = Filter.limsup (fun (k : ℕ) => usub g x (k * M)) Filter.atTop

Block subsequence squeeze (limsup). For M ≥ 1, the full limsup of ecdiv g equals the limsup along the M-block subsequence k ↦ usub g x (k*M).

theorem Oseledets.Kingman.liminf_ecdiv_eq_block {X : Type u_1} {T : X → X} {g : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T g) (hnonpos : ∀ (n : ℕ) (x : X), g (n + 1) x ≤ 0) {M : ℕ} (hM : 1 ≤ M) (x : X) : Filter.liminf (fun (n : ℕ) => ecdiv g n x) Filter.atTop = Filter.liminf (fun (k : ℕ) => usub g x (k * M)) Filter.atTop

Block subsequence squeeze (liminf). For M ≥ 1, the full liminf of ecdiv g equals the liminf along the M-block subsequence k ↦ usub g x (k*M).

Additive assembly via the T^[M]-Birkhoff average

The M-block subsequence value decomposes pointwise (for n ≥ 1) as g (n*M) x / (n*M) = (1/M)·(vM g M n x / n) + (1/M)·birkhoffAverage (T^[M]) (g M) n x, where the Birkhoff average converges a.e. to the finite μ[g M | invariants (T^[M])] x. Feeding this into the EReal additive/scaling laws gives the envelopes of the block subsequence as (1/M)·(envelope of usub (vM g M)) + ↑((1/M)·c x).

theorem Oseledets.Kingman.block_decomp {X : Type u_1} {T : X → X} {g : ℕ → X → ℝ} {M : ℕ} (hM : 1 ≤ M) (n : ℕ) (hn : 1 ≤ n) (x : X) : g (n * M) x / ↑(n * M) = 1 / ↑M * (vM g M n x / ↑n) + 1 / ↑M * birkhoffAverage ℝ T^[M] (g M) n x

The block decomposition identity (pointwise, n ≥ 1): g (n*M) x / (n*M) = (1/M)·(vM g M n x / n) + (1/M)·birkhoffAverage (T^[M]) (g M) n x.

theorem Oseledets.Kingman.usub_vM {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (M : ℕ) (x : X) (n : ℕ) : usub (vM g M) x n = ↑(vM g M n x / ↑n)

usub (vM g M) x n = vM g M n x / n (the normalized companion subsequence).

theorem Oseledets.Kingman.limsup_block_eq {X : Type u_1} {T : X → X} {g : ℕ → X → ℝ} {M : ℕ} (hM : 1 ≤ M) (x : X) {c : ℝ} (hc : Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ T^[M] (g M) n x) Filter.atTop (nhds c)) : Filter.limsup (fun (k : ℕ) => usub g x (k * M)) Filter.atTop = ↑(1 / ↑M) * Filter.limsup (fun (n : ℕ) => usub (vM g M) x n) Filter.atTop + ↑(1 / ↑M * c)

Block-envelope assembly (limsup). A.e. (where the T^[M]-Birkhoff average of g M converges to c x), limsup_k (usub g x (k*M)) = ↑(1/M)·limsup_n (usub (vM g M) x n) + ↑((1/M)·c x).

theorem Oseledets.Kingman.liminf_block_eq {X : Type u_1} {T : X → X} {g : ℕ → X → ℝ} {M : ℕ} (hM : 1 ≤ M) (x : X) {c : ℝ} (hc : Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ T^[M] (g M) n x) Filter.atTop (nhds c)) : Filter.liminf (fun (k : ℕ) => usub g x (k * M)) Filter.atTop = ↑(1 / ↑M) * Filter.liminf (fun (n : ℕ) => usub (vM g M) x n) Filter.atTop + ↑(1 / ↑M * c)

Block-envelope assembly (liminf). A.e., liminf_k (usub g x (k*M)) = ↑(1/M)·liminf_n (usub (vM g M) x n) + ↑((1/M)·c x).

theorem Oseledets.Kingman.ereal_gap_to_liminf {r c α : ℝ} (hr : 0 < r) (_hα : 0 < α) {Lm Lp : EReal} (hLp : Lp ≤ 0) (h : ↑r * Lm + ↑c + ↑α < ↑r * Lp + ↑c) : Lm < ↑(-α / r)

Gap algebra. From the block-envelope identities, the strict gap on E forces the companion liminf strictly below ↑(−M·α). For r > 0, finite c, α > 0, and Lp ≤ 0, if ↑r·Lm + ↑c + ↑α < ↑r·Lp + ↑c then Lm < ↑(−α/r).

theorem Oseledets.Kingman.measure_gap_set_eq_zero {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) (_hTm : Measurable T) {g : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T g) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (hnonpos : ∀ (n : ℕ) (x : X), g (n + 1) x ≤ 0) {Λ : ℝ} (hΛ : Filter.Tendsto (fun (n : ℕ) => (∫ (x : X), g (n + 1) x ∂μ) / (↑n + 1)) Filter.atTop (nhds Λ)) {α : ℝ} (hα : 0 < α) : μ {x : X | Filter.liminf (fun (n : ℕ) => ecdiv g n x) Filter.atTop + ↑α < Filter.limsup (fun (n : ℕ) => ecdiv g n x) Filter.atTop} = 0

The E_α contradiction (Karlsson §3.3). For a non-positive subadditive cocycle and any α > 0, the gap set Bα := {x | liminf (ecdiv g · x) + ↑α < limsup (ecdiv g · x)} is null. The argument:

• Extract a genuinely T-invariant measurable E =ᵐ Bα (both envelopes are a.e. T-invariant, liminf_ecdiv_comp_ae / limsup_ecdiv_comp_ae); then (T^[M])⁻¹ E = E for every M.
• Fix ε > 0; pick M ≥ 1 with (∫ g M)/M ≤ Λ + ε (Fekete). On E, the block squeeze (limsup_ecdiv_eq_block / liminf_ecdiv_eq_block) and the assembly (limsup_block_eq / liminf_block_eq) reduce the g-gap to the companion usub (vM g M) envelopes; the strict gap and limsup (usub (vM g M)) ≤ 0 force liminf_n (vM g M n x / n) < ↑(−M·α) (ereal_gap_to_liminf), hence ∃ k, vM g M (k+1) x < (k+1)·(−M·α) (the hBneg input).
• setIntegral_div_le_level over T^[M] gives limsup_n ↑((∫_E vM g M (n+1))/(n+1)) ≤ ↑((−Mα)·(μ E).toReal), while the X-integral ratio (∫_X vM g M (n+1))/(n+1) → M·Λ − ∫ g M ≥ −Mε and vM ≤ 0 (so ∫_E ≥ ∫_X) give the matching lower bound ↑(−Mε). Hence α·(μ E).toReal ≤ ε; letting ε → 0 forces μ E = 0 = μ Bα.

theorem Oseledets.Kingman.ae_ereal_limsup_le_liminf_nonpos {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) (hTm : Measurable T) {g : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T g) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (hnonpos : ∀ (n : ℕ) (x : X), g (n + 1) x ≤ 0) (hbdd : BddBelow (Set.range fun (n : ℕ) => (∫ (x : X), g (n + 1) x ∂μ) / (↑n + 1))) : ∀ᵐ (x : X) ∂μ, Filter.liminf (fun (n : ℕ) => ecdiv g n x) Filter.atTop = Filter.limsup (fun (n : ℕ) => ecdiv g n x) Filter.atTop

Stopping-time direction (the hard core of Kingman), non-positive case. A.e. the EReal liminf of the normalized non-positive subadditive cocycle equals its EReal limsup.

The unconditional liminf ≤ limsup reduces this to μ {liminf < limsup} = 0, and that bad set is the countable union over ℚ⁺ of the gap sets Bα, each null by measure_gap_set_eq_zero (Karlsson §3.3, the E_α contradiction).

theorem Oseledets.Kingman.ae_ereal_limsup_le_liminf {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) (hTm : Measurable 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))) : ∀ᵐ (x : X) ∂μ, Filter.liminf (fun (n : ℕ) => ecdiv g n x) Filter.atTop = Filter.limsup (fun (n : ℕ) => ecdiv g n x) Filter.atTop

Stopping-time direction (the hard core of Kingman). A.e. the EReal liminf of the normalized cocycle equals its EReal limsup, proved by the Riesz/Derriennic "leaders" route (Karlsson, A proof of the subadditive ergodic theorem).

Reduced here to the non-positive case ae_ereal_limsup_le_liminf_nonpos applied to the companion vcoc g (vcoc_subadditive, vcoc_nonpos, vcoc_integrable, vcoc_bddBelow): the normalized gap ecdiv g − ecdiv (vcoc g) = ↑(birkhoffAverage (g 1) (·+1)) converges a.e. (Birkhoff) to the finite μ[g 1 | invariants T], and adding an a.e.-convergent finite-valued real sequence preserves the liminf/limsup (both become e + ↑(limit)).

Ingredients:

• sum_leaders_nonpos — Riesz's combinatorial leader lemma (Karlsson Lemma 3.2).
• sum_leaders_cocycle_nonpos / sum_psiCoc_comp_nonpos — pointwise leader inequality.
• limsup_setIntegral_div_nonpos — Derriennic's maximal inequality (Karlsson Lemma 3.4).