1
Introduction
▶
1.1
Setting
1.2
The three headline theorems of the multiplicative core
1.3
Structure of the proof
1.4
Beyond the multiplicative theory
1.5
A finite-dimensional quantum-information layer
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
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
9
Kolmogorov–Sinai entropy
▶
9.1
Partitions and Shannon entropy
9.2
Conditional entropy
9.3
Kolmogorov–Sinai entropy as a Fekete limit
9.4
The generator theorems
9.5
The Abramov–Rokhlin addition formula
9.6
The Margulis–Ruelle inequality and Rokhlin’s formula
10
Generators: Shannon–McMillan–Breiman and Krieger’s theorem
▶
10.1
The information function and its chain rules
10.2
The pointwise Shannon–McMillan–Breiman theorem
10.3
The Rokhlin tower lemma
10.4
The coding stack
10.5
The generator theorems
11
Multifractal analysis
▶
11.1
The coarse-grained formalism
11.2
Structure of the spectrum: convexity and monotonicity
11.3
The measure and flow layer
11.4
Local dimension and Hausdorff dimension
11.5
The symbolic entropy–dimension identity
11.6
The Bernoulli-suspension flow: a genuinely multifractal witness
12
Smooth maps and worked examples
▶
12.1
The derivative cocycle of a smooth self-map
12.2
Uniformly expanding maps: the foliation-free right-hand-side identity
12.3
Rokhlin’s entropy formula for an expanding map
12.4
The doubling map
12.5
The Arnold cat map
13
Quantum relative entropy and its monotonicity
▶
13.1
Density matrices and von Neumann entropy
13.2
Umegaki relative entropy and Klein’s inequality
13.3
Lieb’s joint-convexity theorem
13.4
The data-processing inequality
14
Petz recovery and quantum dynamical entropy
▶
14.1
Kraus channels and the Petz recovery map
14.2
Petz’s equality theorem
▶
14.2.1
The Choi \(-\log \) Loewner inequality
14.2.2
The modular realisation of relative entropy
14.2.3
The general channel: contraction rigidity (issue #28, no injectivity)
14.3
The modular-cocycle intertwining and the injectivity-free route
14.4
The Connes–Narnhofer–Thirring dynamical entropy and its abelian corner
Dependency graph
Ergodic Theory in Lean 4
Marcel Morgenstern
1
Introduction
1.1
Setting
1.2
The three headline theorems of the multiplicative core
1.3
Structure of the proof
1.4
Beyond the multiplicative theory
1.5
A finite-dimensional quantum-information layer
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
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
9
Kolmogorov–Sinai entropy
9.1
Partitions and Shannon entropy
9.2
Conditional entropy
9.3
Kolmogorov–Sinai entropy as a Fekete limit
9.4
The generator theorems
9.5
The Abramov–Rokhlin addition formula
9.6
The Margulis–Ruelle inequality and Rokhlin’s formula
10
Generators: Shannon–McMillan–Breiman and Krieger’s theorem
10.1
The information function and its chain rules
10.2
The pointwise Shannon–McMillan–Breiman theorem
10.3
The Rokhlin tower lemma
10.4
The coding stack
10.5
The generator theorems
11
Multifractal analysis
11.1
The coarse-grained formalism
11.2
Structure of the spectrum: convexity and monotonicity
11.3
The measure and flow layer
11.4
Local dimension and Hausdorff dimension
11.5
The symbolic entropy–dimension identity
11.6
The Bernoulli-suspension flow: a genuinely multifractal witness
12
Smooth maps and worked examples
12.1
The derivative cocycle of a smooth self-map
12.2
Uniformly expanding maps: the foliation-free right-hand-side identity
12.3
Rokhlin’s entropy formula for an expanding map
12.4
The doubling map
12.5
The Arnold cat map
13
Quantum relative entropy and its monotonicity
13.1
Density matrices and von Neumann entropy
13.2
Umegaki relative entropy and Klein’s inequality
13.3
Lieb’s joint-convexity theorem
13.4
The data-processing inequality
14
Petz recovery and quantum dynamical entropy
14.1
Kraus channels and the Petz recovery map
14.2
Petz’s equality theorem
14.2.1
The Choi \(-\log \) Loewner inequality
14.2.2
The modular realisation of relative entropy
14.2.3
The general channel: contraction rigidity (issue #28, no injectivity)
14.3
The modular-cocycle intertwining and the injectivity-free route
14.4
The Connes–Narnhofer–Thirring dynamical entropy and its abelian corner