Fourier theory on ZMod N

Basic definitions and properties of the discrete Fourier transform for functions on ZMod N.

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.
• 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] (Φ : ZMod N → ℂ) (k : ZMod N) : ℂ

The discrete Fourier transform on ℤ / N ℤ (with the counting measure)

Equations

• ZMod.dft Φ k = Fourier.fourierIntegral ZMod.toCircle MeasureTheory.Measure.count Φ k

def ZMod.term𝓕 : Lean.ParserDescr

The discrete Fourier transform on ℤ / N ℤ (with the counting measure)

Equations

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

theorem ZMod.dft_apply {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) (k : ZMod N) : ZMod.dft Φ k = ∑ j : ZMod N, ZMod.toCircle (-(j * k)) • Φ j

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

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

theorem DirichletCharacter.fourierTransform_eq_inv_mul_gaussSum {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (k : ZMod N) (hχ : χ.IsPrimitive) : 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).