The return criterion: growth of the periodic-point count, with no derivative

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

A self-map f of a type has return growth h when, for every t ≥ 1, the set of points with f^[t] x = x is finite and nonempty, and (1/t) log #{x | f^[t] x = x} → h. For a hyperbolic toral automorphism this h is the topological entropy and equals the Lyapunov exponent; the definition itself mentions neither a lift, a derivative nor a direction, only which points come back.

• returnCount f t := Nat.card {x // f^[t] x = x}, HasReturnGrowth f h;
• iterate_add_right — (· + c)^[t] = (· + t • c) in an additive monoid;
• add_right_eq_self_iff — a translation of an additive group fixes a point iff it is trivial;
• ★★ not_hasReturnGrowth_add_right — no translation of an infinite additive group has return growth: its return set at every t is infinite or empty;
• ★★★ cat_hasReturnGrowth — the cat map has return growth 2 log φ (#176).

Honest scope

• HasReturnGrowth asks for a limit; a limsup version would cover maps whose counts oscillate, and is not needed for either example.
• Translations are the only non-example proved; a general toral automorphism with an eigenvalue on the unit circle (e.g. a shear, #153) also has return sets that are infinite at some t, and is not treated.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §3.2 (periodic points and topological entropy); Mathlib/Dynamics/CatMapPeriodicPoints.lean (#176); specs/BACKLOG.md #177, #19, #176, #148.

The criterion

noncomputable def returnCount {α : Type u_1} (f : α → α) (t : ℕ) : ℕ

The number of points returning after t steps (0 if infinitely many, by Nat.card's convention; HasReturnGrowth rules that case out).

Equations

• returnCount f t = Nat.card { x : α // f^[t] x = x }

structure HasReturnGrowth {α : Type u_1} (f : α → α) (h : ℝ) : Prop

f has return growth h: at every t ≥ 1 finitely many but at least one point returns, and the count grows at rate h.

• finite (t : ℕ) : Finite { x : α // f^[t + 1] x = x }
• nonempty (t : ℕ) : Nonempty { x : α // f^[t + 1] x = x }
• tendsto : Filter.Tendsto (fun (t : ℕ) => Real.log ↑(returnCount f (t + 1)) / (↑t + 1)) Filter.atTop (nhds h)

Translations fail it

theorem iterate_add_right {M : Type u_1} [AddCommMonoid M] (c : M) (t : ℕ) : (fun (x : M) => x + c)^[t] = fun (x : M) => x + t • c

theorem add_right_eq_self_iff {G : Type u_1} [AddGroup G] (c x : G) : x + c = x ↔ c = 0

A translation fixes a point iff it is the trivial translation.

theorem not_hasReturnGrowth_add_right {G : Type u_1} [AddCommGroup G] [Infinite G] (c : G) (h : ℝ) : ¬HasReturnGrowth (fun (x : G) => x + c) h

★★ No translation of an infinite additive group has return growth: at every t its return set is all of the group (t • c = 0) or empty.

The cat map has it

theorem cat_hasReturnGrowth : HasReturnGrowth MeasureTheory.cat (2 * Real.log Real.goldenRatio)

★★★ The cat map has return growth 2 log φ: #Fix(cat^[t]) = L₂ₜ − 2 ≥ 1 is finite and positive at every t ≥ 1, and grows at the Lyapunov exponent (#176).