English
For n ≠ 0, translating by T/(2n) negates the Fourier monomial: f_n(x + T/(2n)) = - f_n(x).
Русский
При n ≠ 0 поворот на T/(2n) меняет знак мономиалы Фурье: f_n(x + T/(2n)) = - f_n(x).
LaTeX
$$$f_n\\bigl(x + \\tfrac{T}{2n}\\bigr) = -f_n(x) \\quad (n \\neq 0).$$$
Lean4
/-- For `n ≠ 0`, a translation by `T / 2 / n` negates the function `fourier n`. -/
theorem fourier_add_half_inv_index {n : ℤ} (hn : n ≠ 0) (hT : 0 < T) (x : AddCircle T) :
@fourier T n (x + ↑(T / 2 / n)) = -fourier n x :=
by
rw [fourier_apply, zsmul_add, ← QuotientAddGroup.mk_zsmul, toCircle_add, Metric.unitSphere.coe_mul]
have : (@toCircle T (n • (T / 2 / n) : ℝ) : ℂ) = -1 :=
by
rw [zsmul_eq_mul, toCircle, Function.Periodic.lift_coe, Circle.coe_exp]
convert Complex.exp_pi_mul_I using 3
field_simp
rw [this]; simp
