fourier_one — Mathlib

English

For every x ∈ AddCircle(T), f_1(x) = x considered as a point on the unit circle, i.e., the first monomial equals the identity character.

Русский

Для каждого x ∈ AddCircle(T) мономиала f_1(x) соответствует экспоненте и равна точке на единичной окружности; первый мономиал — это характеристическая функция верха круга.

LaTeX

$$$f_1(x) = e^{\\frac{2\\pi i x}{T}}$ for all $x\\in AddCircle(T).$$$

Lean4

theorem fourier_one {x : AddCircle T} : fourier 1 x = toCircle x := by
  rw [fourier_apply, one_zsmul]
    -- simp normal form is `fourier_neg'`

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