Deterministic core of Ruelle's spectral upper bound

This file formalises, deterministically, the analytic heart of Ruelle's argument (Publ. IHES 50, 1979, Lemma 1.4 / Prop 1.3) for the per-vector spectral upper bound

limsup (1/n) log ‖Mⁿ v‖ ≤ λ⁽ʳ⁾ for v in the limit slow space.

We abstract the SVD data of a sequence of operators f n : E →ₗ E on a finite-dimensional real inner product space E by:

• a per-time orthonormal right-singular basis e n : OrthonormalBasis (Fin d) ℝ E;
• per-time singular values σ n : Fin d → ℝ (≥ 0);
• the defining Parseval identity ‖f n u‖² = Σ_j (σ n j)² · ⟪e n j, u⟫².

From this single identity we derive both halves of Ruelle's one-step sandwich:

• normSq_apply_le_of_mem_span — restricted SVD upper bound on a "slow" right-singular span;
• singularValue_norm_proj_le_norm_apply — SVD lower bound via a "fast" right-singular projection.

The convention here matches Ruelle's (increasing): the index set is split by a cut into a "slow / low" part (small indices, small singular values) and a "fast / high" part (large indices, large singular values).

Main results

• oneStep_sandwich: the one-step two-sided estimate. For u in the slow span at time n, the fast projection of f (n+1) u decays at the full pairwise band gap (t·‖fastProj‖ ≤ b·s·‖u‖), combining the slow SVD upper bound at time n with the fast SVD lower bound at time n+1 through the one-step operator bound b.
• The k-uniform forward leakage chain. geometric_recursion solves the discrete linear recursion a(i+1) ≤ q·a i + c i exactly; geometric_recursion_uniform and chain_leakage_exp package it with a uniform source rate / explicit exp rates, giving the sub-exponential envelope a k ≤ exp(-kγ)·a 0 + R·k·exp(-(k-1)·min γ γ') at the full pairwise gap. This is the analytic engine of Ruelle's Lemma 1.4 band-distance induction (his displayed geometric-series computation).
• orthogonal_block_mass_symm: the reverse-side block-norm symmetry. For any orthonormal change of basis the off-diagonal block over (A,Aᶜ) carries the same squared (Frobenius) mass as the transposed block over (Aᶜ,A), so the slow→fast and fast→slow leakages coincide. This is pure orthogonality (Parseval in each basis), pinning the reverse side to the forward rate for the dominant gap.
• normSq_apply_le_band_sum: the band-grouped Parseval envelope (Ruelle's part b). For a partition of the right-singular indices into bands with per-band singular-value caps, ‖f n v‖² ≤ Σ_r (cap r)²·‖fastProj n (band r) v‖²; fed the leakage envelopes this yields the λ⁽ᵖ⁾ growth.

structure Oseledets.RuelleCofactor.SVDData (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : ℕ) : Type u_2

SVD data for a sequence of operators on a finite-dimensional real inner product space.

e n is the time-n orthonormal right-singular basis, σ n j ≥ 0 the j-th singular value, and apply n u = f n u the image, satisfying the Parseval identity ‖apply n u‖² = Σ_j (σ n j)² ⟪e n j, u⟫².

• e : ℕ → OrthonormalBasis (Fin d) ℝ E

  The (right-singular) orthonormal basis at time n.

• σ : ℕ → Fin d → ℝ

  The singular values at time n.

• σ_nonneg (n : ℕ) (j : Fin d) : 0 ≤ self.σ n j

  Singular values are nonnegative.

• apply : ℕ → E → E

  The image of u under the time-n operator.

• normSq_apply (n : ℕ) (u : E) : ‖self.apply n u‖ ^ 2 = ∑ j : Fin d, self.σ n j ^ 2 * inner ℝ ((self.e n) j) u ^ 2

  The Parseval / SVD identity for the squared norm of the image.

theorem Oseledets.RuelleCofactor.SVDData.normSq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) (n : ℕ) (u : E) : ‖u‖ ^ 2 = ∑ j : Fin d, inner ℝ ((S.e n) j) u ^ 2

Parseval for the orthonormal basis: ‖u‖² = Σ_j ⟪e n j, u⟫².

theorem Oseledets.RuelleCofactor.SVDData.normSq_apply_le_of_mem_span {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) (n : ℕ) (lo : Finset (Fin d)) (s : ℝ) (hs : 0 ≤ s) (hσ : ∀ j ∈ lo, S.σ n j ≤ s) (u : E) (hu : u ∈ Submodule.span ℝ (Set.range fun (j : ↥lo) => (S.e n) ↑j)) : ‖S.apply n u‖ ^ 2 ≤ s ^ 2 * ‖u‖ ^ 2

SVD upper bound on a slow span. If u lies in the span of the right-singular vectors e n j with j in lo (the "slow / low" indices), and every such singular value is ≤ s, then ‖f n u‖ ≤ s · ‖u‖. Pure SVD: in the Parseval sum only the lo-terms survive, each bounded by s² ⟪e n j, u⟫².

theorem Oseledets.RuelleCofactor.SVDData.singularValue_norm_proj_le_norm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) (n : ℕ) (hi : Finset (Fin d)) (t : ℝ) (ht : 0 ≤ t) (hσ : ∀ j ∈ hi, t ≤ S.σ n j) (u : E) : (t * ‖∑ j ∈ hi, inner ℝ ((S.e n) j) u • (S.e n) j‖) ^ 2 ≤ ‖S.apply n u‖ ^ 2

SVD lower bound via a fast projection. Fix a "fast / high" index set hi with every singular value there ≥ t ≥ 0. Let w = Σ_{j ∈ hi} ⟪e n j, u⟫ • e n j be the orthogonal projection of u onto the fast span. Then t · ‖w‖ ≤ ‖f n u‖.

The one-step two-sided sandwich

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

The orthogonal projection of u onto the span of the time-n right-singular vectors with index in hi (the "fast" band at time n): Σ_{j ∈ hi} ⟪e n j, u⟫ • e n j.

Equations

• S.fastProj n hi u = ∑ j ∈ hi, inner ℝ ((S.e n) j) u • (S.e n) j

theorem Oseledets.RuelleCofactor.SVDData.normSq_fastProj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) (n : ℕ) (hi : Finset (Fin d)) (u : E) : ‖S.fastProj n hi u‖ ^ 2 = ∑ j ∈ hi, inner ℝ ((S.e n) j) u ^ 2

‖fastProj n hi u‖² = Σ_{j ∈ hi} ⟪e n j, u⟫² (orthonormality of e n).

theorem Oseledets.RuelleCofactor.SVDData.singularValue_norm_fastProj_le_norm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) (n : ℕ) (hi : Finset (Fin d)) (t : ℝ) (ht : 0 ≤ t) (hσ : ∀ j ∈ hi, t ≤ S.σ n j) (u : E) : (t * ‖S.fastProj n hi u‖) ^ 2 ≤ ‖S.apply n u‖ ^ 2

Restated lower bound in terms of fastProj: t · ‖fastProj n hi u‖ ≤ ‖f n u‖.

theorem Oseledets.RuelleCofactor.SVDData.oneStep_sandwich {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) (n : ℕ) (lo hi : Finset (Fin d)) (s t b : ℝ) (hs : 0 ≤ s) (ht : 0 ≤ t) (hb : 0 ≤ b) (hσlo : ∀ j ∈ lo, S.σ n j ≤ s) (hσhi : ∀ j ∈ hi, t ≤ S.σ (n + 1) j) (u : E) (hu : u ∈ Submodule.span ℝ (Set.range fun (j : ↥lo) => (S.e n) ↑j)) (hstep : ‖S.apply (n + 1) u‖ ≤ b * ‖S.apply n u‖) : t * ‖S.fastProj (n + 1) hi u‖ ≤ b * s * ‖u‖

Ruelle's one-step two-sided SVD sandwich.

Fix consecutive times n, n+1. Let u lie in the time-n slow span (indices lo, each singular value ≤ s), and let hi be a fast band at time n+1 (each singular value ≥ t > 0). Suppose the one-step operator bound ‖f (n+1) u‖ ≤ b · ‖f n u‖ holds with b ≥ 0. Then the time-(n+1) fast projection of u satisfies

t · ‖fastProj (n+1) hi u‖  ≤  b · s · ‖u‖ .

This is the leakage at the full pairwise band gap: combining the SVD lower bound at time n+1 (fastProj term) with the SVD upper bound on the slow span at time n (s‖u‖) through the one-step step bound b.

The band-grouped Parseval envelope

theorem Oseledets.RuelleCofactor.SVDData.band_partial_normSq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) (n : ℕ) (B : Finset (Fin d)) (Sr : ℝ) (hSr : 0 ≤ Sr) (hσ : ∀ j ∈ B, S.σ n j ≤ Sr) (v : E) : ∑ j ∈ B, S.σ n j ^ 2 * inner ℝ ((S.e n) j) v ^ 2 ≤ Sr ^ 2 * ‖S.fastProj n B v‖ ^ 2

Band-restricted Parseval mass. The partial Parseval sum over a band B is exactly Σ_{j ∈ B} (σ n j)² ⟪e n j, v⟫², and is bounded by Sr² · ‖fastProj n B v‖² whenever every singular value in B is ≤ Sr. (This is the per-band term that, with the leakage envelope on ‖fastProj n B v‖, yields the λ⁽ᵖ⁾ growth.)

theorem Oseledets.RuelleCofactor.SVDData.normSq_apply_le_band_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (S : SVDData E d) {ι : Type u_2} (n : ℕ) (bands : Finset ι) (B : ι → Finset (Fin d)) (Sr : ι → ℝ) (hSr : ∀ r ∈ bands, 0 ≤ Sr r) (hσ : ∀ r ∈ bands, ∀ j ∈ B r, S.σ n j ≤ Sr r) (hdisj : (↑bands).PairwiseDisjoint B) (hcover : Finset.univ ⊆ bands.biUnion B) (v : E) : ‖S.apply n v‖ ^ 2 ≤ ∑ r ∈ bands, Sr r ^ 2 * ‖S.fastProj n (B r) v‖ ^ 2

Band-grouped SVD envelope. Let bands : Finset ι index a partition of Fin d into bands via B : ι → Finset (Fin d) (covering all indices: Finset.univ ⊆ ⋃_{r ∈ bands} B r), with a per-band singular-value cap Sr : ι → ℝ (σ n j ≤ Sr r for j ∈ B r, 0 ≤ Sr r). Then

‖f n v‖²  ≤  Σ_{r ∈ bands} (Sr r)² · ‖fastProj n (B r) v‖² .

This sums the band-restricted Parseval masses (band_partial_normSq_le). With the leakage envelopes on each ‖fastProj n (B r) v‖, the right side is ≤ (#bands)·K²·exp(2n(λ⁽ᵖ⁾+δ))·‖v‖², giving limsup (1/n) log‖f n v‖ ≤ λ⁽ᵖ⁾ (Ruelle's part b).

The k-uniform forward chain (geometric recursion)

Ruelle's Lemma 1.4 controls the leakage of slow mass into the fast bands accumulated over the window n, n+1, …, n+k. Iterating the one-step sandwich along the window produces, for the mass arriving in a fixed fast band, a discrete linear recursion

a (i+1)  ≤  q · a i  +  R · ρ^i ,

whose solution is the geometric envelope below. Here a i is the band-leakage budget at time n+i, q ∈ [0,1) the one-step survival/decay factor of the gap, R·ρ^i the fresh mass injected at step i (itself decaying at the source rate ρ). This is the core analytic engine of Lemma 1.4: the band-distance induction reduces to iterating exactly this recursion, and the resulting geometric sum is Ruelle's displayed computation. It is stated and proved abstractly so it can be driven by the sandwich factors at each step.

theorem Oseledets.RuelleCofactor.SVDData.geometric_recursion (a c : ℕ → ℝ) (q : ℝ) (hq : 0 ≤ q) (hrec : ∀ (i : ℕ), a (i + 1) ≤ q * a i + c i) (k : ℕ) : a k ≤ q ^ k * a 0 + ∑ i ∈ Finset.range k, q ^ (k - 1 - i) * c i

Discrete geometric recursion (Grönwall-type). If a (i+1) ≤ q · a i + c i for all i, with 0 ≤ q, then for every k,

a k  ≤  q^k · a 0  +  Σ_{i<k} q^{k-1-i} · c i .

This is the exact solution of Ruelle's per-step leakage recursion; the second term is the accumulated freshly-injected mass, each contribution surviving k-1-i further steps at factor q.

theorem Oseledets.RuelleCofactor.SVDData.geometric_recursion_uniform (a : ℕ → ℝ) (q ρ R : ℝ) (hq : 0 ≤ q) (hρ : 0 ≤ ρ) (hR : 0 ≤ R) (hrec : ∀ (i : ℕ), a (i + 1) ≤ q * a i + R * ρ ^ i) (k : ℕ) : a k ≤ q ^ k * a 0 + R * ↑k * max q ρ ^ (k - 1)

Geometric envelope with a uniform source rate. Specialising geometric_recursion to the source c i = R · ρ^i with 0 ≤ ρ, 0 ≤ R, the accumulated sum collapses (each surviving term has total exponent (k-1-i)+i = k-1) to the sub-exponential envelope

a k  ≤  q^k · a 0  +  R · k · (max q ρ)^(k-1) .

The k·M^(k-1) envelope suffices for the Lyapunov application: it is sub-exponential in k and is killed by the strictly-positive band gap in the exponent. This is the form consumed by the band-distance induction.

theorem Oseledets.RuelleCofactor.SVDData.chain_leakage_exp (a : ℕ → ℝ) (γ γ' R : ℝ) (hR : 0 ≤ R) (hrec : ∀ (i : ℕ), a (i + 1) ≤ Real.exp (-γ) * a i + R * Real.exp (-γ') ^ i) (k : ℕ) : a k ≤ Real.exp (-↑k * γ) * a 0 + R * ↑k * Real.exp (-(↑k - 1) * min γ γ')

k-uniform forward leakage envelope (exponential form).

This is Ruelle's Lemma 1.4 leakage bound in its application-facing form. Model the band-leakage budget a i over the window n, n+1, … by the recursion a (i+1) ≤ q·a i + R·ρ^i, where:

• a 0 is the initial slow mass (= ‖u‖, taken ≤ 1 for a unit vector);
• q = exp(-(γ)) is the one-step gap survival factor, γ ≥ 0 the per-step band gap;
• R·ρ^i is the freshly injected leakage at step i, with source rate ρ = exp(-γ') ≤ exp(-γ).

Then, writing M = max q ρ = exp(-(min γ γ')), the time-(n+k) leakage obeys

a k  ≤  exp(-k·γ)·a 0  +  R·k·exp(-(k-1)·min γ γ') ,

an envelope decaying at the full pairwise gap min γ γ' (up to the harmless polynomial k and boundary factor). This packages geometric_recursion_uniform with explicit exp rates so it composes directly with the SVD sandwich factors.

The reverse side (orthogonal block-norm symmetry)

Ruelle's reverse-side estimate bounds the entries of the orthogonal change-of-basis matrix S_{ij} = ⟪e_n j, e_m i⟫ on the other side of the band diagonal (slow i at time m, fast j at time n) at the full pairwise rate. The deep route is the cofactor/permutation expansion. Here we record the elementary structural fact that already pins the reverse-side block to the same Frobenius mass as the forward-side block, which is the quantitative heart of the rate transfer for the dominant gap: for any orthonormal change of basis, the off-diagonal block over (A, Aᶜ) carries the same squared mass as the transposed block over (Aᶜ, A).

This is purely orthogonality (SᵀS = I = SSᵀ, realised as Parseval in each basis): no permutation combinatorics. It gives the reverse-side leakage Σ_{j∈Aᶜ}⟪e_m i, e_n j⟫² (summed over slow i∈A) exactly in terms of the forward-side leakage, hence at the forward rate.

theorem Oseledets.RuelleCofactor.SVDData.orthonormalBasis_normSq_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (b : OrthonormalBasis (Fin d) ℝ E) (u : E) : ‖u‖ ^ 2 = ∑ i : Fin d, inner ℝ (b i) u ^ 2

Parseval in an orthonormal basis b: ‖u‖² = Σ_i ⟪b i, u⟫².

theorem Oseledets.RuelleCofactor.SVDData.orthogonal_block_mass_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {d : ℕ} (b b' : OrthonormalBasis (Fin d) ℝ E) (A : Finset (Fin d)) : ∑ i ∈ A, ∑ j ∈ Aᶜ, inner ℝ (b' i) (b j) ^ 2 = ∑ i ∈ Aᶜ, ∑ j ∈ A, inner ℝ (b' i) (b j) ^ 2

Orthogonal off-diagonal block-norm symmetry. For two orthonormal bases b, b' of a finite-dimensional real inner product space and any index set A, the cross-overlap mass of "A-rows against Aᶜ-columns" equals that of "Aᶜ-rows against A-columns":

Σ_{i∈A} Σ_{j∈Aᶜ} ⟪b' i, b j⟫²  =  Σ_{i∈Aᶜ} Σ_{j∈A} ⟪b' i, b j⟫² .

Equivalently the slow→fast leakage equals the fast→slow leakage. Proof: each side equals |A| − Σ_{i∈A}Σ_{j∈A} ⟪b' i, b j⟫², using that every row sums to 1 (Parseval of b' i in basis b) and every column sums to 1 (Parseval of b j in basis b').