The Derriennic "leaders" route and the maximal inequality

The Derriennic / Karlsson route towards limsup ≤ liminf almost everywhere: the "leaders" construction and Derriennic's maximal inequality (Karlsson, A proof of the subadditive ergodic theorem, Lemma 3.4 / Prop 3.5).

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

The Derriennic "leaders" route to limsup ≤ liminf a.e.

We follow Karlsson, A proof of the subadditive ergodic theorem (Riesz/Derriennic route). The four ingredients are:

• sum_leaders_nonpos: Riesz's combinatorial "leader" lemma (Karlsson Lemma 3.2), pure finite induction, no measure theory.
• sum_bcoc_telescope: the telescoping identity a n x − a (n−k) (T^[k] x) = ∑ bₙ₋ᵢ(T^[i]x).
• limsup_setIntegral_div_nonpos: Derriennic's maximal inequality (Karlsson Lemma 3.4 / Prop 3.5): for a T-invariant set B on which liminf (aₙ/n) < α, one has limsup (1/n) ∫_B aₙ ≤ α·μ(B).
• the E_{α,β} two-bound contradiction (Karlsson §3.3), mirroring the additive measure_setOf_lt_limsup_eq_zero in Birkhoff.lean.

noncomputable def Oseledets.Kingman.leaderSet (S : ℕ → ℝ) (n : ℕ) : Finset ℕ

The set of leaders of length n for partial sums S.

Equations

• Oseledets.Kingman.leaderSet S n = {u ∈ Finset.range n | ∃ (j : ℕ), u < j ∧ j ≤ n ∧ S j < S u}

theorem Oseledets.Kingman.mem_leaderSet_shift (S : ℕ → ℝ) (s n u : ℕ) (hsn : s ≤ n) : u + s ∈ leaderSet S n ∧ s ≤ u + s ↔ u ∈ leaderSet (fun (j : ℕ) => S (j + s)) (n - s)

A leader u ≥ s of length n (with s ≤ n) is, after shifting indices down by s, a leader of the shifted partial sums S (· + s) of length n − s, and conversely. (The leader condition only inspects partial sums strictly after u, so dropping the prefix [0, s) is harmless.) This is the reindexing engine of the leader-lemma induction.

theorem Oseledets.Kingman.sum_leaders_nonpos (n : ℕ) (S : ℕ → ℝ) : ∑ u ∈ leaderSet S n, (S (u + 1) - S u) ≤ 0

Riesz's leader lemma (Karlsson, Lemma 3.2), in partial-sum form. Given a sequence of partial sums S : ℕ → ℝ (think S j = c 0 + … + c (j−1), S 0 = 0), call an index u < n a leader (of length n) if some later partial sum drops strictly below S u, i.e. ∃ j, u < j ≤ n ∧ S j < S u. (This matches Karlsson's "a forward partial sum c u + … + c (j−1) = S j − S u is negative".) Then the sum of the increments S (u+1) − S u over the leaders is non-positive. Strong induction on n.

theorem Oseledets.Kingman.sum_leaders_cocycle_nonpos {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (n : ℕ) (x : X) : ∑ k ∈ leaderSet (fun (j : ℕ) => g n x - g (n - j) (T^[j] x)) n, (g (n - k) (T^[k] x) - g (n - (k + 1)) (T^[k + 1] x)) ≤ 0

Leader inequality for the cocycle (Karlsson, §3.2, the pointwise input of his Lemma 3.4). Fix x and length n, and consider the partial sums S j := g n x − g (n−j) (T^[j] x) (so S 0 = 0, and the increment S (k+1) − S k equals g (n−k) (T^[k] x) − g (n−k−1) (T^[k+1] x)). With these partial sums an index k is a leader exactly when T^[k] x lies in Karlsson's set Λ_{n−k}. The leader lemma sum_leaders_nonpos then bounds the sum of the increments over the leaders by 0. This is the purely pointwise/combinatorial heart of Derriennic's maximal inequality (the measure theory enters only when one integrates this inequality over a T-invariant set).

Derriennic's maximal inequality (Karlsson Lemma 3.4 / Prop 3.5)

Karlsson's Λ-set and A-set, and the integral telescoping of sum_leaders_cocycle_nonpos over a T-invariant set B.

def Oseledets.Kingman.bcoc {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (i : ℕ) (x : X) : ℝ

The increment of the cocycle: bcoc g i x = g i x − g (i−1) (T x). (Karlsson's b_i.)

Equations

• Oseledets.Kingman.bcoc g i x = g i x - g (i - 1) (T x)

def Oseledets.Kingman.lambdaSet {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (m : ℕ) : Set X

Karlsson's set Λ_m = {y | inf_{1≤k≤m} (g m y − g (m−k)(T^[k] y)) < 0}.

Equations

• Oseledets.Kingman.lambdaSet g m = {y : X | ∃ (k : ℕ), 1 ≤ k ∧ k ≤ m ∧ g m y - g (m - k) (T^[k] y) < 0}

def Oseledets.Kingman.aSet {X : Type u_1} (g : ℕ → X → ℝ) (m : ℕ) : Set X

Karlsson's set A_m = {y | inf_{1≤k≤m} g k y < 0} ⊆ Λ_m.

Equations

• Oseledets.Kingman.aSet g m = {y : X | ∃ (k : ℕ), 1 ≤ k ∧ k ≤ m ∧ g k y < 0}

theorem Oseledets.Kingman.aSet_subset_lambdaSet {X : Type u_1} {T : X → X} {g : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T g) (m : ℕ) : aSet g m ⊆ lambdaSet g m

A_m ⊆ Λ_m by subadditivity: g m y ≤ g (m−k) y + g k (T^[m−k] y)… actually the inclusion uses g m y ≤ g (m−k) (·); we prove it via g m y − g (m−k)(T^[k] y) ≤ g k y when k ≤ m. Indeed g m y = g (k + (m−k)) y ≤ g k y + g (m−k) (T^[k] y).

theorem Oseledets.Kingman.mem_leaderSet_iff_mem_lambdaSet {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (n k : ℕ) (x : X) : k ∈ leaderSet (fun (j : ℕ) => g n x - g (n - j) (T^[j] x)) n ↔ k < n ∧ T^[k] x ∈ lambdaSet g (n - k)

The leader-membership identification (Karlsson, §3.2): an index k is a leader of the partial sums S j = g n x − g (n−j)(T^[j] x) of length n exactly when k < n and T^[k] x ∈ Λ_{n−k}.

theorem Oseledets.Kingman.sum_bcoc_telescope {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (n : ℕ) (x : X) : ∑ k ∈ Finset.range n, bcoc g (n - k) (T^[k] x) = g n x - g 0 (T^[n] x)

Telescoping (Karlsson §3.2): ∑_{k<n} bcoc g (n−k) (T^[k] x) = g n x − g 0 (T^[n] x).

theorem Oseledets.Kingman.sum_bcoc_lambda_nonpos {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (n : ℕ) (x : X) : ∑ k ∈ Finset.range n with T^[k] x ∈ lambdaSet g (n - k), bcoc g (n - k) (T^[k] x) ≤ 0

Pointwise leader inequality, Λ-form. Summing the increments bcoc g (n−k) along the orbit over the indices k < n with T^[k] x ∈ Λ_{n−k} gives a non-positive number. (Recast of sum_leaders_cocycle_nonpos via the membership identification.)

noncomputable def Oseledets.Kingman.psiCoc {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (i : ℕ) : X → ℝ

Karlsson's localized increment ψ_i = 1_{Λ_i} · bcoc g i.

Equations

• Oseledets.Kingman.psiCoc g i = (Oseledets.Kingman.lambdaSet g i).indicator (Oseledets.Kingman.bcoc g i)

theorem Oseledets.Kingman.sum_psiCoc_comp_nonpos {X : Type u_1} {T : X → X} (g : ℕ → X → ℝ) (n : ℕ) (x : X) : ∑ k ∈ Finset.range n, psiCoc g (n - k) (T^[k] x) ≤ 0

Indicator form of the pointwise leader inequality. The full-range orbit sum of the localized increments ψ_{n−k} ∘ T^[k] is non-positive (it equals the filtered leader sum of sum_bcoc_lambda_nonpos, the extra terms being zero off Λ).

theorem Oseledets.Kingman.integrable_bcoc {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : ℕ → X → ℝ} (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (i : ℕ) : MeasureTheory.Integrable (bcoc g i) μ

bcoc g i = g i − g (i−1) ∘ T is integrable.

theorem Oseledets.Kingman.nullMeasurableSet_lambdaSet {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : ℕ → X → ℝ} (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (m : ℕ) : MeasureTheory.NullMeasurableSet (lambdaSet g m) μ

lambdaSet g m is null-measurable: a finite union over 1 ≤ k ≤ m of the null-measurable sets {g m − g (m−k) ∘ T^[k] < 0}.

theorem Oseledets.Kingman.integrable_psiCoc {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : ℕ → X → ℝ} (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (i : ℕ) : MeasureTheory.Integrable (psiCoc g i) μ

psiCoc g i is integrable (indicator of a null-measurable set of an integrable function).

theorem Oseledets.Kingman.setIntegral_comp_iterate_of_invariants {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {h : X → ℝ} (hh : MeasureTheory.AEStronglyMeasurable h μ) {s : Set X} (hs : MeasurableSet s) (hsinv : T ⁻¹' s = s) (k : ℕ) : ∫ (x : X) in s, h (T^[k] x) ∂μ = ∫ (x : X) in s, h x ∂μ

Set-integral invariance under T^[k] for a measurable T-invariant set s: ∫_s (h ∘ T^[k]) = ∫_s h.

theorem Oseledets.Kingman.sum_setIntegral_psiCoc_nonpos {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : ℕ → X → ℝ} (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) {B : Set X} (hB : MeasurableSet B) (hBinv : T ⁻¹' B = B) (n : ℕ) : ∑ i ∈ Finset.Icc 1 n, ∫ (x : X) in B, psiCoc g i x ∂μ ≤ 0

Integrated leader inequality (Karlsson Lemma 3.4, the telescoped integral). For a measurable T-invariant set B, the partial sum of localized increment integrals is non-positive: ∑_{i=1}^n ∫_{B} ψ_i ≤ 0, where ψ_i = 1_{Λ_i} bcoc g i.

theorem Oseledets.Kingman.sum_setIntegral_bcoc_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {g : ℕ → X → ℝ} (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) {B : Set X} (hB : MeasurableSet B) (hBinv : T ⁻¹' B = B) (m : ℕ) : ∑ i ∈ Finset.Icc 1 m, ∫ (x : X) in B, bcoc g i x ∂μ = ∫ (x : X) in B, g m x ∂μ - ∫ (x : X) in B, g 0 x ∂μ

Integrated telescoping over an invariant set B: ∑_{i=1}^m ∫_B bcoc g i = ∫_B g m − ∫_B g 0.

theorem Oseledets.Kingman.aSet_mono {X : Type u_1} {g : ℕ → X → ℝ} : Monotone (aSet g)

aSet g is monotone in the length.

theorem Oseledets.Kingman.nullMeasurableSet_aSet {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {g : ℕ → X → ℝ} (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) (m : ℕ) : MeasureTheory.NullMeasurableSet (aSet g m) μ

aSet g m is null-measurable.

noncomputable def Oseledets.Kingman.erealAddCoeIso (c : ℝ) : EReal ≃o EReal

Translation by a finite (real-coerced) constant is an order isomorphism of EReal.

Equations

• Oseledets.Kingman.erealAddCoeIso c = { toFun := fun (y : EReal) => y + ↑c, invFun := fun (y : EReal) => y - ↑c, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem Oseledets.Kingman.ereal_limsup_add_coe (u : ℕ → ℝ) (c : ℝ) : Filter.limsup (fun (n : ℕ) => ↑(u n) + ↑c) Filter.atTop = Filter.limsup (fun (n : ℕ) => ↑(u n)) Filter.atTop + ↑c

EReal limsup of a finite shift. For a real sequence u and a real constant c, limsup (fun n => ↑(u n) + ↑c) = limsup (fun n => ↑(u n)) + ↑c. Used to convert the shifted maximal inequality (Prop 3.5) from the non-positive case.

theorem Oseledets.Kingman.limsup_setIntegral_div_nonpos {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) {g : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T g) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) {B : Set X} (hB : MeasurableSet B) (hBinv : T ⁻¹' B = B) (hBneg : ∀ᵐ (x : X) ∂μ, x ∈ B → ∃ (k : ℕ), g (k + 1) x < 0) : Filter.limsup (fun (n : ℕ) => ↑((∫ (x : X) in B, g (n + 1) x ∂μ) / (↑n + 1))) Filter.atTop ≤ 0

Derriennic's maximal inequality (Karlsson Lemma 3.4). For a measurable T-invariant set B on which (a.e.) liminf (cdiv g · x) < 0, the normalized integral (∫_B g (n+1))/(n+1) has non-positive limsup.

theorem Oseledets.Kingman.setIntegral_div_le_level {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} [MeasureTheory.IsFiniteMeasure μ] (hT : MeasureTheory.MeasurePreserving T μ μ) {a : ℕ → X → ℝ} (hsub : IsSubadditiveCocycle T a) (hint : ∀ (n : ℕ), MeasureTheory.Integrable (a n) μ) {B : Set X} (hB : MeasurableSet B) (hBinv : T ⁻¹' B = B) (β : ℝ) (hBneg : ∀ᵐ (x : X) ∂μ, x ∈ B → ∃ (k : ℕ), a (k + 1) x < (↑k + 1) * β) : Filter.limsup (fun (n : ℕ) => ↑((∫ (x : X) in B, a (n + 1) x ∂μ) / (↑n + 1))) Filter.atTop ≤ ↑(β * (μ B).toReal)

The β-version of the maximal inequality (Karlsson Prop 3.5). For a measurable T-invariant set B on which (a.e.) liminf (cdiv a · x) < β, the normalized integral (∫_B a(n+1))/(n+1) has EReal limsup ≤ β · (μ B).toReal. Proved by applying limsup_setIntegral_div_nonpos to the shifted subadditive cocycle a'(n) x := a n x − n·β (subtracting the additive n·β preserves subadditivity), then undoing the constant shift.