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 recording the fully qualified name of the corresponding Lean declaration, and a green checkmark records that the statement (and, where shown, its proof) is fully formalized. The continuous integration deliberately does not build a doc-gen4 API reference (doing so would regenerate documentation for the entire Mathlib import closure), so the annotations are names to be looked up in the Lean source repository linked from this blueprint.

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 of the multiplicative core

The multiplicative core of 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 companion results (Chapter 6), the two-sided splitting (Chapter 7), and the continuous-flow theorem (Chapter 8) complete the multiplicative core.

1.4 Beyond the multiplicative theory

The library does not stop at the multiplicative theorems. Four further layers, each with its own chapter, extend the development across classical entropy theory, symbolic dynamics, dimension theory, and smooth examples.

Kolmogorov–Sinai entropy (Chapter 9): the Shannon entropy of a finite measurable partition, conditional entropy, the Kolmogorov–Sinai entropy as a Fekete limit over iterated joins, the generator theorems and the Abramov–Rokhlin addition formula, closing where the additive and multiplicative theories meet—the Margulis–Ruelle inequality \(h(T)\le \sum _{\lambda _i{\gt}0}\lambda _i\) and Rokhlin’s volume-distortion identity.
Generators (Chapter 10): the pointwise Shannon–McMillan–Breiman theorem (entropy equipartition), the Rokhlin–Kakutani tower lemma, a symbolic coding stack, and Krieger’s finite generator theorem: an ergodic aperiodic automorphism of entropy below \(\log k\) admits a two-sided generating partition with at most \(k\) cells.
Multifractal analysis (Chapter 11): the coarse-grained formalism—partition function \(Z_q\), mass exponent \(\tau (q)\), Rényi dimensions \(D_q\), singularity spectrum \(f(\alpha )\)—together with the pointwise local dimension, the Frostman/Billingsley bridge to Hausdorff dimension, and a Bernoulli-suspension witness whose Rényi spectrum is provably \(q\)-dependent.
Smooth maps and worked examples (Chapter 12): the derivative cocycle connecting the MET to smooth dynamics, the foliation-free expanding-case identity of the Pesin and Rokhlin right-hand sides, and the classical examples—the doubling map with its instantiated Rokhlin equality at rate \(\log 2\), and the ergodic Arnold cat map with its explicit Lyapunov spectrum.

Like the headline theorems, every result in these layers is formalized sorry-free and passes the same guarded axiom audit. The blueprint documents these principal chains rather than every module of the library; some supporting material (for instance the singular-filtration measurability layer) is not given a chapter of its own.

1.5 A finite-dimensional quantum-information layer

Built on the same matrix and continuous-functional-calculus infrastructure, the development also formalizes a self-contained finite-dimensional quantum-information layer, documented in the final two chapters. Chapter 13 develops the quantum relative entropy and its monotonicity: density matrices and the von Neumann entropy, the Umegaki relative entropy and Klein’s inequality, Lieb’s joint-convexity theorem, and the data-processing inequality for completely positive trace-preserving maps. Chapter 14 treats the Petz recovery map and both directions of Petz’s equality theorem—recovery implies saturation of the data-processing inequality and, fully generally, saturation implies recoverability—together with the CNT quantum dynamical entropy, whose abelian corner recovers the classical Kolmogorov–Sinai entropy of the ergodic-theory core. Like the rest of the development, these results are formalized sorry-free and pass the same guarded axiom audit.