English
For each integer n, the function f_n: AddCircle(T) → ℂ defined by f_n([x]) = e^{2π i n x / T} is a continuous map on the circle of circumference T; these functions are the exponential Fourier monomials.
Русский
Для каждого целого n функция f_n: AddCircle(T) → ℂ, заданная f_n([x]) = e^{2π i n x / T}, является непрерывной на окружности радиуса T; эти функции образуют экспоненциальные мономиалы Фурье.
LaTeX
$$$f_n: AddCircle(T) \\to \\mathbb{C}, \\quad f_n([x]) = e^{2\\pi i n x / T}, \\quad n \\in \\mathbb{Z}, x \\in AddCircle(T).$$$
Lean4
/-- The family of exponential monomials `fun x => exp (2 π i n x / T)`, parametrized by `n : ℤ` and
considered as bundled continuous maps from `ℝ / ℤ • T` to `ℂ`. -/
def fourier (n : ℤ) : C(AddCircle T, ℂ) where
toFun x := toCircle (n • x :)
continuous_toFun := continuous_induced_dom.comp <| continuous_toCircle.comp <| continuous_zsmul _
