1
Introduction
▶
1.1
Setting
1.2
The three headline theorems
1.3
Structure of the proof
2
The linear cocycle and Furstenberg–Kesten
▶
2.1
The measure-preserving system and the linear cocycle
2.2
Measurability of the operator norm and the inverse
2.3
Positivity and submultiplicativity of the log-norm
2.4
Birkhoff-sum sandwich bounds
2.5
Integrability of each level
2.6
The Furstenberg–Kesten theorems
3
Ergodic theorems
▶
3.1
Maximal ergodic inequality
3.2
Birkhoff
3.3
Kingman
4
Lyapunov exponents and the limsup filtration
▶
4.1
Ultrametric growth functions
4.2
The upper Lyapunov growth function
4.3
The Lyapunov spectrum and the descending exponent list
4.4
The limsup filtration
4.5
Measurability of the filtration
5
The one-sided multiplicative ergodic theorem
▶
5.1
The Oseledets limit
5.2
The per-vector lower bound
5.3
The spectral upper bound and the determinant squeeze
5.4
Spectral identification of the filtration
5.5
Ruelle’s reverse cofactor bound and the top-gap envelope
5.6
Constancy of the spectrum
5.7
Assembling the target theorem
6
Companion results and extensions
▶
6.1
The bundled predicate and uniqueness
6.2
The top exponent as operator-norm growth
6.3
A.e.-constant multiplicities
6.4
The Lyapunov spectrum
6.5
Exponent sums
6.6
Exterior (wedge) growth
6.7
The trace–determinant identity
6.8
The inverse / time-reversed spectrum
6.9
Restriction to invariant subbundles
6.10
The non-ergodic spectrum
6.11
Regularity of the exponents
6.12
Singular one-sided bounds
7
The two-sided splitting
▶
7.1
The invertible setup and the backward generator
7.2
The strong one-sided export with dimensions
7.3
The Kingman means identification
7.4
Restricted cocycles and their exponent
7.5
The transversality crux
7.6
Spectral reflection
7.7
Measurability of the intersection bundle
7.8
Assembling the splitting
8
The continuous-flow multiplicative ergodic theorem
▶
8.1
Overview
8.2
The continuous-time data
8.3
Reduction to the discrete theorem
8.4
Between integer times
8.5
Equivariance at every real time
8.6
The continuous-flow theorem
Dependency graph
The Oseledets Multiplicative Ergodic Theorem in Lean 4
Marcel Morgenstern
1
Introduction
1.1
Setting
1.2
The three headline theorems
1.3
Structure of the proof
2
The linear cocycle and Furstenberg–Kesten
2.1
The measure-preserving system and the linear cocycle
2.2
Measurability of the operator norm and the inverse
2.3
Positivity and submultiplicativity of the log-norm
2.4
Birkhoff-sum sandwich bounds
2.5
Integrability of each level
2.6
The Furstenberg–Kesten theorems
3
Ergodic theorems
3.1
Maximal ergodic inequality
3.2
Birkhoff
3.3
Kingman
4
Lyapunov exponents and the limsup filtration
4.1
Ultrametric growth functions
4.2
The upper Lyapunov growth function
4.3
The Lyapunov spectrum and the descending exponent list
4.4
The limsup filtration
4.5
Measurability of the filtration
5
The one-sided multiplicative ergodic theorem
5.1
The Oseledets limit
5.2
The per-vector lower bound
5.3
The spectral upper bound and the determinant squeeze
5.4
Spectral identification of the filtration
5.5
Ruelle’s reverse cofactor bound and the top-gap envelope
5.6
Constancy of the spectrum
5.7
Assembling the target theorem
6
Companion results and extensions
6.1
The bundled predicate and uniqueness
6.2
The top exponent as operator-norm growth
6.3
A.e.-constant multiplicities
6.4
The Lyapunov spectrum
6.5
Exponent sums
6.6
Exterior (wedge) growth
6.7
The trace–determinant identity
6.8
The inverse / time-reversed spectrum
6.9
Restriction to invariant subbundles
6.10
The non-ergodic spectrum
6.11
Regularity of the exponents
6.12
Singular one-sided bounds
7
The two-sided splitting
7.1
The invertible setup and the backward generator
7.2
The strong one-sided export with dimensions
7.3
The Kingman means identification
7.4
Restricted cocycles and their exponent
7.5
The transversality crux
7.6
Spectral reflection
7.7
Measurability of the intersection bundle
7.8
Assembling the splitting
8
The continuous-flow multiplicative ergodic theorem
8.1
Overview
8.2
The continuous-time data
8.3
Reduction to the discrete theorem
8.4
Between integer times
8.5
Equivariance at every real time
8.6
The continuous-flow theorem