Affine cat maps are translation-conjugate to the cat map

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

For c ∈ T² the affine cat map p ↦ A p + c, A = [[2, 1], [1, 1]], is conjugate to the cat map by a translation: A − I = [[1, 1], [1, 0]] has determinant −1, so it is invertible over ℤ and b := (−c₂, c₂ − c₁) solves b − A b = c, whence A p + c = b + A (p − b) (★★ affineCat_eq_conj). Strong mixing is invariant under conjugation by a measure-preserving measurable equivalence (★★ Mixing.conj_measurableEquiv, a preimage computation), so every affine cat map is strongly mixing (★★★ affineCat_mixing) and ergodic, and its lift to the plane has the same derivative catR as the cat map's, hence the same Lyapunov exponent 2 log φ off the stable line.

• ★★ Mixing.conj_measurableEquiv — strong mixing transports along a measure-preserving measurable equivalence: Mixing f μ → Mixing (e ∘ f ∘ e.symm) μ;
• MeasureTheory.affineCat, affineCatShift — the affine map and its conjugating translation;
• ★★ MeasureTheory.affineCat_eq_conj — affineCat c = τ_b ∘ cat ∘ τ_{−b};
• ★★★ MeasureTheory.affineCat_mixing, affineCat_ergodic, measurePreserving_affineCat;
• MeasureTheory.affineCatR, fderiv_affineCatR, ★ affineCatR_fderiv_hasLyapunovExponent, affineCat_coe — the lift to the plane, its constant derivative catR, the exponent, and the descent to the torus.

Honest scope

• The concrete matrix only, as in the rest of the cat-map line. For a general hyperbolic A ∈ SL₂(ℤ) the same statement needs det (A − I) = 2 − tr A ≠ 0, which holds whenever A is hyperbolic (|tr A| > 2), but A − I is then invertible over ℤ only when |2 − tr A| = 1, i.e. tr A = 3 or tr A = 1; otherwise the conjugacy exists over ℚ (finitely many torsion classes) and is not attempted here.
• Mixing.conj_measurableEquiv is stated for a measurable equivalence; conjugation by a merely measure-preserving bijection with measurable inverse is the same proof.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8 (affine maps of the torus); Mathlib/Dynamics/CatMapWitness.lean (cat, cat_add, catHom), CatMapStrongMixing.lean (Mixing, cat_mixing), LyapunovExponent.lean (catR, ellUR, hasLyapunovExponent_catR); specs/BACKLOG.md #175, #19, #153, #147, #148.

Strong mixing is invariant under conjugation

theorem Mixing.conj_measurableEquiv {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α} (h : Mixing f μ) (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) : Mixing (⇑e ∘ f ∘ ⇑e.symm) μ

★★ Strong mixing transports along a measure-preserving measurable equivalence.

The affine cat map

noncomputable def MeasureTheory.affineCat (c : Torus2) : Torus2 → Torus2

The affine cat map p ↦ A p + c.

Equations

• MeasureTheory.affineCat c p = MeasureTheory.cat p + c

noncomputable def MeasureTheory.affineCatShift (c : Torus2) : Torus2

The translation conjugating affineCat c to cat: b = (−c₂, c₂ − c₁) solves b − A b = c, since (A − I)⁻¹ = [[0, 1], [1, −1]] over ℤ.

Equations

• MeasureTheory.affineCatShift c = (-c.2, c.2 - c.1)

theorem MeasureTheory.affineCat_apply (c p : Torus2) : affineCat c p = cat p + c

theorem MeasureTheory.affineCatShift_sub_cat (c : Torus2) : affineCatShift c - cat (affineCatShift c) = c

b − A b = c for b = affineCatShift c.

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

★★ The affine cat map is translation-conjugate to the cat map: affineCat c = τ_b ∘ cat ∘ τ_{−b} with b = affineCatShift c.

theorem MeasureTheory.affineCat_mixing (c : Torus2) : Mixing (affineCat c) volume

★★★ Every affine cat map is strongly mixing.

theorem MeasureTheory.affineCat_ergodic (c : Torus2) : Ergodic (affineCat c) volume

theorem MeasureTheory.measurePreserving_affineCat (c : Torus2) : MeasurePreserving (affineCat c) volume volume

The lift to the plane and its Lyapunov exponent

noncomputable def MeasureTheory.affineCatR (c : ℝ × ℝ) : ℝ × ℝ → ℝ × ℝ

The lift of affineCat to the plane.

Equations

• MeasureTheory.affineCatR c v = MeasureTheory.catR v + c

theorem MeasureTheory.fderiv_affineCatR (c v : ℝ × ℝ) : fderiv ℝ (affineCatR c) v = catR

theorem MeasureTheory.affineCatR_fderiv_hasLyapunovExponent (c v : ℝ × ℝ) {w : ℝ × ℝ} (hw : ellUR w ≠ 0) : HasLyapunovExponent (fderiv ℝ (affineCatR c) v) w (2 * Real.log Real.goldenRatio)

★ The lift's derivative has exponent 2 log φ in every direction off the stable line — the offset does not enter.

theorem MeasureTheory.affineCat_coe (a b x y : ℝ) : affineCat (↑a, ↑b) (↑x, ↑y) = (↑(affineCatR (a, b) (x, y)).1, ↑(affineCatR (a, b) (x, y)).2)

The affine cat map descends from its lift.