Assembling the Oseledets limit #
The final assembly of the singular-value layer. The eigenvalues μᵢ,ₙ = σᵢ^{1/n} of qpow A T n x
converge a.e. to the exponentials e^{λᵢ} of the Lyapunov exponents λᵢ = Γ_{i+1} − Γ_i, so the
candidate matrices qpow A T n x converge a.e. to a limiting positive semidefinite matrix
oseledetsLimit, assembled from the block approximant stepVal and the convergent band projectors.
This produces the orbit log-growth limits along the eigenspace filtration.
Main definitions #
Oseledets.stepVal— the block-value step function whose CFC onqpowis the block approximant.Oseledets.oseledetsLimit— the limiting matrixΛ x = lim_n qpow A T n x.
Main results #
Oseledets.tendsto_qpow,Oseledets.tendsto_oseledetsLimit— a.e. convergence of the candidates.Oseledets.oseledetsLimit_isSelfAdjoint,Oseledets.oseledetsLimit_posSemidef,Oseledets.oseledetsLimit_eigenvalues₀_eq— structure of the limit and its eigenvalues.Oseledets.ae_tendsto_log_cocycle_apply_of_eq_exponents— the orbit log-growth limit along the eigenspace filtration.
Assembling the Oseledets limit qpow A T n x → Λ x #
The final assembly. The eigenvalues μᵢ,ₙ = σᵢ^{1/n} of qpow A T n x converge a.e. to the
exponentials e^{λᵢ} of the (deterministic, antitone) Lyapunov exponents λᵢ = Γ_{i+1} − Γ_i. We
group the spectrum at thresholds cₖ = exp((λₖ + λₖ₋₁)/2), one per index 1 ≤ k < d. The candidate
limit at level n is the block approximant
Λₙ x := e^{λ_{d-1}} • 1 + ∑_{k=1}^{d-1} (e^{λₖ₋₁} − e^{λₖ}) • bandProjector (Ioi cₖ) n x.
Two facts combine:
‖qpow A T n x − Λₙ x‖ ≤ maxᵢ |μᵢ,ₙ − e^{λᵢ}| → 0(the spectral-block operator-norm boundnorm_cfc_le_of_forall_eigenvalue_abs_le, sinceΛₙ = cfc h (qpow…)for the block-value step functionh, and on the spectrumhreproduces the right exponential);Λₙ x → Λ xbecause each band projector converges a.e. (tendsto_bandProjector_of_gapat the genuine gaps; the non-gap terms have coefficient0). Henceqpow A T n x → Λ xa.e., dischargingoseledetsLimitExists.
Telescoping of the exponential increments. For any f : ℕ → ℝ and j < d,
f (d-1) + ∑_{k ∈ Ico (j+1) d} (f (k-1) − f k) = f j. The Abel-summation identity behind the block
approximant: summing the increments e^{λₖ₋₁} − e^{λₖ} over the indices above j telescopes to
e^{λⱼ} − e^{λ_{d-1}}.
The block-value step function for an antitone exponent sequence lam. On ℝ,
stepVal lam D t = e^{λ_{D-1}} + ∑_{k=1}^{D-1} (e^{λₖ₋₁} − e^{λₖ}) · 𝟙_{(cₖ, ∞)}(t), where
cₖ = exp((λₖ + λₖ₋₁)/2) is the threshold strictly inside the k-th gap. It is the function whose
continuous functional calculus on qpow A T n x produces the block approximant.
Equations
Instances For
The step function reproduces the exponentials on the spectrum. If lam is antitone on
[0, D) (hanti) and j < D, then stepVal lam D (e^{λⱼ}) = e^{λⱼ}: the threshold indicators
select exactly the increments above index j, which telescope (sum_Ico_increment_telescope).
The block approximant cfc (stepVal) (qpow) as a band-projector combination. Expanding the
step function stepVal lam D through the linearity of the continuous functional calculus (valid on
the finite matrix spectrum): the CFC of the block-value step function on qpow A T n x is the
explicit linear combination of band projectors
e^{λ_{D-1}} • 1 + ∑_{k=1}^{D-1} (e^{λₖ₋₁} − e^{λₖ}) • bandProjector (Ioi cₖ) n x. This is the form
whose a.e. convergence follows from the per-gap band-projector convergence.
The spectral-deviation bound for M − cfc g M. For a self-adjoint matrix M, the operator
norm of M − cfc g M is at most the sum over the sorted eigenvalues of |μⱼ − g μⱼ|. (Writing
M = cfc id M and M − cfc g M = cfc (· − g ·) M, this is
norm_cfc_le_of_forall_eigenvalue_abs_le
with the per-eigenvalue deviation bounded by the full sum of nonnegative deviations.)
The deterministic per-index Lyapunov exponents. Packaged from the ergodic Γ_k limits: for
an ergodic, invertible, log-integrable cocycle there is an antitone constant sequence lam : ℕ → ℝ
(supported on [0, d)) such that, for μ-a.e. x and every i < d, the normalized log of the
i-th singular value of A⁽ⁿ⁾ converges to lam i. The lam i = Γ_{i+1} − Γ_i are the logarithms
of the eigenvalues of the Oseledets limit.
The per-term band-projector convergence. For μ-a.e. x and every threshold index
k ∈ [1, d), the k-th block term (e^{λₖ₋₁} − e^{λₖ}) • bandProjector (Ioi cₖ) n x converges. At
a
genuine gap (λₖ < λₖ₋₁) this is the band-projector convergence tendsto_bandProjector_of_gap; at
a
non-gap the coefficient e^{λₖ₋₁} − e^{λₖ} vanishes, so the term is constantly 0.
The Oseledets limit exists. Discharges oseledetsLimitExists: for μ-a.e. x, the
candidate matrices qpow A T n x = (Qₙ)^{1/(2n)} converge in the matrix metric to a single
matrix Λ x.
The proof combines the four banked ingredients. The eigenvalues μⱼ,ₙ = σⱼ^{1/n} converge to the
exponentials e^{λⱼ} of the deterministic exponents (exists_lam_tendsto_singularValue +
eigenvalues_qpow_tendsto). The block approximant Λₙ x = cfc (stepVal lam d) (qpow…) then
satisfies
‖qpow A T n x − Λₙ x‖ ≤ ∑ⱼ |μⱼ,ₙ − stepVal(μⱼ,ₙ)| → 0 (norm_sub_cfc_le_sum_eigenvalue_dev, with
each summand eventually |μⱼ,ₙ − e^{λⱼ}| since stepVal reproduces the exponentials on the
spectrum — stepVal_exp_lam), while Λₙ x converges as a finite combination of convergent
band projectors (ae_forall_tendsto_block_term + cfc_stepVal_qpow_eq). Hence qpow A T n x
converges; Λ is read off pointwise by Classical.choice.
A named, measurable Oseledets limit Λ #
The existence statement oseledetsLimitExists (tendsto_qpow) only asserts an a.e.-existing limit
via Classical.choice. Here we pin a concrete, measurable representative oseledetsLimit A T,
defined entrywise as the real limUnder of the (measurable) matrix entries of qpow A T n x. On
the a.e.-full convergence set this entrywise limit equals the matrix limit, so oseledetsLimit
discharges oseledetsLimitExists while being genuinely (not merely a.e.) measurable.
The Gram matrix x ↦ gram A T n x = (A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾ is measurable.
The matrix root x ↦ qpow A T n x = (Qₙ)^{1/(2n)} = cfc (·^{1/(2n)}) (gram A T n x) is
measurable. The function t ↦ t^{1/(2n)} is continuous (nonnegative exponent), the Gram matrix is
measurable (measurable_gram) and self-adjoint (gram_isSelfAdjoint), so the continuous-functional
-calculus measurability crux measurable_cfc_continuous applies.
The named Oseledets limit. Defined entrywise as the real limUnder of the matrix
entries of qpow A T n x. On the a.e.-full convergence set (tendsto_qpow) this equals the matrix
limit; off it the value is irrelevant (the construction is total and measurable regardless).
Equations
- Oseledets.oseledetsLimit A T x = Matrix.of fun (i j : Fin d) => Filter.atTop.limUnder fun (n : ℕ) => Oseledets.qpow A T n x i j
Instances For
The named Oseledets limit oseledetsLimit A T is measurable: each entry is a real
limUnder of measurable functions (measurable_qpow), and a limUnder over atTop valued in the
completely metrizable space ℝ of measurable functions is measurable
(StronglyMeasurable.limUnder).
oseledetsLimit is the a.e. limit of qpow. For μ-a.e. x,
qpow A T n x → oseledetsLimit A T x in the matrix metric. (On the a.e.-full convergence set the
entrywise limUnder recovers the matrix limit; matrix convergence reduces to entrywise
convergence in finite dimensions.)
Eigen-data of the Oseledets limit Λ #
The named limit oseledetsLimit A T x inherits the self-adjointness and positive
semidefiniteness of the approximants qpow A T n x (both closed under the matrix limit, proved
entrywise / via the continuity of the quadratic form). The eigenvalue equality
eigenvalues₀ (Λ x) i = e^{λᵢ} additionally requires continuity of the sorted eigenvalues in the
Hermitian matrix, which is absent from Mathlib (see the blocker flag in the module summary).
For μ-a.e. x, the Oseledets limit oseledetsLimit A T x is self-adjoint, as the
matrix-metric limit of the self-adjoint approximants qpow A T n x (self-adjointness Mᴴ = M is
an entrywise closed condition).
For μ-a.e. x, the Oseledets limit oseledetsLimit A T x is positive semidefinite,
as the matrix-metric limit of the PSD approximants qpow A T n x: it is self-adjoint, and the
quadratic form xᵀ Λ x = lim_n xᵀ (qpow A T n x) x ≥ 0 is a limit of nonnegatives (the quadratic
form is continuous in the matrix).
Antitonicity of the per-point Lyapunov exponents. For μ-a.e. x, the per-point
exponents lamSing A T x · are antitone on [0, d). (A.e. each index has a genuine
singular-value limit lamSing = λᵢ by tendsto_log_singularValue, and the deterministic exponents
λᵢ are antitone by exists_lam_tendsto_singularValue.) This is the order datum pinning the
intended descending spectrum e^{lamSing 0} ≥ e^{lamSing 1} ≥ ⋯ of Λ.
The eigenvalues of qpow converge to e^{lamSing}. For μ-a.e. x and every sorted
index i, the i-th sorted eigenvalue of the approximant qpow A T n x converges to
e^{lamSing A T x i}. This is the eigenvalue statement at the level of the approximants; the
full
eigenvalue equality for Λ itself (oseledetsLimit_eigenvalues₀_eq) additionally needs continuity
of the sorted eigenvalues in the Hermitian matrix, which is absent from Mathlib — see the blocker
note below.
The eigenvalue equality eigenvalues₀ (Λ x) i = e^{lamSing A T x i}. For μ-a.e. x
and every sorted index i, the i-th sorted eigenvalue of the Oseledets limit Λ x is exactly
e^{lamSing A T x i}.
This is the headline spectral statement of the Oseledets limit. The proof passes the
approximant-level eigenvalue convergence eigenvalues₀ (qpow A T n x) i → e^{lamSing i}
(eigenvalues₀_qpow_tendsto_exp_lamSing) through the matrix limit qpow A T n x → Λ x
(tendsto_oseledetsLimit) using continuity of the sorted eigenvalues eigenvalues₀
(Weyl.tendsto_eigenvalues₀, the new Weyl perturbation infrastructure in ExteriorNorm.lean):
eigenvalues₀ (qpow A T n x) i → eigenvalues₀ (Λ x) i, and uniqueness of limits forces the two
limits to agree.
The two-sided growth limit (1/n)·log‖A⁽ⁿ⁾(x) v‖ #
For a single nonzero vector v, the normalized log-growth of the cocycle image A⁽ⁿ⁾(x) v
converges (not merely limsup/liminf) to the largest Lyapunov exponent active on v. The
quadratic-form foundation ‖A⁽ⁿ⁾ v‖² = ⟪gram_n v, v⟫ ties the growth to the Gram spectrum
(= qpow_n^{2n}). We bank here:
- the foundational identity
norm_sq_cocycle_apply_eq_inner_gram; - the per-vector operator-norm sandwich
‖A⁽ⁿ⁾⁻¹‖⁻¹ ‖v‖ ≤ ‖A⁽ⁿ⁾ v‖ ≤ ‖A⁽ⁿ⁾‖ ‖v‖; - the genuine two-sided limit in the equal-exponents (conformal/isotropic) regime
(
tendsto_log_cocycle_apply_of_eq_exponents, and its a.e. ergodic packagingae_tendsto_log_cocycle_apply_of_eq_exponents): when the top Furstenberg–Kesten exponentℓ_top = lim (1/n)log‖A⁽ⁿ⁾‖and the bottom exponentℓ_bot = lim (1/n)log‖(A⁽ⁿ⁾)⁻¹‖satisfyℓ_bot = -ℓ_top(all Lyapunov exponents coincide), then every nonzerovgrows at the common rateℓ_top.
The fully general per-vector limit (with the top active Oseledets exponent depending on v's
Λ-eigencomponents) needs the band-projector convergence tendsto_bandProjector_of_gap to control
the eigencomponent of v at the dominant exponent; that assembly is flagged in the module summary
and left for a follow-up.
Foundation. The squared norm of the cocycle image is the Gram quadratic form:
‖A⁽ⁿ⁾(x) v‖² = ⟪gram_n v, v⟫. (‖f v‖² = ⟪f v, f v⟫ = ⟪(adjoint f ∘ f) v, v⟫, and
adjoint(toEuclideanLin M) ∘ toEuclideanLin M = toEuclideanLin (Mᵀ M) = toEuclideanLin (gram).)
Upper bound. ‖A⁽ⁿ⁾(x) v‖ ≤ ‖A⁽ⁿ⁾(x)‖ ‖v‖ — the per-vector L² operator-norm bound.
Lower bound. ‖v‖ ≤ ‖A⁽ⁿ⁾(x)⁻¹‖ · ‖A⁽ⁿ⁾(x) v‖ for an invertible cocycle, i.e.
‖A⁽ⁿ⁾⁻¹‖⁻¹ ‖v‖ ≤ ‖A⁽ⁿ⁾ v‖. (v = A⁽ⁿ⁾⁻¹ (A⁽ⁿ⁾ v), then the op-norm bound.)
Nonvanishing. A⁽ⁿ⁾(x) v ≠ 0 for v ≠ 0 (invertibility ⟹ injectivity).
Equal-exponents two-sided limit. If the top and (negated) bottom Furstenberg–Kesten
exponents coincide at x — i.e. (1/n)log‖A⁽ⁿ⁾‖ → ℓ and (1/n)log‖(A⁽ⁿ⁾)⁻¹‖ → -ℓ — then for
every nonzero v the normalized log-growth of A⁽ⁿ⁾ v converges to ℓ. This is the genuine
two-sided growth limit (not merely limsup) in the isotropic/conformal regime where all Lyapunov
exponents agree: the operator-norm sandwich ‖A⁽ⁿ⁾⁻¹‖⁻¹ ‖v‖ ≤ ‖A⁽ⁿ⁾ v‖ ≤ ‖A⁽ⁿ⁾‖ ‖v‖ squeezes the
normalized log between two sequences both tending to ℓ (the (1/n)log‖v‖ correction vanishes).
A.e. equal-exponents two-sided limit. For an ergodic, integrable, invertible cocycle
whose top Furstenberg–Kesten exponent ℓ_top and bottom exponent ℓ_bot satisfy ℓ_bot = -ℓ_top
(all Lyapunov exponents equal — the conformal/isotropic regime), there is a single exponent ℓ such
that for μ-a.e. x and every nonzero v, (1/n)log‖A⁽ⁿ⁾(x) v‖ → ℓ. The two FK exponents are
produced internally by furstenbergKesten_norm/_bot; the hypothesis heq ties them together.