English
The HasDerivAt of the Fourier coefficient function with respect to the variable y expresses the derivative of the Fourier monomial on AddCircle.
Русский
Существование производной коэффициента Фурье по переменной y выражает производную мононима Фурье на AddCircle.
LaTeX
$$$$ \\text{HasDerivAt}(\\;\\widehat{n}(y)\\;, \\text{something}, x) $$$$
Lean4
theorem hasDerivAt_fourier (n : ℤ) (x : ℝ) :
HasDerivAt (fun y : ℝ => fourier n (y : AddCircle T)) (2 * π * I * n / T * fourier n (x : AddCircle T)) x :=
by
simp_rw [fourier_coe_apply]
refine (?_ : HasDerivAt (fun y => exp (2 * π * I * n * y / T)) _ _).comp_ofReal
rw [(fun α β => by ring : ∀ α β : ℂ, α * exp β = exp β * α)]
refine (hasDerivAt_exp _).comp (x : ℂ) ?_
convert hasDerivAt_mul_const (2 * ↑π * I * ↑n / T) using 1
ext1 y; ring
