forward_graded_overlap_of_topGapEnvelope — forward graded overlap via the top-gap

envelope (Ruelle Lemma 1.4)

This module proves the forward graded overlap estimate using the envelope TopGapMassEnvelope, in which the cut c₀ is restricted to the top gap below λ_e: no stratum value of lam0 lies in (log c₀, λ_e) (encoded ∀ i, lam0 i ≤ log c₀ ∨ lam0 e ≤ lam0 i). An arbitrary-cut chain envelope is not available here: at a cut interior to the spectrum, directions belonging to intermediate strata can oscillate in and out of the band under singular-value fluctuations, so the band mass need not decay. Restricting the cut to the top gap removes that obstruction.

• forward_graded_overlap_of_topGapEnvelope carries the single isolated analytic hypothesis htopgap : ∀ᵐ x ∂μ, TopGapMassEnvelope A T lam0 x. The gap-pair cut selection goes through exists_topgap_cut (a top-gap, spectrum-avoiding cut).
• The remainder of the module is the Step-A engine for discharging htopgap via Ruelle's per-stratum strong induction: qpow↔rpow singular-value comparisons, σ-localization at all times, the tempered one-step operator factor, the per-step band-mass recursion (bandMass_oneStep_recursion, built on Oseledets.RuelleCofactor.SVDData.oneStep_recursion and toEuclideanLin_bandProjector_eq_fastProj), and the a₀ = 0 initialization (bandMass_init_zero).

Main definitions

• Oseledets.TopGapMassEnvelope — the top-gap band-mass envelope predicate along an orbit.

Main results

• Oseledets.forward_graded_overlap_of_topGapEnvelope — the forward graded-overlap bound obtained from the top-gap band-mass envelope (the headline result of the module).
• Oseledets.exists_topgap_cut — existence of a top-gap spectral cut.

Implementation notes

With the top-gap cut c₀ = exp(λ_e − g/2) (g the top gap), the direct bottom-stratum leakage rate is log c₀ − λ_a = λ_e − g/2 − λ_a, which misses the target rate λ_e − λ_a − δ whenever δ < g/2. The leakage source is not of mass one: it is itself the graded overlap of u_a(n) with the intermediate strata, decaying at rate λ_r − λ_a, so the recursion is self-referential and Ruelle's strong induction over distinct stratum values is mathematically required. Slacks must be quantized against the minimum distinct-stratum gap, since raw index-adjacent gaps can vanish under multiplicity.

σ-cap helpers: converting qpow-eigenvalue (= σ^{1/m}) comparisons to σ comparisons

theorem Oseledets.qpow_eigenvalue_eq_rpow {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (m : ℕ) (x : X) (j : Fin (Fintype.card (Fin d))) : ⋯.eigenvalues₀ j = (Matrix.toEuclideanLin (cocycle A T m x)).singularValues ↑j ^ (↑m)⁻¹

The j-th qpow eigenvalue at time m equals σ_j(m)^{1/m}.

theorem Oseledets.rpow_inv_le_iff_le_pow {σ c₀ : ℝ} (hσ : 0 ≤ σ) (hc₀ : 0 < c₀) {m : ℕ} (hm : 1 ≤ m) : σ ^ (↑m)⁻¹ ≤ c₀ ↔ σ ≤ c₀ ^ m

For m ≥ 1 and c₀ > 0: σ^{1/m} ≤ c₀ ↔ σ ≤ c₀^m.

theorem Oseledets.lt_rpow_inv_iff_pow_lt {σ c₀ : ℝ} (hσ : 0 ≤ σ) (hc₀ : 0 < c₀) {m : ℕ} (hm : 1 ≤ m) : c₀ < σ ^ (↑m)⁻¹ ↔ c₀ ^ m < σ

For m ≥ 1 and c₀ > 0: c₀ < σ^{1/m} ↔ c₀^m < σ.

σ-localization: the qpow eigenvalue σ_j(t)^{1/t} converges to exp(λ_j)

theorem Oseledets.rpow_inv_eq_exp_log {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) {j : ℕ} (hj : j < d) {t : ℕ} (_ht : 1 ≤ t) : (Matrix.toEuclideanLin (cocycle A T t x)).singularValues j ^ (↑t)⁻¹ = Real.exp ((↑t)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T t x)).singularValues j))

σ_j(t)^{1/t} = exp((1/t)·log σ_j(t)) for t ≥ 1 (the singular value is positive).

theorem Oseledets.eventually_qpow_eigenvalue_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 < η) : ∀ᶠ (t : ℕ) in Filter.atTop, ∀ j < d, Real.exp (lam0 j - η) < (Matrix.toEuclideanLin (cocycle A T t x)).singularValues j ^ (↑t)⁻¹ ∧ (Matrix.toEuclideanLin (cocycle A T t x)).singularValues j ^ (↑t)⁻¹ < Real.exp (lam0 j + η)

σ-localization. If at x the normalized log of σ_j(·) converges to λ_j for every j < d, then for any η > 0 there is N such that for all t ≥ N and all j < d, exp(λ_j − η) < σ_j(t)^{1/t} < exp(λ_j + η).

The one-step recursion specialised to the cocycle SVD chain at a fixed cut

We instantiate Oseledets.RuelleCofactor.SVDData.oneStep_recursion on chainSVD A T x with slow cap c₀^t, fast floor c₀^{t+1}, and step factor b = ‖A(T^[t] x)‖, identifying fastProj with the band projector via toEuclideanLin_bandProjector_eq_fastProj. This produces the per-step inequality on the band masses.

theorem Oseledets.chain_oneStep_opNorm {X : Type u_1} {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (t : ℕ) (x : X) (w : EuclideanSpace ℝ (Fin d)) : ‖(Matrix.toEuclideanLin (cocycle A T (t + 1) x)) w‖ ≤ ‖A (T^[t] x)‖ * ‖(Matrix.toEuclideanLin (cocycle A T t x)) w‖

The one-step operator factor along the orbit: ‖toEuclideanLin (cocycle (t+1) x) w‖ ≤ ‖A(T^[t] x)‖ · ‖toEuclideanLin (cocycle t x) w‖.

Step A — the top-gap fast-band-mass envelope (Ruelle Lemma 1.4 core)

In this envelope the cut c₀ is restricted to the top gap below λ_e, i.e. no stratum value lies in (log c₀, λ_e). It is stated here as the single isolated analytic hypothesis TopGapMassEnvelope, established by Ruelle's band-distance strong induction over strata (eqns (1.3)/(1.4)); the deterministic engine Oseledets.RuelleCofactor.SVDData.{oneStep_recursion, chain_geometric_sum} and the σ-localization layer above are its ingredients. Everything downstream (Step B) is discharged from it.

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

Top-gap fast-band-mass envelope. For a gap pair λ_a < λ_e and any cut c₀ in the open interior of the top gap below λ_e (exp λ_a < c₀ < exp λ_e, with every stratum value of lam0 either strictly below log c₀ or at least λ_e, encoded ∀ i, lam0 i < Real.log c₀ ∨ lam0 e ≤ lam0 i), the time-m band mass of the time-n slow eigenvector u_a(n) decays like exp(−n(λ_e − λ_a − δ)) uniformly in m ≥ n.

The strictness in the first disjunct is essential: at a boundary cut log c₀ = λ_p (the largest stratum below λ_e) the λ_p-directions can oscillate in and out of the band under σ-fluctuations, so the envelope fails there. Gap-interior cuts are all the Step-B consumer ever uses (exists_topgap_cut produces the gap midpoint).

Equations

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

Top-gap cut selection for lam0

theorem Oseledets.exists_topgap_cut {d : ℕ} (lam0 : ℕ → ℝ) {a e : Fin d} (hgap : lam0 ↑a < lam0 ↑e) : ∃ (c₀ : ℝ), Real.exp (lam0 ↑a) < c₀ ∧ c₀ < Real.exp (lam0 ↑e) ∧ (∀ (i : Fin d), lam0 ↑i < Real.log c₀ ∨ lam0 ↑e ≤ lam0 ↑i) ∧ ∀ (i : Fin d), Real.exp (lam0 ↑i) ≠ c₀

Top-gap cut below lam0 e. For a gap pair lam0 a < lam0 e, there is a cut c₀ with exp (lam0 a) < c₀ < exp (lam0 e), strictly interior to the top spectral gap below lam0 e (encoded ∀ i, lam0 i < log c₀ ∨ lam0 e ≤ lam0 i), and with c₀ avoiding every exp (lam0 i).

Step B — the almost-everywhere wrapper

This is the theorem forward_graded_overlap_of_topGapEnvelope. It carries the single isolated analytic hypothesis htopgap (the top-gap envelope TopGapMassEnvelope). The gap-cut is selected by exists_topgap_cut (the top-gap selection).

theorem Oseledets.forward_graded_overlap_of_topGapEnvelope {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))) (b' : X → OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d))) (hb' : ∀ᵐ (x : X) ∂μ, ∀ (e : Fin d), (Matrix.toEuclideanLin (lambdaHat A T x)) ((b' x) e) = Real.exp (lamSing A T x ↑e) • (b' x) e) (hident : ∀ᵐ (x : X) ∂μ, ∀ (c : ℝ), 0 < c → (∀ (i : Fin d), Real.exp (lamSing A T x ↑i) ≠ c) → Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds (cfc ((Set.Ioi c).indicator 1) (lambdaHat A T x)))) (htopgap : ∀ᵐ (x : X) ∂μ, TopGapMassEnvelope A T lam0 x) : ∀ᵐ (x : X) ∂μ, ∀ (δ : ℝ), 0 < δ → ∃ (c : ℝ), 1 ≤ c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (a e : Fin d), |inner ℝ ((b' x) e) ((sortedGramEigenbasis A T n x) ⟨↑a, ⋯⟩)| ≤ c * Real.exp (-↑n * (max (lam0 ↑e - lam0 ↑a) 0 - δ))

The per-step band-mass recursion at a fixed cut (engine instantiation)

We instantiate Oseledets.RuelleCofactor.SVDData.oneStep_recursion on chainSVD A T x. The fast band at time t is hiBand A T t x c₀; its complement is the slow band. We supply:

• slow cap s valid at time t: every slow σ_j(t) ≤ s;
• fast floor c₀^{t+1} at time t+1: every fast σ_j(t+1) ≥ c₀^{t+1} (from the band definition);
• step factor b = ‖A(T^[t] x)‖ (from chain_oneStep_opNorm). The band projector mass is fastProj via toEuclideanLin_bandProjector_eq_fastProj.

theorem Oseledets.fast_sigma_floor {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) {c₀ : ℝ} (hc₀ : 0 < c₀) {t : ℕ} (x : X) (j : Fin (Fintype.card (Fin d))) (hj : j ∈ hiBand A T (t + 1) x c₀) : c₀ ^ (t + 1) ≤ (Matrix.toEuclideanLin (cocycle A T (t + 1) x)).singularValues ↑j

Fast indices at time t+1 have σ ≥ c₀^{t+1}.

theorem Oseledets.bandMass_oneStep_recursion {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) {c₀ : ℝ} (hc₀ : 0 < c₀) {t : ℕ} (x : X) {s : ℝ} (hs : 0 ≤ s) (hslow : ∀ j ∈ (hiBand A T t x c₀)ᶜ, (Matrix.toEuclideanLin (cocycle A T t x)).singularValues ↑j ≤ s) (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‖ + ‖A (T^[t] x)‖ * s / c₀ ^ (t + 1) * ‖(chainSVD A T x).slowProj t (hiBand A T t x c₀) u‖

The per-step band-mass recursion (one application of oneStep_recursion). With slow cap s, fast floor c₀^{t+1}, step factor b = ‖A(T^[t]x)‖: ‖P^{>c₀}_{t+1} u‖ ≤ ‖P^{>c₀}_t u‖ + (b·s/c₀^{t+1})·‖slowProj_t u‖.

Initialization (a_0 = 0): the time-n slow eigenvector has no fast-band mass at

time n

theorem Oseledets.bandMass_init_zero {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (n : ℕ) (x : X) (c₀ : ℝ) {a : Fin (Fintype.card (Fin d))} (ha : a ∉ hiBand A T n x c₀) : (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c₀).indicator 1) n x)) ((sortedGramEigenbasis A T n x) a) = 0

If the index ⟨a⟩ is NOT in the fast band at time n (i.e. σ_a(n)^{1/n} ≤ c₀), then the band projector at cut c₀, time n, annihilates the basis vector u_a(n).