Return growth is invariant under conjugation; the affine cat maps have it

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

For a bijection e : α ≃ β and f : α → α, (e ∘ f ∘ e.symm)^[t] = e ∘ f^[t] ∘ e.symm, so e restricts to a bijection between the t-return sets of f and of its conjugate. Hence the return counts agree at every t, and HasReturnGrowth (#177) transports along e in both directions. Applied to the translation conjugacy affineCat c = τ_b ∘ cat ∘ τ_{−b} (#175), every affine cat map has the cat map's return count L₂ₜ − 2 (#176) at every t ≥ 1 and return growth 2 log φ.

• iterate_conj, iterate_conj_apply — the iterates of a conjugate;
• fixedPointsEquivConj — e as a bijection of return sets; returnCount_conj;
• ★★ HasReturnGrowth.conj, hasReturnGrowth_conj_iff — return growth is conjugation-invariant;
• HasReturnGrowth.unique — a map has return growth at most at one rate;
• MeasureTheory.affineCat_eq_conj_equiv, returnCount_affineCat, card_fixedPoints_affineCat_iterate;
• ★★★ MeasureTheory.affineCat_hasReturnGrowth — every affine cat map has return growth 2 log φ.

Honest scope

• Conjugation by a bijection only; a semiconjugacy (a surjection e with e ∘ f = g ∘ e) carries return sets forward but not their cardinalities, and no such statement is made.
• The concrete cat matrix only, through #175's conjugacy; for a general hyperbolic B ∈ GL₂(ℤ) the affine class p ↦ B p + c is conjugate to toral B by a translation whenever B − I is invertible over ℤ, which the scope note of CatMapAffine.lean discusses and which is not attempted here.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8, §3.2; Mathlib/Dynamics/ReturnCriterion.lean (#177, HasReturnGrowth, cat_hasReturnGrowth), Mathlib/Dynamics/CatMapAffine.lean (#175, affineCat_eq_conj), Mathlib/Dynamics/CatMapPeriodicPoints.lean (#176, card_fixedPoints_cat_iterate); specs/BACKLOG.md #182, #19, #175, #177.

Iterates and return sets of a conjugate

theorem iterate_conj {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : α → α) (t : ℕ) : (⇑e ∘ f ∘ ⇑e.symm)^[t] = ⇑e ∘ f^[t] ∘ ⇑e.symm

theorem iterate_conj_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : α → α) (t : ℕ) (y : β) : (⇑e ∘ f ∘ ⇑e.symm)^[t] y = e (f^[t] (e.symm y))

def fixedPointsEquivConj {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : α → α) (t : ℕ) : { x : α // f^[t] x = x } ≃ { y : β // (⇑e ∘ f ∘ ⇑e.symm)^[t] y = y }

e restricts to a bijection between the t-return sets of f and of its conjugate.

Equations

• One or more equations did not get rendered due to their size.

theorem returnCount_conj {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : α → α) (t : ℕ) : returnCount (⇑e ∘ f ∘ ⇑e.symm) t = returnCount f t

Return growth transports

theorem HasReturnGrowth.conj {α : Type u_1} {β : Type u_2} {f : α → α} {h : ℝ} (H : HasReturnGrowth f h) (e : α ≃ β) : HasReturnGrowth (⇑e ∘ f ∘ ⇑e.symm) h

★★ Return growth is invariant under conjugation by a bijection.

theorem symm_conj_conj {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : α → α) : ⇑e.symm ∘ (⇑e ∘ f ∘ ⇑e.symm) ∘ ⇑e.symm.symm = f

theorem hasReturnGrowth_conj_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : α → α) (h : ℝ) : HasReturnGrowth (⇑e ∘ f ∘ ⇑e.symm) h ↔ HasReturnGrowth f h

theorem HasReturnGrowth.unique {α : Type u_1} {f : α → α} {h h' : ℝ} (H : HasReturnGrowth f h) (H' : HasReturnGrowth f h') : h = h'

A map has return growth at most at one rate.

The affine cat maps

theorem MeasureTheory.affineCat_eq_conj_equiv (c : Torus2) : affineCat c = ⇑(MeasurableEquiv.addLeft (affineCatShift c)).toEquiv ∘ cat ∘ ⇑(MeasurableEquiv.addLeft (affineCatShift c)).symm

#175's conjugacy, read through the underlying Equiv.

theorem MeasureTheory.returnCount_affineCat (c : Torus2) (t : ℕ) : returnCount (affineCat c) t = returnCount cat t

The affine cat map has the cat map's return count at every t.

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

#Fix((affineCat c)^[t]) = L₂ₜ − 2, as for the cat map (#176).

theorem MeasureTheory.affineCat_hasReturnGrowth (c : Torus2) : HasReturnGrowth (affineCat c) (2 * Real.log Real.goldenRatio)

★★★ Every affine cat map has return growth 2 log φ: the base-read offset of #175 is invisible to the return criterion, stroke by stroke.