Periodic points of the cat map grow at the Lyapunov exponent

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #176 (out of #19 and #150).

The fixed points of cat^[t] on T² are the kernel of the toral endomorphism Aᵗ − I. Lifting to the plane, they are the points C⁻¹m mod ℤ² for m ∈ ℤ², C = Aᵗ − I, so the fixed-point set is ℤ² / Cℤ², whose order is |det C| (Mathlib's Submodule.natAbs_det_basis_change). With Aᵗ = [[F₂ₜ₊₁, F₂ₜ], [F₂ₜ, F₂ₜ₋₁]] (catR_pow_apply) and Cassini's identity, det C = 2 − tr Aᵗ = 2 − L₂ₜ where L₂ₜ = 2F₂ₜ₊₁ − F₂ₜ is the Lucas number, so

#Fix(cat^[t]) = L₂ₜ − 2 = φ²ᵗ + φ⁻²ᵗ − 2 = (φᵗ − φ⁻ᵗ)²,

and (1/t) log #Fix(cat^[t]) → 2 log φ: the periodic points grow at exactly the Lyapunov exponent of hasLyapunovExponent_catR — the cat-map instance of topological entropy = Lyapunov exponent.

• MeasureTheory.lucasEven — L₂ₜ = 2F₂ₜ₊₁ − F₂ₜ, with ★ lucasEven_eq its Binet form φ²ᵗ + ψ²ᵗ and three_le_lucasEven_succ;
• MeasureTheory.cassini — F₍ₙ₊₂₎Fₙ − F₍ₙ₊₁₎² = (−1)ⁿ⁺¹;
• MeasureTheory.catLatMat, catLat, ★ det_catLatMat — the integer matrix Aᵗ − I and its determinant 2 − L₂ₜ;
• MeasureTheory.cat_iterate_coe — cat^[t] descends from catR ^ t;
• MeasureTheory.catFixLift, catFixLift_mem, catFixLift_surjective, ker_catFixLift — the parametrisation of the fixed points by ℤ², with kernel Cℤ²;
• ★★★ MeasureTheory.card_fixedPoints_cat_iterate — #Fix(cat^[t]) = L₂ₜ − 2 for t ≥ 1;
• ★★ MeasureTheory.tendsto_log_card_fixedPoints_cat — the growth rate is 2 log φ.

Honest scope

• The cat matrix only; for a general hyperbolic A ∈ SL₂(ℤ) the same argument gives |det(Aᵗ − I)| = |tr Aᵗ − 2| and growth at log of the spectral radius.
• "Topological entropy" is not defined here; the statement is the growth rate of the periodic-point count, which is what that entropy equals for a hyperbolic toral automorphism.
• t ≥ 1 throughout (cat^[0] = id has every point fixed).

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8 and §3.2 (periodic points of toral automorphisms, |det(Aⁿ − I)|); Walters, An Introduction to Ergodic Theory, §8.2; Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean (Submodule.natAbs_det_basis_change); in-corpus CatMapWitness.lean (cat), LyapunovExponent.lean (catR, cat_coe, hasLyapunovExponent_catR), ClassicalOtoc.lean (catR_pow_apply); specs/BACKLOG.md #176, #19, #150, #148.

Lucas numbers and Cassini

def MeasureTheory.lucasEven (n : ℕ) : ℤ

The even Lucas number L₂ₙ = 2F₂ₙ₊₁ − F₂ₙ, as an integer.

Equations

• MeasureTheory.lucasEven n = 2 * ↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n))

theorem MeasureTheory.cassini (n : ℕ) : ↑(Nat.fib (n + 2)) * ↑(Nat.fib n) - ↑(Nat.fib (n + 1)) ^ 2 = (-1) ^ (n + 1)

Cassini's identity, F₍ₙ₊₂₎ Fₙ − F₍ₙ₊₁₎² = (−1)ⁿ⁺¹.

theorem MeasureTheory.three_le_lucasEven_succ (s : ℕ) : 3 ≤ lucasEven (s + 1)

L₂ₜ ≥ 3 for t ≥ 1.

theorem MeasureTheory.lucasEven_eq (n : ℕ) : ↑(lucasEven n) = Real.goldenRatio ^ (2 * n) + Real.goldenConj ^ (2 * n)

★ Binet for the even Lucas numbers: L₂ₙ = φ²ⁿ + ψ²ⁿ.

The lattice Aᵗ − I

def MeasureTheory.catLatMat (t : ℕ) : Matrix (Fin 2) (Fin 2) ℤ

The integer matrix Aᵗ − I = [[F₂ₜ₊₁ − 1, F₂ₜ], [F₂ₜ, F₂ₜ₊₁ − F₂ₜ − 1]].

Equations

• MeasureTheory.catLatMat t = !![↑(Nat.fib (2 * t + 1)) - 1, ↑(Nat.fib (2 * t)); ↑(Nat.fib (2 * t)), ↑(Nat.fib (2 * t + 1)) - ↑(Nat.fib (2 * t)) - 1]

theorem MeasureTheory.det_catLatMat (s : ℕ) : (catLatMat (s + 1)).det = 2 - lucasEven (s + 1)

★ det(Aᵗ − I) = 2 − L₂ₜ for t ≥ 1, by Cassini.

noncomputable def MeasureTheory.catLat (t : ℕ) : (Fin 2 → ℤ) →ₗ[ℤ] Fin 2 → ℤ

The lattice map ℤ² → ℤ², m ↦ (Aᵗ − I) m.

Equations

• MeasureTheory.catLat t = Matrix.toLin' (MeasureTheory.catLatMat t)

theorem MeasureTheory.catLat_apply (t : ℕ) (m : Fin 2 → ℤ) : (catLat t) m = ![(↑(Nat.fib (2 * t + 1)) - 1) * m 0 + ↑(Nat.fib (2 * t)) * m 1, ↑(Nat.fib (2 * t)) * m 0 + (↑(Nat.fib (2 * t + 1)) - ↑(Nat.fib (2 * t)) - 1) * m 1]

theorem MeasureTheory.det_catLat (s : ℕ) : LinearMap.det (catLat (s + 1)) = 2 - lucasEven (s + 1)

theorem MeasureTheory.det_catLat_ne_zero (s : ℕ) : LinearMap.det (catLat (s + 1)) ≠ 0

theorem MeasureTheory.catLat_injective (s : ℕ) : Function.Injective ⇑(catLat (s + 1))

Aᵗ − I is injective on ℤ²: multiply by the adjugate.

The iterate descends from catR ^ t

theorem MeasureTheory.cat_iterate_coe (t : ℕ) (x y : ℝ) : cat^[t] (↑x, ↑y) = (↑((catR ^ t) (x, y)).1, ↑((catR ^ t) (x, y)).2)

cat^[t] on the torus is the descent of catR ^ t on the plane.

The real matrices Aᵗ − I and its adjugate

noncomputable def MeasureTheory.catCr (t : ℕ) (v : ℝ × ℝ) : ℝ × ℝ

The real matrix Aᵗ − I acting on the plane.

Equations

• MeasureTheory.catCr t v = ((↑(Nat.fib (2 * t + 1)) - 1) * v.1 + ↑(Nat.fib (2 * t)) * v.2, ↑(Nat.fib (2 * t)) * v.1 + (↑(Nat.fib (2 * t + 1)) - ↑(Nat.fib (2 * t)) - 1) * v.2)

noncomputable def MeasureTheory.catAdjR (t : ℕ) (w : ℝ × ℝ) : ℝ × ℝ

The adjugate of Aᵗ − I, acting on the plane.

Equations

• MeasureTheory.catAdjR t w = ((↑(Nat.fib (2 * t + 1)) - ↑(Nat.fib (2 * t)) - 1) * w.1 - ↑(Nat.fib (2 * t)) * w.2, -↑(Nat.fib (2 * t)) * w.1 + (↑(Nat.fib (2 * t + 1)) - 1) * w.2)

noncomputable def MeasureTheory.catDetR (t : ℕ) : ℝ

det(Aᵗ − I) as a real number.

Equations

• MeasureTheory.catDetR t = (↑(Nat.fib (2 * t + 1)) - 1) * (↑(Nat.fib (2 * t + 1)) - ↑(Nat.fib (2 * t)) - 1) - ↑(Nat.fib (2 * t)) * ↑(Nat.fib (2 * t))

theorem MeasureTheory.catDetR_eq (t : ℕ) : catDetR t = ↑(catLatMat t).det

theorem MeasureTheory.catDetR_succ (s : ℕ) : catDetR (s + 1) = ↑(2 - lucasEven (s + 1))

theorem MeasureTheory.catDetR_succ_ne_zero (s : ℕ) : catDetR (s + 1) ≠ 0

theorem MeasureTheory.catR_pow_eq_catCr_add (t : ℕ) (v : ℝ × ℝ) : (catR ^ t) v = catCr t v + v

theorem MeasureTheory.catCr_add (t : ℕ) (v w : ℝ × ℝ) : catCr t (v + w) = catCr t v + catCr t w

theorem MeasureTheory.catCr_smul (t : ℕ) (c : ℝ) (v : ℝ × ℝ) : catCr t (c • v) = c • catCr t v

theorem MeasureTheory.catAdjR_add (t : ℕ) (v w : ℝ × ℝ) : catAdjR t (v + w) = catAdjR t v + catAdjR t w

theorem MeasureTheory.catAdjR_catCr (t : ℕ) (v : ℝ × ℝ) : catAdjR t (catCr t v) = catDetR t • v

theorem MeasureTheory.catCr_catAdjR (t : ℕ) (w : ℝ × ℝ) : catCr t (catAdjR t w) = catDetR t • w

theorem MeasureTheory.catCr_intCast (t : ℕ) (k : Fin 2 → ℤ) : catCr t (↑(k 0), ↑(k 1)) = (↑((catLat t) k 0), ↑((catLat t) k 1))

On integer vectors, catCr is catLat.

The fixed points, parametrised by ℤ²

noncomputable def MeasureTheory.catFixVec (s : ℕ) (m : Fin 2 → ℤ) : ℝ × ℝ

The real lift of the fixed point attached to m ∈ ℤ²: (Aᵗ − I)⁻¹ m.

Equations

• MeasureTheory.catFixVec s m = (MeasureTheory.catDetR (s + 1))⁻¹ • MeasureTheory.catAdjR (s + 1) (↑(m 0), ↑(m 1))

theorem MeasureTheory.catCr_catFixVec (s : ℕ) (m : Fin 2 → ℤ) : catCr (s + 1) (catFixVec s m) = (↑(m 0), ↑(m 1))

theorem MeasureTheory.catFixVec_add (s : ℕ) (m n : Fin 2 → ℤ) : catFixVec s (m + n) = catFixVec s m + catFixVec s n

theorem MeasureTheory.coe_intCast_eq_zero (k : ℤ) : ↑↑k = 0

The integer k is 0 on the circle.

noncomputable def MeasureTheory.catFixLift (s : ℕ) : (Fin 2 → ℤ) →+ Torus2

ℤ² → T², m ↦ (Aᵗ − I)⁻¹ m mod ℤ²: the parametrisation of the fixed points.

Equations

• MeasureTheory.catFixLift s = AddMonoidHom.mk' (fun (m : Fin 2 → ℤ) => (↑(MeasureTheory.catFixVec s m).1, ↑(MeasureTheory.catFixVec s m).2)) ⋯

theorem MeasureTheory.catFixLift_apply (s : ℕ) (m : Fin 2 → ℤ) : (catFixLift s) m = (↑(catFixVec s m).1, ↑(catFixVec s m).2)

theorem MeasureTheory.catFixLift_mem (s : ℕ) (m : Fin 2 → ℤ) : cat^[s + 1] ((catFixLift s) m) = (catFixLift s) m

Every parametrised point is fixed.

theorem MeasureTheory.exists_int_of_coe_eq_zero {x : ℝ} (hx : ↑x = 0) : ∃ (k : ℤ), ↑k = x

A real number whose class is 0 is an integer.

theorem MeasureTheory.catFixLift_surjective (s : ℕ) (p : Torus2) (hp : cat^[s + 1] p = p) : ∃ (m : Fin 2 → ℤ), (catFixLift s) m = p

Every fixed point is parametrised.

theorem MeasureTheory.catFixLift_eq_zero_iff (s : ℕ) (m : Fin 2 → ℤ) : (catFixLift s) m = 0 ↔ m ∈ (catLat (s + 1)).range

The kernel of the parametrisation is the lattice (Aᵗ − I)ℤ².

The count

theorem MeasureTheory.card_fixedPoints_cat_iterate (s : ℕ) : Nat.card { p : Torus2 // cat^[s + 1] p = p } = (lucasEven (s + 1) - 2).natAbs

★★★ The number of fixed points of cat^[t] is L₂ₜ − 2 (t ≥ 1): the fixed-point set is ℤ² / (Aᵗ − I)ℤ², of order |det(Aᵗ − I)| = L₂ₜ − 2.

theorem MeasureTheory.card_fixedPoints_cat_iterate_int (s : ℕ) : ↑(Nat.card { p : Torus2 // cat^[s + 1] p = p }) = lucasEven (s + 1) - 2

The count, as an integer: L₂ₜ − 2.

The growth rate is the Lyapunov exponent

theorem MeasureTheory.card_fixedPoints_cat_iterate_real (s : ℕ) : ↑(Nat.card { p : Torus2 // cat^[s + 1] p = p }) = Real.goldenRatio ^ (2 * (s + 1)) + (Real.goldenRatio ^ (2 * (s + 1)))⁻¹ - 2

The count in closed form: φ²ᵗ + φ⁻²ᵗ − 2.

theorem MeasureTheory.tendsto_log_card_fixedPoints_cat : Filter.Tendsto (fun (s : ℕ) => Real.log ↑(Nat.card { p : Torus2 // cat^[s + 1] p = p }) / (↑s + 1)) Filter.atTop (nhds (2 * Real.log Real.goldenRatio))

★★ The periodic points of the cat map grow at the Lyapunov exponent: (1/t) log #Fix(cat^[t]) → 2 log φ.