Arnold's cat map is strongly mixing on L²(T²)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #147; consumed by SigmaLayer/FibreRelaxation.lean.

CatMapMixing.lean proved decay of correlations, with a rate, for the indicators of rectangles of arcs. This file proves the statement with no rate and no restriction on the observables: for every f, g ∈ L²(T²),

∫ f(cat^n p) g(p) dp ⟶ (∫ f)(∫ g) as n → ∞,

★★★ tendsto_integral_comp_cat_iterate_mul. That is strong mixing in its textbook form, and it is packaged as such: ★★★ cat_mixing : Mixing cat volume, where Mixing is the predicate μ (f^[n] ⁻¹' s ∩ t) → μ s · μ t for all measurable s, t, shaped after Mathlib's Ergodic (and implying it, Mixing.ergodic; hence cat_ergodic).

The argument

The ε/3 argument of every textbook, with the dense class chosen to make the exact statement trivial.

1. Trigonometric polynomials are dense in L²(T²). Mathlib has the Fourier basis of L²(Fin 2 → T) (UnitAddTorus.hasSum_mFourier_series_L2); the measurable equivalence finTwoArrow : (Fin 2 → T) ≃ᵐ T × T carries Haar to Haar and the monomial mFourier n to the character chi (n 0, n 1), so every g ∈ L²(T²) is within any δ > 0 in energy of a finite combination of characters, ★★ exists_trigPoly_integral_normSq_sub_lt.
2. Characters decorrelate exactly after finitely many steps. ∫ χ_v(cat^n p) χ_w(p) is 1 if catZ^n v + w = 0 and 0 otherwise (integral_chi_iterate_mul_chi); for v ≠ 0 the orbit catZ^n v leaves every bounded set (tendsto_supNormZ_catZ_iterate_atTop, from the golden-ratio growth of CatMapMixing.lean), so for two trigonometric polynomials the correlation is equal to the product of the means from some lag on, ★★ eventually_integral_trigPoly_iterate_mul.
3. Cauchy–Schwarz pays for the rest. With P, Q the approximants of f, g at energy η², fg − PQ = (f−P)g + f(g−Q) − (f−P)(g−Q) and each piece is bounded by the product of the L² norms (norm_integral_mul_sub_integral_mul_le); composition with cat^n preserves the energy. The same identity on the four means gives the other side, and the total error is 2η(‖f‖₂ + ‖g‖₂ + η).

Honest scope

• No rate. The theorem is convergence; the rate for a general observable depends on the observable (on the decay of its Fourier coefficients), and the rate for rectangles is CatMapMixing.lean's business.
• The concrete matrix only, as upstream: the argument uses the growth of the frequency orbit and nothing else, so a general hyperbolic element of SL₂(ℤ) would go the same way with its own growth lemma; not attempted.
• Mixing is the two-set (strong) mixing; weak mixing and mixing of higher order are not defined.

References: Walters, An Introduction to Ergodic Theory (1982), Def. 1.6 and Thm. 1.28 (the approximation argument); Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §4.2 (the Fourier proof for toral automorphisms). In-corpus: Mathlib/Dynamics/CatMapWitness.lean (the map and the characters), Mathlib/Dynamics/CatMapMixing.lean (the growth lemma, Cauchy–Schwarz, the rate for rectangles), specs/BACKLOG.md #147, specs/residues.tsv R-019.

Strong mixing, as a predicate

structure Mixing {α : Type u_1} [MeasurableSpace α] (f : α → α) (μ : MeasureTheory.Measure α := by volume_tac) extends MeasureTheory.MeasurePreserving f μ μ : Prop

A map f : α → α is (strongly) mixing with respect to μ if it preserves μ and μ (f^[n] ⁻¹' s ∩ t) → μ s * μ t for all measurable s, t. Shaped after Ergodic.

• measurable : Measurable f
• map_eq : Measure.map f μ = μ
• tendsto_measure_preimage_iterate_inter ⦃s t : Set α⦄ : MeasurableSet s → MeasurableSet t → Filter.Tendsto (fun (n : ℕ) => μ (f^[n] ⁻¹' s ∩ t)) Filter.atTop (nhds (μ s * μ t))

theorem Mixing.ergodic {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α} (h : Mixing f μ) : Ergodic f μ

A mixing map is ergodic. A strictly invariant set s has μ (f^[n] ⁻¹' s ∩ sᶜ) = 0 at every lag, so the limit μ s * μ sᶜ vanishes and one factor is zero.

Trigonometric polynomials on T²

noncomputable def MeasureTheory.trigPoly {ι : Type u_1} (S : Finset ι) (a : ι → ℂ) (v : ι → ℤ × ℤ) : Torus2 → ℂ

A finite combination of characters on T²: ∑ i ∈ S, a i • χ_{v i}.

Equations

• MeasureTheory.trigPoly S a v p = ∑ i ∈ S, a i * MeasureTheory.chi (v i) p

theorem MeasureTheory.continuous_trigPoly {ι : Type u_1} (S : Finset ι) (a : ι → ℂ) (v : ι → ℤ × ℤ) : Continuous (trigPoly S a v)

theorem MeasureTheory.norm_trigPoly_le {ι : Type u_1} (S : Finset ι) (a : ι → ℂ) (v : ι → ℤ × ℤ) (p : Torus2) : ‖trigPoly S a v p‖ ≤ ∑ i ∈ S, ‖a i‖

theorem MeasureTheory.memLp_two_trigPoly {ι : Type u_1} (S : Finset ι) (a : ι → ℂ) (v : ι → ℤ × ℤ) : MemLp (trigPoly S a v) 2 volume

theorem MeasureTheory.integral_chi (v : ℤ × ℤ) : ∫ (p : Torus2), chi v p = if v = 0 then 1 else 0

∫ χ_v = [v = 0].

theorem MeasureTheory.integral_trigPoly {ι : Type u_1} (S : Finset ι) (a : ι → ℂ) (v : ι → ℤ × ℤ) : ∫ (p : Torus2), trigPoly S a v p = ∑ i ∈ S, if v i = 0 then a i else 0

The mean of a trigonometric polynomial is its constant coefficient.

Density of trigonometric polynomials in L²(T²)

Mathlib's Fourier basis lives on Fin 2 → T; finTwoArrow carries it to T × T.

theorem MeasureTheory.mFourier_eq_chi_finTwoArrow (n : Fin 2 → ℤ) (x : Fin 2 → AddCircle 1) : (UnitAddTorus.mFourier n) x = chi (n 0, n 1) (MeasurableEquiv.finTwoArrow x)

Mathlib's monomial mFourier n on Fin 2 → T is the character chi (n 0, n 1) on T².

theorem MeasureTheory.measurePreserving_finTwoArrow_haar : MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi fun (x : Fin 2) => AddCircle.haarAddCircle) volume

finTwoArrow carries the product of Haar measures on Fin 2 → T to Haar on T².

theorem MeasureTheory.exists_trigPoly_integral_normSq_sub_lt {g : Torus2 → ℂ} (hg : MemLp g 2 volume) {δ : ℝ} (hδ : 0 < δ) : ∃ (S : Finset (Fin 2 → ℤ)) (a : (Fin 2 → ℤ) → ℂ), ∫ (p : Torus2), ‖g p - trigPoly S a (fun (n : Fin 2 → ℤ) => (n 0, n 1)) p‖ ^ 2 < δ

★★ Trigonometric polynomials are dense in L²(T²): every L² function is within any δ > 0 in energy of a finite combination of characters. Mathlib's UnitAddTorus.hasSum_mFourier_series_L2 on Fin 2 → T, transported along finTwoArrow.

Characters decorrelate exactly after finitely many steps

theorem MeasureTheory.one_le_supNormZ {v : ℤ × ℤ} (hv : v ≠ 0) : 1 ≤ supNormZ v

theorem MeasureTheory.tendsto_supNormZ_catZ_iterate_atTop {v : ℤ × ℤ} (hv : v ≠ 0) : Filter.Tendsto (fun (n : ℕ) => supNormZ (catZ^[n] v)) Filter.atTop Filter.atTop

The frequency orbit of a nonzero index escapes to infinity, from the golden-ratio growth φ^{2n} ≤ φ³ ‖catZ^[n] v‖ ‖v‖ of CatMapMixing.lean.

theorem MeasureTheory.eventually_catZ_iterate_ne {v : ℤ × ℤ} (hv : v ≠ 0) (w : ℤ × ℤ) : ∀ᶠ (n : ℕ) in Filter.atTop, catZ^[n] v ≠ w

theorem MeasureTheory.continuous_chi_iterate_mul_chi (v w : ℤ × ℤ) (n : ℕ) : Continuous fun (p : Torus2) => chi v (cat^[n] p) * chi w p

theorem MeasureTheory.integrable_chi_iterate_mul_chi (v w : ℤ × ℤ) (n : ℕ) : Integrable (fun (p : Torus2) => chi v (cat^[n] p) * chi w p) volume

theorem MeasureTheory.integral_chi_iterate_mul_chi (v w : ℤ × ℤ) (n : ℕ) : ∫ (p : Torus2), chi v (cat^[n] p) * chi w p = if catZ^[n] v + w = 0 then 1 else 0

∫ χ_v(cat^n p) χ_w(p) = [catZ^n v + w = 0].

theorem MeasureTheory.eventually_integral_trigPoly_iterate_mul {ι : Type u_1} {κ : Type u_2} (S : Finset ι) (a : ι → ℂ) (v : ι → ℤ × ℤ) (T : Finset κ) (b : κ → ℂ) (w : κ → ℤ × ℤ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∫ (p : Torus2), trigPoly S a v (cat^[n] p) * trigPoly T b w p = (∫ (p : Torus2), trigPoly S a v p) * ∫ (p : Torus2), trigPoly T b w p

★★ Exact decorrelation of trigonometric polynomials: from some lag on, the correlation of two trigonometric polynomials under the cat map equals the product of their means.

The ε/3 argument

theorem MeasureTheory.memLp_two_comp_cat_iterate {F : Torus2 → ℂ} (hF : MemLp F 2 volume) (n : ℕ) : MemLp (fun (p : Torus2) => F (cat^[n] p)) 2 volume

theorem MeasureTheory.integral_normSq_comp_cat_iterate {F : Torus2 → ℂ} (hF : AEStronglyMeasurable F volume) (n : ℕ) : ∫ (p : Torus2), ‖F (cat^[n] p)‖ ^ 2 = ∫ (p : Torus2), ‖F p‖ ^ 2

theorem MeasureTheory.norm_integral_mul_le_sqrt {F G : Torus2 → ℂ} (hF : MemLp F 2 volume) (hG : MemLp G 2 volume) : ‖∫ (p : Torus2), F p * G p‖ ≤ √(∫ (p : Torus2), ‖F p‖ ^ 2) * √(∫ (p : Torus2), ‖G p‖ ^ 2)

Cauchy–Schwarz: ‖∫ F G‖ ≤ ‖F‖₂ ‖G‖₂.

theorem MeasureTheory.norm_integral_le_sqrt {F : Torus2 → ℂ} (hF : MemLp F 2 volume) : ‖∫ (p : Torus2), F p‖ ≤ √(∫ (p : Torus2), ‖F p‖ ^ 2)

‖∫ F‖ ≤ ‖F‖₂ on a probability space.

theorem MeasureTheory.norm_integral_mul_sub_integral_mul_le {f P g Q : Torus2 → ℂ} (hf : MemLp f 2 volume) (hP : MemLp P 2 volume) (hg : MemLp g 2 volume) (hQ : MemLp Q 2 volume) : ‖(∫ (p : Torus2), f p * g p) - ∫ (p : Torus2), P p * Q p‖ ≤ √(∫ (p : Torus2), ‖f p - P p‖ ^ 2) * √(∫ (p : Torus2), ‖g p‖ ^ 2) + √(∫ (p : Torus2), ‖f p‖ ^ 2) * √(∫ (p : Torus2), ‖g p - Q p‖ ^ 2) + √(∫ (p : Torus2), ‖f p - P p‖ ^ 2) * √(∫ (p : Torus2), ‖g p - Q p‖ ^ 2)

The bilinear error identity fg − PQ = (f−P)g + f(g−Q) − (f−P)(g−Q), integrated and bounded by Cauchy–Schwarz.

theorem MeasureTheory.tendsto_integral_comp_cat_iterate_mul {f g : Torus2 → ℂ} (hf : MemLp f 2 volume) (hg : MemLp g 2 volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (p : Torus2), f (cat^[n] p) * g p) Filter.atTop (nhds ((∫ (p : Torus2), f p) * ∫ (p : Torus2), g p))

★★★ The cat map is strongly mixing on L²(T²): for every f, g ∈ L², ∫ f(cat^n p) g(p) dp → (∫ f)(∫ g). The ε/3 argument through trigonometric polynomials.

theorem MeasureTheory.tendsto_integral_comp_cat_iterate_mul_real {f g : Torus2 → ℝ} (hf : MemLp f 2 volume) (hg : MemLp g 2 volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (p : Torus2), f (cat^[n] p) * g p) Filter.atTop (nhds ((∫ (p : Torus2), f p) * ∫ (p : Torus2), g p))

★★★ The real-valued form of tendsto_integral_comp_cat_iterate_mul.

theorem MeasureTheory.memLp_two_indicator_one {s : Set Torus2} (hs : MeasurableSet s) : MemLp (s.indicator 1) 2 volume

theorem MeasureTheory.tendsto_measureReal_preimage_cat_iterate_inter {s t : Set Torus2} (hs : MeasurableSet s) (ht : MeasurableSet t) : Filter.Tendsto (fun (n : ℕ) => volume.real (cat^[n] ⁻¹' s ∩ t)) Filter.atTop (nhds (volume.real s * volume.real t))

★★ The set form: vol (cat^[n] ⁻¹' s ∩ t) → vol s · vol t, in real numbers.

theorem MeasureTheory.cat_mixing : Mixing cat volume

★★★ Arnold's cat map is strongly mixing for Haar measure on T².

theorem MeasureTheory.cat_ergodic : Ergodic cat volume

The cat map is ergodic, as a corollary of mixing.