invDFT_def — Mathlib

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 Ψ

Похожие утверждения