Commit 2024-08-29 01:14 b3e3fe2a

View on Github →

feat(Analysis/Fourier/ZMod): more API for discrete Fourier transform (#14535) Define the discrete Fourier transform as a LinearEquiv, rather than just a map; and prove the Fourier inversion formula, as well as a bunch of more routine lemmas.

Estimated changes

modified theorem ZMod.dft_apply
added theorem ZMod.dft_apply_zero
added theorem ZMod.dft_comp_neg
added theorem ZMod.dft_comp_unitMul
added theorem ZMod.dft_const_mul
added theorem ZMod.dft_const_smul
modified theorem ZMod.dft_def
added theorem ZMod.dft_dft
added theorem ZMod.dft_eq_fourier
added theorem ZMod.dft_mul_const
added theorem ZMod.dft_smul_const
added theorem ZMod.invDFT_apply'
added theorem ZMod.invDFT_apply
added theorem ZMod.invDFT_def'
added theorem ZMod.invDFT_def