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. Several further layers, each with its own chapter, extend the development across suspension flows, classical entropy theory, symbolic dynamics, dimension theory, smooth examples, Pesin’s entropy formula, cohomological rigidity, and the descriptive set theory underpinning the singular filtration.

Suspension flows (Chapter 9): the exponents, ergodicity, and entropy of the flow built over a base map under a roof function. The representative-free flow exponent descends the base exponent through the Abramov normalization \(\lambda _{\mathrm{flow}}=\lambda _{\mathrm{base}}/\! \int \tau \), with the six cat-map instances; the time-one map of a Bernoulli suspension is ergodic exactly for an irrational roof; and for a rational roof the flow’s Kolmogorov–Sinai entropy descends to \(H_\nu /r\), giving the power rule \(h(T^{n})=n\, h(T)\).
Kolmogorov–Sinai entropy (Chapter 10): 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 11): 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 12): 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 13): 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.
Pesin’s entropy formula (Chapter 14): the volume case of the reverse inequality \(\sum _{\lambda _i{\gt}0}\lambda _i\le h_\mu (T)\) via a generator-free Rokhlin inequality, assembling both directions into the entropy formula \(h_\mu (T)=\sum _{\lambda _i{\gt}0}\lambda _i\) for an SRB (volume-absolutely-continuous) measure, crowned by the fully non-vacuous doubling-map instance \(h_\mu (T)=\sum \lambda ^{+}=\log 2\); the mixed-spectrum Ledrappier–Young case is stated honestly as the remaining wall.
Livšic theory (Chapter 15): the cohomological rigidity of Hölder cocycles—the abstract Livšic iff (a cocycle is a coboundary exactly when its periodic sums vanish), instantiated over the one-sided and two-sided full shifts, subshifts of finite type, the doubling map, and the Arnold cat map, together with the continuous, bounded, and full measurable rigidity tiers and the flow obstruction.

The final descriptive-set-theoretic layer (Chapter 18) develops Lusin’s theorem, Novikov’s generalized separation, the Kunugui–Novikov and compact-section projection theorems, and their payoff: the everywhere-Borel measurability of the singular Lyapunov filtration, refining the almost-everywhere measurability of the multiplicative core.

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.

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 16 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 17 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.