Chain recursion for the fast-band-mass envelope

Deterministic engine for the uniform-in-m fast-band-mass envelope appearing in Ruelle's proof of the multiplicative ergodic theorem (the proof of Lemma 1.4 in [Ruelle, Ergodic theory of differentiable dynamical systems]): the slow/fast orthogonal decomposition over an SVDData, the one-step band-leakage recursion (oneStep_recursion, an application of oneStep_sandwich), the contraction-free chain solver (chain_geometric_sum), and the band↔SVD adapter identifying bandProjector with the explicit fast projection (toEuclideanLin_bandProjector_eq_fastProj), plus band-mass monotonicity in the cut and the lower-bound lemma bandProjector_mass_ge_abs_inner_of_fix.

NOTE: the lower-bound lemma shows the envelope at an arbitrary cut c₀ ∈ (exp λ_a, exp λ_e) is unprovable when an intermediate stratum λ_a < λ_c < λ_e lies above the cut (the band then contains the λ_c Oseledets direction, whose overlap with u_a(n) decays only at rate λ_c − λ_a). The sound statement restricts the cut to the top gap below λ_e; the engine here closes that corrected envelope.

Main results

• Oseledets.RuelleCofactor.SVDData.oneStep_recursion: the deterministic one-step band-leakage recursion for the fast-band mass along an SVD chain.
• Oseledets.RuelleCofactor.SVDData.chain_geometric_sum: the contraction-free chain solver — a recursion a (i+1) ≤ a i + R·ρ^i with a 0 = 0 is bounded by R/(1−ρ) uniformly in the index.
• Oseledets.toEuclideanLin_bandProjector_eq_fastProj: the band projector equals the explicit fast projection over the SVD chain Oseledets.chainSVD.
• Oseledets.norm_bandProjector_mono: band mass is monotone in the cut.
• Oseledets.bandProjector_mass_ge_abs_inner_of_fix: a uniform band-mass bound dominates the overlap with any unit vector fixed by the limit projector (the obstruction lemma for the arbitrary-cut envelope).

Implementation notes

Fix x in the a.e.-good set. Write σ_j(t) = (toEuclideanLin (cocycle A T t x)).singularValues j (antitone in j), u_a(n) = sortedGramEigenbasis A T n x ⟨a⟩ (a unit right-singular vector of cocycle A T n x), λ_j = lam0 j.

We are given a gap pair λ_a < λ_e, a cut c₀ with exp λ_a < c₀ < exp λ_e, and we must bound, uniformly in m ≥ n, ‖P^{>c₀}_m u_a(n)‖ ≤ C·exp(−n(λ_e − λ_a − δ)), where P^{>c₀}_m = bandProjector A T (indicator (Ioi c₀) 1) m x is the orthogonal projector onto the span of the time-m Gram eigenvectors u_j(m) whose exp-scale eigenvalue σ_j(m)^{1/m} exceeds c₀.

The deterministic SVD chain (Oseledets.RuelleCofactor.SVDData)

Instantiate Oseledets.RuelleCofactor.SVDData (EuclideanSpace ℝ (Fin d)) (card (Fin d)) at the point x by:

• e t := sortedGramEigenbasis A T t x — the time-t Gram eigenbasis (right-singular basis);
• σ t j := σ_j(t) — the time-t singular values;
• apply t u := toEuclideanLin (cocycle A T t x) u. The Parseval field is norm_sq_cocycle_apply_eq_sum_singularValues (with real_inner_comm to flip the inner-product order to the ⟪e j, u⟫ convention of Oseledets.Lyapunov.RuelleCore).

For this S:

• S.fastProj m hi u = Σ_{j∈hi} ⟪e m j, u⟫ • e m j and, when hi = hiBand m := {j : c₀ < σ_j(m)^{1/m}}, ‖S.fastProj m hi u‖ = ‖toEuclideanLin (P^{>c₀}_m) u‖ (the band projector is the orthogonal projection onto exactly this span — proved in toEuclideanLin_bandProjector_eq_fastProj).

The recursion

u := u_a(n) lies in the time-n slow span loBand n := {j : σ_j(n)^{1/n} ≤ c₀} (it equals the single basis vector u_a(n), and eventually σ_a(n)^{1/n} < c₀ so a ∈ loBand n). For each step t = n+k → t+1:

• the slow cap at time t for the slow span is s_t := c₀^t (every slow eigenvalue σ_j(t) ≤ c₀^t);
• the fast floor at time t+1 for the fast band is tt_{t+1} := c₀^{t+1};
• the one-step bound is ‖A⁽ᵗ⁺¹⁾u‖ ≤ b_t ‖A⁽ᵗ⁾u‖ with b_t := ‖A(Tᵗx)‖. oneStep_sandwich then gives c₀^{t+1}·‖fastProj(t+1) u‖ ≤ b_t · c₀^t · ‖u‖ i.e. ‖fastProj(t+1) u‖ ≤ (b_t/c₀)·‖u‖. This is too lossy on its own (the b_t are only tempered, b_t ≤ exp(tη)). Ruelle's improvement: the slow part of u at time t — not all of u — feeds the fast band at t+1, and the slow part's mass is what fastProj(t) u already controls. The correct one-step recursion (his displayed computation) is, with a_k := ‖fastProj(n+k) u‖: a_{k+1} ≤ exp(−γ̄)·a_k + R·exp(−k γ'), where γ̄ = λ_e − λ_a − δ* is the per-step gap survival and R·exp(−kγ') the freshly-injected slow leakage. chain_leakage_exp solves this: a_k ≤ exp(−kγ̄)·a_0 + R·k·exp(−(k−1)·min γ̄ γ'). With a_0 = 0 (at m = n, u_a(n) is orthogonal to the fast band, since eventually σ_a(n)^{1/n} < c₀), a_k ≤ R·k·exp(−(k−1)·min γ̄ γ'), and since a_k is measured at absolute time m = n+k, this carries the exp(−n γ) prefactor. The polynomial k and the exp(−kγ̄) tail give a constant uniform in k = m − n.

The δ*/stratum-gap and c₀-endpoint subtleties are handled where this engine is consumed. The deterministic recursion engine itself (oneStep_sandwich, chain_leakage_exp) is proved in Oseledets.Lyapunov.RuelleCore; this file builds the band / SVDData adapter on top of it.

References

• D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58 (the proof of Lemma 1.4).

noncomputable def Oseledets.RuelleCofactor.SVDData.slowProj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D : ℕ} (S : SVDData E D) (t : ℕ) (hi : Finset (Fin D)) (u : E) : E

The slow projection onto the complement of hi.

Equations

• S.slowProj t hi u = ∑ j ∈ hiᶜ, inner ℝ ((S.e t) j) u • (S.e t) j

theorem Oseledets.RuelleCofactor.SVDData.fastProj_add_slowProj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D : ℕ} (S : SVDData E D) (t : ℕ) (hi : Finset (Fin D)) (u : E) : S.fastProj t hi u + S.slowProj t hi u = u

u reconstructs as fast + slow.

theorem Oseledets.RuelleCofactor.SVDData.slowProj_mem_span {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D : ℕ} (S : SVDData E D) (t : ℕ) (hi : Finset (Fin D)) (u : E) : S.slowProj t hi u ∈ Submodule.span ℝ (Set.range fun (j : ↥hiᶜ) => (S.e t) ↑j)

The slow projection lies in the slow span (the span of e t j, j ∈ hiᶜ).

theorem Oseledets.RuelleCofactor.SVDData.norm_fastProj_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D : ℕ} (S : SVDData E D) (t : ℕ) (hi : Finset (Fin D)) (u : E) : ‖S.fastProj t hi u‖ ≤ ‖u‖

The fast projection is contractive: ‖fastProj t hi u‖ ≤ ‖u‖.

theorem Oseledets.RuelleCofactor.SVDData.fastProj_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D : ℕ} (S : SVDData E D) (t : ℕ) (hi : Finset (Fin D)) (u v : E) : S.fastProj t hi (u + v) = S.fastProj t hi u + S.fastProj t hi v

fastProj t hi is additive.

theorem Oseledets.RuelleCofactor.SVDData.oneStep_recursion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {D : ℕ} (S : SVDData E D) (t : ℕ) (hiT hiT1 : Finset (Fin D)) (s tt b : ℝ) (hs : 0 ≤ s) (htt : 0 < tt) (hb : 0 ≤ b) (hσlo : ∀ j ∈ hiTᶜ, S.σ t j ≤ s) (hσhi : ∀ j ∈ hiT1, tt ≤ S.σ (t + 1) j) (u : E) (hstep : ‖S.apply (t + 1) (S.slowProj t hiT u)‖ ≤ b * ‖S.apply t (S.slowProj t hiT u)‖) : ‖S.fastProj (t + 1) hiT1 u‖ ≤ ‖S.fastProj t hiT u‖ + b * s / tt * ‖S.slowProj t hiT u‖

One-step recursion (deterministic). Fix consecutive times t, t+1 with fast bands hi t, hi (t+1). Assume the slow cap s at time t (every σ t j ≤ s for j ∈ (hi t)ᶜ), the fast floor tt > 0 at time t+1 (every σ (t+1) j ≥ tt for j ∈ hi (t+1)), and the step bound ‖apply (t+1) w‖ ≤ b·‖apply t w‖ for the slow part w = slowProj t (hi t) u. Then

‖fastProj (t+1) (hi (t+1)) u‖
  ≤ ‖fastProj t (hi t) u‖ + (b·s/tt)·‖slowProj t (hi t) u‖. 

theorem Oseledets.RuelleCofactor.SVDData.chain_geometric_sum (a : ℕ → ℝ) (R ρ : ℝ) (hR : 0 ≤ R) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (h0 : a 0 = 0) (hrec : ∀ (i : ℕ), a (i + 1) ≤ a i + R * ρ ^ i) (k : ℕ) : a k ≤ R / (1 - ρ)

Contraction-free chain solution. If a 0 = 0 and a (i+1) ≤ a i + R·ρ^i for all i with 0 ≤ R, 0 ≤ ρ < 1, then a k ≤ R/(1−ρ) for every k — uniformly in k. (Geometric series; no per-step contraction needed because the source already decays.)

The band / SVDData adapter

bandProjector A T χ m x = cfc χ (qpow A T m x), and qpow = cfc (·^{1/2m}) (gram), so by CFC composition bandProjector A T χ m x = cfc (χ ∘ (·^{1/2m})) (gram A T m x). Hence it acts on the sorted Gram eigenbasis u_j(m) = sortedGramEigenbasis A T m x j diagonally, with eigenvalue χ (σ_j(m)^{1/m}) (the indicator of the exp-scale band).

theorem Oseledets.toEuclideanLin_bandProjector_sortedGramEigenbasis {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))) : (Matrix.toEuclideanLin (bandProjector A T χ m x)) ((sortedGramEigenbasis A T m x) j) = χ (⋯.eigenvalues₀ j) • (sortedGramEigenbasis A T m x) j

The band projector acts diagonally on the sorted Gram eigenbasis with eigenvalue χ (qpow-eigenvalue).

noncomputable def Oseledets.chainSVD {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : RuelleCofactor.SVDData (EuclideanSpace ℝ (Fin d)) (Fintype.card (Fin d))

The SVD chain data at a point x: time-t Gram eigenbasis, singular values, and the cocycle action. The Parseval field is norm_sq_cocycle_apply_eq_sum_singularValues.

Equations

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

@[simp]

theorem Oseledets.chainSVD_apply {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (t : ℕ) (u : EuclideanSpace ℝ (Fin d)) : (chainSVD A T x).apply t u = (Matrix.toEuclideanLin (cocycle A T t x)) u

@[simp]

theorem Oseledets.chainSVD_e {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (t : ℕ) : (chainSVD A T x).e t = sortedGramEigenbasis A T t x

@[simp]

theorem Oseledets.chainSVD_σ {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (t : ℕ) (j : Fin (Fintype.card (Fin d))) : (chainSVD A T x).σ t j = (Matrix.toEuclideanLin (cocycle A T t x)).singularValues ↑j

noncomputable def Oseledets.hiBand {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (m : ℕ) (x : X) (c₀ : ℝ) : Finset (Fin (Fintype.card (Fin d)))

The "fast band" finset at time m: indices whose exp-scale (qpow) eigenvalue exceeds c₀.

Equations

• Oseledets.hiBand A T m x c₀ = {j : Fin (Fintype.card (Fin d)) | c₀ < ⋯.eigenvalues₀ j}

theorem Oseledets.toEuclideanLin_bandProjector_eq_fastProj {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (m : ℕ) (x : X) (c₀ : ℝ) (u : EuclideanSpace ℝ (Fin d)) : (Matrix.toEuclideanLin (bandProjector A T ((Set.Ioi c₀).indicator 1) m x)) u = (chainSVD A T x).fastProj m (hiBand A T m x c₀) u

The band projector applied to u equals the explicit fast projection S.fastProj m (hiBand …) u onto the time-m Gram eigenvectors above the cut.

theorem Oseledets.norm_bandProjector_mono {X : Type u_1} [MeasurableSpace X] {d : ℕ} {T : X → X} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (m : ℕ) (x : X) {c₁ c₀ : ℝ} (hc : c₁ ≤ c₀) (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‖

Band monotonicity in the cut. If c₁ ≤ c₀ then the higher-cut band mass is dominated by the lower-cut band mass: ‖P^{>c₀}_m u‖ ≤ ‖P^{>c₁}_m u‖. (Higher cut ⟹ smaller fast index set ⟹ smaller projection.)

Obstruction: the arbitrary-cut envelope is too strong under intermediate strata

The deterministic chain (above) shows the fast-band mass ‖P^{>c₀}_m u_a(n)‖ decays at the rate of the first lam0-stratum strictly above log c₀. An envelope claiming decay at the rate λ_e − λ_a for an arbitrary cut c₀ ∈ (exp λ_a, exp λ_e) is strictly stronger. When a third stratum λ_c satisfies λ_a < λ_c < λ_e, a cut c₀ ∈ (exp λ_a, exp λ_c) produces a band that contains the λ_c Oseledets direction, so the band mass is ≍ exp(−n(λ_c − λ_a)), which is asymptotically larger than the claimed C·exp(−n(λ_e − λ_a − δ)) (for δ < λ_e − λ_c). Hence the envelope at that cut is false.

The lemma below makes the obstruction precise: the uniform-in-m band-mass envelope dominates the overlap with any unit vector that the limit projector Pinf fixes — including an intermediate-stratum limit eigenvector b'_c (which Pinf fixes because exp λ_c > c₀). So the arbitrary-cut envelope at this cut forces

|⟪b'_c, u_a(n)⟫|  ≤  C · exp(−n(λ_e − λ_a − δ)) .

But the genuine graded-overlap rate between the adjacent strata λ_a < λ_c is only λ_c − λ_a (this is exactly the conclusion forward_graded_overlap proves for the pair (a,c), and the overlap is generically of that exact order — nonzero leading coefficient). Whenever the adjacent overlap is non-degenerate (the generic case), |⟪b'_c, u_a(n)⟫| ≍ exp(−n(λ_c − λ_a)), which exceeds C·exp(−n(λ_e − λ_a − δ)) for all large n (take δ < λ_e − λ_c). Hence the arbitrary-cut envelope is not provable in general: it is a strictly stronger claim than the band mass actually satisfies at cuts c₀ ∈ (exp λ_a, exp λ_c) whenever a third stratum λ_c ∈ (λ_a, λ_e) exists.

NOTE. The conclusion of forward_graded_overlap is still correct (the λ_e-eigenvector overlap |⟪b'_e, u_a(n)⟫| does decay at λ_e − λ_a); only the route through the arbitrary-cut envelope — bounding that overlap by the band mass at an arbitrary cut and claiming the band mass also decays at λ_e − λ_a — is unsound when intermediate strata are present. A sound envelope must restrict the cut to lie above the immediately preceding stratum below λ_e (i.e. c₀ ∈ (exp λ_{e−1}, exp λ_e)), or the consumer must transfer to the band at the cut whose first stratum above is exactly λ_e.

theorem Oseledets.bandProjector_mass_ge_abs_inner_of_fix {d : ℕ} {P : ℕ → Matrix (Fin d) (Fin d) ℝ} {Pinf : Matrix (Fin d) (Fin d) ℝ} (hP : Filter.Tendsto P Filter.atTop (nhds Pinf)) (hPinfsa : IsSelfAdjoint Pinf) (w u : EuclideanSpace ℝ (Fin d)) (hwnorm : ‖w‖ = 1) (hfix : (Matrix.toEuclideanLin Pinf) w = w) {B : ℝ} (hbound : ∀ᶠ (m : ℕ) in Filter.atTop, ‖(Matrix.toEuclideanLin (P m)) u‖ ≤ B) : |inner ℝ w u| ≤ B