The Oseledets Multiplicative Ergodic Theorem in Lean 4

6 Companion results and extensions

The Oseledets multiplicative ergodic theorem \(\texttt{oseledets\_ filtration}\) delivers, \(\mu \)-a.e., a strictly decreasing \(A\)-equivariant flag \(\mathbb {R}^d = V_0(x) \supsetneq \cdots \supsetneq V_k(x) = 0\) together with a strictly decreasing exponent list \(\lambda _0 {\gt} \cdots {\gt} \lambda _{k-1}\) governing the growth \(\tfrac 1n \log \left\lVert A^{(n)}(x)v \right\rVert \to \lambda _i\) on each stratum \(V_i \setminus V_{i+1}\). This chapter collects its companion results. Many are surprisingly cheap: they follow from the statement of the main theorem, quantified over an arbitrary witness of its conclusion, with no access to the construction. To make this precise we bundle the conclusion as a predicate.

6.1 The bundled predicate and uniqueness

Definition 6.1 Bundled Oseledets filtration
#

For a measure \(\mu \), map \(T\), generator \(A\), count \(k\), exponent list \(\lambda : \mathrm{Fin}\, k \to \mathbb {R}\) and flag \(V : \mathrm{Fin}(k+1) \to X \to \mathrm{Submodule}\), the predicate \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\) asserts: \(\lambda \) is strictly antitone; each level \(V_i\) is a measurable subspace family; and \(\mu \)-a.e. \(x\) carries the strictly decreasing \(A\)-equivariant flag \(\mathbb {R}^d = V_0(x) \supsetneq \cdots \supsetneq V_k(x) = 0\) with exact growth rate \(\lambda _i\) on the stratum \(V_i \setminus V_{i+1}\). This is byte-identical to the conclusion of the main theorem.

Theorem 6.2 Repackaged existence
#

Under the standing hypotheses (ergodic \(T\), invertible measurable \(A\) with \(\log ^+\left\lVert A \right\rVert , \log ^+\left\lVert A^{-1} \right\rVert \in L^1\)), there exist \(k, \lambda , V\) with \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\).

Proof

Destructure the conclusion of \(\texttt{oseledets\_ filtration}\) and repackage its three conjuncts as the bundled predicate; the data match definitionally.

Theorem 6.3 Canonical sublevel characterization

If \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\) holds, then \(\mu \)-a.e. each interior flag level is exactly a growth-sublevel set: for every \(i\) and vector \(v\),

\[ v \in V_i(x) \iff v = 0 \ \lor \ \limsup _n \tfrac 1n \log \left\lVert A^{(n)}(x)v \right\rVert \le \lambda _i. \]
Proof

At a good point pick the stratum index \(j\) of \(v \ne 0\); the per-stratum convergence gives \(\limsup = \lambda _j\). Membership in \(V_i\) forces \(i \le j\), so by antitonicity \(\lambda _j \le \lambda _i\); conversely if \(v \notin V_i\) then \(j {\lt} i\) and \(\lambda _j {\gt} \lambda _i\) strictly, contradicting the bound. The disjunct \(v = 0\) handles \(\log 0\). No machinery beyond the a.e. block is used.

Theorem 6.4 Uniqueness of the spectrum and filtration
#

On a probability space, any two Oseledets filtration data \((k, \lambda , V)\) and \((k_2, \lambda _2, V_2)\) for the same cocycle agree: \(k = k_2\), the exponents coincide under the index cast, and \(\mu \)-a.e. the flags agree level by level.

Proof

At a single good point the set of realized growth limits equals \(\mathrm{range}\, \lambda \) and \(\mathrm{range}\, \lambda _2\); two strictly antitone enumerations of one finite set coincide, giving \(k = k_2\) and \(\lambda = \lambda _2\). Levelwise identity then follows from the sublevel characterization \(\ref{ae_mem_iff_limsup_le}\) applied to both data.

6.2 The top exponent as operator-norm growth

Lemma 6.5 Nontriviality
#

On a probability space with \(0 {\lt} d\), any Oseledets filtration has \(0 {\lt} k\).

Proof

If \(k = 0\) then at a good point \(\mathbb {R}^d = V_0(x) = V_{\mathrm{last}}(x) = 0\), forcing \(\mathrm{finrank} = 0\), contradicting \(d {\gt} 0\).

Theorem 6.6 Top exponent = norm growth

On a probability space, with \(A\) invertible and \(0 {\lt} k\), \(\mu \)-a.e. the operator-norm growth rate of the cocycle converges to the top exponent:

\[ \tfrac 1n \log \left\lVert A^{(n)}(x) \right\rVert \to \lambda _0. \]
Proof

Two-sided squeeze from the flag block. Lower: a vector \(v\) in the top stratum has \(\tfrac 1n\log \left\lVert A^{(n)}v \right\rVert \to \lambda _0\) and \(\left\lVert A^{(n)}v \right\rVert \le \left\lVert A^{(n)} \right\rVert \, \left\lVert v \right\rVert \). Upper: the column-sum bound \(\left\lVert M \right\rVert \le \sum _j \left\lVert M e_j \right\rVert \) on the \(L^2\) operator norm, each basis vector being nonzero, gives eventually \(\tfrac 1n\log \left\lVert A^{(n)} \right\rVert \le \lambda _0 + \varepsilon \). Neither Furstenberg–Kesten nor singular values are needed.

Corollary 6.7 Identification of the Furstenberg–Kesten constant

Any constant \(c\) to which \(\tfrac 1n\log \left\lVert A^{(n)}(x) \right\rVert \) converges \(\mu \)-a.e. (e.g. the Furstenberg–Kesten constant) equals \(\lambda _0\).

Proof

Both \(\ref{tendsto_log_opNorm_cocycle}\) and the hypothesis hold at a common good point; uniqueness of limits gives \(\lambda _0 = c\).

6.3 A.e.-constant multiplicities

Theorem 6.8 Deterministic dimension profile

For ergodic \(T\) and invertible \(A\), every Oseledets filtration has a deterministic dimension profile: there is a strictly decreasing \(m : \mathrm{Fin}(k+1) \to \mathbb {N}\) with \(m_0 = d\), \(m_k = 0\) and, \(\mu \)-a.e., \(\mathrm{finrank}\, V_i(x) = m_i\).

Proof

The dimension \(x \mapsto \mathrm{finrank}\, V_i(x)\) is measurable via the trace of the orthogonal projector, and \(T\)-invariant a.e. because equivariance through the invertible \(A(x)\) preserves dimension. Ergodicity makes each invariant \(\mathbb {N}\)-valued function a.e. constant. The profile structure (\(\mathrm{StrictAnti}\), endpoints) is read off one good point.

Corollary 6.9 Per-exponent multiplicities

For ergodic \(T\) and invertible \(A\), each exponent \(\lambda _i\) carries a positive deterministic multiplicity \(m_i = \dim V_i - \dim V_{i+1}\) with \(\sum _i m_i = d\).

Proof

Set \(m_i\) to the consecutive dimension drops of \(\ref{exists_finrank_ae_eq}\); positivity is strict antitonicity, and the telescoping sum equals \(m_0 - m_k = d\).

Theorem 6.10 MET with multiplicities

Under the standing hypotheses there exist \(k, \lambda , V\) and a strictly decreasing \(m\) with \(m_0 = d\), \(m_k = 0\), such that \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\) holds and \(\mu \)-a.e. \(\mathrm{finrank}\, V_i(x) = m_i\).

Proof

Obtain a witness from \(\ref{oseledets_filtration'}\) and apply \(\ref{exists_finrank_ae_eq}\) to it.

6.4 The Lyapunov spectrum

Definition 6.11 Sorted spectrum
#

The full Lyapunov spectrum with multiplicity is the total function \(\mathrm{exponents} : \mathrm{Fin}\, d \to \mathbb {R}\), whose \(i\)-th entry is the deterministic limit of \(\tfrac 1n\log \sigma _i(A^{(n)})\), sorted non-increasingly. The top entry is \(\mathrm{topExponent}\).

Theorem 6.12 Defining \(\sigma \)-limit and order

For each sorted index \(i\) and \(\mu \)-a.e. \(x\), \(\tfrac 1n\log \sigma _i(A^{(n)}(x)) \to \mathrm{exponents}_i\); moreover \(\mathrm{exponents}\) is antitone.

Proof

The deterministic exponent sequence is extracted by \(\mathrm{Classical.choose}\) from the singular-value convergence theorem underlying the MET; antitonicity and the a.e. limit are its defining specification.

Theorem 6.13 Eigenvalue tie

\(\mu \)-a.e., \(\exp (\mathrm{exponents}_i)\) is the \(i\)-th sorted eigenvalue of the Oseledets limit matrix \(\Lambda (x)\).

Proof

The \(\sigma \)-limit identifies \(\mathrm{lamSing}(x,i) = \mathrm{exponents}_i\) a.e.; combine with the eigenvalues of \(\Lambda \) being \(e^{\mathrm{lamSing}}\).

6.5 Exponent sums

Theorem 6.14 Sign characterizations of exponent sums
#

The sum \(\mathrm{sumPosExp}\) of the strictly positive exponents is nonnegative, vanishes iff all exponents are \(\le 0\), and is strictly positive iff some exponent is positive (and dually \(\mathrm{sumNegExp} \le 0\) with the mirror characterizations).

Proof

Each summand of \(\mathrm{sumPosExp}\) is strictly positive on the filter, so the sum is \(\ge 0\); a sum of nonnegatives vanishes iff the filter is empty, i.e. no exponent is positive.

Theorem 6.15 Telescoping identity for partial sums
#

For \(k \le d\), the ergodic growth rate \(\Gamma _k\) of the product of the top-\(k\) singular values equals the sum of the top-\(k\) exponents: \(\Gamma _k = \sum _{i{\lt}k} \mathrm{exponents}_i\).

Proof

Since \(\mathrm{sprod}_k = \prod _{i{\lt}k}\sigma _i\), the normalized \(\log \mathrm{sprod}_k\) is the finite sum of the per-index \(\tfrac 1n\log \sigma _i\), each converging to \(\mathrm{exponents}_i\). The sum of convergents converges to the sum of limits; uniqueness against the defining limit of \(\Gamma _k\) closes it.

6.6 Exterior (wedge) growth

Definition 6.16 Exterior cocycle generator
#

The \(k\)-th exterior generator \(\mathrm{extGen}\, k\, A\) sends \(x\) to the \(k\)-th compound matrix \(C_k(A x)\) of \(k\times k\) minors. Its iterated cocycle is the compound of the iterate: \(\mathrm{cocycle}(\mathrm{extGen}\, k\, A)\, T\, n\, x = C_k(A^{(n)}(x))\).

Theorem 6.17 \(k\)-volume growth rate

For \(k \le d\) and \(\mu \)-a.e. \(x\), the operator-norm growth of the compound cocycle converges to \(\Gamma _k\): \(\tfrac 1n\log \left\lVert C_k(A^{(n)}(x)) \right\rVert \to \Gamma _k\), the \(k\)-dimensional volume growth rate.

Proof

The operator norm of the compound matrix is \(\mathrm{sprod}_k\), the product of the top-\(k\) singular values; rewrite and apply the defining a.e. limit of \(\Gamma _k\).

Corollary 6.18 Positive sum as a maximal partial sum
#

Writing \(k_+ = \# \{ i : 0 {\lt} \mathrm{exponents}_i\} \), the positive-exponent sum equals the partial sum \(\Gamma _{k_+} = \sum _{i{\lt}k_+}\mathrm{exponents}_i\).

Proof

By antitonicity the strictly positive entries are exactly the top \(k_+\) indices, so the filtered positive sum coincides with the top-\(k_+\) prefix sum, which is \(\Gamma _{k_+}\) via \(\ref{gammaK_eq_sum_top_exponents}\).

6.7 The trace–determinant identity

Lemma 6.19 Product of singular values is the absolute determinant
#

For every \(n\), \(x\): \(\mathrm{sprod}\, A\, T\, d\, n\, x = \left\lvert \det A^{(n)}(x) \right\rvert \).

Proof

Squaring, \(\mathrm{sprod}_d^2 = \prod _i \sigma _i^2 = \det (M^{\top } M) = (\det M)^2\) for the symmetric Gram operator; take the nonnegative square root. No invertibility is needed.

Theorem 6.20 Determinant identity

The sum of all Lyapunov exponents equals the integral of \(\log \left\lvert \det \right\rvert \) of the generator:

\[ \sum _i \mathrm{exponents}_i = \int _X \log \left\lvert \det A(x) \right\rvert \, d\mu . \]
Proof

Two a.e. limits of \(\tfrac 1n\log \left\lvert \det A^{(n)} \right\rvert \): it equals \(\tfrac 1n\log \mathrm{sprod}_d \to \Gamma _d = \sum _i\mathrm{exponents}_i\) by \(\ref{sprod_d_eq_abs_det}\) and \(\ref{gammaK_eq_sum_top_exponents}\); and \(\log \left\lvert \det A^{(n)} \right\rvert \) is the additive Birkhoff sum of \(\log \left\lvert \det A \right\rvert \), whose ergodic average tends to \(\int \log \left\lvert \det A \right\rvert \). Uniqueness of limits closes the identity.

Corollary 6.21 Volume contraction

If \(\sum _i \mathrm{exponents}_i {\lt} 0\) then \(\mu \)-a.e. \(\left\lvert \det A^{(n)}(x) \right\rvert \to 0\).

Proof

Since \(\tfrac 1n\log \left\lvert \det A^{(n)} \right\rvert \) tends to a negative constant, \(\log \left\lvert \det A^{(n)} \right\rvert \to -\infty \), so its exponential tends to \(0\).

6.8 The inverse / time-reversed spectrum

Theorem 6.22 Inverse cocycle exponents

For each sorted index \(i\) and \(\mu \)-a.e. \(x\), the singular-value exponents of the inverse-matrix cocycle are the negated, reversed exponents of \(A\):

\[ \tfrac 1n\log \sigma _i\! \big((A^{(n)}(x))^{-1}\big) \to -\, \mathrm{exponents}_{\mathrm{rev}\, i}. \]
Proof

Singular-value reciprocity \(\sigma _i(M^{-1}) = \sigma _{\mathrm{rev}\, i}(M)^{-1}\) for invertible \(M\), applied to the iterate, turns the forward limit \(\mathrm{exponents}_{\mathrm{rev}\, i}\) into its negative.

Corollary 6.23 Top of the reversed spectrum is minus the bottom
#

\(\mu \)-a.e. the largest exponent of the inverse cocycle is \(-\, \mathrm{exponents}_{d-1}\), the negative of the smallest forward exponent.

Proof

Specialize \(\ref{tendsto_log_singularValue_inv_cocycle}\) at \(i = 0\), where \(\mathrm{rev}\, 0 = d-1\).

6.9 Restriction to invariant subbundles

Definition 6.24 Invariant subbundle
#

An invariant subbundle is a measurable family of fibre subspaces \(W(x) \le \mathbb {R}^d\) that is \(A\)-equivariant a.e.: \(A(x)\, W(x) = W(Tx)\).

Lemma 6.25 Dimension interlacing
#

At each ambient flag level, the dimension captured by the subbundle is bounded by the ambient dimension: \(\dim \big(W(x) \cap V_i(x)\big) \le \dim V_i(x)\), so the restricted multiplicities are a sub-multiset of the ambient ones.

Proof

Monotonicity of \(\mathrm{finrank}\) under \(W \cap V_i \le V_i\).

Theorem 6.26 Restricted strict Oseledets filtration
#

For ergodic \(T\), invertible \(A\), and an invariant subbundle \(W\), collapsing the constant-dimension levels of \(i \mapsto W \cap V_i\) yields a genuine strict Oseledets filtration inside \(W\): a strictly antitone \(\lambda '\) and a measurable family \(V'\) with, \(\mu \)-a.e., \(V'_0(x) = W(x)\), \(V'_{k'}(x) = 0\), strictly descending and \(A\)-equivariant, with exact growth rate \(\lambda '_i\) per stratum and all levels \(\le W(x)\).

Proof

Obtain a forward witness via \(\ref{oseledets_filtration'}\), restrict the flag to \(W\) and read its a.e.-constant dimension profile (the restricted analogue of \(\ref{exists_finrank_ae_eq}\)); enumerate the first-occurrence surviving indices via an order embedding to collapse repeats into a strict flag, inheriting equivariance and per-stratum growth. The top level is \(W\), not \(\top \), so the result is stated directly rather than through \(\ref{IsOseledetsFiltration}\).

6.10 The non-ergodic spectrum

Theorem 6.27 Non-ergodic exponents
#

For merely measure-preserving \(T\) (no ergodicity) and invertible measurable \(A\) with the standing integrability, there is a family of \(T\)-invariant integrable functions \(\lambda _i : X \to \mathbb {R}\) such that for each \(i {\lt} d\) and \(\mu \)-a.e. \(x\), \(\tfrac 1n\log \sigma _i(A^{(n)}(x)) \to \lambda _i(x)\). The exponents become invariant functions rather than constants.

Proof

The non-ergodic Kingman theorem applied to the subadditive cocycle \(\log \mathrm{sprod}_k\) produces invariant integrable partial-sum limits \(G_k\); set \(\lambda _i = G_{i+1} - G_i\), with the per-\(\sigma \) telescoping as in the ergodic case.

Corollary 6.28 Non-ergodic positive-exponent sum
#

Summing the positive parts \(\max (\lambda _i(x),0)\) over \(i {\lt} d\) yields a single \(T\)-invariant integrable function \(G_+ : X \to \mathbb {R}\), the non-ergodic analogue of the positive-exponent sum.

Proof

A finite sum of positive parts of the invariant integrable functions of \(\ref{exists_exponents_nonergodic}\) is invariant and integrable.

6.11 Regularity of the exponents

Theorem 6.29 Fekete infimum representation
#

The partial-sum growth rate is the infimum over \(n\) of the normalized integrals:

\[ \Gamma _k = \inf _n \frac{1}{n+1}\int _X \log \mathrm{sprod}_k(n+1,x)\, d\mu . \]
Proof

The integral sequence is subadditive (Fekete), so it converges to its infimum; a Fatou estimate against the dominating Birkhoff averages of \(\log ^+\left\lVert A^{\pm 1} \right\rVert \) identifies that limit with the a.e. growth rate \(\Gamma _k\) in both directions.

Theorem 6.30 Upper semicontinuity of partial sums and top exponent
#

Along a filter of generators \(B_i \to A\) for which each fixed-\(n\) integral is continuous, the partial-sum rate is upper semicontinuous: \(\limsup _i \Gamma _k(B_i) \le \Gamma _k(A)\); specializing \(k=1\) gives the same for the top exponent. This is USC, not continuity — equality can fail when a spectral gap closes.

Proof

\(\Gamma _k\) is an infimum of the per-\(n\) continuous normalized integrals (\(\ref{gammaK_eq_iInf}\)); for each \(n\), \(\Gamma _k(B_i)\) is below the \(n\)-th integral, whose limit along the filter is the \(n\)-th integral of \(A\), so \(\limsup _i \Gamma _k(B_i)\) is at most every term of the infimum.

Theorem 6.31 Lower semicontinuity of the bottom exponent
#

The bottom exponent \(\lambda _d = \Gamma _d - \Gamma _{d-1}\) is lower semicontinuous in the generator: \(\lambda _d(A) \le \liminf _i \lambda _d(B_i)\).

Proof

Writing \(\Gamma _d = \int \log \left\lvert \det \right\rvert \) (the determinant identity \(\ref{sumAllExp_eq_integral_log_abs_det}\)), which is continuous in the generator under the hypothesis, and \(\Gamma _{d-1}\) upper semicontinuous (\(\ref{gammaK_upperSemicontinuous}\)), the difference \(\Gamma _d - \Gamma _{d-1}\) is lower semicontinuous.

6.12 Singular one-sided bounds

Theorem 6.32 Forward top value
#

For ergodic \(T\) and a possibly-singular measurable generator with only \(\log ^+\left\lVert A \right\rVert \in L^1\) (no invertibility, no inverse integrability), the normalized positive-part log-norms \(\tfrac 1n\log ^+\left\lVert A^{(n)}(x) \right\rVert \) converge \(\mu \)-a.e. to a constant \(\lambda _1^+\).

Proof

Apply the ergodic Kingman theorem to the subadditive, bounded-below, integrable cocycle \(\log ^+\left\lVert A^{(n)} \right\rVert \); only the forward integrability is used.

Theorem 6.33 Upper bound on the singular top exponent
#

Under the same singular hypotheses there is \(\lambda _1^+\) with, \(\mu \)-a.e.,

\[ \limsup _n\Big(\tfrac 1n\log \left\lVert A^{(n)}(x) \right\rVert : \mathrm{EReal}\Big) \le \lambda _1^+. \]

The \(\limsup \) is taken in \(\mathrm{EReal}\) so the bound is unconditional even when the growth tends to \(-\infty \); this is one-sided only.

Proof

Termwise \(\log \le \log ^+\), then pass to the \(\mathrm{EReal}\) \(\limsup \); since the \(\log ^+\) sequence converges to \(\lambda _1^+\) (\(\ref{tendsto_top_posLogNorm}\)), its \(\limsup \) is \(\lambda _1^+\).

Theorem 6.34 Sharp \(\limsup \) in the expanding case
#

There is a forward top value \(\lambda _1^+\) (the a.e. limit of \(\tfrac 1n\log ^+\left\lVert A^{(n)} \right\rVert \)) such that, whenever \(\lambda _1^+ {\gt} 0\), \(\mu \)-a.e. the genuine log-norm \(\limsup \) is exactly \(\lambda _1^+\):

\[ \limsup _n\Big(\tfrac 1n\log \left\lVert A^{(n)}(x) \right\rVert : \mathrm{EReal}\Big) = \lambda _1^+. \]

The positivity hypothesis is essential; in the contracting case \(\lambda _1^+ = 0\) the genuine growth may tend to \(-\infty \) and equality fails.

Proof

The \(\le \) half is \(\ref{limsup_logNorm_le_top}\). For \(\ge \): where \(\tfrac 1n\log ^+\left\lVert A^{(n)} \right\rVert \to \lambda _1^+ {\gt} 0\) the sequence is eventually positive, forcing \(\log \left\lVert A^{(n)} \right\rVert {\gt} 0\), so \(\log ^+ = \log \) eventually; the two \(\mathrm{EReal}\) sequences agree eventually, hence so do their \(\limsup \)s, which equal \(\lambda _1^+\).

Theorem 6.35 Singular top-\(k\) volume upper bound
#

For ergodic \(T\) and a possibly-singular generator with \(\log ^+\left\lVert A \right\rVert \in L^1\), there is a constant \(\Gamma _k^+\) with, \(\mu \)-a.e.,

\[ \limsup _n\Big(\tfrac 1n\log \mathrm{sprod}_k(x) : \mathrm{EReal}\Big) \le \Gamma _k^+. \]

The top-\(k\) volume growth is bounded above unconditionally (the \(\mathrm{EReal}\) \(\limsup \) allows volume collapse), again one-sided only.

Proof

Since \(\mathrm{sprod}_k \ge 0\) is submultiplicative with no invertibility, the same \(\log ^+\)-of-a-nonnegative-subadditive-quantity Kingman construction gives the a.e.-constant value \(\Gamma _k^+\) and the termwise \(\log \le \log ^+\) domination transfers to the \(\mathrm{EReal}\) \(\limsup \).