English
Given hab with a<b, if f has HasDerivAt f on [[a,b]] with derivative f', then the Fourier coefficient on [a,b] equals a certain combination involving f(b)-f(a) and the derivative Fourier coefficients.
Русский
Пусть hab: a<b; если f имеет производную HasDerivAt на [[a,b]] и hf' существует, то коэффициент Фурье на [a,b] задан как сумма через f(b)-f(a) и коэффициенты производной.
LaTeX
$$$$ \\text{fourierCoeffOn}_{hab} f n = \\frac{1}{-2 i \\pi n} ( \\mathrm{fourier}(-n)(a)(f(b)-f(a)) - (b-a) \\mathrm{fourierCoeffOn}_{hab} f' n ) $$$$
Lean4
/-- Express Fourier coefficients of `f` on an interval in terms of those of its derivative. -/
theorem fourierCoeffOn_of_hasDerivAt {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0)
(hf : ∀ x, x ∈ [[a, b]] → HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' volume a b) :
fourierCoeffOn hab f n =
1 / (-2 * π * I * n) * (fourier (-n) (a : AddCircle (b - a)) * (f b - f a) - (b - a) * fourierCoeffOn hab f' n) :=
fourierCoeffOn_of_hasDerivAt_Ioo hab hn (fun x hx ↦ hf x hx |>.continuousAt.continuousWithinAt)
(fun x hx ↦ hf x <| mem_Icc_of_Ioo hx) hf'
