Fourier analysis on the 2-torus 𝕋² = (ℝ/ℤ)²

This module packages the Fourier-analytic infrastructure on the 2-torus that the toral-automorphism ergodicity argument (issue #3) consumes: the ℤ²-indexed family of additive characters

e_{(m,n)} : (a, b) ↦ exp(2πi(m·a + n·b))

is a Hilbert basis (orthonormal and complete) of L²(𝕋², Haar), together with Parseval. The single interface the ergodicity proof needs is eq_zero_of_forall_char_inner_eq_zero: an L² function that is orthogonal to every character is 0.

Provenance: this is a thin specialization, not a re-proof

Mathlib already builds the full d-dimensional torus Fourier theory in Mathlib.Analysis.Fourier.AddCircleMulti for UnitAddTorus d = (d → ℝ/ℤ):

• UnitAddTorus.mFourier n — the monomial x ↦ ∏ i, exp(2πi·nᵢ·xᵢ) (a ContinuousMap);
• UnitAddTorus.orthonormal_mFourier — orthonormality in L²;
• UnitAddTorus.span_mFourierLp_closure_eq_top — completeness (the Lᵖ span is dense), itself obtained by Stone–Weierstrass directly on the product torus (mFourierSubalgebra_closure_eq_top), so completeness needs no separate product-Hilbert- basis / tensor construction;
• UnitAddTorus.mFourierBasis — the resulting HilbertBasis (d → ℤ) ℂ L²;
• UnitAddTorus.hasSum_sq_mFourierCoeff — Parseval.

Taking d := Fin 2 is exactly the 2-torus. We re-export those results under 2-torus-flavoured names, verify the explicit closed form e_{(m,n)}(a,b) = exp(2πi(m·a + n·b)), and add the orthogonality interface, all sorry-free and reducing to the Mathlib statements.

A measure-normalisation subtlety (load-bearing)

AddCircleMulti states all of its L² results relative to a file-local measure instance MeasureSpace UnitAddCircle := ⟨AddCircle.haarAddCircle⟩ (the Haar probability measure, total mass 1). That local instance does not leak to importers, where the ambient MeasureSpace (AddCircle 1) instead resolves to AddCircle.measureSpace 1 (volume = ENNReal.ofReal 1 • addHaarMeasure ⊤). The two measures are propositionally equal but not definitionally equal, so without intervention every reference to mFourierBasis, mFourierLp, … fails to typecheck in an importing file (Lp ℂ 2 volume is a different type). No Mathlib file imports AddCircleMulti, so this was never exercised upstream.

We resolve it the same way AddCircleMulti does: re-declare the same local instance MeasureSpace UnitAddCircle := ⟨haarAddCircle⟩ here, so our volume agrees with Mathlib's. The resulting volume on 𝕋² = UnitAddTorus (Fin 2) is then the product of the normalised Haar probability measures on the two circle factors, i.e. the normalised Haar probability measure on 𝕋² — exactly the measure the ergodicity statement is about. Downstream consumers (the toral-automorphism slice) must adopt the same instance; for an ergodicity statement, which is about an invariant probability measure, this is the intended normalisation.

Main definitions

• Torus2 — abbreviation for UnitAddTorus (Fin 2) = Fin 2 → ℝ/ℤ.
• torusChar m n — the character e_{(m,n)}, a ContinuousMap.
• torusCharLp m n — torusChar m n as an element of L²(𝕋²).
• torusFourierBasis — the (Fin 2 → ℤ)-indexed Hilbert basis of L²(𝕋²) (defeq UnitAddTorus.mFourierBasis).
• torusFourierCoeff f m n — the (m,n)-th Fourier coefficient.

Main statements

• torusChar_apply — the explicit formula e_{(m,n)}(a,b) = exp(2πi(m·a + n·b)).
• orthonormal_torusChar — the characters are orthonormal in L².
• torusFourierBasis_repr — the basis coordinates are the Fourier coefficients.
• hasSum_sq_torusFourierCoeff — Parseval's identity.
• eq_zero_of_forall_torusFourierCoeff_eq_zero — completeness in bare form: an L² function with all Fourier coefficients zero is 0.
• eq_zero_of_forall_char_inner_eq_zero — the ergodicity interface: an L² function orthogonal to every character is 0.

@[implicit_reducible]

noncomputable def Oseledets.Fourier.instMeasureSpaceUnitAddCircle' : MeasureTheory.MeasureSpace UnitAddCircle

Normalise the measure on each circle factor ℝ/ℤ to be the Haar probability measure (total mass 1). This re-declares the file-local instance of Mathlib.Analysis.Fourier.AddCircleMulti, so that volume in this file agrees with the measure mFourierBasis/mFourierLp are stated for. Without it, the ambient AddCircle.measureSpace 1 (a propositionally-but-not-definitionally equal mass-1 Haar measure) makes those Mathlib results fail to typecheck.

Equations

• Oseledets.Fourier.instMeasureSpaceUnitAddCircle' = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

@[reducible, inline]

abbrev Oseledets.Fourier.Torus2 : Type

The 2-torus 𝕋² = (ℝ/ℤ)², modelled as UnitAddTorus (Fin 2) = Fin 2 → ℝ/ℤ. With the local Haar-probability instance above, its volume is the product of the normalised Haar probability measures on the two circle factors, i.e. the normalised Haar probability measure on 𝕋².

Equations

• Oseledets.Fourier.Torus2 = UnitAddTorus (Fin 2)

The characters and their algebra

noncomputable def Oseledets.Fourier.torusChar (m n : ℤ) : C(Torus2, ℂ)

The (m, n)-th additive character e_{(m,n)} : (a,b) ↦ exp(2πi(m·a + n·b)) of the 2-torus, bundled as a continuous map. Definitionally it is UnitAddTorus.mFourier ![m, n].

Equations

• Oseledets.Fourier.torusChar m n = UnitAddTorus.mFourier ![m, n]

theorem Oseledets.Fourier.torusChar_eq_mFourier (m n : ℤ) : torusChar m n = UnitAddTorus.mFourier ![m, n]

theorem Oseledets.Fourier.torusChar_apply_coe (m n : ℤ) (a b : ℝ) : (torusChar m n) ![↑a, ↑b] = Complex.exp (2 * ↑Real.pi * Complex.I * ↑m * ↑a) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑b)

The 2-torus character at a point given by two real coordinate representatives: e_{(m,n)}((a, b)) = exp(2πi·m·a) · exp(2πi·n·b).

theorem Oseledets.Fourier.torusChar_apply (m n : ℤ) (a b : ℝ) : (torusChar m n) ![↑a, ↑b] = Complex.exp (2 * ↑Real.pi * Complex.I * (↑m * ↑a + ↑n * ↑b))

The explicit closed form of the 2-torus character as a single exponential: e_{(m,n)}((a, b)) = exp(2πi(m·a + n·b)).

theorem Oseledets.Fourier.torusChar_conj (m n : ℤ) (x : Torus2) : (starRingEnd ℂ) ((torusChar m n) x) = (torusChar (-m) (-n)) x

The conjugate of a 2-torus character is the character with negated indices.

theorem Oseledets.Fourier.torusChar_mul (m n p q : ℤ) (x : Torus2) : (torusChar m n) x * (torusChar p q) x = (torusChar (m + p) (n + q)) x

Characters multiply by adding indices: e_{(m,n)} · e_{(p,q)} = e_{(m+p, n+q)}.

theorem Oseledets.Fourier.torusChar_zero (x : Torus2) : (torusChar 0 0) x = 1

The trivial character e_{(0,0)} is the constant function 1.

theorem Oseledets.Fourier.norm_torusChar (m n : ℤ) : ‖torusChar m n‖ = 1

Each character has sup-norm 1 (it is unimodular).

The L² characters, orthonormality, and the Hilbert basis

noncomputable def Oseledets.Fourier.torusCharLp (m n : ℤ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The character e_{(m,n)} as an element of L²(𝕋²). Definitionally mFourierLp 2 ![m, n].

Equations

• Oseledets.Fourier.torusCharLp m n = UnitAddTorus.mFourierLp 2 ![m, n]

theorem Oseledets.Fourier.torusCharLp_eq (m n : ℤ) : torusCharLp m n = UnitAddTorus.mFourierLp 2 ![m, n]

theorem Oseledets.Fourier.coeFn_torusCharLp (m n : ℤ) : ↑↑(torusCharLp m n) =ᵐ[MeasureTheory.volume] ⇑(UnitAddTorus.mFourier ![m, n])

theorem Oseledets.Fourier.orthonormal_torusChar : Orthonormal ℂ fun (p : ℤ × ℤ) => torusCharLp p.1 p.2

Orthonormality. The 2-torus characters form an orthonormal family in L²(𝕋²).

noncomputable def Oseledets.Fourier.torusFourierBasis : HilbertBasis (Fin 2 → ℤ) ℂ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The Hilbert basis. The (Fin 2 → ℤ)-indexed family of characters is a Hilbert basis of L²(𝕋²): it is orthonormal and its span is dense (completeness). This is exactly UnitAddTorus.mFourierBasis for d = Fin 2; the (m, n) face is recovered through ![m, n].

Equations

• Oseledets.Fourier.torusFourierBasis = UnitAddTorus.mFourierBasis

theorem Oseledets.Fourier.torusFourierBasis_eq : torusFourierBasis = UnitAddTorus.mFourierBasis

theorem Oseledets.Fourier.torusFourierBasis_apply (m n : ℤ) : torusFourierBasis ![m, n] = torusCharLp m n

The basis vector of torusFourierBasis at ![m, n] is the L² character torusCharLp m n.

Fourier coefficients, series convergence and Parseval

noncomputable def Oseledets.Fourier.torusFourierCoeff (f : Torus2 → ℂ) (m n : ℤ) : ℂ

The (m, n)-th Fourier coefficient of f : 𝕋² → ℂ: ∫ exp(-2πi(m·a + n·b)) · f(a,b) d(a,b). Definitionally mFourierCoeff f ![m, n].

Equations

• Oseledets.Fourier.torusFourierCoeff f m n = UnitAddTorus.mFourierCoeff f ![m, n]

theorem Oseledets.Fourier.torusFourierCoeff_eq (f : Torus2 → ℂ) (m n : ℤ) : torusFourierCoeff f m n = UnitAddTorus.mFourierCoeff f ![m, n]

theorem Oseledets.Fourier.torusFourierBasis_repr (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (m n : ℤ) : ↑(torusFourierBasis.repr f) ![m, n] = torusFourierCoeff (↑↑f) m n

The basis coordinate of f at ![m, n] is its (m, n)-th Fourier coefficient.

theorem Oseledets.Fourier.hasSum_torusFourier_series_L2 (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasSum (fun (n : Fin 2 → ℤ) => UnitAddTorus.mFourierCoeff (↑↑f) n • UnitAddTorus.mFourierLp 2 n) f

L² convergence of the Fourier series. Every L² function on 𝕋² is the L²-limit of its Fourier series ∑ c_n · e_n (indexed over n : Fin 2 → ℤ, i.e. (m, n) ∈ ℤ²).

theorem Oseledets.Fourier.hasSum_sq_torusFourierCoeff (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasSum (fun (p : ℤ × ℤ) => ‖torusFourierCoeff (↑↑f) p.1 p.2‖ ^ 2) (∫ (t : Torus2), ‖↑↑f t‖ ^ 2)

Parseval's identity (norms): the sum of squared moduli of the Fourier coefficients over (m, n) ∈ ℤ² equals the squared L² norm ∫ |f|².

The ergodicity interface: orthogonal to all characters ⟹ zero

theorem Oseledets.Fourier.eq_zero_of_forall_torusFourierCoeff_eq_zero (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (h : ∀ (m n : ℤ), torusFourierCoeff (↑↑f) m n = 0) : f = 0

If every Fourier coefficient of an L² function vanishes, the function is 0 in L². This is the completeness of the character system in its bare form: the only L² function whose all Fourier coefficients are zero is the zero function.

theorem Oseledets.Fourier.eq_zero_of_forall_char_inner_eq_zero (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (h : ∀ (m n : ℤ), inner ℂ (torusCharLp m n) f = 0) : f = 0

The ergodicity interface. An L² function on 𝕋² that is orthogonal to every character e_{(m,n)} is 0. (The inner is the L² inner product ⟪e_{(m,n)}, f⟫ = ∫ conj(e)·f.)

theorem Oseledets.Fourier.ext_of_forall_char_inner_eq (f g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (h : ∀ (m n : ℤ), inner ℂ (torusCharLp m n) f = inner ℂ (torusCharLp m n) g) : f = g

Restatement of the interface for ergodicity: two L² functions with equal Fourier coefficients against every character are equal.