The return criterion for orientation-reversing toral automorphisms, and on all of GL₂(ℤ)

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #180 (out of #19, #178, #179).

For B with det B = −1 the eigenvalues have product −1, so tr B = λ − λ⁻¹, the trace recurrence is tr Bᵗ⁺² = tr B · tr Bᵗ⁺¹ + tr Bᵗ, the closed form is tr Bᵗ = εᵗ (μᵗ + (−1)ᵗ μ⁻ᵗ) with μ = (|tr B| + √(tr B² + 4))/2 the spectral radius and ε the sign of the trace, and det(Bᵗ − 1) = (−1)ᵗ − tr Bᵗ + 1. Hyperbolicity is tr B ≠ 0:

• ★★★ hasReturnGrowth_toral_neg — det B = −1, tr B ≠ 0 give return growth log μ;
• ★★ not_hasReturnGrowth_toral_of_trace_eq_zero_neg — tr B = 0 gives B² = 1, every point returns at the second stroke;
• ★★★ hasReturnGrowth_toral_iff_neg — for det B = −1: return growth iff tr B ≠ 0;
• ★★★ hasReturnGrowth_toral_iff_of_det — on all of GL₂(ℤ): toral B has return growth at some rate iff (det B = 1 ∧ |tr B| > 2) ∨ (det B = −1 ∧ tr B ≠ 0).

Also tendsto_log_div_of_bounds, the squeeze c μᵗ ≤ uₜ ≤ C μᵗ ⇒ (1/t) log uₜ → log μ used by both this file and (inline) #178, now a lemma.

Honest scope

• The parity of t enters the bounds: at odd strokes the count is μᵗ − μ⁻ᵗ, at even strokes μᵗ + μ⁻ᵗ − 2; both are at least (1 − μ⁻²)² μᵗ and at most 4 μᵗ.
• Matrices with |det| ≠ 1 are not automorphisms of the torus and are out of scope.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8; Mathlib/Dynamics/ToralReturns.lean (#178), ToralReturnsConverse.lean (#179); specs/BACKLOG.md #180, #19.

The squeeze, as a lemma

theorem MeasureTheory.tendsto_log_div_of_bounds {u : ℕ → ℝ} {μ c C : ℝ} (hμ : 1 < μ) (hc : 0 < c) (hC : 0 < C) (h : ∀ (s : ℕ), c * μ ^ (s + 1) ≤ u s ∧ u s ≤ C * μ ^ (s + 1)) : Filter.Tendsto (fun (s : ℕ) => Real.log (u s) / (↑s + 1)) Filter.atTop (nhds (Real.log μ))

The squeeze: c μᵗ ≤ uₜ ≤ C μᵗ for t ≥ 1 gives (1/t) log uₜ → log μ.

The signed recurrence and the closed form

theorem MeasureTheory.det_pow_sub_one_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (t : ℕ) : (B ^ t - 1).det = (-1) ^ t - (B ^ t).trace + 1

theorem MeasureTheory.trace_pow_add_two_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (t : ℕ) : (B ^ (t + 2)).trace = B.trace * (B ^ (t + 1)).trace + (B ^ t).trace

noncomputable def MeasureTheory.spectralRadiusNeg (B : Matrix (Fin 2) (Fin 2) ℤ) : ℝ

The spectral radius of an orientation-reversing element: (|tr B| + √(tr B² + 4)) / 2.

Equations

• MeasureTheory.spectralRadiusNeg B = (|↑B.trace| + √(↑B.trace ^ 2 + 4)) / 2

theorem MeasureTheory.spectralRadiusNeg_pos (B : Matrix (Fin 2) (Fin 2) ℤ) : 0 < spectralRadiusNeg B

theorem MeasureTheory.one_lt_spectralRadiusNeg (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : ↑B.trace ≠ 0) : 1 < spectralRadiusNeg B

theorem MeasureTheory.spectralRadiusNeg_sub_inv (B : Matrix (Fin 2) (Fin 2) ℤ) : spectralRadiusNeg B - (spectralRadiusNeg B)⁻¹ = |↑B.trace|

μ − μ⁻¹ = |tr B|.

theorem MeasureTheory.trace_pow_eq_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (t : ℕ) : ↑(B ^ t).trace = traceSign B ^ t * (spectralRadiusNeg B ^ t + (-1) ^ t * (spectralRadiusNeg B)⁻¹ ^ t)

★★ The closed form of the trace, det B = −1: tr Bᵗ = εᵗ (μᵗ + (−1)ᵗ μ⁻ᵗ).

Nonvanishing and bounds, by parity

theorem MeasureTheory.traceSign_pow_even (B : Matrix (Fin 2) (Fin 2) ℤ) {t : ℕ} (ht : Even t) : traceSign B ^ t = 1

theorem MeasureTheory.count_bounds_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (hτ : ↑B.trace ≠ 0) (s : ℕ) : (1 - (spectralRadiusNeg B)⁻¹ ^ 2) ^ 2 * spectralRadiusNeg B ^ (s + 1) ≤ |(-1) ^ (s + 1) - ↑(B ^ (s + 1)).trace + 1| ∧ |(-1) ^ (s + 1) - ↑(B ^ (s + 1)).trace + 1| ≤ 4 * spectralRadiusNeg B ^ (s + 1) ∧ (-1) ^ (s + 1) - ↑(B ^ (s + 1)).trace + 1 ≠ 0

The fixed-point count at stroke t ≥ 1, with its two-sided bound.

theorem MeasureTheory.det_pow_sub_one_ne_zero_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (hτ : ↑B.trace ≠ 0) (s : ℕ) : (B ^ (s + 1) - 1).det ≠ 0

det(Bᵗ − 1) ≠ 0 for t ≥ 1.

theorem MeasureTheory.card_fixedPoints_toral_pow_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (hτ : ↑B.trace ≠ 0) (s : ℕ) : Nat.card { p : Torus2 // toral (B ^ (s + 1)) p = p } = ((-1) ^ (s + 1) - (B ^ (s + 1)).trace + 1).natAbs

★★ The fixed points of toral Bᵗ for det B = −1: |(−1)ᵗ − tr Bᵗ + 1| in number.

theorem MeasureTheory.hasReturnGrowth_toral_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (hτ : ↑B.trace ≠ 0) : HasReturnGrowth (toral B) (Real.log (spectralRadiusNeg B))

★★★ An orientation-reversing hyperbolic toral automorphism has return growth log μ.

The converse and the characterisation on GL₂(ℤ)

theorem MeasureTheory.not_hasReturnGrowth_toral_of_trace_eq_zero_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) (hτ : B.trace = 0) (h : ℝ) : ¬HasReturnGrowth (toral B) h

★★ tr B = 0, det B = −1 give B² = 1: every point returns at the second stroke.

theorem MeasureTheory.hasReturnGrowth_toral_iff_neg (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = -1) : (∃ (h : ℝ), HasReturnGrowth (toral B) h) ↔ B.trace ≠ 0

★★★ For det B = −1: return growth at some rate iff tr B ≠ 0.

theorem MeasureTheory.hasReturnGrowth_toral_iff_of_det (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = 1 ∨ B.det = -1) : (∃ (h : ℝ), HasReturnGrowth (toral B) h) ↔ B.det = 1 ∧ 2 < |↑B.trace| ∨ B.det = -1 ∧ B.trace ≠ 0

★★★ The return criterion on GL₂(ℤ): for det B = ±1, toral B has return growth at some rate iff (det B = 1 ∧ |tr B| > 2) ∨ (det B = −1 ∧ tr B ≠ 0).