The per-vector spectral upper bound on the limit slow space

For an ergodic cocycle A⁽ⁿ⁾ = cocycle A T n of invertible matrices over (X, μ, T), a vector in the limit slow space vslow A T (exp t) x has normalized log-growth bounded above by the threshold t:

∀ᵐ x, ∀ t, ∀ v ∈ vslow A T (exp t) x, v ≠ 0 → limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ t.

The reverse-side overlap transfer of Oseledets.RuelleCofactor combines with the almost-everywhere singular-value asymptotics to yield this bound.

Main results

• Oseledets.specTerm_envelope_slow: at a slow singular index (one whose exponent satisfies lamj ≤ lami), the spectral term obeys specTerm ≤ exp(n(2 lami + ε)) eventually, by pure SVD and Cauchy–Schwarz; no overlap-decay input is needed.
• Oseledets.reverse_graded_overlap_bound: for orthonormal bases b, b', forward graded decay of the change-of-basis entries together with Ruelle's cofactor bound yields the transposed-graded reverse decay.
• Oseledets.limsup_le_of_mem_vslow: the per-vector spectral upper bound itself.

Implementation notes

The bound limsup_le_of_mem_vslow follows from the envelope criterion limsup_inv_mul_log_norm_cocycle_apply_le. Its two side conditions hold outright: positivity 0 < ‖A⁽ⁿ⁾ v‖ for every n from cocycle_apply_ne_zero (det (A x) ≠ 0 makes A⁽ⁿ⁾ invertible, hence injective on v ≠ 0), and the IsCoboundedUnder (· ≤ ·) condition from a bounded-below lower bound (isCoboundedUnder_le_of_boundedUnder_ge).

The criterion takes the per-index envelope specTerm ≤ exp(n(2t + ε)) for every spectral index j. Slow indices (lam j ≤ t) follow from specTerm_envelope_slow. Fast indices (t < lam j) rest on Ruelle's chain of singular-value estimates, entering through two hypotheses: hfwd, the forward graded overlap bound (the level-increasing entries of the change of basis between the limit eigenbasis and the time-n Gram eigenbasis decay at the graded rate, the forward chain of Ruelle's Lemma 1.4); and hbridge, the band-limit bridge from the reverse graded entry bound to the fast-index specTerm envelope (via tendsto_bandProjector_of_gap). The forward bound is converted into the reverse bound by reverse_graded_overlap_bound, which consumes hrev, Ruelle's reverse-side cofactor bound for orthogonal matrices with graded forward decay (Oseledets.RuelleCofactor.entry_reverse_bound_of_orthogonal).

References

• David Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58

Positivity of the cocycle applied to a nonzero vector

theorem Oseledets.eventually_pos_norm_cocycle_apply {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) {v : EuclideanSpace ℝ (Fin d)} (hv : v ≠ 0) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖

Eventual (in fact universal) positivity of ‖A⁽ⁿ⁾ v‖. Since det (A x) ≠ 0, every cocycle matrix A⁽ⁿ⁾ is invertible, hence toEuclideanLin (A⁽ⁿ⁾) is injective, so it sends the nonzero v to a nonzero (positive-norm) vector for every n.

The slow-index specTerm envelope

theorem Oseledets.inner_sq_sortedGramEigenbasis_le {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (n : ℕ) (x : X) (v : EuclideanSpace ℝ (Fin d)) (j : Fin (Fintype.card (Fin d))) : inner ℝ v ((sortedGramEigenbasis A T n x) j) ^ 2 ≤ ‖v‖ ^ 2

The squared overlap with the orthonormal Gram eigenbasis is bounded by ‖v‖² (Cauchy–Schwarz, the basis vectors being unit).

theorem Oseledets.eventually_const_le_exp (C : ℝ) (hC : 0 ≤ C) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, C ≤ Real.exp (↑n * δ)

A nonnegative constant C is eventually dominated by exp(n·δ) for any δ > 0.

theorem Oseledets.specTerm_envelope_slow {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} {v : EuclideanSpace ℝ (Fin d)} {lami lamj : ℝ} (j : Fin (Fintype.card (Fin d))) (hjd : ↑j < d) (hσ : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues ↑j)) Filter.atTop (nhds lamj)) (hslow : lamj ≤ lami) (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, specTerm T A n x v j ≤ Real.exp (↑n * (2 * lami + ε))

The slow-index specTerm envelope. If the j-th singular exponent converges to lamj ≤ lami (a slow index), then specTermⱼ(n) ≤ exp(n(2 lami + ε)) eventually, for every ε > 0. Pure SVD + Cauchy–Schwarz: specTerm = σⱼ²·⟪v,uⱼ⟫² ≤ σⱼ²·‖v‖², with σⱼ² ≤ exp(n(2lamj+ε/2)) ≤ exp(n(2lami+ε/2)) and ‖v‖² ≤ exp(n·ε/2) eventually. No overlap-decay input is needed at a slow index.

The reverse-side graded overlap transfer

An orthonormal change-of-basis matrix S i j = ⟪b' j, b i⟫ is orthogonal (S Sᵀ = 1, pure Parseval). If its forward (level-increasing) entries decay at the graded rate c·exp(-(g j - g i)₊), then Ruelle's cofactor bound hrev transfers this to the reverse (level-decreasing) entries: |S i j| ≤ (d-1)!·c^{d-1}·exp(-(g i - g j)). Oseledets.RuelleCofactor.SVDData.orthogonal_block_mass_symm is the Frobenius-mass companion; here hrev supplies the per-entry graded transfer.

theorem Oseledets.reverse_graded_overlap_bound {d : ℕ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hrev : ∀ (S : Matrix (Fin d) (Fin d) ℝ), S * S.transpose = 1 → ∀ (g : Fin d → ℝ) (c : ℝ), 1 ≤ c → (∀ (a b : Fin d), |S a b| ≤ c * Real.exp (-max (g b - g a) 0)) → ∀ (i j : Fin d), |S i j| ≤ ↑(d - 1).factorial * c ^ (d - 1) * Real.exp (-(g i - g j))) (b b' : OrthonormalBasis (Fin d) ℝ E) (g : Fin d → ℝ) (c : ℝ) (hc : 1 ≤ c) (hfwd : ∀ (a e : Fin d), |inner ℝ (b' e) (b a)| ≤ c * Real.exp (-max (g e - g a) 0)) (i j : Fin d) : |inner ℝ (b' j) (b i)| ≤ ↑(d - 1).factorial * c ^ (d - 1) * Real.exp (-(g i - g j))

Reverse-side graded overlap transfer. For orthonormal bases b, b' of a finite-dimensional real inner product space, the change-of-basis matrix S i j = ⟪b' j, b i⟫ is orthogonal; given the forward graded decay of its entries, the cofactor bound hrev yields the transposed-graded reverse bound on every entry.

The per-vector spectral upper bound

The Ruelle-dependent content enters through three hypotheses:

• hrev — Ruelle's reverse-side cofactor bound (Oseledets.RuelleCofactor.entry_reverse_bound_of_orthogonal), with the exact statement needed;
• hfwd — the forward graded overlap bound, uniform in the band index, the output of the forward chain of Ruelle's Lemma 1.4 (Oseledets.RuelleCofactor.SVDData.oneStep_sandwich and Oseledets.RuelleCofactor.chain_leakage_exp, the full pairwise gap);
• hbridge — the band-limit bridge: from the reverse graded entry bound to the fast-index specTerm envelope, via the band-limit identification tendsto_bandProjector_of_gap.

The slow indices (lam j ≤ t) need no Ruelle input; they follow from specTerm_envelope_slow.

theorem Oseledets.limsup_le_of_mem_vslow {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {d : ℕ} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (hT : Ergodic T μ) (_hTmeas : Measurable 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)⁻¹) μ) (hrev : ∀ (S : Matrix (Fin d) (Fin d) ℝ), S * S.transpose = 1 → ∀ (g : Fin d → ℝ) (c : ℝ), 1 ≤ c → (∀ (a b : Fin d), |S a b| ≤ c * Real.exp (-max (g b - g a) 0)) → ∀ (i j : Fin d), |S i j| ≤ ↑(d - 1).factorial * c ^ (d - 1) * Real.exp (-(g i - g j))) (lam : ℕ → ℝ) (hlam : ∀ i < d, ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues i)) Filter.atTop (nhds (lam i))) (b' : X → OrthonormalBasis (Fin d) ℝ (EuclideanSpace ℝ (Fin d))) (g : X → Fin d → ℝ) (hfwd : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), ∀ v ∈ vslow A T (Real.exp t) x, v ≠ 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 (-max (g x e - g x a) 0)) (hbridge : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), ∀ v ∈ vslow A T (Real.exp t) x, v ≠ 0 → (∃ (c : ℝ), 1 ≤ c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i e : Fin d), |inner ℝ ((b' x) e) ((sortedGramEigenbasis A T n x) ⟨↑i, ⋯⟩)| ≤ ↑(d - 1).factorial * c ^ (d - 1) * Real.exp (-(g x i - g x e))) → ∀ (j : Fin (Fintype.card (Fin d))), t < lam ↑j → ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, specTerm T A n x v j ≤ Real.exp (↑n * (2 * t + ε))) : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), ∀ v ∈ vslow A T (Real.exp t) x, v ≠ 0 → Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop ≤ t

Per-vector spectral upper bound on the limit slow space.

For μ-a.e. x, every threshold t, and every nonzero v in the limit slow space vslow A T (exp t) x, the cocycle growth obeys limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ t.

The proof feeds the envelope criterion limsup_inv_mul_log_norm_cocycle_apply_le the per-index specTerm envelopes: slow indices (lam j ≤ t) from specTerm_envelope_slow (no Ruelle input); fast indices (t < lam j) from Ruelle's chain, which enters as two hypotheses:

• hfwd — the forward graded overlap bound, uniform in the band index (Ruelle Lemma 1.4, SVDData.oneStep_sandwich + chain_leakage_exp): the level-increasing entries of the change of basis between the limit eigenbasis b' and the time-n Gram eigenbasis decay at the graded rate.
• hbridge — the band-limit bridge (tendsto_bandProjector_of_gap): from the reverse graded entry bound (produced here by applying hrev via reverse_graded_overlap_bound) to the fast-index specTerm envelope.

The hypothesis hrev is consumed by reverse_graded_overlap_bound, which turns the forward graded decay hfwd into the reverse graded decay that hbridge requires. Positivity and the cobounded side condition are discharged by cocycle_apply_ne_zero and isBoundedUnder_log_norm_cocycle_apply.