dft_comp_neg

Mathlib.Analysis.Fourier.ZMod

URI: https://scilib.ai/kg/mathlib#ZMod.dft_comp_neg

English

The DFT commutes with negation of the index: 𝓕(Φ(-j)) = (𝓕Φ)(-k) for all k.

Русский

Печатение Фурье взаимно с отрицанием индекса: 𝓕(Φ(-j)) = 𝓕Φ(-k).

LaTeX

$$$\\\\mathcal{F}(j \\mapsto \\Phi(-j)) = k \\mapsto \\\\mathcal{F}\\\\Phi(-k)$$$

Lean4

theorem dft_comp_neg (Φ : ZMod N → E) : 𝓕 (fun j ↦ Φ (-j)) = fun k ↦ 𝓕 Φ (-k) :=
  auxDFT_neg ..

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

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

Разделы

Аффилиация

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