invDFT_def'

Mathlib.Analysis.Fourier.ZMod

URI: https://scilib.ai/kg/mathlib#ZMod.invDFT_def'

English

The inverse DFT is the same as 𝓕⁻ Ψ = (N)^{-1} 𝓕 Ψ with the negation of the index inside the kernel.

Русский

Обратное преобразование Фурье эквивалентно 𝓕⁻ Ψ = (N)^{-1} 𝓕 Ψ(-k).

LaTeX

$$$\\mathcal{F}^{-1} \\Psi = (N)^{-1} \\mathcal{F} \\Psi(-\\cdot).$$$

Lean4

theorem invDFT_def' (Ψ : ZMod N → E) : 𝓕⁻ Ψ = fun k ↦ (N : ℂ)⁻¹ • 𝓕 Ψ (-k) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru