The genuine Arnold cat map as a hyperbolic toral automorphism

This module formalizes the genuine Arnold cat map: the automorphism of the 2-torus 𝕋² = UnitAddTorus (Fin 2) = Fin 2 → UnitAddCircle induced by the unimodular hyperbolic matrix M = !![2,1;1,1] ∈ SL₂(ℤ), and proves it is measure-preserving and ergodic for the Haar (volume) measure. This replaces the constant-cocycle realization in Oseledets/Examples/Elementary.lean (where the cat-map matrix is merely a constant cocycle over the doubling map) with real toral dynamics.

Strategy

• Measure-preservation. catTorus is a continuous surjective additive automorphism of the compact group 𝕋². Since volume is a Haar probability measure (product of Haar on the unit circle), AddMonoidHom.measurePreserving applies (a continuous surjective hom of compact groups with equal total mass is measure-preserving).

• Ergodicity (Fourier / character argument). The Koopman operator sends the character mFourier n to mFourier (catℤ ·ᵥ n) (the matrix is symmetric, so the index action by Mᵀ is the action by M). For a measurable invariant set s, the indicator 1_s ∈ L² has Fourier coefficients constant along the orbit p ↦ catℤᵖ ·ᵥ n. For n ≠ 0 that orbit is infinite (Oseledets.CatMapToral.orbit_infinite, the hyperbolicity input), and ℓ²-summability forces the coefficient to 0. Hence only the n = 0 coefficient survives, so 1_s is a.e. constant and s is a.e. empty or full.

Main results

• Oseledets.CatMapToral.catTorus — the cat-map automorphism of 𝕋².
• Oseledets.CatMapToral.measurePreserving_catTorus — catTorus preserves volume.
• Oseledets.CatMapToral.ergodic_catTorus — catTorus is ergodic for volume.

@[implicit_reducible]

noncomputable def instMeasureSpaceUnitAddCircle_oseledets : MeasureTheory.MeasureSpace UnitAddCircle

Normalise the circle measure to total mass 1 (AddCircle.haarAddCircle), matching the convention of Mathlib.Analysis.Fourier.AddCircleMulti (where mFourierBasis and the Fourier coefficient API are stated). With this MeasureSpace instance, volume on UnitAddTorus (Fin 2) is the product Haar probability measure on 𝕋², which is exactly the basis the Fourier API uses.

Equations

• instMeasureSpaceUnitAddCircle_oseledets = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem instIsAddHaarMeasureUnitAddCircleVolume_oseledets : MeasureTheory.volume.IsAddHaarMeasure

theorem instIsProbabilityMeasureUnitAddCircleVolume_oseledets : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

@[reducible, inline]

abbrev Oseledets.CatMapToral.T2 : Type

The 2-torus 𝕋² = Fin 2 → UnitAddCircle.

Equations

• Oseledets.CatMapToral.T2 = UnitAddTorus (Fin 2)

def Oseledets.CatMapToral.catℤinv : Matrix (Fin 2) (Fin 2) ℤ

The inverse cat-map matrix M⁻¹ = !![1,-1;-1,2] (note det M = 1).

Equations

• Oseledets.CatMapToral.catℤinv = !![1, -1; -1, 2]

theorem Oseledets.CatMapToral.catℤ_mul_inv : catℤ * catℤinv = 1

M · M⁻¹ = 1.

theorem Oseledets.CatMapToral.catℤinv_mul : catℤinv * catℤ = 1

M⁻¹ · M = 1.

The cat-map automorphism of the torus

def Oseledets.CatMapToral.torusMap (A : Matrix (Fin 2) (Fin 2) ℤ) : T2 → T2

The general toral endomorphism induced by an integer matrix A, (torusMap A y) i = ∑ j, A i j • y j.

Equations

• Oseledets.CatMapToral.torusMap A y i = ∑ j : Fin 2, A i j • y j

def Oseledets.CatMapToral.catTorus : T2 → T2

The cat-map automorphism T_M : 𝕋² → 𝕋², induced by M = !![2,1;1,1].

Equations

• Oseledets.CatMapToral.catTorus = Oseledets.CatMapToral.torusMap Oseledets.CatMapToral.catℤ

theorem Oseledets.CatMapToral.torusMap_mul (A B : Matrix (Fin 2) (Fin 2) ℤ) : torusMap (A * B) = torusMap A ∘ torusMap B

torusMap of a matrix product is the composition of torusMaps. (The ℤ-action on UnitAddCircle makes each component additive, and matrix multiplication is the composition of the index actions.)

theorem Oseledets.CatMapToral.torusMap_one : torusMap 1 = id

torusMap 1 = id.

theorem Oseledets.CatMapToral.catTorus_leftInverse : Function.LeftInverse (torusMap catℤinv) catTorus

catTorus is a bijection, with two-sided inverse torusMap catℤinv.

theorem Oseledets.CatMapToral.catTorus_rightInverse : Function.RightInverse (torusMap catℤinv) catTorus

theorem Oseledets.CatMapToral.catTorus_bijective : Function.Bijective catTorus

catTorus is a bijection (it has the two-sided inverse torusMap catℤinv).

theorem Oseledets.CatMapToral.catTorus_surjective : Function.Surjective catTorus

catTorus is surjective.

def Oseledets.CatMapToral.catTorusHom : T2 →+ T2

catTorus packaged as an additive monoid homomorphism of 𝕋² (each component is a finite sum of ℤ-scalings, hence additive).

Equations

• Oseledets.CatMapToral.catTorusHom = { toFun := Oseledets.CatMapToral.catTorus, map_zero' := Oseledets.CatMapToral.catTorusHom._proof_1, map_add' := Oseledets.CatMapToral.catTorusHom._proof_2 }

@[simp]

theorem Oseledets.CatMapToral.catTorusHom_apply (y : T2) : catTorusHom y = catTorus y

theorem Oseledets.CatMapToral.continuous_torusMap (A : Matrix (Fin 2) (Fin 2) ℤ) : Continuous (torusMap A)

Every torusMap is continuous.

theorem Oseledets.CatMapToral.continuous_catTorus : Continuous catTorus

catTorus is continuous.

Measure preservation

theorem Oseledets.CatMapToral.measurePreserving_catTorus : MeasureTheory.MeasurePreserving catTorus MeasureTheory.volume MeasureTheory.volume

The cat-map automorphism preserves Haar (volume). catTorus is a continuous surjective additive automorphism of the compact group 𝕋², and volume is a Haar probability measure, so AddMonoidHom.measurePreserving applies (equal total mass 1).

noncomputable def Oseledets.CatMapToral.catTorusEquiv : T2 ≃ᵐ T2

catTorus as a measurable equivalence of 𝕋² (continuous bijection with continuous inverse on a compact Hausdorff space).

Equations

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

@[simp]

theorem Oseledets.CatMapToral.catTorusEquiv_apply (y : T2) : catTorusEquiv y = catTorus y

theorem Oseledets.CatMapToral.measurePreserving_catTorusEquiv : MeasureTheory.MeasurePreserving (⇑catTorusEquiv) MeasureTheory.volume MeasureTheory.volume

The measurable-equivalence packaging catTorusEquiv also preserves Haar (volume).

The Koopman / character relation

The Koopman operator sends a character to a character, with the index transformed by the (transpose of the) matrix. Since catℤ is symmetric, catℤᵀ = catℤ, so the index action is just n ↦ catℤ ·ᵥ n.

theorem Oseledets.CatMapToral.fourier_add_point {k : ℤ} {x y : UnitAddCircle} : (fourier k) (x + y) = (fourier k) x * (fourier k) y

The character property in the point argument: fourier k is multiplicative under addition.

theorem Oseledets.CatMapToral.fourier_zsmul_point {k a : ℤ} {x : UnitAddCircle} : (fourier k) (a • x) = (fourier (k * a)) x

One ℤ-scaling inside fourier: fourier k (a • x) = fourier (k * a) x.

theorem Oseledets.CatMapToral.fourier_sum_zsmul {k : ℤ} (a : Fin 2 → ℤ) (z : Fin 2 → UnitAddCircle) : (fourier k) (∑ j : Fin 2, a j • z j) = ∏ j : Fin 2, (fourier (k * a j)) (z j)

fourier of a finite sum of scalings is the product of the scaled-index characters: fourier k (∑ j, a j • z j) = ∏ j, fourier (k * a j) (z j).

theorem Oseledets.CatMapToral.fourier_sum_index (c : Fin 2 → ℤ) (x : UnitAddCircle) : (fourier (∑ i : Fin 2, c i)) x = ∏ i : Fin 2, (fourier (c i)) x

Additivity of fourier in the index over a finite sum: fourier (∑ i, c i) x = ∏ i, fourier (c i) x.

theorem Oseledets.CatMapToral.mFourier_catTorus (n : Fin 2 → ℤ) (y : T2) : (UnitAddTorus.mFourier n) (catTorus y) = (UnitAddTorus.mFourier (Matrix.vecMul n catℤ)) y

Koopman / character relation. Composing a character with the cat-map automorphism gives the character at the vecMul-transformed index: mFourier n (catTorus y) = mFourier (catℤ.vecMul n) y. Equivalently mFourier (catℤ.vecMul n) = mFourier n ∘ catTorus.

theorem Oseledets.CatMapToral.mFourier_vecMul_eq_comp (n : Fin 2 → ℤ) : ⇑(UnitAddTorus.mFourier (Matrix.vecMul n catℤ)) = ⇑(UnitAddTorus.mFourier n) ∘ catTorus

The Koopman relation as a functional identity: mFourier (catℤ.vecMul n) = (mFourier n) ∘ catTorus.

Fourier coefficient invariance and the orbit-vanishing argument

theorem Oseledets.CatMapToral.mFourierCoeff_vecMul_of_invariant {f : T2 → ℂ} (hf : f =ᵐ[MeasureTheory.volume] f ∘ catTorus) (n : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff f (Matrix.vecMul n catℤ) = UnitAddTorus.mFourierCoeff f n

Fourier coefficients of an invariant function are constant along the index orbit. If f =ᵐ f ∘ catTorus, then mFourierCoeff f (catℤ.vecMul n) = mFourierCoeff f n: composing the character mFourier (-n) with catTorus and changing variables (measure preservation) shows the two integrals agree.

theorem Oseledets.CatMapToral.eq_zero_of_constant_on_infinite_of_summable {ι : Type u_1} {c : ι → ℂ} {S : Set ι} {v : ℂ} (hS : S.Infinite) (hconst : ∀ i ∈ S, c i = v) (hsum : Summable fun (i : ι) => ‖c i‖ ^ 2) : v = 0

A complex sequence that is constant on an infinite set and square-summable vanishes on that set. (Square-summability forces ‖·‖² → 0 along the cofinite filter, but a nonzero constant on an infinite set never tends to 0.)

Identifying the index action with the mulVec orbit

theorem Oseledets.CatMapToral.vecMul_catℤ (n : Fin 2 → ℤ) : Matrix.vecMul n catℤ = catℤ.mulVec n

catℤ is symmetric, so the vecMul index action coincides with the mulVec action.

theorem Oseledets.CatMapToral.iterate_vecMul (p : ℕ) (n : Fin 2 → ℤ) : (fun (m : Fin 2 → ℤ) => Matrix.vecMul m catℤ)^[p] n = (catℤ ^ p).mulVec n

The p-fold iterate of the index action is the p-th matrix power applied by mulVec.

theorem Oseledets.CatMapToral.index_orbit_infinite {n : Fin 2 → ℤ} (hn : n ≠ 0) : (Set.range fun (p : ℕ) => (fun (m : Fin 2 → ℤ) => Matrix.vecMul m catℤ)^[p] n).Infinite

The index orbit {(vecMul · catℤ)ᵖ n} is the mulVec-orbit, hence infinite for n ≠ 0.

Ergodicity

theorem Oseledets.CatMapToral.mFourier_zero_apply (y : T2) : (UnitAddTorus.mFourier 0) y = 1

The constant character mFourier 0 is the constant function 1.

theorem Oseledets.CatMapToral.summable_sq_mFourierCoeff (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Summable fun (n : Fin 2 → ℤ) => ‖UnitAddTorus.mFourierCoeff (↑↑f) n‖ ^ 2

For an L² function f, the Fourier coefficients are square-summable.

theorem Oseledets.CatMapToral.mFourierCoeff_eq_zero_of_invariant {f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hf : ↑↑f =ᵐ[MeasureTheory.volume] ↑↑f ∘ catTorus) {n : Fin 2 → ℤ} (hn : n ≠ 0) : UnitAddTorus.mFourierCoeff (↑↑f) n = 0

Fourier coefficients of an invariant L² function vanish off the origin. If (f : T2 → ℂ) is =ᵐ f ∘ catTorus and f ∈ L², then mFourierCoeff f n = 0 for every nonzero index n. (Constant along the infinite index orbit + square-summable ⇒ zero.)

theorem Oseledets.CatMapToral.ae_eq_const_of_invariant {f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hf : ↑↑f =ᵐ[MeasureTheory.volume] ↑↑f ∘ catTorus) : ↑↑f =ᵐ[MeasureTheory.volume] fun (x : T2) => UnitAddTorus.mFourierCoeff (↑↑f) 0

An invariant L² function is a.e. constant. If f ∈ L² and (f : T2 → ℂ) =ᵐ f∘catTorus, then f is a.e. equal to its zeroth Fourier coefficient. (All higher coefficients vanish by mFourierCoeff_eq_zero_of_invariant, so the Fourier series collapses to the constant term.)

theorem Oseledets.CatMapToral.ergodic_catTorus : Ergodic catTorus MeasureTheory.volume

The Arnold cat map is ergodic. For a measurable catTorus-invariant set s, the indicator 1_s ∈ L² is catTorus-invariant, hence a.e. constant by ae_eq_const_of_invariant; an indicator that is a.e. constant forces s to be a.e. empty or a.e. the whole torus. Together with measurePreserving_catTorus this gives ergodicity.