1 Introduction

This blueprint accompanies a sorry-free Lean 4 + Mathlib formalization of the Oseledets multiplicative ergodic theorem (MET) and a broad layer of companion results. It documents the mathematical content of the development and the dependency structure of its proof: every node carries a \lean annotation pointing at the corresponding Lean declaration, and a green checkmark records that the statement (and, where shown, its proof) is fully formalized. The API documentation generated by doc-gen4 is linked from each node.

1.1 Setting

Throughout, \((X, \mu )\) is a probability space and \(T : X \to X\) is an ergodic measure-preserving transformation. A linear cocycle of dimension \(d\) is generated by a measurable map

\[ A : X \to \mathrm{Mat}_{d}(\mathbb {R}), \qquad \det (A\, x) \neq 0 \text{ for all } x, \]

whose \(n\)-step product along the orbit of \(x\) is

\[ A^{(n)}(x) \; =\; A(T^{n-1}x)\cdots A(Tx)\, A(x), \qquad A^{(0)}(x) = I . \]

We impose the one-sided integrability condition

\[ \log ^{+}\left\lVert A \right\rVert , \ \log ^{+}\left\lVert A^{-1} \right\rVert \in L^{1}(\mu ), \]

where matrices act on \(\mathrm{EuclideanSpace}\ \mathbb {R}\ (\mathrm{Fin}\ d)\) so that \(\left\lVert \cdot \right\rVert \) is the \(L^2\) operator norm (submultiplicative). For \(v \neq 0\) the Lyapunov exponent in the direction \(v\) is the growth rate

\[ \bar\lambda (x, v) \; =\; \limsup _{n\to \infty } \tfrac 1n \log \left\lVert A^{(n)}(x)\, v \right\rVert . \]

1.2 The three headline theorems

The development proves three principal theorems, each formalized sorry-free and verified (by a guarded axiom audit) to depend only on the standard axioms \(\{ \texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}\} \).

One-sided MET (filtration form), : there are finitely many distinct Lyapunov exponents \(\lambda _1 {\gt} \cdots {\gt} \lambda _k\) and, for \(\mu \)-a.e. \(x\), a strictly decreasing, \(A\)-equivariant, measurable filtration

\[ \mathrm{EuclideanSpace}\ \mathbb {R}\ (\mathrm{Fin}\ d) = V^0_x \supsetneq V^1_x \supsetneq \cdots \supsetneq V^k_x = \{ 0\} \]

along which \(\tfrac 1n \log \left\lVert A^{(n)}(x)\, v \right\rVert \to \lambda _i\) for every \(v \in V^i_x \setminus V^{i+1}_x\). This is the central result; it is proved in Chapter 5.
Two-sided splitting, : when both the forward and backward filtrations are available, they are transverse and the space splits a.e. into an \(A\)-equivariant direct sum of Oseledets subspaces \(\mathbb {R}^d = \bigoplus _i E^i_x\) on which the cocycle grows at the exact two-sided rate \(\lambda _i\). Chapter 7.
Continuous-flow MET, : the analogue for a continuous-time linear cocycle over a measurable flow, obtained by reduction to the time-one map together with a between-times sandwich estimate. Chapter 8.

1.3 Structure of the proof

The proof proceeds in layers, mirrored by the chapters of this blueprint. Chapter 2 sets up the cocycle, the operator norm and its measurability, and the Furstenberg–Kesten extremal exponents. Chapter 3 develops the ergodic-theoretic engine: the maximal ergodic inequality, the pointwise Birkhoff theorem, and—crucially—Kingman’s subadditive ergodic theorem, which converts the subadditivity of the log-norms into almost-everywhere limits. Chapter 4 introduces the Lyapunov exponent as a measurable function, the Lyapunov spectrum, and the limsup filtration together with the measurability of its subspaces. Chapter 5 assembles the one-sided theorem through the Oseledets limit, the spectral upper bound and determinant squeeze, the spectral identification of the limsup filtration, and a top-gap envelope induction. The remaining chapters record the companion results (Chapter 6), the two-sided splitting (Chapter 7), and the continuous-flow theorem (Chapter 8).