Forward exact growth and the measurable Oseledets filtration #
This module connects the analytic core of the one-sided Oseledets multiplicative ergodic
theorem (the Oseledets limit Λ = lim ((A⁽ⁿ⁾)ᵀA⁽ⁿ⁾)^{1/2n} of OseledetsLimit.lean, its
band-projector convergence, and the limsup flag of Filtration.lean) to the target theorem
oseledets_filtration.
The mathematical content of this module is the per-vector exact growth limit
(1/n) log‖A⁽ⁿ⁾(x) v‖ → λᵢ for v in the stratum Vᵢ \ Vᵢ₊₁:
- Lower bound
liminf ≥ λᵢ: the Gram quadratic-form band bound⟪gramₙ v, v⟫ ≥ c^{2n} ‖Pᶜₙ v‖²(inner_cfc_ge_band), the band-projector convergencePᶜₙ v → Pᶜ_∞ v ≠ 0, and taking the thresholdc ↑ e^{λᵢ}. - Upper bound
limsup ≤ λᵢ: a spectral decomposition over the sorted Gram eigenbasis, with each overlap term controlled by the tilt of the band projector at its straddling-gap rate, paired against the block's singular-value growth.
Together they upgrade the limsup flag's lambdaBar = λᵢ (lambdaBar_eq_on_stratum) to a
genuine limit, identify the Λ-spectral filtration with lambdaSublevel a.e. (so it inherits
strict antitonicity and A-equivariance), and — with the deterministic exponents from
exists_lam_tendsto_singularValue and the CFC measurability of Measurable.lean — yield
the target theorem.
Main results #
inner_cfc_ge_band: the Gram quadratic-form band bound for a self-adjoint matrix.log_le_liminf_log_cocycle_apply: the per-vector liminf lower boundlog c ≤ liminf (1/n) log‖A⁽ⁿ⁾ v‖from band-projector convergence.limitBandProjector_apply_eq_zero_of_le: kernel propagation between limit band projectors of nested thresholds.norm_sq_bandProjector_apply_eq_sum: the frame Parseval identity for the band projection in the straddled regime.limsup_normLog_inner_le: the per-overlap limsup bound via the handle identity and Cauchy–Schwarz.limsup_inv_mul_log_norm_cocycle_apply_le: the per-vector growth upper bound, conditional on per-index leakage envelopes.tendsto_inv_mul_log_norm_cocycle_apply_of_bandProjector_envelope: the assembled per-vector exact growth limit.
Distinct descending exponent enumeration #
The deterministic singular-value exponents lam : ℕ → ℝ (from
exists_lam_tendsto_singularValue) are antitone on [0, d); their distinct values,
enumerated descending, are the k Lyapunov exponents λ₀ > ⋯ > λ_{k-1} of the target
theorem. This mirrors Filtration.specList.
The finite set of distinct exponent values on [0, d).
Equations
- Oseledets.distinctExp lam d = Finset.image lam (Finset.range d)
Instances For
The number of distinct exponents.
Equations
- Oseledets.numExp lam d = (Oseledets.distinctExp lam d).card
Instances For
The descending enumeration of the distinct exponents (index 0 = largest).
Equations
- Oseledets.expEnum lam d i = ((Oseledets.distinctExp lam d).orderEmbOfFin ⋯) i.rev
Instances For
Membership: r is an enumerated value iff r = lam j for some j < d.
The Gram quadratic-form band bound (lower-bound foundation) #
For a self-adjoint Q and a 0/1 band indicator χ = 𝟙_{(c,∞)}, a continuous shape
f ≥ 0 with f ≥ a above c controls the band projection:
a · ‖(cfc χ Q) v‖² ≤ ⟪(cfc f Q) v, v⟫. Applied with Q = qpow, f = (·)^{2n}
(so cfc f Q = gram) and a = c^{2n} it gives the per-vector lower bound
c^{2n} ‖Pᶜₙ v‖² ≤ ‖A⁽ⁿ⁾ v‖².
The norm identity ‖toEuclideanLin M v‖² = ⟪toEuclideanLin (Mᵀ * M) v, v⟫ (generic
real matrix; the cocycle specialization is norm_sq_cocycle_apply_eq_inner_gram).
Gram quadratic-form band bound. For self-adjoint Q, a 0/1 band indicator
χ = 𝟙_{(c,∞)}, and a continuous f ≥ 0 on the spectrum with a ≤ f t whenever
c < t: a · ‖(cfc χ Q) v‖² ≤ ⟪(cfc f Q) v, v⟫. The band projector is a self-adjoint
idempotent (‖Pv‖² = ⟪Pv,v⟫); the gap cfc (f − a·χ) Q is PosSemidef since
f − a·χ ≥ 0 on the spectrum.
The per-vector lower bound: Gram–CFC identity, band bound, and liminf #
The Gram matrix gramₙ = (A⁽ⁿ⁾)ᵀA⁽ⁿ⁾ is recovered from qpowₙ = (gramₙ)^{1/(2n)} by
raising to the 2n-th power (gram_eq_cfc_qpow). Feeding qpowₙ into the quadratic-form
band bound (inner_cfc_ge_band) with f = (·)^{2n} and threshold c then gives the
per-vector bound c^{2n} ‖Pᶜₙ v‖² ≤ ‖A⁽ⁿ⁾ v‖² (cocycle_apply_sq_ge_band). Taking logs,
dividing by 2n, and sending the band-projector correction to 0
(tendsto_inv_mul_log_norm_bandProjector_apply) yields the per-vector liminf lower bound
log c ≤ liminf (1/n) log‖A⁽ⁿ⁾ v‖ (log_le_liminf_log_cocycle_apply).
Band lower bound. For c ≥ 0, the band projection of v (for the band (c,∞) of
qpowₙ) is controlled by the cocycle growth:
c^{2n} · ‖Pᶜₙ v‖² ≤ ‖A⁽ⁿ⁾ v‖².
Band correction vanishes. If the band projectors Pᶜₙ converge to P with
P v ≠ 0, then the normalized log of the band projection ‖Pᶜₙ v‖ tends to 0: the norm
converges to a positive limit, so its log is bounded, and dividing by n → ∞ kills it.
Per-vector lower bound, eventual form (the analytic core of the liminf bound). If
the band projectors for (c,∞) (with c > 0) converge to P with P v ≠ 0, then
eventually log c + (1/n) log‖Pᶜₙ v‖ ≤ (1/n) log‖A⁽ⁿ⁾ v‖, where the left band-correction
term tends to 0 (tendsto_inv_mul_log_norm_bandProjector_apply). Taking n → ∞ (the
band correction vanishing) yields log c ≤ liminf (1/n) log‖A⁽ⁿ⁾ v‖, which is packaged as
log_le_liminf_log_cocycle_apply below.
Per-vector liminf lower bound. If the band projectors for (c,∞) (with c > 0)
converge to P with P v ≠ 0, then log c ≤ liminf (1/n) log‖A⁽ⁿ⁾ v‖.
The proof combines the eventual lower bound log_add_correction_le_inv_mul_log_cocycle_apply
(whose left side converges to log c, the band correction vanishing by
tendsto_inv_mul_log_norm_bandProjector_apply) with liminf monotonicity. The
IsCoboundedUnder (· ≥ ·) side-condition on the right-hand cocycle sequence — which fails
in general without an a-priori upper growth bound on (1/n) log‖A⁽ⁿ⁾‖, a Furstenberg–Kesten
input — is taken as a hypothesis hcobdd; at the application site it is supplied by the
integrability of the top Furstenberg–Kesten exponent.
Band-projector nesting #
For c ≤ c', the spectral bands satisfy Ioi c' ⊆ Ioi c, so the finer band projector
(threshold c') has range contained in the coarser one (threshold c); algebraically
Pᶜₙ · Pᶜ'ₙ = Pᶜ'ₙ. Passing to the limit and applying to a vector gives the
kernel-propagation form consumed by the upper-bound proof: a vector killed by the coarser
(lower-threshold) limit projector is killed by every finer (higher-threshold) one above
it.
Band-projector nesting (finite n, operator form). For c ≤ c', the band
projectors are nested: cfc 𝟙_{(c,∞)} · cfc 𝟙_{(c',∞)} = cfc 𝟙_{(c',∞)} on qpow. The
coarser band (threshold c) contains the finer one (threshold c').
Band-projector nesting (limit, operator form). Passing bandProjector_mul_of_le
through the two convergent band-projector sequences (matrix multiplication is continuous)
gives P · P' = P' for the limit projectors, where c ≤ c'.
Band-projector nesting (limit, kernel-propagation form). With c ≤ c', a vector
with P v = 0 for the coarser (threshold c) limit projector also has P' v = 0 for the
finer (threshold c') one: transposing P · P' = P' (both limit projectors are symmetric)
gives P' · P = P', hence P' v = P' (P v) = 0.
The exact frame Parseval identity #
In the eventual straddled regime where exactly k qpow-eigenvalues exceed the cut c
and the top-k sorted ones all exceed it, bandProjector_indicator_eq_sortedTopFrame
gives P = W Wᵀ with Wᵀ W = 1, W = sortedTopFrame. The band projection applied to v
therefore has squared norm equal to the sum of squared overlaps with the top sorted Gram
eigenvectors.
Frame Parseval identity. Under the eventual straddled-regime hypotheses (htop,
hcount) of bandProjector_indicator_eq_sortedTopFrame, the squared norm of the band
projection equals the sum of squared overlaps of v with the top-k sorted Gram
eigenvectors (the columns of sortedTopFrame, recovered by colE_sortedTopFrame).
The per-overlap limsup bound #
The handle identity ⟪v, uⱼ(n)⟫ = ⟪v, (Pₙ − Pinf) uⱼ(n)⟫ for slow v/fast uⱼ, its
Cauchy–Schwarz consequence |⟪v,uⱼ⟫| ≤ ‖v‖ · ‖(Pₙ − Pinf) uⱼ‖, the k = 1 Gram residual
via Pythagoras, and the assembled normalized-log/limsup bounds. Everything is parametrized
over a tilt/overlap-rate hypothesis, supplied at the application site by the
band-projector convergence theory.
Handle identity. If v is slow (toEuclideanLin Pinf v = 0) and uⱼ(n) lies in
the step-n fast band (toEuclideanLin Pₙ uⱼ = uⱼ), then ⟪v, uⱼ⟫ = ⟪v, (Pₙ − Pinf) uⱼ⟫.
Both Pₙ and Pinf are self-adjoint.
Handle + Cauchy–Schwarz (per-step bound). For slow v and a step-n fast eigenvector
uj (toEuclideanLin Pn uj = uj), the overlap is controlled by the tilt of the band projector
on uj: |⟪v, uj⟫| ≤ ‖v‖ · ‖(Pn − Pinf) uj‖.
Off-diagonal residual (Pythagoras). The off-diagonal residual numerator squared:
‖C v₀ − ⟪C v₀, v₀⟫ v₀‖² = ‖C v₀‖² − ⟪C v₀, v₀⟫² for a unit vector v₀. This is the
elementary k = 1 Gram off-diagonal residual, requiring no exterior-power machinery.
Per-step log overlap bound. With the per-step handle bound |⟪v,uⱼₙ⟫| ≤ ‖v‖ · tₙ
(hbound) and both sides positive, the normalized-log overlap exponent is dominated by the
tilt exponent plus a vanishing (1/n) log ‖v‖ shift.
Limsup overlap bound. Combining normLog_overlap_le over n with the vanishing of
(1/n) log ‖v‖ and the supplied tilt-rate limsup ((1/n) log tₙ) ≤ r, the overlap
exponent has limsup ≤ r.
Limsup overlap bound (band-projector form). Ties the abstract limsup bound to the
genuine band projectors. Given, eventually in n, self-adjointness of Pₙ/Pinf, the
slow hypothesis Pinf v = 0, and fast-band membership Pₙ uⱼ(n) = uⱼ(n), the handle +
Cauchy–Schwarz supply the per-step bound, and with the tilt rate htilt the overlap
exponent has limsup ≤ r.
Band-projection leakage bound (per-step log form). With ‖P v‖² = Σⱼ cⱼ, cⱼ ≥ 0,
and a common per-step ceiling cⱼ ≤ B, the band-projection leakage exponent is bounded by
(1/2n) log (k·B).
The per-vector growth upper bound and the per-vector limit #
The per-vector upper bound limsup (1/n) log‖A⁽ⁿ⁾v‖ ≤ λᵢ, conditional on the per-index
leakage envelopes, and the assembled per-vector exact-growth limit.
Helper (log of a finite sum). Let s be a finite index type and t : s → ℕ → ℝ with
t m n ≥ 0. If for every m and every ε > 0, eventually t m n ≤ exp (n (L + ε)), and the total
sum is eventually positive, then limsup_n (1/n) log (∑_m t m n) ≤ L.
Helper (limsup ⟹ exp envelope). If a n ≥ 0 and limsup_n (1/n) log (a n) ≤ M, then for
every ε > 0 eventually a n ≤ exp (n (M + ε)).
Spectral Parseval for the Gram quadratic form against the sorted Gram eigenbasis:
⟪gram v, v⟫ = ∑ⱼ (eigenvalues₀ (gram) j) · ⟪v, uⱼ⟫².
Spectral Parseval (cocycle form). The squared cocycle norm is the sum of squared singular
values times squared overlaps with the sorted Gram eigenbasis:
‖A⁽ⁿ⁾ v‖² = ∑ⱼ σⱼ(n)² · ⟪v, uⱼ(n)⟫².
The j-th spectral term σⱼ(n)² · ⟪v,uⱼ(n)⟫².
Equations
- Oseledets.specTerm T A n x v j = (Matrix.toEuclideanLin (Oseledets.cocycle A T n x)).singularValues ↑j ^ 2 * inner ℝ v ((Oseledets.sortedGramEigenbasis A T n x) j) ^ 2
Instances For
∑ⱼ specTermⱼ = ‖A⁽ⁿ⁾ v‖².
Conditional upper bound. Given, for each spectral index j, the per-index exp-envelope
tⱼ(n) ≤ exp(n(2λᵢ + ε)), and eventual positivity of ‖A⁽ⁿ⁾ v‖, the per-vector growth limsup is
≤ λᵢ.
Product envelope. If a n ≤ exp(n·p) and b n ≤ exp(n·q) eventually (a, b ≥ 0), then
a n · b n ≤ exp(n·(p+q)) eventually.
Singular-value square envelope. If (1/n) log σⱼ(n) → λⱼ and each σⱼ(n) > 0, then
for every δ > 0, eventually σⱼ(n)² ≤ exp(n(2λⱼ + δ)).
Per-index envelope (slow & fast unified). If (1/n) log σⱼ(n) → λⱼ, each σⱼ(n) > 0, the
overlap satisfies the leakage bound limsup (1/n) log ⟪v,uⱼ(n)⟫² ≤ 2 rⱼ (with the boundedness
side-condition), and λⱼ + rⱼ ≤ λᵢ, then specTermⱼ(n) ≤ exp(n(2λᵢ + ε)) for every ε > 0.
Per-vector exact growth limit (from limsup ≤ λᵢ and λᵢ ≤ liminf).
Per-vector exact growth limit (assembled). The lower bound is
log_le_liminf_log_cocycle_apply at threshold c = e^{λᵢ}; the upper bound is
limsup_inv_mul_log_norm_cocycle_apply_le. Given band-projector convergence (hP, hPv),
the per-index leakage envelopes (henv), positivity (hpos), the cobounded inputs, and
the boundedness side-conditions, the per-vector growth converges to λᵢ.