The Oseledets singular-value (scalar) layer #
This module builds the scalar (singular-value) layer of the Oseledets multiplicative
ergodic theorem: the genuine ergodic limits
Γ_k = lim_n (1/n) log ∏_{i<k} σᵢ(A⁽ⁿ⁾) and the per-exponent limits
λᵢ = Γ_{i+1} − Γ_i (the logarithms of the eigenvalues of the limiting matrix Λ),
without ever constructing Λ as a matrix limit.
The analytic input is the already-proved submultiplicativity of the product of the top-k
singular values (ExteriorNorm.prod_singularValues_comp_le), turned into a subadditive
cocycle and fed to Kingman's ergodic theorem (tendsto_kingman_ergodic).
Main definitions #
Oseledets.gram— the Gram matrixQₙ = (A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾of the cocycle iterate.Oseledets.sprod— the product of the top-ksingular values oftoEuclideanLin (A⁽ⁿ⁾).
Main results #
LinearMap.singularValues_le_opNorm/Oseledets.sigma_le_opNorm—σᵢ(f) ≤ ‖f‖andσᵢ(toEuclideanLin M) ≤ ‖M‖.Oseledets.sprod_submul,Oseledets.logSprod_subadditive,Oseledets.isSubadditiveCocycle_logSprod— subadditivity oflog sprod.Oseledets.integrable_logSprod,Oseledets.bddBelow_logSprod— integrability/lower bound.Oseledets.tendsto_gammaK— the genuine ergodicΓ_klimit.Oseledets.lamSing,Oseledets.tendsto_log_singularValue,Oseledets.lamSing_antitone— the per-singular-value exponents.Oseledets.sq_singularValues_eq_gram_eigenvalue— squared singular values are Gram eigenvalues.
A singular value is bounded by the operator norm #
σᵢ(f) ≤ ‖f‖ for a linear map f between finite-dimensional inner product spaces.
This is genuinely missing from Mathlib (SingularValues.lean has no connection to the
operator norm); it is upstreamable. The proof: the right singular vectors uᵢ (an
orthonormal eigenvector basis of adjoint f ∘ₗ f) satisfy ‖f uᵢ‖ = σᵢ(f), and
‖f uᵢ‖ ≤ ‖f‖ · ‖uᵢ‖ = ‖f‖.
The norm of the image of a right singular vector is the corresponding singular value:
‖f uᵢ‖ = σᵢ(f), where u is the orthonormal eigenvector basis of adjoint f ∘ₗ f. This is
the analytic heart of the singular value decomposition.
Every singular value of a linear map between finite-dimensional inner
product spaces is bounded by its operator norm: σᵢ(f) ≤ ‖f‖.
The Gram matrix and the singular-value product #
The Gram matrix Qₙ = (A⁽ⁿ⁾)ᵀ · A⁽ⁿ⁾ of the cocycle iterate. Its eigenvalues are the
squared singular values of A⁽ⁿ⁾ (see sq_singularValues_eq_gram_eigenvalue).
Equations
- Oseledets.gram A T n x = (Oseledets.cocycle A T n x).transpose * Oseledets.cocycle A T n x
Instances For
The top-k singular value product of the cocycle iterate, as a Euclidean linear map.
Equations
- Oseledets.sprod A T k n x = ∏ i ∈ Finset.range k, (Matrix.toEuclideanLin (Oseledets.cocycle A T n x)).singularValues i
Instances For
Subadditivity of log sprod in the plain (T^[n]-shifted) split, provided each
sprod is positive (true for an invertible cocycle and k ≤ d).
Kingman index convention. log sprod is a subadditive cocycle in Kingman's sense
g(m+n,x) ≤ g(m,x) + g(n,T^[m]x), obtained from the symmetric cocycle split.
Singular-value/operator-norm bound (matrix form) and sandwich bounds #
Integrability and bounded-below of log sprod #
The sandwich −k·log‖(A⁽ⁿ⁾)⁻¹‖ ≤ log sprod ≤ k·log‖A⁽ⁿ⁾‖ (from the singular-value/operator-norm
bound and its inverse companion) dominates log sprod by integrable functions, reusing the
Furstenberg–Kesten integrability plumbing.
Measurability of the determinant of a measurable square-matrix-valued function (entrywise a polynomial in the measurable entries). Used to read off measurability of the compound-matrix entries, which are minors of the cocycle iterate.
Measurability of x ↦ sprod A T k n x. By the compound-matrix bridge
ExteriorNorm.prod_singularValues_eq_l2_opNorm_compound, the product of the top-k singular
values equals the L2 operator norm of the k-th compound matrix C_k(A⁽ⁿ⁾ x), whose entries
are the k × k minors of A⁽ⁿ⁾ x. Each minor is the determinant of a submatrix of the
(measurable) cocycle iterate, hence measurable; the matrix-valued map is then measurable
entrywise, and the (continuous) L2 operator norm preserves measurability. No exterior-power /
linear-map continuity is needed.
Integrability of log sprod. Each level gₙ = log sprod_k is integrable, dominated
by the two (integrable) Furstenberg–Kesten log-norm cocycles.
Bounded-below proviso (Fekete lower bound). The normalized integrals of log sprod
are bounded below by −k · ∫ log⁺‖A⁻¹‖, keeping the Kingman limit finite.
Squared singular values are the Gram eigenvalues #
The eigenvalue bridge. The squared singular values of toEuclideanLin M are the
eigenvalues of the symmetric operator adjoint ∘ self = toEuclideanLin (Mᵀ M), i.e. the
eigenvalues of the Gram matrix Qₙ = (A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾. This delivers the eigenvalues of the
Oseledets limit Λ as genuine ergodic limits (via tendsto_gammaK) without constructing Λ.
The genuine ergodic Γ_k limit #
The genuine ergodic Γ_k limit (spike form). Under ergodicity, with the
Furstenberg–Kesten-style integrability (hint) and bounded-below (hbdd) provisos and the
positivity proviso (hpos, valid for k ≤ d on an invertible cocycle), the normalized
log sprod_k converges μ-a.e. to a constant Γ_k.
The genuine ergodic Γ_k limit (with the integrability/lower-bound provisos discharged).
For an ergodic
measure-preserving T, an everywhere-invertible measurable cocycle generator with
log⁺‖A‖, log⁺‖A⁻¹‖ ∈ L¹, and k ≤ d, the normalized log sprod_k converges μ-a.e. to a
constant Γ_k.
The per-singular-value exponents #
Per-σ exponent. Differencing the Γ_k limits: if (1/n) log sprod_{i+1} → a and
(1/n) log sprod_i → b for μ-a.e. x and the singular values are positive (k ≤ d), then the
normalized log of the i-th singular value converges to a − b (the i-th Lyapunov exponent
λᵢ = Γ_{i+1} − Γ_i).
Antitonicity of the per-σ exponents. For each fixed n and x, the normalized
logs of the singular values are antitone in the index (since the singular values themselves are
antitone).
The per-point singular-value Lyapunov exponent. The i-th Lyapunov exponent at the
point x, defined as the (junk-on-divergence) limit of the normalized log of the i-th singular
value of A⁽ⁿ⁾. Where the singular-value limit exists (μ-a.e., by tendsto_log_singularValue)
this equals the deterministic exponent λᵢ; lamSing packages it as a concrete per-point datum so
that the spectrum of the Oseledets limit Λ can be labelled by e^{lamSing}.
Equations
- Oseledets.lamSing A T x i = Filter.atTop.limUnder fun (n : ℕ) => (↑n)⁻¹ * Real.log ((Matrix.toEuclideanLin (Oseledets.cocycle A T n x)).singularValues i)
Instances For
If, at x, the normalized log of the i-th singular value converges to lam (true μ-a.e. by
tendsto_log_singularValue), then lamSing A T x i = lam.
The Gram matrix is PosSemidef / self-adjoint, and the matrix root qpow #
The Gram matrix Qₙ = (A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾ is positive semidefinite and self-adjoint, so the
continuous functional calculus applies to it. The candidate Oseledets limit at level n is the
matrix (Qₙ)^{1/(2n)} = cfc (·^{1/(2n)}) Qₙ, whose eigenvalues are the 1/n-th powers of the
singular values of A⁽ⁿ⁾.
The Gram matrix Qₙ = (A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾ is positive semidefinite.
The Gram matrix Qₙ = (A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾ is self-adjoint, hence the continuous
functional calculus applies to it.
The candidate Oseledets limit at level n: the matrix 1/(2n)-th power
(Qₙ)^{1/(2n)} = cfc (·^{1/(2n)}) Qₙ of the Gram matrix, defined via the continuous functional
calculus on the (self-adjoint, positive semidefinite) Gram matrix Qₙ. Its eigenvalues are the
1/n-th powers of the singular values of A⁽ⁿ⁾, which converge to e^{λᵢ}
(see eigenvalues_qpow_tendsto).
Equations
- Oseledets.qpow A T n x = cfc (fun (t : ℝ) => t ^ (2 * ↑n)⁻¹) (Oseledets.gram A T n x)
Instances For
qpow A T n x is self-adjoint (a CFC of a real-valued function is always self-adjoint).
qpow A T n x = (Qₙ)^{1/(2n)} is positive semidefinite: cfc of the nonnegative function
t ↦ t^{1/(2n)} on the PosSemidef (hence nonnegative-spectrum) Gram matrix Qₙ yields a
nonnegative (hence PosSemidef) matrix.
The eigenvalues of qpow converge to e^{λᵢ} #
The eigenvalues of qpow A T n x = (Qₙ)^{1/(2n)} are the 1/n-th powers of the singular values
of A⁽ⁿ⁾. Since (1/n) log σᵢ → λᵢ a.e. (tendsto_log_singularValue), these converge to
e^{λᵢ}. The CFC of a monotone function applied to a Hermitian matrix has, as its sorted
eigenvalues, that function applied to the sorted eigenvalues of the matrix; we package this as a
helper and then chain it with the singular-value layer.
The roots of the characteristic polynomial of cfc f A (for Hermitian A) are f applied to
the eigenvalues of A (cast into 𝕜). The matrix analogue of
Matrix.IsHermitian.roots_charpoly_eq_eigenvalues.
For a Hermitian matrix A with nonnegative eigenvalues and a function f that is monotone on
[0, ∞) (hence preserves the descending order of the eigenvalues), the sorted eigenvalues
eigenvalues₀ of cfc f A are f applied to the sorted eigenvalues of A. The matrix analogue
(with a monotonicity-on-the-spectrum hypothesis) of
Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀. The MonotoneOn form is needed because
the relevant function t ↦ t^{1/(2n)} is Real.rpow, which is monotone only on [0, ∞).
The sorted eigenvalues eigenvalues₀ of the Gram matrix Qₙ = (A⁽ⁿ⁾)ᵀ A⁽ⁿ⁾ are the squared
singular values of A⁽ⁿ⁾: eigenvalues₀ (Qₙ) i = σᵢ(A⁽ⁿ⁾)². This bridges the matrix-eigenvalue
layer (Matrix.IsHermitian.eigenvalues₀) to the singular-value layer
(sq_singularValues_eq_gram_eigenvalue).
The eigenvalues of qpow are the 1/n-th powers of the singular values. The sorted
eigenvalues of qpow A T n x = (Qₙ)^{1/(2n)} are σᵢ(A⁽ⁿ⁾)^{1/n}.
The eigenvalues of qpow converge to e^{λᵢ}. If, at a point x, the normalized log
of the i-th singular value of A⁽ⁿ⁾ converges to λᵢ (which holds μ-a.e. by
tendsto_log_singularValue), then the i-th sorted eigenvalue of qpow A T n x = (Qₙ)^{1/(2n)}
converges to e^{λᵢ}. This is the eigenvalue layer of the Oseledets limit: the eigenvalues of the
candidate matrix limit are the exponentials of the Lyapunov exponents. Stated per eigenvalue-index
i (eigenvalues may repeat across distinct exponents — that is harmless here; the
per-distinct-exponent constraint only bites for the band spectral projectors below).
The Oseledets-limit existence statement (oseledetsLimit) #
The Prop that the band-projector machinery below discharges: a.e., the matrix sequence
(Qₙ)^{1/(2n)} = qpow A T n x converges, in the (complete, finite-dimensional) matrix metric, to
a single matrix Λ x.
The Oseledets-limit existence statement. A.e. the 1/(2n)-th matrix power of the Gram
matrix converges (in the finite-dimensional matrix metric) to a single matrix Λ x. This is the
existence statement of the Oseledets limit; it is proved jointly with its eigen-data conclusions
below (the gapped band-projector-Cauchy estimate).
Equations
- Oseledets.oseledetsLimitExists μ T A = ∃ (Λ : X → Matrix (Fin d) (Fin d) ℝ), ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => Oseledets.qpow A T n x) Filter.atTop (nhds (Λ x))