The n-scaled forward graded overlap bound #
This module proves forward_graded_overlap: almost everywhere, for every δ > 0 there is a
constant c ≥ 1 such that, eventually in n, for all sorted-eigenbasis indices a and
limit-eigenbasis indices e,
|⟪b' x e, u_a(n)⟫| ≤ c · exp(−n·(max(λ_e − λ_a, 0) − δ)),
where u_a(n) = sortedGramEigenbasis A T n x a and b' x e is the limit-eigenbasis vector at
eigenvalue exp(λ_e). This is the a.e. form of the graded-overlap estimate underlying the
forward Oseledets filtration.
Main results #
toEuclideanLin_cfc_fix_eigenvector: the continuous functional calculus fixes an eigenvector at an eigenvalue where the function takes the value1(a general spectral fact).tendsto_toEuclideanLin_apply: continuity ofM ↦ toEuclideanLin M uin the matrixM.abs_inner_le_of_bandProjector_mass_bound: the limit-transfer reduction — the overlap|⟪w, u⟫|is bounded by any eventual fast-band-mass bound, transferred through the projector limit.exists_spectral_cut: a spectrum-avoiding cut strictly between twoexp-levels exists.forward_graded_overlap: the a.e. graded-overlap bound stated above.
Implementation notes #
Fix x in the full-measure set on which all the hypotheses hold. Write λ_a = lam0 a and
u_a(n) = sortedGramEigenbasis A T n x a.
For a trivial pair λ_e ≤ λ_a we have max(λ_e − λ_a, 0) = 0, so the right-hand side is
c · exp(nδ) ≥ 1 ≥ |⟪b'_e, u_a(n)⟫| by Cauchy–Schwarz (both are unit vectors); the bound holds
for all n with c = 1. The content is the gap pairs λ_e > λ_a, where the time-n slow vector
u_a(n) has overlap with the limit fast band decaying like exp(−n(λ_e − λ_a − δ)). There the
proof proceeds in three steps:
- Gap cut. The finitely many values
{exp(λ_j) : j < d}form a finite set, so one may choose a cutc₀withexp(λ_a) < c₀ < exp(λ_e)avoiding all of them;hidentapplies at this cut. - Two-time chain. The time-
nslow vector has fast-band mass at the time-mcut decaying likeexp(−n(λ_e − λ_a − δ)), uniformly inm ≥ n. This is the analytic content packaged here as the hypothesishchain(see below). - Limit transfer. The limit-eigenbasis vector
b'_eat levelexp(λ_e) > c₀is fixed by the limit band projectorPinf = cfc (indicator (Ioi c₀)) (lambdaHat A T x). Self-adjointness ofPinfand convergence of the time-mband projectors toPinfthen bound|⟪b'_e, u_a(n)⟫|by the step-2 mass bound, with no rate needed for the vanishing term.
The finitely many pairs are combined via eventually_all, and c is the maximum of the
step-2 constants over the gap pairs (independent of n, a, e).
The two-time chain envelope is supplied as the hypothesis hchain: for a gap pair λ_a < λ_e and
any cut c₀ strictly between the two exp-levels, the fast-band mass of the time-n slow
eigenvector, measured by the time-m band projector at c₀, decays like exp(−n(λ_e − λ_a − δ))
uniformly in m ≥ n. A single deterministic operator-norm step over [n, m] is too lossy (it
gives exp((m − n)λ₀ − mλ_e), which diverges as m → ∞ in the gap direction), so the per-step
recursion that keeps the vector in the slow cone is genuinely required.
References #
- D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58 (Lemma 1.4 / Proposition 1.3).
Deterministic helper lemmas #
CFC fixes an arbitrary eigenvector at an eigenvalue where f = 1. If M is Hermitian,
toEuclideanLin M v = lam • v, and f lam = 1, then toEuclideanLin (cfc f M) v = v.
Proof: expand v in the (orthonormal) eigenvector basis; the component ⟪b_j, v⟫ is nonzero only
for eigenvalues eigenvalues j = lam (eigenvectors at distinct eigenvalues are orthogonal because
M is self-adjoint), and there f (eigenvalues j) = f lam = 1.
Continuity of matrix→vector application. If P_m → Pinf (in the finite-dimensional matrix
norm) then toEuclideanLin (P_m) u → toEuclideanLin Pinf u.
Limit-transfer reduction (Ruelle Lemma 1.4, step 3). Let w be a unit vector that is fixed
by the limit band projector Pinf (toEuclideanLin Pinf w = w), with Pinf self-adjoint, and
suppose the time-m band projectors P m converge to Pinf. If the fast-band mass
‖toEuclideanLin (P m) u‖ is eventually bounded by B, then |⟪w, u⟫| ≤ B. (No rate is needed
for the vanishing of Pinf − P m.)
Gap-cut selection (Ruelle Lemma 1.4, step 1). For two levels lo < hi, the open interval
(exp lo, exp hi) is infinite, so it contains a point c₀ avoiding the finite spectrum
{exp (g i) : i}. This supplies a spectral cut strictly between the two exp-levels at which the
band projector and hident may be evaluated.