The fast-index spectral envelope from the graded overlap bound

This module proves vslow_bridge_bound_of_forward_graded, which discharges the hbridge hypothesis of Oseledets.limsup_le_of_mem_vslow (see Oseledets/Lyapunov/LimitSlowSpaceSpectralBound.lean), instantiated at lam := lam0, g := fun x e ↦ lam0 (e : ℕ), b' := b'.

The proof consumes:

• hslowperp — slow orthogonality of b' against vslow;
• hfwdN — the n-scaled forward graded overlap bound;
• hlam0 — per-index singular-exponent convergence;
• hrev — Ruelle's reverse cofactor bound.

It produces the fast-index specTerm envelope outright; the reverse-bound premise inside the hbridge conclusion is introduced and ignored.

Main results

• Oseledets.vslow_bridge_bound_of_forward_graded: for a.e. x, every nonzero vector v of the slow subspace vslow A T (Real.exp t) x and every fast index j (one with t < lam0 j) satisfy the eventual spectral-term bound specTerm T A n x v j ≤ Real.exp (n * (2 * t + ε)).

References

The reverse cofactor bound consumed as the hrev premise is the reverse side of Lemma 1.4 in D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.

theorem Oseledets.vslow_bridge_bound_of_forward_graded {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {d : ℕ} {T : X → X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (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))) (hslowperp : ∀ᵐ (x : X) ∂μ, ∀ (t : ℝ), ∀ v ∈ vslow A T (Real.exp t) x, ∀ (e : Fin d), t < lam0 ↑e → inner ℝ ((b' x) e) v = 0) (hfwdN : ∀ᵐ (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 - δ))) (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))) : ∀ᵐ (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 (-(lam0 ↑i - lam0 ↑e))) → ∀ (j : Fin (Fintype.card (Fin d))), t < lam0 ↑j → ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, specTerm T A n x v j ≤ Real.exp (↑n * (2 * t + ε))

The hbridge hypothesis of limsup_le_of_mem_vslow, derived from the n-scaled forward graded overlap bound, slow orthogonality, singular-exponent convergence, and Ruelle's reverse cofactor bound.