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
Suspension flows: exponents, ergodicity, entropy
▶
9.1
The suspension space and its invariant measure
9.2
The flow Lyapunov exponent over the suspension
▶
9.2.1
The Abramov exponent formula
9.2.2
The representative-free descent
9.2.3
The cat-map suspension flow
9.3
Ergodicity of the time-one map
9.4
Entropy descent
9.5
Abstract Abramov flow-entropy homogeneity
9.6
The quotient-level suspension flow cocycle
▶
9.6.1
The cat-map instance
9.7
The Bowen–Walters metric on the suspension
▶
9.7.1
The variable-roof metric
9.8
Functoriality of the suspension on factor maps
10
Kolmogorov–Sinai entropy
▶
10.1
Partitions and Shannon entropy
10.2
Conditional entropy
10.3
Kolmogorov–Sinai entropy as a Fekete limit
10.4
The generator theorems
10.5
The Abramov–Rokhlin addition formula
10.6
The Margulis–Ruelle inequality and Rokhlin’s formula
11
Generators: Shannon–McMillan–Breiman and Krieger’s theorem
▶
11.1
The information function and its chain rules
11.2
The pointwise Shannon–McMillan–Breiman theorem
11.3
The Rokhlin tower lemma
11.4
The coding stack
11.5
The generator theorems
12
Multifractal analysis
▶
12.1
The coarse-grained formalism
12.2
Structure of the spectrum: convexity and monotonicity
12.3
The measure and flow layer
12.4
Local dimension and Hausdorff dimension
12.5
The symbolic entropy–dimension identity
12.6
The Bernoulli-suspension flow: a genuinely multifractal witness
12.7
The dynamical Rényi entropy rate and its factor monotonicity
▶
The static data-processing inequality
The dynamical rate and one-block factor codes
The Bernoulli closed form and the strict witness
The \(q = 1\) anchor: an honest degeneracy boundary
13
Smooth maps and worked examples
▶
13.1
The derivative cocycle of a smooth self-map
13.2
Uniformly expanding maps: the foliation-free right-hand-side identity
13.3
Rokhlin’s entropy formula for an expanding map
13.4
The doubling map
13.5
The Arnold cat map
▶
13.5.1
Strong mixing
13.5.2
Eigenfunction rigidity and the ergodic time-one cat suspension
13.6
The sharp Kolmogorov–Sinai entropy of the cat map
▶
13.6.1
The lower bound: grid partition and eigencoordinate telescoping
13.6.2
The upper bound: the Adler–Weiss two-box generator
13.6.3
The crown equality
13.7
Statistical laws for the cat map
▶
13.7.1
The Fourier-decay class and the Diophantine norm form
13.7.2
Exponential decay of correlations
13.7.3
Green–Kubo variance and concentration
13.7.4
A finite-sample rate for the exponent estimator
13.7.5
Transport to the suspension flow
13.8
The Adler–Weiss coding as a factor and the symbolic flow tower
▶
13.8.1
The coding as a factor and a conjugacy onto its range
13.8.2
The coarse two-box partition: a \(\log 2\) ceiling with strict positivity
13.8.3
Entropy across the two coding stages
13.8.4
The depth-two symbolic flow tower
14
Pesin’s entropy formula (volume case)
▶
14.1
Rokhlin’s inequality: the generator-free lower bound
14.2
The SRB property and the unstable-Jacobian bridge
14.3
The reverse inequality and the spectrum gate
14.4
Pesin’s entropy formula
▶
Vacuity disclosure (honest).
14.5
A witnessed instance: the doubling map
▶
The generator crux: dyadic arcs generate the Borel structure
15
Livšic theory
▶
15.1
The abstract Hölder Livšic theorem
15.2
Concrete instances
▶
15.2.1
The one-sided full shift
15.2.2
The two-sided full shift
15.2.3
Subshifts of finite type and the golden-mean shift
15.2.4
The doubling map
15.2.5
The Arnold cat map
15.3
Measurable rigidity tiers
▶
15.3.1
Continuous and bounded tiers
15.3.2
The full measurable tier via the natural extension
15.4
The flow tier
▶
15.4.1
The tier-III converse for constant-roof suspension flows
15.4.2
Hölder-regularity flow-Livšic
16
Quantum relative entropy and its monotonicity
▶
16.1
Density matrices and von Neumann entropy
16.2
Maximum entropy and strict positivity
16.3
Explicit block-inclusion Kraus form of the partial trace
16.4
Umegaki relative entropy and Klein’s inequality
16.5
Lieb’s joint-convexity theorem
16.6
The data-processing inequality
17
Petz recovery and quantum dynamical entropy
▶
17.1
Kraus channels and the Petz recovery map
17.2
Petz’s equality theorem
▶
17.2.1
The Choi \(-\log \) Loewner inequality
17.2.2
The modular realisation of relative entropy
17.2.3
The general channel: contraction rigidity (issue #28, no injectivity)
17.3
The modular-cocycle intertwining and the injectivity-free route
17.4
The Connes–Narnhofer–Thirring dynamical entropy and its abelian corner
▶
17.4.1
Finite-dimensional vanishing of the CNT rate (issue #26)
17.4.2
The abelian corner as a Fekete limit and the KS equality (issue #26)
17.4.3
Failure of subadditivity: an explicit counterexample (issue #26)
17.5
Genuinely non-commutative sealed dynamics (issue #59)
▶
17.5.1
Shared spectral lemmas
17.5.2
The dephasing recovery seal
17.5.3
The per-resolution non-commutativity certificate
17.5.4
The canonical-MASA incompatibility certificate
17.6
The finite reservoir: cap, generic rate engine, and Pauli saturation (issue #69)
▶
17.6.1
The reservoir cap and the boundedness of the entropy sequence
17.6.2
The generic cumulative-bounded rate engine
17.6.3
Pauli saturation at \(d = 2\): the cap is attained
17.7
The growing-finite quantum world (issue #70)
▶
17.7.1
The growing carrier, the product state, and the linear entropy law
17.7.2
Capacity enlargement and marginal consistency
17.7.3
The spatial entropy rate and its positivity
17.7.4
The Kronecker-lifted dephasing seal, uniform in the block
17.7.5
The bundled growing quantum world
17.8
The quantum Bernoulli shift and the finite modular clock (issue #71)
▶
17.8.1
The directed local system: commuting inclusion and shift
17.8.2
The shift-invariant product-state hierarchy
17.8.3
The temporal site-window rate
17.8.4
The per-level dephasing seal at the tracial blocks
17.8.5
The finite modular clock
17.8.6
The bundled quantum Bernoulli shift
18
Descriptive set theory: projection theorems and the everywhere-Borel filtration
▶
18.1
Lusin’s theorem
18.2
Analytic-set closure lemmas
18.3
Novikov’s generalized first separation theorem
18.4
The reduction ladder
18.5
The compact-section projection theorem
18.6
The everywhere-Borel singular Oseledets filtration
18.7
Descriptive complexity of the continuous-section seal (issue #61)
18.8
An honest frontier: the general \(\sigma \)-compact-section theorem
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
Suspension flows: exponents, ergodicity, entropy
9.1
The suspension space and its invariant measure
9.2
The flow Lyapunov exponent over the suspension
9.2.1
The Abramov exponent formula
9.2.2
The representative-free descent
9.2.3
The cat-map suspension flow
9.3
Ergodicity of the time-one map
9.4
Entropy descent
9.5
Abstract Abramov flow-entropy homogeneity
9.6
The quotient-level suspension flow cocycle
9.6.1
The cat-map instance
9.7
The Bowen–Walters metric on the suspension
9.7.1
The variable-roof metric
9.8
Functoriality of the suspension on factor maps
10
Kolmogorov–Sinai entropy
10.1
Partitions and Shannon entropy
10.2
Conditional entropy
10.3
Kolmogorov–Sinai entropy as a Fekete limit
10.4
The generator theorems
10.5
The Abramov–Rokhlin addition formula
10.6
The Margulis–Ruelle inequality and Rokhlin’s formula
11
Generators: Shannon–McMillan–Breiman and Krieger’s theorem
11.1
The information function and its chain rules
11.2
The pointwise Shannon–McMillan–Breiman theorem
11.3
The Rokhlin tower lemma
11.4
The coding stack
11.5
The generator theorems
12
Multifractal analysis
12.1
The coarse-grained formalism
12.2
Structure of the spectrum: convexity and monotonicity
12.3
The measure and flow layer
12.4
Local dimension and Hausdorff dimension
12.5
The symbolic entropy–dimension identity
12.6
The Bernoulli-suspension flow: a genuinely multifractal witness
12.7
The dynamical Rényi entropy rate and its factor monotonicity
The static data-processing inequality
The dynamical rate and one-block factor codes
The Bernoulli closed form and the strict witness
The \(q = 1\) anchor: an honest degeneracy boundary
13
Smooth maps and worked examples
13.1
The derivative cocycle of a smooth self-map
13.2
Uniformly expanding maps: the foliation-free right-hand-side identity
13.3
Rokhlin’s entropy formula for an expanding map
13.4
The doubling map
13.5
The Arnold cat map
13.5.1
Strong mixing
13.5.2
Eigenfunction rigidity and the ergodic time-one cat suspension
13.6
The sharp Kolmogorov–Sinai entropy of the cat map
13.6.1
The lower bound: grid partition and eigencoordinate telescoping
13.6.2
The upper bound: the Adler–Weiss two-box generator
13.6.3
The crown equality
13.7
Statistical laws for the cat map
13.7.1
The Fourier-decay class and the Diophantine norm form
13.7.2
Exponential decay of correlations
13.7.3
Green–Kubo variance and concentration
13.7.4
A finite-sample rate for the exponent estimator
13.7.5
Transport to the suspension flow
13.8
The Adler–Weiss coding as a factor and the symbolic flow tower
13.8.1
The coding as a factor and a conjugacy onto its range
13.8.2
The coarse two-box partition: a \(\log 2\) ceiling with strict positivity
13.8.3
Entropy across the two coding stages
13.8.4
The depth-two symbolic flow tower
14
Pesin’s entropy formula (volume case)
14.1
Rokhlin’s inequality: the generator-free lower bound
14.2
The SRB property and the unstable-Jacobian bridge
14.3
The reverse inequality and the spectrum gate
14.4
Pesin’s entropy formula
Vacuity disclosure (honest).
14.5
A witnessed instance: the doubling map
The generator crux: dyadic arcs generate the Borel structure
15
Livšic theory
15.1
The abstract Hölder Livšic theorem
15.2
Concrete instances
15.2.1
The one-sided full shift
15.2.2
The two-sided full shift
15.2.3
Subshifts of finite type and the golden-mean shift
15.2.4
The doubling map
15.2.5
The Arnold cat map
15.3
Measurable rigidity tiers
15.3.1
Continuous and bounded tiers
15.3.2
The full measurable tier via the natural extension
15.4
The flow tier
15.4.1
The tier-III converse for constant-roof suspension flows
15.4.2
Hölder-regularity flow-Livšic
16
Quantum relative entropy and its monotonicity
16.1
Density matrices and von Neumann entropy
16.2
Maximum entropy and strict positivity
16.3
Explicit block-inclusion Kraus form of the partial trace
16.4
Umegaki relative entropy and Klein’s inequality
16.5
Lieb’s joint-convexity theorem
16.6
The data-processing inequality
17
Petz recovery and quantum dynamical entropy
17.1
Kraus channels and the Petz recovery map
17.2
Petz’s equality theorem
17.2.1
The Choi \(-\log \) Loewner inequality
17.2.2
The modular realisation of relative entropy
17.2.3
The general channel: contraction rigidity (issue #28, no injectivity)
17.3
The modular-cocycle intertwining and the injectivity-free route
17.4
The Connes–Narnhofer–Thirring dynamical entropy and its abelian corner
17.4.1
Finite-dimensional vanishing of the CNT rate (issue #26)
17.4.2
The abelian corner as a Fekete limit and the KS equality (issue #26)
17.4.3
Failure of subadditivity: an explicit counterexample (issue #26)
17.5
Genuinely non-commutative sealed dynamics (issue #59)
17.5.1
Shared spectral lemmas
17.5.2
The dephasing recovery seal
17.5.3
The per-resolution non-commutativity certificate
17.5.4
The canonical-MASA incompatibility certificate
17.6
The finite reservoir: cap, generic rate engine, and Pauli saturation (issue #69)
17.6.1
The reservoir cap and the boundedness of the entropy sequence
17.6.2
The generic cumulative-bounded rate engine
17.6.3
Pauli saturation at \(d = 2\): the cap is attained
17.7
The growing-finite quantum world (issue #70)
17.7.1
The growing carrier, the product state, and the linear entropy law
17.7.2
Capacity enlargement and marginal consistency
17.7.3
The spatial entropy rate and its positivity
17.7.4
The Kronecker-lifted dephasing seal, uniform in the block
17.7.5
The bundled growing quantum world
17.8
The quantum Bernoulli shift and the finite modular clock (issue #71)
17.8.1
The directed local system: commuting inclusion and shift
17.8.2
The shift-invariant product-state hierarchy
17.8.3
The temporal site-window rate
17.8.4
The per-level dephasing seal at the tracial blocks
17.8.5
The finite modular clock
17.8.6
The bundled quantum Bernoulli shift
18
Descriptive set theory: projection theorems and the everywhere-Borel filtration
18.1
Lusin’s theorem
18.2
Analytic-set closure lemmas
18.3
Novikov’s generalized first separation theorem
18.4
The reduction ladder
18.5
The compact-section projection theorem
18.6
The everywhere-Borel singular Oseledets filtration
18.7
Descriptive complexity of the continuous-section seal (issue #61)
18.8
An honest frontier: the general \(\sigma \)-compact-section theorem