Elementary worked examples of the multiplicative ergodic theorem

This module instantiates the constant-cocycle Lyapunov spectrum (Oseledets.exponents_const, Oseledets/Lyapunov/Extensions/ConstantCocycle.lean) on three classical dynamical systems. In each case the cocycle generator is a fixed real matrix M, so the Lyapunov exponents are exactly Real.log |λᵢ(M)| — the log-moduli of the eigenvalues of M, sorted in non-increasing order. These are documentation examples: they show how to discharge the ergodicity and integrability hypotheses on a concrete base, and how to read off the spectrum of a small matrix.

The three systems are:

• the doubling map y ↦ 2 • y on the circle, with generator M = !![2] (top exponent log 2);
• an irrational rotation y ↦ √2 + y on the circle, with generator M = !![1] (zero exponent: rotations are isometries);
• the Arnold cat-map matrix M = !![2,1;1,1], whose exponents are log((3 ± √5)/2).

A key linear-algebra helper, Oseledets.absMatrix_eq_self_of_posSemidef, shows that for a positive semidefinite generator the absolute value |M| = cfc |·| M is M itself, so its sorted eigenvalues are the eigenvalues of M. All three generators above are positive semidefinite, so the headline spectra are stated directly in terms of the eigenvalues of M.

Main results

• Oseledets.absMatrix_eq_self_of_posSemidef — |M| = M for positive semidefinite M.
• Oseledets.doublingMap_topExponent_eq_log_two — the top Lyapunov exponent of the doubling-map constant cocycle (M = !![2]) is Real.log 2.
• Oseledets.irrationalRotation_exponents_eq_zero — the Lyapunov exponent of the irrational rotation by √2 (constant cocycle M = !![1]) is 0.
• Oseledets.catMapMatrix_exponents — the two Lyapunov exponents of the cat-map matrix M = !![2,1;1,1] are Real.log ((3 + √5) / 2) and Real.log ((3 - √5) / 2).

Implementation notes

The genuine Arnold cat map is the toral automorphism of 𝕋² induced by !![2,1;1,1]. Mathlib has no n-torus type and no proof that hyperbolic toral automorphisms are ergodic, so the cat-map dynamics is not yet formalizable here. We therefore realize the cat-map matrix as a constant cocycle over an arbitrary ergodic base (we reuse the doubling map); the Lyapunov exponents depend only on M, so they coincide with the cat-map exponents even though the underlying dynamics differs. See the docstring of catMapMatrix_exponents for the precise caveat.

References

• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

The absolute value of a positive semidefinite matrix is itself

theorem Oseledets.absMatrix_eq_self_of_posSemidef {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.PosSemidef) : absMatrix M = M

For a positive semidefinite matrix the absolute value is the matrix itself. Since the spectrum of M is contained in [0, ∞), the function |·| agrees with the identity on spectrum ℝ M, so the continuous functional calculus collapses: |M| = cfc |·| M = cfc id M = M.

Consequently, for a positive semidefinite generator the sorted eigenvalues of |M| (which control the Lyapunov spectrum of the constant cocycle) are just the eigenvalues of M.

theorem Oseledets.eigenvalues₀_congr {d : ℕ} {A B : Matrix (Fin d) (Fin d) ℝ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : A = B) (i : Fin (Fintype.card (Fin d))) : hA.eigenvalues₀ i = hB.eigenvalues₀ i

The sorted-eigenvalue function depends only on the matrix, not on the chosen Hermitian witness: equal matrices have equal eigenvalues₀. (IsHermitian is a Prop, hence proof-irrelevant once the matrix is fixed.)

theorem Oseledets.eigenvalues₀_absMatrix_of_posSemidef {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.PosSemidef) (i : Fin (Fintype.card (Fin d))) : ⋯.eigenvalues₀ i = ⋯.eigenvalues₀ i

For a positive semidefinite M, the sorted eigenvalues of |M| are the sorted eigenvalues of M: a direct consequence of absMatrix_eq_self_of_posSemidef.

Sums and products of sorted eigenvalues, via trace and determinant

The trace and determinant of a Hermitian matrix are the sum and product of its eigenvalues. Both Mathlib identities are phrased with eigenvalues (indexed by the matrix index type Fin d); we reindex to eigenvalues₀ (indexed by Fin (Fintype.card (Fin d))) so they can be combined with the Oseledets spectrum, which uses eigenvalues₀.

theorem Oseledets.sum_eigenvalues₀_eq_trace {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.IsHermitian) : ∑ i : Fin (Fintype.card (Fin d)), hM.eigenvalues₀ i = M.trace

The sum of the sorted eigenvalues is the trace. A reindexing of Matrix.IsHermitian.trace_eq_sum_eigenvalues from eigenvalues to eigenvalues₀.

theorem Oseledets.prod_eigenvalues₀_eq_det {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} (hM : M.IsHermitian) : ∏ i : Fin (Fintype.card (Fin d)), hM.eigenvalues₀ i = M.det

The product of the sorted eigenvalues is the determinant. A reindexing of Matrix.IsHermitian.det_eq_prod_eigenvalues from eigenvalues to eigenvalues₀.

The measure setup on the unit circle

For the two circle examples the phase space is UnitAddCircle = AddCircle (1 : ℝ), equipped with its volume measure, which is a probability measure (UnitAddCircle.measure_univ). We record the two instances needed by the constant-cocycle machinery.

instance Oseledets.instFactLtRealOfNat_oseledets : Fact (0 < 1)

The unit circle has length 1 > 0, the standing fact for AddCircle (1 : ℝ).

instance Oseledets.instIsProbabilityMeasureUnitAddCircleVolume_oseledets : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

The volume on UnitAddCircle is a probability measure (total mass 1, UnitAddCircle.measure_univ).

Example 1 — the doubling map

The doubling map T : y ↦ 2 • y on the unit circle is ergodic (AddCircle.ergodic_nsmul). Its derivative is multiplication by 2, so the natural cocycle generator is M = !![2], a 1 × 1 matrix. Its single eigenvalue is 2, and the top Lyapunov exponent is Real.log 2.

noncomputable def Oseledets.doublingMap : UnitAddCircle → UnitAddCircle

The doubling map y ↦ 2 • y on the unit circle.

Equations

• Oseledets.doublingMap y = 2 • y

theorem Oseledets.ergodic_doublingMap : Ergodic doublingMap MeasureTheory.volume

The doubling map is ergodic for the volume (Haar) measure on the unit circle.

def Oseledets.doublingGen : Matrix (Fin 1) (Fin 1) ℝ

The constant cocycle generator of the doubling map: the 1 × 1 matrix !![2].

Equations

• Oseledets.doublingGen = !![2]

theorem Oseledets.doublingGen_transpose : doublingGen.transpose = doublingGen

doublingGen = !![2] is symmetric.

theorem Oseledets.doublingGen_isHermitian : doublingGen.IsHermitian

doublingGen = !![2] is Hermitian (over ℝ, the same as symmetric).

theorem Oseledets.doublingGen_det_ne_zero : doublingGen.det ≠ 0

det !![2] = 2 ≠ 0, so the generator is invertible.

theorem Oseledets.doublingGen_posSemidef : doublingGen.PosSemidef

!![2] is positive semidefinite: xᵀ M x = 2 (x₀)² ≥ 0.

theorem Oseledets.doublingGen_eigenvalue (i : Fin (Fintype.card (Fin 1))) : doublingGen_isHermitian.eigenvalues₀ i = 2

The single eigenvalue of !![2] is 2: the trace of a 1 × 1 matrix is its only entry, and the trace equals the sum (here a single term) of the eigenvalues.

theorem Oseledets.doublingMap_topExponent_eq_log_two : topExponent ergodic_doublingMap ⋯ ⋯ ⋯ ⋯ = Real.log 2

Doubling map: the top Lyapunov exponent is log 2. The constant cocycle with generator M = !![2] over the (ergodic) doubling map has top Lyapunov exponent Real.log 2: the unique exponent is log of the unique eigenvalue 2 of M. This is the priority worked example.

Example 2 — an irrational rotation

The rotation T : y ↦ √2 + y on the unit circle is ergodic because √2 is irrational, hence has infinite additive order (AddCircle.ergodic_add_left). A rotation is an isometry, so its derivative is the identity; the natural cocycle generator is M = !![1], with eigenvalue 1 and Lyapunov exponent log 1 = 0.

def Oseledets.rotationGen : Matrix (Fin 1) (Fin 1) ℝ

The constant cocycle generator of a circle rotation: the 1 × 1 identity !![1].

Equations

• Oseledets.rotationGen = !![1]

theorem Oseledets.rotationGen_transpose : rotationGen.transpose = rotationGen

rotationGen = !![1] is symmetric.

theorem Oseledets.rotationGen_isHermitian : rotationGen.IsHermitian

rotationGen = !![1] is Hermitian.

theorem Oseledets.rotationGen_det_ne_zero : rotationGen.det ≠ 0

det !![1] = 1 ≠ 0.

theorem Oseledets.rotationGen_posSemidef : rotationGen.PosSemidef

!![1] is positive semidefinite: xᵀ M x = (x₀)² ≥ 0.

theorem Oseledets.rotationGen_eigenvalue (i : Fin (Fintype.card (Fin 1))) : rotationGen_isHermitian.eigenvalues₀ i = 1

The single eigenvalue of the identity generator !![1] is 1 (trace = 1).

theorem Oseledets.ergodic_rotation_of_addOrderOf_eq_zero {a : UnitAddCircle} (ha : addOrderOf a = 0) : Ergodic (fun (x : UnitAddCircle) => a + x) MeasureTheory.volume

A rotation by an angle of infinite order is ergodic, parametric version. For any a : UnitAddCircle with addOrderOf a = 0 (equivalently, a is not a rational point of the circle), the rotation y ↦ a + y is ergodic. We use this with a = √2.

theorem Oseledets.addOrderOf_sqrtTwo_eq_zero : addOrderOf ↑√2 = 0

The rotation angle √2, viewed as a point of the unit circle, has infinite additive order: a point of AddCircle (1 : ℝ) has finite order iff its representative is rational, and √2 is irrational.

noncomputable def Oseledets.irrationalRotation : UnitAddCircle → UnitAddCircle

The irrational rotation y ↦ √2 + y on the unit circle.

Equations

• Oseledets.irrationalRotation y = ↑√2 + y

theorem Oseledets.ergodic_irrationalRotation : Ergodic irrationalRotation MeasureTheory.volume

The rotation by √2 is ergodic.

theorem Oseledets.irrationalRotation_exponents_eq_zero (i : Fin (Fintype.card (Fin 1))) : exponents ergodic_irrationalRotation ⋯ ⋯ ⋯ ⋯ ⟨↑i, ⋯⟩ = 0

Irrational rotation: the Lyapunov exponent is 0. The constant cocycle with the isometry generator M = !![1] over the (ergodic) irrational rotation by √2 has Lyapunov exponent 0: the unique eigenvalue of M is 1, and log 1 = 0. Rotations preserve lengths, so they exhibit no exponential growth.

Example 3 — the Arnold cat-map matrix

The Arnold cat map is the toral automorphism of 𝕋² induced by the matrix !![2,1;1,1]. Its ergodicity (hyperbolicity of toral automorphisms) is not available in Mathlib, so we realize the cat-map matrix as a constant cocycle over an ergodic base — concretely, the doubling map. The Lyapunov exponents depend only on the generator, so they are the genuine cat-map exponents.

The matrix is symmetric and positive definite with trace 3 and determinant 1. If a ≥ b are its (sorted) eigenvalues, then a + b = 3 and a b = 1, hence (a - b)² = (a+b)² - 4ab = 5, so a - b = √5, giving a = (3 + √5)/2 and b = (3 - √5)/2. The Lyapunov exponents are log a and log b.

def Oseledets.catMapGen : Matrix (Fin 2) (Fin 2) ℝ

The Arnold cat-map matrix !![2,1;1,1].

Equations

• Oseledets.catMapGen = !![2, 1; 1, 1]

theorem Oseledets.catMapGen_transpose : catMapGen.transpose = catMapGen

catMapGen = !![2,1;1,1] is symmetric.

theorem Oseledets.catMapGen_isHermitian : catMapGen.IsHermitian

catMapGen = !![2,1;1,1] is Hermitian.

theorem Oseledets.catMapGen_posDef : catMapGen.PosDef

The cat-map matrix is positive definite: xᵀ M x = (x₀)² + (x₀ + x₁)² > 0 for x ≠ 0.

theorem Oseledets.catMapGen_posSemidef : catMapGen.PosSemidef

The cat-map matrix is positive semidefinite.

theorem Oseledets.catMapGen_det_ne_zero : catMapGen.det ≠ 0

det !![2,1;1,1] = 2·1 - 1·1 = 1 ≠ 0.

theorem Oseledets.catMapGen_eigenvalues_sum : catMapGen_isHermitian.eigenvalues₀ 0 + catMapGen_isHermitian.eigenvalues₀ 1 = 3

The sum of the two sorted eigenvalues of the cat-map matrix is the trace, 3.

theorem Oseledets.catMapGen_eigenvalues_prod : catMapGen_isHermitian.eigenvalues₀ 0 * catMapGen_isHermitian.eigenvalues₀ 1 = 1

The product of the two sorted eigenvalues of the cat-map matrix is the determinant, 1.

theorem Oseledets.catMapGen_eigenvalues_le : catMapGen_isHermitian.eigenvalues₀ 1 ≤ catMapGen_isHermitian.eigenvalues₀ 0

The larger sorted eigenvalue dominates the smaller: eigenvalues₀ 1 ≤ eigenvalues₀ 0 (eigenvalues₀ is antitone).

theorem Oseledets.catMapGen_eigenvalues_closedForm : catMapGen_isHermitian.eigenvalues₀ 0 = (3 + √5) / 2 ∧ catMapGen_isHermitian.eigenvalues₀ 1 = (3 - √5) / 2

The two sorted eigenvalues of the cat-map matrix are (3 + √5)/2 and (3 - √5)/2.

From a + b = 3, a b = 1, and a ≥ b we get (a - b)² = (a+b)² - 4ab = 5, hence a - b = √5, and solving the linear system gives the closed forms.

theorem Oseledets.ergodic_catMapBase : Ergodic doublingMap MeasureTheory.volume

The constant cocycle realization of the cat-map matrix uses the doubling map as its ergodic base; only the (constant) generator catMapGen matters for the spectrum.

theorem Oseledets.catMapMatrix_exponents : exponents ergodic_catMapBase ⋯ ⋯ ⋯ ⋯ ⟨0, ⋯⟩ = Real.log ((3 + √5) / 2) ∧ exponents ergodic_catMapBase ⋯ ⋯ ⋯ ⋯ ⟨1, ⋯⟩ = Real.log ((3 - √5) / 2)

The cat-map matrix: closed-form Lyapunov spectrum. Realized as a constant cocycle with generator M = !![2,1;1,1] over the (ergodic) doubling map, the two Lyapunov exponents are Real.log ((3 + √5)/2) and Real.log ((3 - √5)/2) — the logs of the eigenvalues of the cat-map matrix.

Honesty caveat. The cocycle here is the constant matrix M = !![2,1;1,1], not the derivative cocycle of the genuine Arnold cat map (the hyperbolic toral automorphism of 𝕋²). The exponents nonetheless coincide with the cat-map exponents, because they are determined by M. The genuine toral-automorphism dynamics requires the ergodicity of hyperbolic toral automorphisms, which is not yet available in Mathlib (there is no n-torus type and no ℤ² Fourier basis).

theorem Oseledets.catMapMatrix_exponents_sum_eq_zero : exponents ergodic_catMapBase ⋯ ⋯ ⋯ ⋯ ⟨0, ⋯⟩ + exponents ergodic_catMapBase ⋯ ⋯ ⋯ ⋯ ⟨1, ⋯⟩ = 0

The cat-map exponents sum to zero (the cocycle is conservative: det M = 1). Equivalently, log a + log b = log (a b) = log 1 = 0.