dft_dft — Mathlib

English

Fourier inversion for the discrete transform: applying the transform twice yields a scalar multiple of the negated input: 𝓕(𝓕Φ)(j) = (N) · Φ(-j).

Русский

Обратное преобразование Фурье для дискретного преобразования: 𝓕(𝓕Φ)(j) = N Φ(-j).

LaTeX

$$$\\\\mathcal{F}(\\\\mathcal{F}\\\\Phi)(j) = (N : \\\\mathbb{C}) \\\\\\Phi(-j)$$$

Lean4

/-- Fourier inversion formula, discrete case. -/
theorem dft_dft (Φ : ZMod N → E) : 𝓕 (𝓕 Φ) = fun j ↦ (N : ℂ) • Φ (-j) :=
  auxDFT_auxDFT ..

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