Lyapunov exponents of linear maps, and the cat map's

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #148; consumed by SigmaLayer/FibreLyapunov.lean.

Mathlib has no notion of Lyapunov exponent (MATHLIB-ABSENT(lyapunovExponent)). This file defines the one notion that needs no manifold: for a continuous linear map A of a real normed space and a direction v, HasLyapunovExponent A v l says log ‖Aⁿ v‖ / n → l. For the derivative of a smooth map this is the Lyapunov exponent of the tangent direction v; for a linear map the derivative is the map itself, and for a translation it is the identity.

The cat map

catR : ℝ² →L ℝ² is the matrix [[2,1],[1,1]], the lift of cat (cat_coe) and the action catZ on frequencies (catR_intCast). Its eigenvalues are φ² and φ⁻² = 2 − φ; the expanding and contracting linear forms ellUR, ellSR of CatMapMixing.lean's integer argument are the real ones here, and the geometric sandwich hasLyapunovExponent_of_geometric_bounds turns their scaling into the exponents:

• ★★ hasLyapunovExponent_catR: every direction off the stable line has exponent 2 log φ;
• ★ hasLyapunovExponent_catR_stable: every nonzero direction on it has exponent −2 log φ;
• hasLyapunovExponent_id: the identity has exponent 0 in every direction.

Honest scope

• Linear maps only. The exponent of a nonlinear map at a point, in a tangent direction, is the exponent of its derivative there; the Oseledets theorem (existence of exponents almost everywhere for a measure-preserving map) is not formalised and is not needed for the maps downstream, whose derivatives are constant.
• log ‖0‖ = 0 in Lean, so the zero direction has exponent 0 trivially; the theorems are stated for nonzero directions where that matters.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8 (the cat map's exponents) and Supplement S; Mathlib/Dynamics/CatMapWitness.lean (cat, catZ), Mathlib/Dynamics/CatMapMixing.lean (ellU, ellS, the golden-ratio facts); specs/BACKLOG.md #148.

The exponent of a direction under a linear map

def HasLyapunovExponent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] E) (v : E) (l : ℝ) : Prop

HasLyapunovExponent A v l: the direction v has Lyapunov exponent l under the continuous linear map A, i.e. log ‖Aⁿ v‖ / n → l.

Equations

• HasLyapunovExponent A v l = Filter.Tendsto (fun (n : ℕ) => Real.log ‖(A ^ n) v‖ / ↑n) Filter.atTop (nhds l)

theorem HasLyapunovExponent.unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : E →L[ℝ] E} {v : E} {l l' : ℝ} (h : HasLyapunovExponent A v l) (h' : HasLyapunovExponent A v l') : l = l'

theorem hasLyapunovExponent_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : E) : HasLyapunovExponent (ContinuousLinearMap.id ℝ E) v 0

The identity stretches nothing: exponent 0 in every direction.

theorem hasLyapunovExponent_of_geometric_bounds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] E) (v : E) {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) (hlow : ∀ (n : ℕ), a * r ^ n ≤ ‖(A ^ n) v‖) (hup : ∀ (n : ℕ), ‖(A ^ n) v‖ ≤ b * r ^ n) : HasLyapunovExponent A v (Real.log r)

The geometric sandwich: a direction squeezed between two geometric envelopes with the same ratio r has exponent log r.

The real cat matrix and its two eigenforms

noncomputable def MeasureTheory.catR : ℝ × ℝ →L[ℝ] ℝ × ℝ

The cat matrix [[2,1],[1,1]] as a continuous linear map of ℝ²: the lift of cat to the plane, and the derivative of cat at every point.

Equations

• MeasureTheory.catR = LinearMap.toContinuousLinearMap { toFun := fun (v : ℝ × ℝ) => (2 * v.1 + v.2, v.1 + v.2), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MeasureTheory.catR_apply (v : ℝ × ℝ) : catR v = (2 * v.1 + v.2, v.1 + v.2)

theorem MeasureTheory.cat_coe (x y : ℝ) : cat (↑x, ↑y) = (↑(catR (x, y)).1, ↑(catR (x, y)).2)

cat is catR read modulo ℤ².

theorem MeasureTheory.catR_intCast (v : ℤ × ℤ) : catR (↑v.1, ↑v.2) = (↑(catZ v).1, ↑(catZ v).2)

The frequency action catZ is catR on integer points.

noncomputable def MeasureTheory.ellUR (v : ℝ × ℝ) : ℝ

The expanding linear form v ↦ v₁ + (φ − 1) v₂ on ℝ²: catR scales it by φ².

Equations

• MeasureTheory.ellUR v = v.1 + (Real.goldenRatio - 1) * v.2

noncomputable def MeasureTheory.ellSR (v : ℝ × ℝ) : ℝ

The contracting linear form v ↦ v₁ − φ v₂ on ℝ²: catR scales it by 2 − φ = φ⁻².

Equations

• MeasureTheory.ellSR v = v.1 - Real.goldenRatio * v.2

theorem MeasureTheory.ellU_eq_ellUR (v : ℤ × ℤ) : ellU v = ellUR (↑v.1, ↑v.2)

theorem MeasureTheory.ellS_eq_ellSR (v : ℤ × ℤ) : ellS v = ellSR (↑v.1, ↑v.2)

theorem MeasureTheory.ellUR_catR (v : ℝ × ℝ) : ellUR (catR v) = Real.goldenRatio ^ 2 * ellUR v

theorem MeasureTheory.ellSR_catR (v : ℝ × ℝ) : ellSR (catR v) = (2 - Real.goldenRatio) * ellSR v

theorem MeasureTheory.ellUR_catR_pow (v : ℝ × ℝ) (n : ℕ) : ellUR ((catR ^ n) v) = Real.goldenRatio ^ (2 * n) * ellUR v

theorem MeasureTheory.ellSR_catR_pow (v : ℝ × ℝ) (n : ℕ) : ellSR ((catR ^ n) v) = (2 - Real.goldenRatio) ^ n * ellSR v

theorem MeasureTheory.two_sub_goldenRatio_pos : 0 < 2 - Real.goldenRatio

theorem MeasureTheory.two_sub_goldenRatio_lt_one : 2 - Real.goldenRatio < 1

theorem MeasureTheory.two_sub_goldenRatio_eq : 2 - Real.goldenRatio = Real.goldenRatio⁻¹ ^ 2

2 − φ = φ⁻².

The sup norm against the two forms

theorem MeasureTheory.abs_ellUR_le (v : ℝ × ℝ) : |ellUR v| ≤ Real.goldenRatio * ‖v‖

theorem MeasureTheory.abs_ellSR_le (v : ℝ × ℝ) : |ellSR v| ≤ Real.goldenRatio ^ 2 * ‖v‖

theorem MeasureTheory.norm_le_abs_ellUR_add_abs_ellSR (v : ℝ × ℝ) : ‖v‖ ≤ |ellUR v| + |ellSR v|

A vector is recovered from its two eigenforms: ‖v‖ ≤ |ℓU v| + |ℓS v|.

The exponents of the cat map

theorem MeasureTheory.norm_catR_pow_le (v : ℝ × ℝ) (n : ℕ) : ‖(catR ^ n) v‖ ≤ (|ellUR v| + |ellSR v|) * (Real.goldenRatio ^ 2) ^ n

theorem MeasureTheory.abs_ellUR_div_mul_le_norm_catR_pow (v : ℝ × ℝ) (n : ℕ) : |ellUR v| / Real.goldenRatio * (Real.goldenRatio ^ 2) ^ n ≤ ‖(catR ^ n) v‖

theorem MeasureTheory.hasLyapunovExponent_catR {v : ℝ × ℝ} (hv : ellUR v ≠ 0) : HasLyapunovExponent catR v (2 * Real.log Real.goldenRatio)

★★ The cat map stretches every direction off the stable line at rate 2 log φ: for v with ellUR v ≠ 0, log ‖catRⁿ v‖ / n → 2 log φ.

theorem MeasureTheory.ellSR_ne_zero_of_ne_zero {v : ℝ × ℝ} (hv : v ≠ 0) (hU : ellUR v = 0) : ellSR v ≠ 0

theorem MeasureTheory.norm_catR_pow_le_of_ellUR_eq_zero {v : ℝ × ℝ} (hU : ellUR v = 0) (n : ℕ) : ‖(catR ^ n) v‖ ≤ |ellSR v| * (2 - Real.goldenRatio) ^ n

theorem MeasureTheory.abs_ellSR_div_mul_le_norm_catR_pow (v : ℝ × ℝ) (n : ℕ) : |ellSR v| / Real.goldenRatio ^ 2 * (2 - Real.goldenRatio) ^ n ≤ ‖(catR ^ n) v‖

theorem MeasureTheory.hasLyapunovExponent_catR_stable {v : ℝ × ℝ} (hv : v ≠ 0) (hU : ellUR v = 0) : HasLyapunovExponent catR v (-(2 * Real.log Real.goldenRatio))

★ On the stable line the cat map contracts at rate 2 log φ: for v ≠ 0 with ellUR v = 0, log ‖catRⁿ v‖ / n → −2 log φ.