English
For n ∈ ℤ and x ∈ AddCircle(T), the Fourier monomial corresponds to exp(2π i n x / T); equivalently, the map x ↦ exp(2π i n x / T) is the evaluation of f_n at x.
Русский
Для n ∈ ℤ и x ∈ AddCircle(T) мономиала Фурье равняется exp(2π i n x / T); то есть f_n(x) = exp(2π i n x / T).
LaTeX
$$$f_n(x) = e^{\\frac{2\\pi i\,n\,x}{T}}$ for all $n \\in \\mathbb{Z}$, $x \\in AddCircle(T).$$$
Lean4
theorem fourier_coe_apply {n : ℤ} {x : ℝ} : fourier n (x : AddCircle T) = Complex.exp (2 * π * Complex.I * n * x / T) :=
by
rw [fourier_apply, ← QuotientAddGroup.mk_zsmul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp,
Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul, Complex.ofReal_mul,
Complex.ofReal_intCast]
norm_num
congr 1; ring
