English
If f has a derivative inside an open interval Ioo (min a b, max a b), then the Fourier coefficient on [a,b] can be expressed in terms of the boundary values f(a), f(b) and the Fourier coefficients of the derivative on [a,b].
Русский
Если у f существует производная внутри открытого интервала Ioo(min(a,b), max(a,b)), то коэффициент Фурье на [a,b] может быть выражен через значения на границе и коэффициенты производной на этом отрезке.
LaTeX
$$$$ \\text{fourierCoeffOn}_{hab} f n = \\frac{1}{-2\\pi i 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_Ioo {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0)
(hf : ContinuousOn f [[a, b]]) (hff' : ∀ x, x ∈ Ioo (min a b) (max 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_hasDeriv_right hab hn hf (fun x hx ↦ hff' x hx |>.hasDerivWithinAt) hf'
