English
For any n ∈ ℤ and x ∈ AddCircle(T), the negative index Fourier satisfies f_{-n}(x) = overline{f_n(x)}; equivalently f_{-n} = conj(f_n).
Русский
Для любого n ∈ ℤ и x ∈ AddCircle(T) мономиала Фурье с индексом −n равна сопряжённой к f_n: f_{-n}(x) = conj(f_n(x)).
LaTeX
$$$f_{-n}(x) = \\overline{f_n(x)} \\quad (n \\in \\mathbb{Z}, x \\in AddCircle(T)).$$$
Lean4
theorem fourier_neg {n : ℤ} {x : AddCircle T} : fourier (-n) x = conj (fourier n x) :=
by
induction x using QuotientAddGroup.induction_on
simp_rw [fourier_apply, toCircle]
rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_zsmul]
simp_rw [Function.Periodic.lift_coe, ← Circle.coe_inv_eq_conj, ← Circle.exp_neg, neg_smul, mul_neg]
