English
For complete target spaces, the discrete Fourier transform agrees with the general Fourier transform in the expected sense.
Русский
Для полных пространств дискретное преобразование Фурье совпадает с общим преобразованием Фурье в обычном смысле.
LaTeX
$$$\\mathcal{F}\\Phi = \\text{Fourier}(\\text{toCircle}, \\text{count}, \\Phi).$$$
Lean4
/-- The discrete Fourier transform agrees with the general one (assuming the target space is a complete
normed space).
-/
theorem dft_eq_fourier {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (Φ : ZMod N → E)
(k : ZMod N) : 𝓕 Φ k = Fourier.fourierIntegral toCircle Measure.count Φ k := by
simp only [dft_apply, stdAddChar_apply, Fourier.fourierIntegral_def, Circle.smul_def,
integral_countable' <| .of_finite .., count_real_singleton, one_smul, tsum_fintype]
