fourier_zero

Mathlib.Analysis.Fourier.AddCircle

URI: https://scilib.ai/kg/mathlib#fourier_zero

← MathLib Explorer

English

The zero Fourier monomial is the constant function 1 on AddCircle(T).

Русский

Нуль мономиалы Фурье соответствует константе 1 на AddCircle(T).

LaTeX

$$$f_0(x) = 1 \\quad \\text{for all } x \\in AddCircle(T).$$$

Lean4

theorem fourier_zero {x : AddCircle T} : fourier 0 x = 1 :=
  by
  induction x using QuotientAddGroup.induction_on
  simp only [fourier_coe_apply]
  norm_num

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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