Fourier theory on ZMod N

Basic definitions and properties of the discrete Fourier transform for functions on ZMod N (taking values in an arbitrary ℂ-vector space).

Main definitions and results

• ZMod.dft: the Fourier transform, with respect to the standard additive character ZMod.stdAddChar (mapping j mod N to exp (2 * π * I * j / N)). The notation 𝓕, scoped in namespace ZMod, is available for this.
• ZMod.dft_dft: the Fourier inversion formula.
• DirichletCharacter.fourierTransform_eq_inv_mul_gaussSum: the discrete Fourier transform of a primitive Dirichlet character χ is a Gauss sum times χ⁻¹.

noncomputable def ZMod.dft {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] : (ZMod N → E) ≃ₗ[ℂ] ZMod N → E

The discrete Fourier transform on ℤ / N ℤ (with the counting measure), bundled as a linear equivalence. Denoted as 𝓕 within the ZMod namespace.

Equations

• ZMod.dft = { toFun := ZMod.auxDFT✝, map_add' := ⋯, map_smul' := ⋯, invFun := fun (Φ : ZMod N → E) (k : ZMod N) => (↑N)⁻¹ • ZMod.auxDFT✝ Φ (-k), left_inv := ⋯, right_inv := ⋯ }

def ZMod.term𝓕 : Lean.ParserDescr

The discrete Fourier transform on ℤ / N ℤ (with the counting measure), bundled as a linear equivalence. Denoted as 𝓕 within the ZMod namespace.

Equations

• ZMod.term𝓕 = Lean.ParserDescr.node `ZMod.term𝓕 1024 (Lean.ParserDescr.symbol "𝓕")

def ZMod.«term𝓕⁻» : Lean.ParserDescr

The inverse Fourier transform on ZMod N.

Equations

• ZMod.«term𝓕⁻» = Lean.ParserDescr.node `ZMod.«term𝓕⁻» 1024 (Lean.ParserDescr.symbol "𝓕⁻")

theorem ZMod.dft_apply {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Φ : ZMod N → E) (k : ZMod N) : dft Φ k = ∑ j : ZMod N, stdAddChar (-(j * k)) • Φ j

theorem ZMod.dft_def {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Φ : ZMod N → E) : dft Φ = fun (k : ZMod N) => ∑ j : ZMod N, stdAddChar (-(j * k)) • Φ j

theorem ZMod.invDFT_apply {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Ψ : ZMod N → E) (k : ZMod N) : dft.symm Ψ k = (↑N)⁻¹ • ∑ j : ZMod N, stdAddChar (j * k) • Ψ j

theorem ZMod.invDFT_def {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Ψ : ZMod N → E) : dft.symm Ψ = fun (k : ZMod N) => (↑N)⁻¹ • ∑ j : ZMod N, stdAddChar (j * k) • Ψ j

theorem ZMod.invDFT_apply' {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Ψ : ZMod N → E) (k : ZMod N) : dft.symm Ψ k = (↑N)⁻¹ • dft Ψ (-k)

theorem ZMod.invDFT_def' {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Ψ : ZMod N → E) : dft.symm Ψ = fun (k : ZMod N) => (↑N)⁻¹ • dft Ψ (-k)

theorem ZMod.dft_apply_zero {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Φ : ZMod N → E) : dft Φ 0 = ∑ j : ZMod N, Φ j

theorem ZMod.dft_eq_fourier {N : ℕ} [NeZero N] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (Φ : ZMod N → E) (k : ZMod N) : dft Φ k = Fourier.fourierIntegral toCircle MeasureTheory.Measure.count Φ k

The discrete Fourier transform agrees with the general one (assuming the target space is a complete normed space).

Compatibility with scalar multiplication

These lemmas are more general than LinearEquiv.map_mul etc, since they allow any scalars that commute with the ℂ-action, rather than just ℂ itself.

theorem ZMod.dft_const_smul {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] {R : Type u_2} [DistribSMul R E] [SMulCommClass R ℂ E] (r : R) (Φ : ZMod N → E) : dft (r • Φ) = r • dft Φ

theorem ZMod.dft_smul_const {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] {R : Type u_2} [Ring R] [Module ℂ R] [Module R E] [IsScalarTower ℂ R E] (Φ : ZMod N → R) (e : E) : (dft fun (j : ZMod N) => Φ j • e) = fun (k : ZMod N) => dft Φ k • e

theorem ZMod.dft_const_mul {N : ℕ} [NeZero N] {R : Type u_2} [Ring R] [Algebra ℂ R] (r : R) (Φ : ZMod N → R) : (dft fun (j : ZMod N) => r * Φ j) = fun (k : ZMod N) => r * dft Φ k

theorem ZMod.dft_mul_const {N : ℕ} [NeZero N] {R : Type u_2} [Ring R] [Algebra ℂ R] (Φ : ZMod N → R) (r : R) : (dft fun (j : ZMod N) => Φ j * r) = fun (k : ZMod N) => dft Φ k * r

theorem ZMod.dft_comp_neg {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Φ : ZMod N → E) : (dft fun (j : ZMod N) => Φ (-j)) = fun (k : ZMod N) => dft Φ (-k)

theorem ZMod.dft_dft {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Φ : ZMod N → E) : dft (dft Φ) = fun (j : ZMod N) => ↑N • Φ (-j)

Fourier inversion formula, discrete case.

theorem ZMod.dft_comp_unitMul {N : ℕ} [NeZero N] {E : Type u_1} [AddCommGroup E] [Module ℂ E] (Φ : ZMod N → E) (u : (ZMod N)ˣ) (k : ZMod N) : dft (fun (j : ZMod N) => Φ (↑u * j)) k = dft Φ (↑u⁻¹ * k)

theorem ZMod.dft_even_iff {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} : Function.Even (dft Φ) ↔ Function.Even Φ

The discrete Fourier transform of Φ is even if and only if Φ itself is.

theorem ZMod.dft_odd_iff {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} : Function.Odd (dft Φ) ↔ Function.Odd Φ

The discrete Fourier transform of Φ is odd if and only if Φ itself is.

theorem DirichletCharacter.fourierTransform_eq_gaussSum_mulShift {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (k : ZMod N) : ZMod.dft (⇑χ) k = gaussSum χ (ZMod.stdAddChar.mulShift (-k))

theorem DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ.IsPrimitive) (k : ZMod N) : ZMod.dft (⇑χ) k = χ⁻¹ (-k) * gaussSum χ ZMod.stdAddChar

For a primitive Dirichlet character χ, the Fourier transform of χ is a constant multiple of χ⁻¹ (and the constant is essentially the Gauss sum).