invDFT_apply — Mathlib

English

The inverse DFT applied to Ψ at k equals (N)^{-1} times the sum of stdAddChar(jk) • Ψ(j).

Русский

Применение обратного DFT к Ψ в точке k даёт (N)^{-1} ∑ stdAddChar(jk) Ψ(j).

LaTeX

$$$\\mathcal{F}^{-1} \\Psi(k) = (\\,N\\,)^{-1} \\sum_{j \\in \\mathbb{Z}/N\\mathbb{Z}} \\mathrm{stdAddChar}(j k) \\cdot \\Psi(j).$$$

Lean4

theorem invDFT_apply (Ψ : ZMod N → E) (k : ZMod N) : 𝓕⁻ Ψ k = (N : ℂ)⁻¹ • ∑ j : ZMod N, stdAddChar (j * k) • Ψ j := by
  simp only [dft, LinearEquiv.coe_symm_mk, auxDFT, mul_neg, neg_neg]

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