fourier_coe_apply' — Mathlib

English

For every n ∈ ℤ and x ∈ AddCircle(T), the complex exponential associated to the real lift of x matches the fourier monomial, i.e., exp(2π i n x / T).

Русский

Для каждого n ∈ ℤ и x ∈ AddCircle(T) экспонента, связанная с представлением x, совпадает с мономиалой Фурье: exp(2π i n x / T).

LaTeX

$$$f_n(x) = e^{\\frac{2\\pi i\\,n\\,x}{T}} \\quad (n \\in \\mathbb{Z},\\ x \\in AddCircle(T)).$$$

Lean4

@[simp]
theorem fourier_coe_apply' {n : ℤ} {x : ℝ} :
    toCircle (n • (x : AddCircle T) :) = Complex.exp (2 * π * Complex.I * n * x / T) := by rw [← fourier_apply];
  exact fourier_coe_apply

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