Exponential decay of correlations for rectangles under Arnold's cat map

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #118(i); consumed by SigmaLayer/FibreCellDecay.lean and Mathlib/Dynamics/CatMapStrongMixing.lean.

CatMapWitness.lean proved that the cat map (x, y) ↦ (2x + y, x + y) on T² decorrelates the single trigonometric observable Re e^{2πix}, with correlations exactly zero at every nonzero lag. That is a witness. This file proves the statement a coarse-graining actually needs: the indicator of any rectangle (a, b) × (c, d) of arcs has correlations decaying like 4 · 2^{-⌊(n−2)/3⌋}, a summable envelope, and the same for the pair correlation of two different rectangles.

The argument

Four stages, each a section below.

1. The frequency orbit grows. catZ (m, n) = (2m + n, m + n) is the transpose action on character indices. The integer quadratic form m² − mn − n² is catZ-invariant and never vanishes on a nonzero integer vector (its discriminant 5 is not a square: a zero would make the golden ratio rational, goldenRatio_irrational), while the expanding linear form is multiplied by φ² at each step. Hence ★ goldenRatio_pow_le_supNormZ_catZ_iterate, φ^{2n} ≤ φ³ ‖catZ^[n] v‖ ‖v‖, and ★ catCutoff_lt_supNormZ_catZ_iterate: for n ≥ 2 every nonzero frequency in the box of half-width catCutoff n = 4^{⌊(n−2)/3⌋} is carried strictly outside it. No eigenvector is ever written down; φ² = φ + 1 does all the work.
2. Arcs. The indicator of an arc of the unit circle, read through the representative in (0, 1], has Fourier coefficients (e^{-2πinb} − e^{-2πina}) / (−2πin) (fourierCoeff_arcInd), hence ★ norm_fourierCoeff_arcInd_le: ‖â(n)‖ ≤ 1/(π|n|).
3. Truncation. trunc R u keeps |n| ≤ R. Mathlib's Parseval (tsum_sq_fourierCoeff) identifies the L² truncation error with the tail of the series (integral_normSq_sub_trunc), Bessel bounds the truncation's energy (integral_normSq_trunc_le), and ∑_{|n|>R} n⁻² ≤ 4/R (tsum_tail_inv_sq_le) give ★★ integral_normSq_arcInd_sub_trunc_le: the error of truncating an arc is at most 1/R.
4. Rectangles and the main term. A rectangle is u(x) v(y); its truncation is the product of the truncations, a trigonometric polynomial on the frequency box, with L² error at most 4/R (integral_normSq_rect_sub_trunc_le, Fubini). Under cat^[n] the box is carried off itself, so by character orthogonality the integral of one truncated rectangle after n steps against another collapses to the product of the means, ★ integral_rect_trunc_mul_rect_trunc. Two Cauchy–Schwarz estimates (normSq_integral_mul_le) control the error terms, and ★★ norm_integral_rect_iterate_mul_sub_le is the bound at lags n ≥ 2; at lags 0, 1 the trivial bound 1 applies.

The results

• ★★ abs_integral_rectIndR_iterate_mul_sub_le_env: for any two rectangles of arcs, |∫ 1_A(cat^n p) 1_B(p) − |A||B|| ≤ catRectEnv n, where catRectEnv n = 1 for n < 2 and 4 / 2^{⌊(n−2)/3⌋} afterwards. This is the pair (mixing) statement.
• ★★★ cat_hasCorrelationDecay_rectIndR: the corpus's HasCorrelationDecay for the indicator of any rectangle of arcs, with ★ summable_catRectEnv (catRectEnv n ≤ 13 (4/5)^n).

Honest scope

• Rectangles of arcs only, with a rate. Indicators of products of arcs, and by linearity their finite combinations. The statement for a general L² observable — convergence of the correlation with no rate — is CatMapStrongMixing.lean (★★★ tendsto_integral_comp_cat_iterate_mul, by the density of trigonometric polynomials and an ε/3 argument); the rate is what this file adds, and it is for rectangles only.
• The concrete matrix only, as in CatMapWitness.lean: [[2,1],[1,1]]. The argument uses nothing about it beyond φ² = φ + 1 and the invariant form, so a general hyperbolic element of SL₂(ℤ) would go the same way with its own quadratic form; not attempted.
• The constants are not sharp. The true rate is φ^{-2n} up to polynomial factors; the cutoff 4^{⌊(n−2)/3⌋} was chosen to keep the envelope's square root a natural number, and the trivial bound covers lags 0 and 1. Nothing downstream is sensitive to this.
• The arc indicator is read through the representative in (0, 1], so its value at the two endpoints is a convention; everything here is insensitive to it.

References: Arnold–Avez, Ergodic Problems of Classical Mechanics (1968), §1.16; the Fourier proof of mixing for hyperbolic toral automorphisms is standard (Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §4.2). In-corpus: Mathlib/Dynamics/CatMapWitness.lean (the map, the characters, the orthogonality), Mathlib/Dynamics/CorrelationDecay.lean (the predicate and its consumers), specs/BACKLOG.md #118, specs/residues.tsv R-019.

Stage 1: the frequency orbit of catZ grows geometrically

catZ (m, n) = (2m + n, m + n) is the transpose action of the cat map on character indices (chi_cat). Its eigenvalues are φ² and φ⁻², with φ the golden ratio, and the integer quadratic form m² − mn − n² is invariant and never vanishes on a nonzero integer vector (its discriminant 5 is not a square, i.e. φ is irrational). The expanding component of a nonzero integer vector is therefore bounded below by 1 / (φ² ‖v‖), and the orbit grows like φ^{2n}.

def MeasureTheory.supNormZ (v : ℤ × ℤ) : ℝ

The sup norm of an integer vector, as a real number.

Equations

• MeasureTheory.supNormZ v = max |↑v.1| |↑v.2|

theorem MeasureTheory.supNormZ_nonneg (v : ℤ × ℤ) : 0 ≤ supNormZ v

theorem MeasureTheory.abs_fst_le_supNormZ (v : ℤ × ℤ) : |↑v.1| ≤ supNormZ v

theorem MeasureTheory.abs_snd_le_supNormZ (v : ℤ × ℤ) : |↑v.2| ≤ supNormZ v

theorem MeasureTheory.supNormZ_le_iff (v : ℤ × ℤ) (R : ℕ) : supNormZ v ≤ ↑R ↔ v.1 ∈ Finset.Icc (-↑R) ↑R ∧ v.2 ∈ Finset.Icc (-↑R) ↑R

The sup norm is bounded by R exactly when both coordinates lie in [-R, R].

noncomputable def MeasureTheory.ellU (v : ℤ × ℤ) : ℝ

The linear form along the expanding eigendirection of catZ: scaled by φ².

Equations

• MeasureTheory.ellU v = ↑v.1 + (Real.goldenRatio - 1) * ↑v.2

noncomputable def MeasureTheory.ellS (v : ℤ × ℤ) : ℝ

The linear form along the contracting eigendirection of catZ: scaled by φ⁻².

Equations

• MeasureTheory.ellS v = ↑v.1 - Real.goldenRatio * ↑v.2

theorem MeasureTheory.ellU_catZ (v : ℤ × ℤ) : ellU (catZ v) = Real.goldenRatio ^ 2 * ellU v

theorem MeasureTheory.ellU_catZ_iterate (v : ℤ × ℤ) (n : ℕ) : ellU (catZ^[n] v) = Real.goldenRatio ^ (2 * n) * ellU v

theorem MeasureTheory.ellU_mul_ellS (v : ℤ × ℤ) : ellU v * ellS v = ↑(v.1 ^ 2 - v.1 * v.2 - v.2 ^ 2)

The product of the two forms is the integer quadratic form m² − mn − n².

theorem MeasureTheory.quadForm_ne_zero {v : ℤ × ℤ} (hv : v ≠ 0) : v.1 ^ 2 - v.1 * v.2 - v.2 ^ 2 ≠ 0

The quadratic form has no nonzero integer zero: a zero would make φ rational.

theorem MeasureTheory.one_le_abs_ellU_mul_ellS {v : ℤ × ℤ} (hv : v ≠ 0) : 1 ≤ |ellU v * ellS v|

On a nonzero integer vector the invariant form has absolute value at least 1.

theorem MeasureTheory.abs_ellS_le (v : ℤ × ℤ) : |ellS v| ≤ Real.goldenRatio ^ 2 * supNormZ v

theorem MeasureTheory.abs_ellU_le (v : ℤ × ℤ) : |ellU v| ≤ Real.goldenRatio * supNormZ v

theorem MeasureTheory.goldenRatio_pow_le_supNormZ_catZ_iterate {v : ℤ × ℤ} (hv : v ≠ 0) (n : ℕ) : Real.goldenRatio ^ (2 * n) ≤ Real.goldenRatio ^ 3 * (supNormZ (catZ^[n] v) * supNormZ v)

★ The frequency orbit grows geometrically. For a nonzero integer vector v, φ^{2n} ≤ φ³ · ‖catZ^[n] v‖ · ‖v‖: the orbit cannot stay small, because the invariant form is a nonzero integer and the expanding component is multiplied by φ² at every step.

The lag-dependent frequency cutoff

theorem MeasureTheory.three_halves_lt_goldenRatio : 3 / 2 < Real.goldenRatio

3/2 < φ, since 2 < √5.

theorem MeasureTheory.goldenRatio_pow_six : Real.goldenRatio ^ 6 = 8 * Real.goldenRatio + 5

φ⁶ = 8φ + 5, so in particular 16 < φ⁶.

theorem MeasureTheory.sixteen_le_goldenRatio_pow_six : 16 ≤ Real.goldenRatio ^ 6

def MeasureTheory.catCutoff (n : ℕ) : ℕ

The frequency cutoff at lag n: a perfect square 4^{⌊(n−2)/3⌋}, chosen so that its square stays below φ^{2n-3} (the orbit growth) for n ≥ 2, and so that its square root 2^{⌊(n−2)/3⌋} is a natural number.

Equations

• MeasureTheory.catCutoff n = 4 ^ ((n - 2) / 3)

theorem MeasureTheory.catCutoff_pos (n : ℕ) : 0 < catCutoff n

theorem MeasureTheory.catCutoff_eq_sq (n : ℕ) : catCutoff n = (2 ^ ((n - 2) / 3)) ^ 2

theorem MeasureTheory.catCutoff_sq_mul_lt {n : ℕ} (hn : 2 ≤ n) : ↑(catCutoff n) ^ 2 * Real.goldenRatio ^ 3 < Real.goldenRatio ^ (2 * n)

R(n)² · φ³ < φ^{2n} for n ≥ 2: the cutoff is small enough for the orbit growth to beat it.

theorem MeasureTheory.catCutoff_lt_supNormZ_catZ_iterate {n : ℕ} (hn : 2 ≤ n) {v : ℤ × ℤ} (hv : v ≠ 0) (hR : supNormZ v ≤ ↑(catCutoff n)) : ↑(catCutoff n) < supNormZ (catZ^[n] v)

★ Separation. For n ≥ 2, a nonzero frequency inside the cutoff box at lag n is carried strictly outside it by catZ^[n]. This is the one fact the main-term computation uses.

Stage 2: arcs of the circle and their Fourier coefficients

An arc is read through the representative in (0, 1]. Its Fourier coefficients are the usual (e^{-2πinb} − e^{-2πina}) / (−2πin), of modulus at most 1/(π|n|).

noncomputable def MeasureTheory.unitRep (x : AddCircle 1) : ℝ

The representative of a point of the unit circle in (0, 1].

Equations

• MeasureTheory.unitRep x = ↑((AddCircle.equivIoc 1 0) x)

theorem MeasureTheory.measurable_unitRep : Measurable unitRep

theorem MeasureTheory.unitRep_mem_Ioc (x : AddCircle 1) : unitRep x ∈ Set.Ioc 0 1

theorem MeasureTheory.haarAddCircle_one_eq_volume : AddCircle.haarAddCircle = volume

haarAddCircle on the unit circle is volume.

noncomputable def MeasureTheory.arcInd (a b : ℝ) : AddCircle 1 → ℂ

The indicator of the arc {x | unitRep x ∈ (a, b)}, as a complex observable.

Equations

• MeasureTheory.arcInd a b x = (Set.Ioo a b).indicator (fun (x : ℝ) => 1) (MeasureTheory.unitRep x)

theorem MeasureTheory.arcInd_eq_liftIoc (a b : ℝ) : arcInd a b = AddCircle.liftIoc 1 0 ((Set.Ioo a b).indicator fun (x : ℝ) => 1)

theorem MeasureTheory.measurable_arcInd (a b : ℝ) : Measurable (arcInd a b)

theorem MeasureTheory.arcInd_apply (a b : ℝ) (x : AddCircle 1) : arcInd a b x = if unitRep x ∈ Set.Ioo a b then 1 else 0

theorem MeasureTheory.norm_arcInd_le (a b : ℝ) (x : AddCircle 1) : ‖arcInd a b x‖ ≤ 1

theorem MeasureTheory.fourierCoeff_zero_eq_integral (u : AddCircle 1 → ℂ) : fourierCoeff u 0 = ∫ (x : AddCircle 1), u x

The zeroth coefficient of any integrable observable is its mean.

theorem MeasureTheory.fourierCoeff_arcInd {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (n : ℤ) : fourierCoeff (arcInd a b) n = ∫ (x : ℝ) in a..b, Complex.exp (-(2 * ↑Real.pi * Complex.I * ↑n) * ↑x)

★ The Fourier coefficients of an arc, as an interval integral.

theorem MeasureTheory.fourierCoeff_arcInd_zero {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) : fourierCoeff (arcInd a b) 0 = ↑(b - a)

The mean of an arc is its length.

theorem MeasureTheory.norm_fourierCoeff_arcInd_le {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeff (arcInd a b) n‖ ≤ 1 / (Real.pi * |↑n|)

★ The coefficient bound ‖â(n)‖ ≤ 1 / (π |n|) for n ≠ 0.

Stage 3: truncation, Parseval, and the tail of an arc's Fourier series

trunc R u keeps the frequencies |n| ≤ R. Parseval (Mathlib's tsum_sq_fourierCoeff) turns the L² error of the truncation into the tail ∑_{|n|>R} ‖û(n)‖², which for an arc is at most 1/R by the coefficient bound of Stage 2 and ∑_{|n|>R} n⁻² ≤ 4/R.

@[reducible, inline]

abbrev MeasureTheory.freqBox (R : ℕ) : Finset ℤ

The frequency box [-R, R].

Equations

• MeasureTheory.freqBox R = Finset.Icc (-↑R) ↑R

theorem MeasureTheory.zero_mem_freqBox (R : ℕ) : 0 ∈ freqBox R

noncomputable def MeasureTheory.trunc (R : ℕ) (u : AddCircle 1 → ℂ) : AddCircle 1 → ℂ

The truncation of u to the frequencies |n| ≤ R.

Equations

• MeasureTheory.trunc R u x = ∑ n ∈ MeasureTheory.freqBox R, fourierCoeff u n * (fourier n) x

theorem MeasureTheory.norm_fourier_eq_one (n : ℤ) (x : AddCircle 1) : ‖(fourier n) x‖ = 1

theorem MeasureTheory.integrable_of_bounded {u : AddCircle 1 → ℂ} (hu : Measurable u) {C : ℝ} (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ C) : Integrable u AddCircle.haarAddCircle

theorem MeasureTheory.memLp_two_of_bounded {u : AddCircle 1 → ℂ} (hu : Measurable u) {C : ℝ} (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ C) : MemLp u 2 AddCircle.haarAddCircle

theorem MeasureTheory.integrable_const_mul_fourier (c : ℂ) (n : ℤ) : Integrable (fun (x : AddCircle 1) => c * (fourier n) x) AddCircle.haarAddCircle

theorem MeasureTheory.norm_fourierCoeff_le_one {u : AddCircle 1 → ℂ} (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) (n : ℤ) : ‖fourierCoeff u n‖ ≤ 1

A coefficient of an observable bounded by 1 is bounded by 1.

theorem MeasureTheory.continuous_trunc (R : ℕ) (u : AddCircle 1 → ℂ) : Continuous (trunc R u)

theorem MeasureTheory.norm_trunc_le (R : ℕ) {u : AddCircle 1 → ℂ} (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) (x : AddCircle 1) : ‖trunc R u x‖ ≤ ↑(freqBox R).card

theorem MeasureTheory.memLp_two_trunc (R : ℕ) {u : AddCircle 1 → ℂ} (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) : MemLp (trunc R u) 2 AddCircle.haarAddCircle

theorem MeasureTheory.fourierCoeff_trunc (R : ℕ) {u : AddCircle 1 → ℂ} (m : ℤ) : fourierCoeff (trunc R u) m = if m ∈ freqBox R then fourierCoeff u m else 0

The coefficients of the truncation: those of u inside the box, 0 outside.

theorem MeasureTheory.fourierCoeff_sub_trunc (R : ℕ) {u : AddCircle 1 → ℂ} (hu : Measurable u) (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) (m : ℤ) : fourierCoeff (u - trunc R u) m = if m ∈ freqBox R then 0 else fourierCoeff u m

theorem MeasureTheory.integral_normSq_eq_tsum_of_memLp {g : AddCircle 1 → ℂ} (hg : MemLp g 2 AddCircle.haarAddCircle) : ∫ (x : AddCircle 1), ‖g x‖ ^ 2 ∂AddCircle.haarAddCircle = ∑' (n : ℤ), ‖fourierCoeff g n‖ ^ 2

Parseval, for a bounded measurable observable: ∫ ‖g‖² = ∑ ‖ĝ(n)‖².

theorem MeasureTheory.summable_sq_fourierCoeff_of_memLp {g : AddCircle 1 → ℂ} (hg : MemLp g 2 AddCircle.haarAddCircle) : Summable fun (n : ℤ) => ‖fourierCoeff g n‖ ^ 2

theorem MeasureTheory.integral_normSq_sub_trunc (R : ℕ) {u : AddCircle 1 → ℂ} (hu : Measurable u) (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) : ∫ (x : AddCircle 1), ‖u x - trunc R u x‖ ^ 2 ∂AddCircle.haarAddCircle = ∑' (n : ℤ), ‖if n ∈ freqBox R then 0 else fourierCoeff u n‖ ^ 2

The L² error of the truncation is the tail of the series.

theorem MeasureTheory.integral_normSq_trunc_le (R : ℕ) {u : AddCircle 1 → ℂ} (hu : Measurable u) (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) : ∫ (x : AddCircle 1), ‖trunc R u x‖ ^ 2 ∂AddCircle.haarAddCircle ≤ ∫ (x : AddCircle 1), ‖u x‖ ^ 2 ∂AddCircle.haarAddCircle

Bessel: the truncation has no more energy than the observable.

The tail of ∑ n⁻² over |n| > R

theorem MeasureTheory.sum_tail_inv_sq_le (R : ℕ) (hR : 1 ≤ R) (s : Finset ℤ) : (∑ n ∈ s, if n ∈ freqBox R then 0 else 1 / ↑n ^ 2) ≤ 4 / ↑R

The finite tail bound: a finite set of integers outside the box contributes at most 4/R.

theorem MeasureTheory.summable_tail_inv_sq (R : ℕ) : Summable fun (n : ℤ) => if n ∈ freqBox R then 0 else 1 / ↑n ^ 2

theorem MeasureTheory.tsum_tail_inv_sq_le (R : ℕ) (hR : 1 ≤ R) : (∑' (n : ℤ), if n ∈ freqBox R then 0 else 1 / ↑n ^ 2) ≤ 4 / ↑R

★ ∑_{|n|>R} n⁻² ≤ 4/R.

theorem MeasureTheory.integral_normSq_arcInd_sub_trunc_le {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (R : ℕ) (hR : 1 ≤ R) : ∫ (x : AddCircle 1), ‖arcInd a b x - trunc R (arcInd a b) x‖ ^ 2 ∂AddCircle.haarAddCircle ≤ 1 / ↑R

★★ The L² error of truncating an arc is at most 1/R.

Stage 4: rectangles on the torus, and the main term

A rectangle observable is a product u(x) v(y) of two circle observables. Its truncation at the cutoff R is the product of the two truncations, a trigonometric polynomial supported on the frequency box; under cat^[n] that box is carried off itself (Stage 1), so the integral of the truncated product against another truncated rectangle collapses to the product of the means. The truncation errors are controlled by Stage 3 through Cauchy–Schwarz.

structure MeasureTheory.BddC (u : AddCircle 1 → ℂ) : Prop

Bounded measurable observables on the circle, the class everything below lives in.

• measurable : Measurable u
• bound : ∃ (C : ℝ), ∀ (x : AddCircle 1), ‖u x‖ ≤ C

structure MeasureTheory.BddT (F : Torus2 → ℂ) : Prop

Bounded measurable observables on the torus.

• measurable : Measurable F
• bound : ∃ (C : ℝ), ∀ (p : Torus2), ‖F p‖ ≤ C

theorem MeasureTheory.BddC.arcInd (a b : ℝ) : BddC (MeasureTheory.arcInd a b)

theorem MeasureTheory.BddC.trunc (R : ℕ) {u : AddCircle 1 → ℂ} (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) : BddC (MeasureTheory.trunc R u)

theorem MeasureTheory.BddC.sub {u v : AddCircle 1 → ℂ} (hu : BddC u) (hv : BddC v) : BddC (u - v)

theorem MeasureTheory.BddC.integrable {u : AddCircle 1 → ℂ} (hu : BddC u) : Integrable u volume

theorem MeasureTheory.BddC.integrable_normSq {u : AddCircle 1 → ℂ} (hu : BddC u) : Integrable (fun (x : AddCircle 1) => ‖u x‖ ^ 2) volume

theorem MeasureTheory.BddC.integral_normSq_le_one {u : AddCircle 1 → ℂ} (hu : Measurable u) (hub : ∀ (x : AddCircle 1), ‖u x‖ ≤ 1) : ∫ (x : AddCircle 1), ‖u x‖ ^ 2 ≤ 1

The energy of an observable bounded by 1 is at most 1.

def MeasureTheory.rect (u v : AddCircle 1 → ℂ) : Torus2 → ℂ

A rectangle observable: the product of two circle observables.

Equations

• MeasureTheory.rect u v p = u p.1 * v p.2

theorem MeasureTheory.BddT.rect {u v : AddCircle 1 → ℂ} (hu : BddC u) (hv : BddC v) : BddT (MeasureTheory.rect u v)

theorem MeasureTheory.BddT.sub {F G : Torus2 → ℂ} (hF : BddT F) (hG : BddT G) : BddT (F - G)

theorem MeasureTheory.BddT.mul {F G : Torus2 → ℂ} (hF : BddT F) (hG : BddT G) : BddT fun (p : Torus2) => F p * G p

theorem MeasureTheory.BddT.comp_cat_iterate {F : Torus2 → ℂ} (hF : BddT F) (n : ℕ) : BddT fun (p : Torus2) => F (cat^[n] p)

theorem MeasureTheory.BddT.integrable {F : Torus2 → ℂ} (hF : BddT F) : Integrable F volume

theorem MeasureTheory.BddT.integrable_normSq {F : Torus2 → ℂ} (hF : BddT F) : Integrable (fun (p : Torus2) => ‖F p‖ ^ 2) volume

theorem MeasureTheory.BddT.memLp_two {F : Torus2 → ℂ} (hF : BddT F) : MemLp F 2 volume

theorem MeasureTheory.integral_rect (u v : AddCircle 1 → ℂ) : ∫ (p : Torus2), rect u v p = (∫ (x : AddCircle 1), u x) * ∫ (y : AddCircle 1), v y

The mean of a rectangle is the product of the means (Fubini).

theorem MeasureTheory.integral_normSq_rect (u v : AddCircle 1 → ℂ) : ∫ (p : Torus2), ‖rect u v p‖ ^ 2 = (∫ (x : AddCircle 1), ‖u x‖ ^ 2) * ∫ (y : AddCircle 1), ‖v y‖ ^ 2

The energy of a rectangle is the product of the energies.

theorem MeasureTheory.integral_comp_cat_iterate (g : Torus2 → ℝ) (hg : Measurable g) (n : ℕ) : ∫ (p : Torus2), g (cat^[n] p) = ∫ (p : Torus2), g p

Composition with the cat map preserves integrals of real observables.

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

Cauchy–Schwarz on the torus, in squared form, for two L² observables.

The truncation error of a rectangle of arcs

theorem MeasureTheory.normSq_add_le (x y : ℂ) : ‖x + y‖ ^ 2 ≤ 2 * ‖x‖ ^ 2 + 2 * ‖y‖ ^ 2

‖x + y‖² ≤ 2‖x‖² + 2‖y‖².

theorem MeasureTheory.integral_normSq_rect_sub_trunc_le {a b c d : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (hc : 0 ≤ c) (hcd : c < d) (hd : d ≤ 1) (R : ℕ) (hR : 1 ≤ R) : ∫ (p : Torus2), ‖rect (arcInd a b) (arcInd c d) p - rect (trunc R (arcInd a b)) (trunc R (arcInd c d)) p‖ ^ 2 ≤ 4 / ↑R

★ The L² error of truncating a rectangle of arcs is at most 4/R.

The main term

theorem MeasureTheory.BddT.chi (a : ℤ × ℤ) : BddT (MeasureTheory.chi a)

theorem MeasureTheory.BddT.const_mul (c : ℂ) {F : Torus2 → ℂ} (hF : BddT F) : BddT fun (p : Torus2) => c * F p

theorem MeasureTheory.rect_trunc_eq_sum (R : ℕ) (u v : AddCircle 1 → ℂ) (p : Torus2) : rect (trunc R u) (trunc R v) p = ∑ k ∈ freqBox R ×ˢ freqBox R, fourierCoeff u k.1 * fourierCoeff v k.2 * chi k p

A truncated rectangle is a trigonometric polynomial on the product frequency box.

theorem MeasureTheory.rect_trunc_comp_cat_iterate (R : ℕ) (u v : AddCircle 1 → ℂ) (n : ℕ) (p : Torus2) : rect (trunc R u) (trunc R v) (cat^[n] p) = ∑ k ∈ freqBox R ×ˢ freqBox R, fourierCoeff u k.1 * fourierCoeff v k.2 * chi (catZ^[n] k) p

theorem MeasureTheory.catZ_zero : catZ 0 = 0

theorem MeasureTheory.catZ_iterate_zero (n : ℕ) : catZ^[n] 0 = 0

theorem MeasureTheory.supNormZ_neg (v : ℤ × ℤ) : supNormZ (-v) = supNormZ v

theorem MeasureTheory.zero_mem_freqBox_prod (R : ℕ) : 0 ∈ freqBox R ×ˢ freqBox R

theorem MeasureTheory.integral_chi_mul_chi (a b : ℤ × ℤ) : ∫ (p : Torus2), chi a p * chi b p = if a + b = 0 then 1 else 0

The integral of a product of two characters is 1 when the indices cancel and 0 otherwise.

theorem MeasureTheory.integral_rect_trunc_mul_rect_trunc {n : ℕ} (hn : 2 ≤ n) (u v u' v' : AddCircle 1 → ℂ) : ∫ (p : Torus2), rect (trunc (catCutoff n) u) (trunc (catCutoff n) v) (cat^[n] p) * rect (trunc (catCutoff n) u') (trunc (catCutoff n) v') p = fourierCoeff u 0 * fourierCoeff v 0 * (fourierCoeff u' 0 * fourierCoeff v' 0)

★ The main term. For n ≥ 2 the truncated rectangles at the cutoff catCutoff n have, after n steps of the cat map, no frequency in common except 0, so the integral of their product is the product of their means.

Stage 5: the correlation bound, and HasCorrelationDecay for rectangles

Write f = T + D with T the truncation at the lag-dependent cutoff and D the error. Then ∫ f∘catⁿ · f' = ∫ T∘catⁿ · T' + ∫ T∘catⁿ · D' + ∫ D∘catⁿ · f': the first term is the product of the means (Stage 4), and the other two are at most 2 / 2^{⌊(n−2)/3⌋} each by Cauchy–Schwarz and the truncation error 4 / R.

theorem MeasureTheory.mul_le_one_of_le_one {a b : ℝ} (ha : a ≤ 1) (hb0 : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1

a ≤ 1, 0 ≤ b ≤ 1 give a * b ≤ 1 (the deprecated mul_le_one_of_le_one, spelled out).

noncomputable def MeasureTheory.catRectEnv (n : ℕ) : ℝ

The decay envelope for rectangles of arcs: 1 at lags 0 and 1 (the trivial bound), and 4 / 2^{⌊(n−2)/3⌋} afterwards.

Equations

• MeasureTheory.catRectEnv n = if n < 2 then 1 else 4 / 2 ^ ((n - 2) / 3)

theorem MeasureTheory.norm_integral_rect_iterate_mul_sub_le {a b c d a' b' c' d' : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (hc : 0 ≤ c) (hcd : c < d) (hd : d ≤ 1) (ha' : 0 ≤ a') (hab' : a' < b') (hb' : b' ≤ 1) (hc' : 0 ≤ c') (hcd' : c' < d') (hd' : d' ≤ 1) {n : ℕ} (hn : 2 ≤ n) : ‖(∫ (p : Torus2), rect (arcInd a b) (arcInd c d) (cat^[n] p) * rect (arcInd a' b') (arcInd c' d') p) - (∫ (p : Torus2), rect (arcInd a b) (arcInd c d) p) * ∫ (p : Torus2), rect (arcInd a' b') (arcInd c' d') p‖ ≤ 4 / 2 ^ ((n - 2) / 3)

★★ Exponential decay of correlations for rectangles of arcs under the cat map, complex form, at lags n ≥ 2.

The real form

noncomputable def MeasureTheory.arcIndR (a b : ℝ) : AddCircle 1 → ℝ

The real indicator of the arc (a, b).

Equations

• MeasureTheory.arcIndR a b x = (Set.Ioo a b).indicator (fun (x : ℝ) => 1) (MeasureTheory.unitRep x)

theorem MeasureTheory.arcInd_eq_ofReal (a b : ℝ) (x : AddCircle 1) : arcInd a b x = ↑(arcIndR a b x)

theorem MeasureTheory.measurable_arcIndR (a b : ℝ) : Measurable (arcIndR a b)

theorem MeasureTheory.arcIndR_nonneg (a b : ℝ) (x : AddCircle 1) : 0 ≤ arcIndR a b x

theorem MeasureTheory.arcIndR_le_one (a b : ℝ) (x : AddCircle 1) : arcIndR a b x ≤ 1

noncomputable def MeasureTheory.rectIndR (a b c d : ℝ) : Torus2 → ℝ

The real indicator of the rectangle (a, b) × (c, d) of the torus.

Equations

• MeasureTheory.rectIndR a b c d p = MeasureTheory.arcIndR a b p.1 * MeasureTheory.arcIndR c d p.2

theorem MeasureTheory.rect_arcInd_eq_ofReal (a b c d : ℝ) (p : Torus2) : rect (arcInd a b) (arcInd c d) p = ↑(rectIndR a b c d p)

theorem MeasureTheory.measurable_rectIndR (a b c d : ℝ) : Measurable (rectIndR a b c d)

theorem MeasureTheory.rectIndR_nonneg (a b c d : ℝ) (p : Torus2) : 0 ≤ rectIndR a b c d p

theorem MeasureTheory.rectIndR_le_one (a b c d : ℝ) (p : Torus2) : rectIndR a b c d p ≤ 1

theorem MeasureTheory.abs_integral_rectIndR_iterate_mul_sub_le {a b c d a' b' c' d' : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (hc : 0 ≤ c) (hcd : c < d) (hd : d ≤ 1) (ha' : 0 ≤ a') (hab' : a' < b') (hb' : b' ≤ 1) (hc' : 0 ≤ c') (hcd' : c' < d') (hd' : d' ≤ 1) {n : ℕ} (hn : 2 ≤ n) : |(∫ (p : Torus2), rectIndR a b c d (cat^[n] p) * rectIndR a' b' c' d' p) - (∫ (p : Torus2), rectIndR a b c d p) * ∫ (p : Torus2), rectIndR a' b' c' d' p| ≤ 4 / 2 ^ ((n - 2) / 3)

★★ The real form at lags n ≥ 2.

theorem MeasureTheory.abs_integral_rectIndR_iterate_mul_sub_le_one (a b c d a' b' c' d' : ℝ) (n : ℕ) : |(∫ (p : Torus2), rectIndR a b c d (cat^[n] p) * rectIndR a' b' c' d' p) - (∫ (p : Torus2), rectIndR a b c d p) * ∫ (p : Torus2), rectIndR a' b' c' d' p| ≤ 1

Both integrals of a [0,1]-valued rectangle pair lie in [0, 1], so the trivial bound is 1.

theorem MeasureTheory.abs_integral_rectIndR_iterate_mul_sub_le_env {a b c d a' b' c' d' : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (hc : 0 ≤ c) (hcd : c < d) (hd : d ≤ 1) (ha' : 0 ≤ a') (hab' : a' < b') (hb' : b' ≤ 1) (hc' : 0 ≤ c') (hcd' : c' < d') (hd' : d' ≤ 1) (n : ℕ) : |(∫ (p : Torus2), rectIndR a b c d (cat^[n] p) * rectIndR a' b' c' d' p) - (∫ (p : Torus2), rectIndR a b c d p) * ∫ (p : Torus2), rectIndR a' b' c' d' p| ≤ catRectEnv n

★★ The pair correlation of two rectangles of arcs decays with the envelope catRectEnv.

The envelope is summable

theorem MeasureTheory.five_fourth_pow_le_two_mul_two_pow (m : ℕ) : (5 / 4) ^ m ≤ 2 * 2 ^ (m / 3)

(5/4)^m ≤ 2 · 2^{⌊m/3⌋}, because (5/4)³ < 2 and (5/4)² < 2.

theorem MeasureTheory.catRectEnv_nonneg (n : ℕ) : 0 ≤ catRectEnv n

theorem MeasureTheory.catRectEnv_le_geometric (n : ℕ) : catRectEnv n ≤ 13 * (4 / 5) ^ n

The envelope is dominated by the geometric sequence 13 · (4/5)^n.

theorem MeasureTheory.summable_catRectEnv : Summable catRectEnv

★ The envelope is summable.

theorem MeasureTheory.cat_hasCorrelationDecay_rectIndR {a b c d : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (hc : 0 ≤ c) (hcd : c < d) (hd : d ≤ 1) : HasCorrelationDecay volume cat (rectIndR a b c d) catRectEnv

★★★ A rectangle of arcs has exponentially decaying correlations under the cat map, in the corpus's HasCorrelationDecay form.