The top-gap band-mass envelope topGapMassEnvelope_ae

This file assembles the deterministic and almost-everywhere statements behind the top-gap fast-band-mass envelope used in the Oseledets multiplicative ergodic theorem. The target theorem is

theorem topGapMassEnvelope_ae : ∀ᵐ x ∂μ, TopGapMassEnvelope A T lam0 x.

The proof is organized in three layers.

• PART A (ChainCore) is pure real analysis: it solves the band-mass recursion and bounds the accumulated multi-source geometric leakage. Its central statement, multi_source_envelope, converts the per-step multi-source recursion directly into an m-uniform per-stratum-rate sum.
• PART B is measure-free: the dynamical facts enter only through the plain predicates Localized and Tempered, so each sub-lemma is provable in isolation without any measure theory.
• PART C performs band stabilization, transfers the per-stratum bound to all gap-interior cuts, and wraps the result into the almost-everywhere statement.

Main definitions

• Oseledets.Localized, Oseledets.Tempered — the per-orbit localization and temperedness predicates on the singular-value spectrum.
• Oseledets.stratumBand — the spectral band associated with a stratum.
• Oseledets.canonSlack, Oseledets.canonCut, Oseledets.PerStratumEnvelope — the canonical per-stratum slack and cut, and the inductively-built per-stratum band-mass envelope.

Main results

• Oseledets.topGapMassEnvelope_ae — the almost-everywhere top-gap band-mass envelope (the headline result of the module).
• Oseledets.topGapMassEnvelope_of_perStratum, Oseledets.perStratumEnvelope_step — the deterministic per-stratum envelope and the inductive step it is built from.

Implementation notes

Fix the pair (λ_a, v), the canonical slack δ* = canonSlack = min(δ/4, G/2, (v−λ_a)/4), the canonical cut log c_v = v − δ*, and δ' = δ/4 for the induction hypothesis. A single slack η ≤ min(δ, G)/16 simultaneously discharges all six constraints below (worst cases shown; uses w ≤ pred(v) ≤ v − G for slow strata and v − λ_a ≥ G):

1. ρ_w < 1 (geometric convergence): need (v−δ*) − w − 2η > 0; worst w = v−G gives G − δ* − 2η ≥ G − G/2 − G/8 = 3G/8 > 0.
2. bottom-stratum slack (w ≤ λ_a, mass ≤ 1): rate (v−δ*) − w − 2η ≥ (v−λ_a) − δ* − 2η; need δ* + 2η ≤ δ; δ/4 + δ/8 = 3δ/8 ≤ δ.
3. intermediate slack (λ_a < w < v, IH mass): combined rate v − λ_a − δ* − δ' − 2η; need δ* + δ' + 2η ≤ δ; δ/4 + δ/4 + δ/8 ≤ δ.
4. canonical-cut gap separation (mem_hiBand_iff_of_localized at γ = v − δ*): slow side η < (v−δ*) − λ_j ≥ G/2; fast side (incl. λ_j = v) η < δ* + (λ_j − v), worst λ_j = v gives η < δ*; both follow from η ≤ min(δ,G)/16 < δ*.
5. intermediate sub-band inclusion stratumBand w ⊆ hiBand(m, canonCut_w): need η < δ*_w = min(δ'/4, G/2, (w−λ_a)/4) ≥ min(δ/16, G/4); η ≤ min(δ,G)/16. This is the binding constraint, which is why the slack is min(δ,G)/16 rather than min(δ/8, G/8).
6. initialization a_0 = 0 (canonCut_init_zero): need λ_a + η < v − δ*, i.e. η < (v−λ_a) − δ* ≥ G/2.

Note η < δ* always holds: δ* = min(δ/4, G/2, (v−λ_a)/4) ≥ min(δ/4, G/4) (using v−λ_a ≥ G), and η ≤ min(δ,G)/16 < min(δ/4, G/4) ≤ δ*.

Conventions: the cast Fintype.card (Fin d) = d is realized via ⟨(a : ℕ), lt_of_lt_of_eq a.isLt (Fintype.card_fin d).symm⟩; hiBand membership is σ_j(t)^{1/t} > c; bandProjector cuts the exponential scale.

Key points to keep in mind:

1. The slack δ* is quantized against the minimal distinct-stratum gap G (exists_distinctGap), never against raw index-adjacent gaps.
2. The qpow scale σ^{1/t} and σ^{1/(t+1)} are never mixed; the conversion happens at each fixed time.
3. The cut stays strictly gap-interior.
4. All Eventually thresholds are collected once and threaded as a single n₀.
5. The envelope is two-time: a fixed n controls all m ≥ n.
6. The single slack is η ≤ min(δ,G)/16.

PART A — abstract deterministic chain core (measure-free, matrix-free)

These lemmas are pure real-analysis: they solve the band-mass recursion and bound the accumulated multi-source geometric leakage. No matrices, no measure, no inner-product space. They are the easiest sub-lemmas to prove in isolation and the analytic crux of the whole argument.

theorem Oseledets.ChainCore.chain_le_partial_sum (a src : ℕ → ℝ) (h0 : a 0 = 0) (hrec : ∀ (k : ℕ), a (k + 1) ≤ a k + src k) (k : ℕ) : a k ≤ ∑ i ∈ Finset.range k, src i

A1 — telescoping chain solver. If a 0 = 0 and a (k+1) ≤ a k + src k for all k, then a k ≤ ∑_{i<k} src i for every k. (Elementary induction; we keep the raw partial-sum form so the geometric bound can be applied separately.)

theorem Oseledets.ChainCore.geom_partial_sum_le {r K : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hK : 0 ≤ K) (k : ℕ) : ∑ i ∈ Finset.range k, K * r ^ i ≤ K / (1 - r)

A2 — tail geometric bound. For 0 ≤ r < 1 and 0 ≤ K, the partial sums of the geometric series ∑_{i<k} K·r^i are bounded uniformly by K/(1-r).

theorem Oseledets.ChainCore.single_source_envelope (a src : ℕ → ℝ) {M ρ : ℝ} (n : ℕ) (hM : 0 ≤ M) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (h0 : a 0 = 0) (hrec : ∀ (k : ℕ), a (k + 1) ≤ a k + src k) (hsrc : ∀ (k : ℕ), src k ≤ M * ρ ^ (n + k)) (k : ℕ) : a k ≤ M / (1 - ρ) * ρ ^ n

A3 — single-source geometric envelope at a shifted base. This is the per-stratum source shape produced by PART B. Given the chain a 0 = 0, a (k+1) ≤ a k + src k, with each source term controlled by a geometric tail starting at absolute time n: src k ≤ M · ρ ^ (n + k) for 0 ≤ ρ < 1, 0 ≤ M, then for all k, a k ≤ (M / (1 - ρ)) · ρ ^ n.

This is the m-uniform (here k-uniform) envelope: the same n (hence same ρ^n prefactor) controls every k, i.e. every absolute time m = n + k ≥ n. Proof: A1 then A2 after factoring ρ^n out of ρ^(n+k) = ρ^n · ρ^k.

theorem Oseledets.ChainCore.multi_source_envelope {W : Type u_1} (Wf : Finset W) (a : ℕ → ℝ) (srcw : W → ℕ → ℝ) (Mw ρw : W → ℝ) (n : ℕ) (hM : ∀ w ∈ Wf, 0 ≤ Mw w) (hρ0 : ∀ w ∈ Wf, 0 ≤ ρw w) (hρ1 : ∀ w ∈ Wf, ρw w < 1) (h0 : a 0 = 0) (hrec : ∀ (k : ℕ), a (k + 1) ≤ a k + ∑ w ∈ Wf, srcw w k) (hsrc : ∀ w ∈ Wf, ∀ (k : ℕ), srcw w k ≤ Mw w * ρw w ^ (n + k)) (k : ℕ) : a k ≤ ∑ w ∈ Wf, Mw w / (1 - ρw w) * ρw w ^ n

A4 — multi-source geometric envelope. PART B's recursion has the multi-source form a (k+1) ≤ a k + ∑_{w ∈ W} srcw w k with finitely many strata W, each source geometric: srcw w k ≤ Mw w · (ρw w) ^ (n + k) with 0 ≤ ρw w < 1, 0 ≤ Mw w. Then, with a 0 = 0, for all k, a k ≤ ∑_{w ∈ W} (Mw w / (1 - ρw w)) · (ρw w) ^ n.

This is the central abstract statement: it converts the per-step multi-source recursion into a single k-uniform bound whose RHS is a finite sum of per-stratum geometric envelopes, each with its OWN rate. Proof: A1 (with src k = ∑_w srcw w k), then Finset.sum_comm to reorder ∑_{i<k} ∑_w into ∑_w ∑_{i<k}, then A2 per stratum.

PART B — deterministic SVD layer at a fixed x

Everything here is at a FIXED point x on an eventual time window. The dynamical localization/tempering facts are TAKEN AS PLAIN HYPOTHESES (no measure theory), so each sub-lemma is independently provable. We build:

• the per-stratum sub-band finsets stratumBand;
• the sub-band mass comparison (subband_mass_le_bandMass);
• the multi-source one-step recursion (bandMass_oneStep_multisource);
• the per-stratum envelope detPerStratumEnvelope, by strong induction over distinct stratum values, consuming PART A.

Notation / windows packaged as hypotheses

For a fixed x, set σ_j(t) = (toEuclideanLin (cocycle A T t x)).singularValues j. We work with the abstract localization predicate

Localized A T x lam0 η N : ∀ t ≥ N, ∀ j < d, exp(λ_j − η) < σ_j(t)^{1/t} < exp(λ_j + η)

and the tempering predicate

Tempered A T x η N : ∀ t ≥ N, ‖A(T^[t] x)‖ ≤ exp(t·η)

both produced (a.e.) in PART C from eventually_qpow_eigenvalue_localized and tendsto_logNorm_orbit_div_atTop_zero.

def Oseledets.Localized {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (lam0 : ℕ → ℝ) (η : ℝ) (N : ℕ) : Prop

Localization window predicate (the σ-localization fact, abstracted as a hypothesis).

Equations

• One or more equations did not get rendered due to their size.

def Oseledets.Tempered {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (η : ℝ) (N : ℕ) : Prop

Tempering window predicate (the one-step operator factor, abstracted as a hypothesis).

Equations

• Oseledets.Tempered A T x η N = ∀ (t : ℕ), N ≤ t → ‖A (T^[t] x)‖ ≤ Real.exp (↑t * η)

theorem Oseledets.exists_localized {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) (hconv : ∀ j < d, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues j)) Filter.atTop (nhds (lam0 j))) {η : ℝ} (hη : 0 < η) : ∃ (N : ℕ), Localized A T x lam0 η N

B0a — localization is producible. From the σ-convergence at x we get, for each η > 0, a localization threshold N. (Thin wrapper around eventually_qpow_eigenvalue_localized.)

theorem Oseledets.exists_tempered {X : Type u_1} {d : ℕ} {T : X → X} {A : X → Matrix (Fin d) (Fin d) ℝ} (x : X) (htemp : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖A (T^[n] x)‖) Filter.atTop (nhds 0)) {η : ℝ} (hη : 0 < η) : ∃ (N : ℕ), Tempered A T x η N

B0b — tempering is producible. From (1/t)·log‖A(T^[t]x)‖ → 0 at x we get, for each η > 0, a tempering threshold N. (Tendsto.eventually of · < η then exp-monotone; the t = 0 slot is harmless because the window only constrains t ≥ N and we can take N ≥ 1.)

Per-stratum sub-bands

noncomputable def Oseledets.stratumBand {d : ℕ} [NeZero d] (lam0 : ℕ → ℝ) (v : ℝ) : Finset (Fin (Fintype.card (Fin d)))

The time-m sub-band of stratum value v: indices j whose Lyapunov value lam0 j equals v. This is a time-independent finset (it depends only on lam0), but we keep m for symmetry with hiBand; the localization hypothesis is what ties it to the actual time-m band.

Equations

• Oseledets.stratumBand lam0 v = {j : Fin (Fintype.card (Fin d)) | lam0 ↑j = v}

Sub-band mass and its comparison to a band-projector mass

subBandMass S m B u := ‖S.fastProj m B u‖, the projection of u onto the sub-band B at time m. When B ⊆ hiBand A T m x c the sub-band sits inside the fast band of cut c, so its mass is dominated by the full band mass (Pythagoras over an index subset).

theorem Oseledets.subband_mass_le_bandMass {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (m : ℕ) (x : X) (c : ℝ) (B : Finset (Fin (Fintype.card (Fin d)))) (hB : B ⊆ hiBand A T m x c) (u : EuclideanSpace ℝ (Fin d)) : ‖(chainSVD A T x).fastProj m B u‖ ≤ ‖(Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c).indicator 1) m x)) u‖

B1 — sub-band mass ≤ band mass (Pythagoras over index subsets). If B ⊆ hiBand A T m x c then the projection of u onto B is dominated by the cut-c band projector mass.

The slow band partitions into per-stratum sub-bands

Under localization with η small relative to the distinct-stratum gap G, and a cut c whose log c is STRICTLY between consecutive strata, (hiBand A T m x c)ᶜ is the disjoint union of the stratumBands of distinct stratum values w with w < log c. We package the per-step slow-cap-and-floor data this needs into one combinatorial lemma.

theorem Oseledets.mem_hiBand_iff_of_localized {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (_hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) {η : ℝ} (hη : 0 < η) {N : ℕ} (hloc : Localized A T x lam0 η N) {γ : ℝ} (hgapsep : ∀ j < d, lam0 j + η < γ ∨ γ < lam0 j - η) {t : ℕ} (ht : N ≤ t) (_ht1 : 1 ≤ t) (j : Fin (Fintype.card (Fin d))) : j ∈ hiBand A T t x (Real.exp γ) ↔ γ < lam0 ↑j

B2 — slow-band stratum decomposition. Under localization at time t with η, if log c avoids every stratum then the complement of hiBand A T t x c is {j : lam0 j < log c} (membership characterization). Stated as the membership equivalence at a single time t past the localization threshold, with c = exp γ, γ strictly gap-separated from every stratum by more than η.

Per-stratum sub-band caps from localization

The slow sub-band stratumBand lam0 w of stratum value w has every singular value capped at time t by σ_j(t) ≤ exp(t(w+η)) (from σ_j(t)^{1/t} < exp(λ_j+η) = exp(w+η) and rpow_inv_le_iff_le_pow). The fast floor at t+1 for the cut c = exp γ is c^{t+1}.

theorem Oseledets.stratum_sigma_cap {X : Type u_1} {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (_hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) {η : ℝ} (_hη : 0 < η) {N : ℕ} (hloc : Localized A T x lam0 η N) {w : ℝ} {t : ℕ} (ht : N ≤ t) (ht1 : 1 ≤ t) (j : Fin (Fintype.card (Fin d))) (hj : j ∈ stratumBand lam0 w) : (Matrix.toEuclideanLin (cocycle A T t x)).singularValues ↑j ≤ Real.exp (↑t * (w + η))

B3 — per-stratum slow cap. Under localization, every index in stratumBand lam0 w has, at time t ≥ N, σ_j(t) ≤ exp(t(w+η)).

The multi-source one-step recursion

This refines the single-cap bandMass_oneStep_recursion. Instead of bounding the slow-projection norm ‖slowProj_t u‖ by a single cap, we split the slow band into per-stratum sub-bands and bound the leakage source as a sum over strata, each with its own sub-band mass and its own σ-cap. We use the triangle-inequality route: write slowProj_t u = ∑_w fastProj_t (B_w) u over the partition {B_w} of (hiBand)ᶜ, so that the operator step bound distributes; each sub-band term is bounded via oneStep_sandwich applied to that sub-band's span (each fastProj_t (B_w) u lies in the span of e_t over B_w ⊆ (hiBand)ᶜ).

Private SVDData-level helpers for the multi-source recursion (prefix htgmulti_)

theorem Oseledets.bandMass_oneStep_multisource {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {W : Type u_2} (A : X → Matrix (Fin d) (Fin d) ℝ) {c₀ : ℝ} (hc₀ : 0 < c₀) {t : ℕ} (x : X) (Wf : Finset W) (sval : W → ℝ) (hsval : ∀ w ∈ Wf, 0 ≤ sval w) (Bw : W → Finset (Fin (Fintype.card (Fin d)))) (hcap : ∀ w ∈ Wf, ∀ j ∈ Bw w, (Matrix.toEuclideanLin (cocycle A T t x)).singularValues ↑j ≤ sval w) (hpart : (hiBand A T t x c₀)ᶜ = Wf.biUnion Bw) (hdisj : (↑Wf).PairwiseDisjoint Bw) (u : EuclideanSpace ℝ (Fin d)) : ‖(Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c₀).indicator 1) (t + 1) x)) u‖ ≤ ‖(Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c₀).indicator 1) t x)) u‖ + ∑ w ∈ Wf, ‖A (T^[t] x)‖ * sval w / c₀ ^ (t + 1) * ‖(chainSVD A T x).fastProj t (Bw w) u‖

B4 — multi-source one-step band-mass recursion. Fix a cut c = exp γ > 0 and a finite set of distinct stratum values Wf whose sub-bands {stratumBand lam0 w : w ∈ Wf} partition the slow band (hiBand A T t x c)ᶜ at time t (hypothesis hpart). With per-stratum slow caps sw : ℝ (σ_j(t) ≤ sw w for j ∈ stratumBand lam0 w), the fast floor c^{t+1}, and the tempered step factor b = ‖A(T^[t]x)‖, the band mass satisfies

‖P^{>c}_{t+1} u‖ ≤ ‖P^{>c}_t u‖ + ∑_{w∈Wf} (b·(sw w)/c^{t+1}) · ‖fastProj_t (stratumBand lam0 w) u‖.

Route: bandMass_oneStep_recursion reduces P^{>c}_{t+1} to P^{>c}_t + (b·s/c^{t+1})·‖slowProj‖ with a single cap; here we instead expand slowProj over the partition and apply the SVD sandwich per sub-band (each sub-band is a slow span), summing. The cleanest formalization re-runs the oneStep_recursion derivation once per sub-band against hiT1 = hiBand (t+1) and uses additivity of fastProj (t+1) over the partition pieces.

PART B (continued) — the per-stratum envelope by strong induction

The conclusion shape

PerStratumEnvelope A T lam0 x a v says: for every δ > 0 there is C ≥ 1 such that eventually in n, for all m ≥ n, the time-m mass of the time-n slow eigenvector u_a(n) at the canonical δ-dependent cut for the pair (lam0 a, v) decays like exp(−n(v − lam0 a − δ)).

The cut is not a free parameter inside the predicate; it is the canonical cut canonCut a v δ = exp(v − δ*) with δ* = min(δ/4, G/2, (v − lam0 a)/4). Running the recursion at this δ-dependent cut is what makes the induction close. We carry the distinct-stratum gap G = distinctGap lam0 as a parameter.

theorem Oseledets.exists_distinctGap {d : ℕ} [NeZero d] (lam0 : ℕ → ℝ) : ∃ (G : ℝ), 0 < G ∧ ∀ (i j : Fin d), lam0 ↑i < lam0 ↑j → lam0 ↑i + G ≤ lam0 ↑j

B-gap — existence of a positive distinct-stratum gap. The slacks are quantized against this gap, never against raw index-adjacent gaps. There is G > 0 below every gap between distinct stratum values: lam0 i < lam0 j ⟹ lam0 i + G ≤ lam0 j. (The min over the finitely many positive differences lam0 j − lam0 i is positive; if there is at most one distinct stratum the statement is vacuous and any G = 1 works.) Kept as a producer so G stays an abstract parameter elsewhere.

noncomputable def Oseledets.canonSlack (lam0 : ℕ → ℝ) (a : ℕ) (v G δ : ℝ) : ℝ

The canonical δ-dependent slack δ* for the pair (lam0 a, v): strictly positive, ≤ δ/4, ≤ G/2, ≤ (v − lam0 a)/4.

Equations

• Oseledets.canonSlack lam0 a v G δ = min (min (δ / 4) (G / 2)) ((v - lam0 a) / 4)

noncomputable def Oseledets.canonCut (lam0 : ℕ → ℝ) (a : ℕ) (v G δ : ℝ) : ℝ

The canonical cut for the pair (lam0 a, v) at slack δ: exp(v − δ*), strictly interior to the gap below v (since δ* ≤ G/2 < G and the predecessor stratum is ≤ v − G).

Equations

• Oseledets.canonCut lam0 a v G δ = Real.exp (v - Oseledets.canonSlack lam0 a v G δ)

def Oseledets.PerStratumEnvelope {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (lam0 : ℕ → ℝ) (x : X) (G : ℝ) (a : Fin d) (v : ℝ) : Prop

The per-stratum envelope (conclusion shape). For index a and distinct stratum value v > lam0 a: for every δ > 0 there is C ≥ 1 with eventually-in-n, for-all-m ≥ n, the canonical-cut band mass ≤ C·exp(−n(v − lam0 a − δ)).

Equations

• One or more equations did not get rendered due to their size.

Initialization (a_0 = 0) at the canonical cut

At time n past localization with η small, σ_a(n)^{1/n} < exp(lam0 a + η) < canonCut a v G δ (because log(canonCut) = v − δ* > lam0 a + η for η small), so a ∉ hiBand(n, canonCut) and bandMass_init_zero gives a_0 = 0.

theorem Oseledets.canonCut_init_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (_hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) (a : Fin d) {v G δ η : ℝ} {N n : ℕ} (hloc : Localized A T x lam0 η N) (hn : N ≤ n) (_hn1 : 1 ≤ n) (_hav : lam0 ↑a < v) (_hη : 0 < η) (hηsmall : lam0 ↑a + η < v - canonSlack lam0 (↑a) v G δ) : (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (canonCut lam0 (↑a) v G δ)).indicator 1) n x)) ((sortedGramEigenbasis A T n x) ⟨↑a, ⋯⟩) = 0

B5 — initialization. Under localization with η small relative to v − lam0 a − δ*, the index a is below the canonical cut at time n, so the band projector annihilates u_a(n).

The inductive step

The heart of PART B. Given the localization/tempering windows and the inductive hypothesis — the per-stratum envelope PerStratumEnvelope … a w for every distinct stratum value w with lam0 a < w < v — produce PerStratumEnvelope … a v.

Mechanism:

• Run the recursion at c = canonCut a v G δ = exp(v − δ*), δ* = canonSlack.
• The slow band of c at time m is (by mem_hiBand_iff_of_localized) exactly the disjoint union of stratumBand lam0 w over distinct strata w < v − δ*, i.e. all distinct w ≤ pred(v) < v.
• Per-step source for stratum w (B4 term): (‖A(T^[m]x)‖ · exp(m(w+η)) / c^{m+1}) · mass_w(m), with ‖A(T^[m]x)‖ ≤ exp(mη) (Tempered), σ-cap exp(m(w+η)) (B3), c^{m+1} = exp((m+1)(v−δ*)). The coefficient is ≤ exp(mη)·exp(m(w+η))/exp((m+1)(v−δ*)) = exp(−(m+1)(v−δ*))·exp(m(w+2η)) = exp(−(v−δ*)) · exp(−m((v−δ*) − w − 2η)), a geometric factor in m with ratio ρ_w = exp(−((v−δ*) − w − 2η)) < 1 once η < ((v−δ*)−w)/2 (guaranteed: w ≤ pred(v) ≤ v−G, δ* ≤ G/2, so (v−δ*)−w ≥ G/2 > 0; satisfied by the single slack η ≤ min(δ,G)/16, see η-budget point 5 in the file header).
• mass_w(m) bound:
  • bottom strata w ≤ lam0 a: mass_w(m) ≤ ‖u_a(n)‖ = 1 (B1 with the trivial cut, or directly norm_fastProj_le). Contribution geometric envelope: Mw = exp(−(v−δ*)), ρ_w as above; the single_source sum gives ≈ K·exp(−n((v−δ*) − w − 2η)) ≤ K·exp(−n(v − lam0 a − δ)) (since w ≤ lam0 a, δ* + 2η ≤ δ).
  • intermediate strata lam0 a < w < v: by the IH PerStratumEnvelope … a w at δ' = δ/4, the mass at its own canonical cut canonCut_w = exp(w − δ*_w) ≤ C_w·exp(−n(w − lam0 a − δ')), uniformly in m ≥ n; transfer mass_w(m) ≤ ‖P^{>canonCut_w}_m u_a(n)‖ via B1, which needs stratumBand lam0 w ⊆ hiBand(m, canonCut_w): under localization σ_j(m)^{1/m} > exp(w − η) for j ∈ stratumBand w, and canonCut_w = exp(w − δ*_w) < exp(w − η) provided η < δ*_w. Since δ*_w = min(δ'/4, G/2, (w−lam0 a)/4) ≥ min(δ/16, G/4) (using w − lam0 a ≥ G), it suffices to take η ≤ min(G, δ)/16; the binding constraint is this intermediate sub-band inclusion, not the ρ_w < 1 one. The geometric source then has Mw = C_w·exp(−n(w − lam0 a − δ'))·exp(−(v−δ*)) and the m-sum gives ≈ K_w·exp(−n((v−δ*) − w − 2η))·exp(−n(w − lam0 a − δ')) = K_w·exp(−n(v − lam0 a − δ* − δ' − 2η)) ≤ K_w·exp(−n(v − lam0 a − δ)) (δ* + δ' + 2η ≤ δ/4 + δ/4 + δ/8 ≤ δ).
• Assemble via A4 (multi-source envelope): a_k ≤ ∑_w (Mw/(1−ρw))·ρw^n, each term ≤ C_w'·exp(−n·rate_v) with rate_v = v − lam0 a − δ; the final C = max over w of C_w' (finite sum bounded by (#strata)·max), with 1 ≤ C.

theorem Oseledets.perStratumEnvelope_step {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) {G : ℝ} (hG : 0 < G) (hGgap : ∀ (i j : Fin d), lam0 ↑i < lam0 ↑j → lam0 ↑i + G ≤ lam0 ↑j) (hconv : ∀ j < d, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues j)) Filter.atTop (nhds (lam0 j))) (htemp : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖A (T^[n] x)‖) Filter.atTop (nhds 0)) (a : Fin d) (v : ℝ) (hav : lam0 ↑a < v) (hvstratum : ∃ (j : Fin d), lam0 ↑j = v) (IH : ∀ (w : ℝ), lam0 ↑a < w → w < v → (∃ (j : Fin d), lam0 ↑j = w) → PerStratumEnvelope A T lam0 x G a w) : PerStratumEnvelope A T lam0 x G a v

B6 — the inductive step. All windows + IH ⟹ the per-stratum envelope for v. The IH is phrased over the finite set of distinct stratum values strictly between lam0 a and v.

theorem Oseledets.perStratumEnvelope_of_lt {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) {G : ℝ} (hG : 0 < G) (hGgap : ∀ (i j : Fin d), lam0 ↑i < lam0 ↑j → lam0 ↑i + G ≤ lam0 ↑j) (hconv : ∀ j < d, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues j)) Filter.atTop (nhds (lam0 j))) (htemp : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖A (T^[n] x)‖) Filter.atTop (nhds 0)) (a : Fin d) (v : ℝ) (hav : lam0 ↑a < v) (hvstratum : ∃ (j : Fin d), lam0 ↑j = v) : PerStratumEnvelope A T lam0 x G a v

B7 — the strong induction. For every index a and every distinct stratum value v with lam0 a < v, the per-stratum envelope holds. Strong induction on the number of distinct stratum values in (lam0 a, v) (equivalently Finset well-founded recursion), discharging each level by perStratumEnvelope_step.

PART C — band stabilization + transfer to all gap-interior cuts + a.e. wrapper

Band stabilization

Under localization with η small, the band at any cut whose log is strictly gap-separated from every stratum stabilizes: j ∈ hiBand A T m x c ↔ log c < lam0 j, for all m past the localization threshold. Hence two gap-interior cuts to the same top gap below lam0 e give equal bands, so equal band-projector masses.

theorem Oseledets.bandMass_eq_of_gap_interior {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) {η : ℝ} (hη : 0 < η) {N : ℕ} (hloc : Localized A T x lam0 η N) {c₀ c₁ : ℝ} (hc₀ : 0 < c₀) (hc₁ : 0 < c₁) (hsep0 : ∀ j < d, lam0 j + η < Real.log c₀ ∨ Real.log c₀ < lam0 j - η) (hsep1 : ∀ j < d, lam0 j + η < Real.log c₁ ∨ Real.log c₁ < lam0 j - η) (hsame : ∀ (j : Fin (Fintype.card (Fin d))), Real.log c₀ < lam0 ↑j ↔ Real.log c₁ < lam0 ↑j) {m : ℕ} (hm : N ≤ m) (hm1 : 1 ≤ m) (u : EuclideanSpace ℝ (Fin d)) : ‖(Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c₀).indicator 1) m x)) u‖ = ‖(Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c₁).indicator 1) m x)) u‖

C1 — band mass equality for two gap-interior cuts (band stabilization). If log c₀ and log c₁ are both strictly gap-separated from every stratum by more than η (hsep0, hsep1) and they have the same membership pattern (hsame : ∀ j, log c₀ < lam0 j ↔ log c₁ < lam0 j), then for every m past the localization threshold the band-projector masses agree.

Transfer: per-stratum envelope (canonical cuts) ⟹ TopGapMassEnvelope (all cuts)

For the pair (a, e) with lam0 a < lam0 e and a gap-interior cut c₀ (∀ i, lam0 i < log c₀ ∨ lam0 e ≤ lam0 i), the canonical cut canonCut a (lam0 e) G δ is also gap-interior to the same top gap below lam0 e (its log = lam0 e − δ* with δ* ≤ G/2, and the predecessor stratum is ≤ lam0 e − G). Both cuts have membership lam0 j > cut ↔ lam0 e ≤ lam0 j, so by C1 their band masses agree past localization, and the per-stratum envelope at v = lam0 e transfers. The constant C is uniform over the finitely many pairs via a Finset max.

theorem Oseledets.topGap_bound_at_cut_of_perStratum {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) {G : ℝ} (hG : 0 < G) (hGgap : ∀ (i j : Fin d), lam0 ↑i < lam0 ↑j → lam0 ↑i + G ≤ lam0 ↑j) (hconv : ∀ j < d, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues j)) Filter.atTop (nhds (lam0 j))) (a e : Fin d) (hgap : lam0 ↑a < lam0 ↑e) (_henv : PerStratumEnvelope A T lam0 x G a (lam0 ↑e)) {δ : ℝ} (hδ : 0 < δ) {C : ℝ} (_hC1 : 1 ≤ C) (hCenv : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), n ≤ m → ‖(Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi (canonCut lam0 (↑a) (lam0 ↑e) G δ)).indicator 1) m x)) ((sortedGramEigenbasis A T n x) ⟨↑a, ⋯⟩)‖ ≤ C * Real.exp (-↑n * (lam0 ↑e - lam0 ↑a - δ))) (c₀ : ℝ) (hc₀lo : Real.exp (lam0 ↑a) < c₀) (hc₀hi : c₀ < Real.exp (lam0 ↑e)) (hc₀gap : ∀ (i : Fin d), lam0 ↑i < Real.log c₀ ∨ lam0 ↑e ≤ lam0 ↑i) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), n ≤ m → ‖(Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c₀).indicator 1) m x)) ((sortedGramEigenbasis A T n x) ⟨↑a, ⋯⟩)‖ ≤ C * Real.exp (-↑n * (lam0 ↑e - lam0 ↑a - δ))

C2 — transfer to a single gap-interior cut. From PerStratumEnvelope … a (lam0 e) and localization, the TopGap-style bound holds at the arbitrary gap-interior cut c₀.

theorem Oseledets.topGapMassEnvelope_of_perStratum {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (x : X) (lam0 : ℕ → ℝ) {G : ℝ} (hG : 0 < G) (hGgap : ∀ (i j : Fin d), lam0 ↑i < lam0 ↑j → lam0 ↑i + G ≤ lam0 ↑j) (hconv : ∀ j < d, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues j)) Filter.atTop (nhds (lam0 j))) (henv : ∀ (a e : Fin d), lam0 ↑a < lam0 ↑e → PerStratumEnvelope A T lam0 x G a (lam0 ↑e)) : TopGapMassEnvelope A T lam0 x

C3 — uniform-C transfer (the per-x deterministic TopGapMassEnvelope). Assembling C2 across the finitely many gap pairs (a, e) with a single constant C via a Finset max over Fin d × Fin d gives TopGapMassEnvelope A T lam0 x, given the per-stratum envelopes for all gap pairs.

The a.e. wrapper — assembling the target theorem

Collect the a.e. windows (σ-convergence for every j < d, tempering) from hlam0 and tendsto_logNorm_orbit_div_atTop_zero, fix the distinct gap G (deterministic), build all per-stratum envelopes via perStratumEnvelope_of_lt, and transfer via topGapMassEnvelope_of_perStratum.

theorem Oseledets.topGapMassEnvelope_ae {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {d : ℕ} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (lam0 : ℕ → ℝ) (hlam0 : ∀ i < d, ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues i)) Filter.atTop (nhds (lam0 i))) : ∀ᵐ (x : X) ∂μ, TopGapMassEnvelope A T lam0 x

The top-gap band-mass envelope topGapMassEnvelope_ae: almost everywhere the top-gap fast-band-mass envelope holds, discharging htopgap in forward_graded_overlap_of_topGapEnvelope.