English
There exists an antiderivative relation for the Fourier monomial with respect to the variable, yielding a factor corresponding to −2π i n / T.
Русский
Существует связь интегрирования по переменной в мономе Фурье, приводящая к фактору −2π i n / T.
LaTeX
$$$$ \\int \\frac{d}{dy} \\mathrm{fourier}_{n}(y) \, dy = \\frac{1}{-2\\pi i n / T} \\mathrm{fourier}_{n}(y) $$$$
Lean4
theorem has_antideriv_at_fourier_neg (hT : Fact (0 < T)) {n : ℤ} (hn : n ≠ 0) (x : ℝ) :
HasDerivAt (fun y : ℝ => (T : ℂ) / (-2 * π * I * n) * fourier (-n) (y : AddCircle T))
(fourier (-n) (x : AddCircle T)) x :=
by
convert (hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1
· ext1 y; rw [div_div_eq_mul_div]; ring
· simp [mul_div_cancel_left₀, hn, (Fact.out : 0 < T).ne', Real.pi_pos.ne']
