mFourier_neg

Mathlib.Analysis.Fourier.AddCircleMulti

URI: https://scilib.ai/kg/mathlib#UnitAddTorus.mFourier_neg

English

Let n: d → Z and x ∈ UnitAddTorus d. Then mFourier(-n)(x) equals the complex conjugate of mFourier(n)(x).

Русский

Пусть n: d → ℤ и x ∈ UnitAddTorus d. Тогда mFourier(-n)(x) равно сопряжённому mFourier(n)(x).

LaTeX

$$$ mFourier(-n)(x) = \overline{ mFourier(n)(x) } $$$

Lean4

theorem mFourier_neg : mFourier (-n) x = conj (mFourier n x) := by
  simp only [mFourier, Pi.neg_apply, fourier_neg, ContinuousMap.coe_mk, map_prod]

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

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

Разделы

Аффилиация

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