English
The inverse DFT is the normalized dual of the DFT, i.e., 𝓕⁻ Ψ = (N)^{-1} 𝓕 Ψ with negation on the dual argument.
Русский
Обратное преобразование Фурье — нормированное двойственное преобразование: 𝓕⁻ Ψ = (N)^{-1} 𝓕 Ψ(-k).
LaTeX
$$$\\mathcal{F}^{-1} \\Psi = (N)^{-1} \\mathcal{F} \\Psi(-\\cdot).$$$
Lean4
theorem invDFT_def (Ψ : ZMod N → E) : 𝓕⁻ Ψ = fun k ↦ (N : ℂ)⁻¹ • ∑ j : ZMod N, stdAddChar (j * k) • Ψ j :=
funext <| invDFT_apply Ψ