invDFT_apply'

Mathlib.Analysis.Fourier.ZMod

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

English

A variant: 𝓕⁻ Ψ k = (N)^{-1} 𝓕 Ψ(-k).

Русский

Вариант: 𝓕⁻ Ψ k = (N)^{-1} 𝓕 Ψ(-k).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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