Block-rate overlap bounds against sorted Gram singular directions

This file proves the block-specific overlap decay rate consumed by the spectral split of the Oseledets multiplicative ergodic theorem: writing A⁽ⁿ⁾ = cocycle A T n x,

limsup_n (1/n) · log |⟪v, uⱼ(n)⟫| ≤ λᵢ − λ_l,

where v is a slow vector (upper Lyapunov growth lambdaBar A T x v ≤ λᵢ) and uⱼ(n) = sortedGramEigenbasis A T n x j is a sorted Gram singular vector whose singular value σⱼ(n) has exponent λ_l. For a fast direction (λ_l > λᵢ) the rate is the full multi-gap difference λᵢ − λ_l, the sum of all adjacent spectral gaps between the two exponents.

Eigenvector-perturbation arguments (Davis–Kahan / sin-Θ bounds) only reach the nearest adjacent gap, because the residual leak at a nested cut is cut-invariant. The proof here instead goes through the sharp Gram-eigenvector cross bound |⟪uⱼ(n), v⟫| ≤ ‖A⁽ⁿ⁾ v‖ / σⱼ(n). The required slow-growth input limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ is not an output of the spectral split it feeds: it is the inequality lambdaBar A T x v ≤ λᵢ, the defining property of membership in the limsup flag Oseledets.vflag, which is established strictly upstream of the overlap split. No circularity arises.

Main results

• abs_inner_gramEig_le_norm_div_singularValue: for a linear map f on a finite-dimensional real inner product space and a unit eigenvector u of the Gram operator adjoint f ∘ₗ f with eigenvalue μ > 0, every vector v satisfies |⟪u, v⟫| ≤ ‖f v‖ / √μ.
• abs_inner_sortedGramEigenbasis_le_cocycle: the cocycle instance |⟪uⱼ(n), v⟫| ≤ ‖A⁽ⁿ⁾ v‖ / σⱼ(n).
• limsup_log_div_le_of_limsup_le_of_tendsto: if aₙ ≤ pₙ / qₙ eventually (all three sequences eventually positive), limsup (1/n) log pₙ ≤ P, and (1/n) log qₙ → Q, then limsup (1/n) log aₙ ≤ P − Q.
• overlap_limsup_le_of_slow_growth and overlap_limsup_le_of_lambdaBar: the block-rate overlap bound, with the slow-growth hypothesis stated as a limsup bound and in its native lambdaBar form respectively.

The abstract Gram-eigenvector cross bound

theorem Oseledets.abs_inner_gramEig_le_norm_div_singularValue {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E →ₗ[ℝ] E) {u v : E} (hu : ‖u‖ = 1) {μ : ℝ} (hμ : 0 < μ) (heig : (LinearMap.adjoint f) (f u) = μ • u) : |inner ℝ u v| ≤ ‖f v‖ / √μ

Let f : E →ₗ[ℝ] E be a linear map on a finite-dimensional real inner product space and u a unit eigenvector of the Gram operator adjoint f ∘ₗ f with eigenvalue μ > 0 (adjoint f (f u) = μ • u). Then every vector v satisfies

|⟪u, v⟫| ≤ ‖f v‖ / √μ.

Indeed μ · ⟪u, v⟫ = ⟪adjoint f (f u), v⟫ = ⟪f u, f v⟫, so Cauchy–Schwarz gives |⟪u, v⟫| ≤ ‖f u‖ · ‖f v‖ / μ, and ‖f u‖² = ⟪adjoint f (f u), u⟫ = μ for unit u, so ‖f u‖ = √μ. Pure linear algebra: no perturbation theory and no symmetry of f is used.

The per-n cocycle overlap bound

theorem Oseledets.abs_inner_sortedGramEigenbasis_le_cocycle {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) (j : Fin (Fintype.card (Fin d))) (v : EuclideanSpace ℝ (Fin d)) (hσpos : 0 < (Matrix.toEuclideanLin (cocycle A T n x)).singularValues ↑j) : |inner ℝ ((sortedGramEigenbasis A T n x) j) v| ≤ ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖ / (Matrix.toEuclideanLin (cocycle A T n x)).singularValues ↑j

For the sorted Gram singular vector uⱼ(n) = sortedGramEigenbasis A T n x j and any fixed vector v:

|⟪uⱼ(n), v⟫| ≤ ‖A⁽ⁿ⁾ · v‖ / σⱼ(n),

where σⱼ(n) = (toEuclideanLin (cocycle A T n x)).singularValues j is the j-th singular value of A⁽ⁿ⁾ and ‖A⁽ⁿ⁾ · v‖ the cocycle growth of the fixed v. This instantiates abs_inner_gramEig_le_norm_div_singularValue at the Gram eigenvalue μⱼ(n) = eigenvalues₀ (gram) j = σⱼ(n)², so that √(μⱼ(n)) = σⱼ(n).

The rate-assembly lemma

theorem Oseledets.limsup_log_div_le_of_limsup_le_of_tendsto {a p q : ℕ → ℝ} {P Q : ℝ} (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, a n ≤ p n / q n) (hapos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < a n) (hppos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hqpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < q n) (hPlim : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log (p n)) Filter.atTop ≤ P) (hPbdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log (p n)) (hPcob : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log (p n)) (hQtend : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (q n)) Filter.atTop (nhds Q)) (hacob : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log (a n)) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log (a n)) Filter.atTop ≤ P - Q

The limsup arithmetic behind the block rate. If aₙ ≤ pₙ / qₙ eventually (with aₙ, pₙ, qₙ eventually positive), limsup (1/n) log pₙ ≤ P, and (1/n) log qₙ → Q, then limsup (1/n) log aₙ ≤ P − Q.

Mechanism: (1/n) log aₙ ≤ (1/n) log pₙ − (1/n) log qₙ eventually; the limsup of the right-hand side is ≤ limsup (1/n) log pₙ + limsup (−(1/n) log qₙ) = P + (−Q) (the second limsup is −Q since (1/n) log qₙ → Q).

The block-rate overlap bound from the slow-growth limsup

theorem Oseledets.overlap_limsup_le_of_slow_growth {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (j : Fin (Fintype.card (Fin d))) {v : EuclideanSpace ℝ (Fin d)} {lamI lamL : ℝ} (hσpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < (Matrix.toEuclideanLin (cocycle A T n x)).singularValues ↑j) (hslow : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop ≤ lamI) (hslowbdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) (hslowcob : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) (hsing : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues ↑j)) Filter.atTop (nhds lamL)) (hvgrowpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) (hovpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < |inner ℝ v ((sortedGramEigenbasis A T n x) j)|) (hovcob : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log |inner ℝ v ((sortedGramEigenbasis A T n x) j)|) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log |inner ℝ v ((sortedGramEigenbasis A T n x) j)|) Filter.atTop ≤ lamI - lamL

The block-rate overlap bound. For the sorted Gram singular vector uⱼ(n) = sortedGramEigenbasis A T n x j and a slow vector v, with:

• the slow growth limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ — this is lambdaBar A T x v ≤ λᵢ, the defining property of v being slow, supplied by the limsup-flag filtration (Oseledets/Lyapunov/Filtration.lean), which is strictly upstream of the overlap split;
• the singular exponent (1/n) log σⱼ(n) → λ_l (see tendsto_log_singularValue);

the overlap exponent obeys the block rate

limsup (1/n) log |⟪v, uⱼ(n)⟫| ≤ λᵢ − λ_l.

The per-n input is abs_inner_sortedGramEigenbasis_le_cocycle (|⟪uⱼ, v⟫| ≤ ‖A⁽ⁿ⁾ v‖ / σⱼ, sharp); the rate is assembled by limsup_log_div_le_of_limsup_le_of_tendsto.

The lambdaBar form

The slow-growth limsup hypothesis of overlap_limsup_le_of_slow_growth is, up to the toEuclideanCLM/toEuclideanLin coercion, exactly lambdaBar A T x v (lambdaBar_eq_limsup_growthSeq in Oseledets/Lyapunov/GrowthFunction.lean). The connector below restates the overlap bound with the filtration's native slow-vector hypothesis lambdaBar A T x v ≤ λᵢ, making explicit that the slow growth is supplied by Oseledets/Lyapunov/Filtration.lean (lambdaBar_eq_on_stratum / mem_vflag), strictly upstream of the overlap split — not by the spectral split it feeds.

theorem Oseledets.limsup_log_norm_cocycle_eq_lambdaBar {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (v : EuclideanSpace ℝ (Fin d)) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop = lambdaBar A T x v

The lambdaBar form of the slow-growth limsup: the cocycle map's toEuclideanLin and toEuclideanCLM agree, so limsup (1/n) log ‖toEuclideanLin (cocycle) v‖ = lambdaBar A T x v.

theorem Oseledets.overlap_limsup_le_of_lambdaBar {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (j : Fin (Fintype.card (Fin d))) {v : EuclideanSpace ℝ (Fin d)} {lamI lamL : ℝ} (hσpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < (Matrix.toEuclideanLin (cocycle A T n x)).singularValues ↑j) (hslow : lambdaBar A T x v ≤ lamI) (hslowbdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) (hslowcob : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) (hsing : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (cocycle A T n x)).singularValues ↑j)) Filter.atTop (nhds lamL)) (hvgrowpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) (hovpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < |inner ℝ v ((sortedGramEigenbasis A T n x) j)|) (hovcob : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log |inner ℝ v ((sortedGramEigenbasis A T n x) j)|) : Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log |inner ℝ v ((sortedGramEigenbasis A T n x) j)|) Filter.atTop ≤ lamI - lamL

The block-rate overlap bound in the filtration's native form: from the slow-vector hypothesis lambdaBar A T x v ≤ λᵢ (the genuine "v is slow" datum, from Oseledets/Lyapunov/Filtration.lean, upstream of the spectral split). The two boundedness side-conditions on the cocycle growth are supplied by Furstenberg–Kesten-type bounds on the growth sequence.