Commit 2024-07-07 12:05 5943c090

View on Github →

feat(Analysis/Fourier): discrete Fourier transform on ZMod N (#13353) We write down basic definitions for the discrete Fourier transform, and compute the Fourier transforms of primitive Dirichlet characters (a minor reformulation of a result from an earlier PR).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Fourier/ZMod.lean

added theorem DirichletCharacter.fourierTransform_eq_gaussSum_mulShift

added theorem DirichletCharacter.fourierTransform_eq_inv_mul_gaussSum

added theorem ZMod.dft_apply

added theorem ZMod.dft_def

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

added theorem ZMod.stdAddChar_apply

added theorem ZMod.stdAddChar_coe

added theorem ZMod.toCircle_apply

added theorem ZMod.toCircle_intCast

added theorem ZMod.toCircle_natCast

Modified Mathlib/MeasureTheory/MeasurableSpace/Instances.lean

Modified Mathlib/Topology/Instances/AddCircle.lean

added theorem ZMod.toAddCircle_apply

added theorem ZMod.toAddCircle_eq_zero

added theorem ZMod.toAddCircle_inj

added theorem ZMod.toAddCircle_injective

added theorem ZMod.toAddCircle_intCast

added theorem ZMod.toAddCircle_natCast

Created Mathlib/Topology/Instances/ZMod.lean