English
For a,b with a<b, the Fourier coefficient on [a,b] can be computed as the average value over the interval of the product of the conjugate Fourier basis element with f, i.e. the integral of fourier(-n) times f over [a,b] divided by (b−a).
Русский
Для a<b коэффициент Фурье на интервале [a,b] равен усреднённому за интервал произведению четырехier(-n) и f, то есть интегралу от fourier(-n)·f на [a,b], делённому на (b−a).
LaTeX
$$$$ \\widehat{f}_{[a,b],n} = \\frac{1}{b-a}\\int_{a}^{b} \\widehat{(-n)}(x) \\cdot f(x) \\, dx $$$$
Lean4
theorem fourierCoeffOn_eq_integral {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b) :
fourierCoeffOn hab f n = (1 / (b - a)) • ∫ x in a..b, fourier (-n) (x : AddCircle (b - a)) • f x :=
by
haveI := Fact.mk (by linarith : 0 < b - a)
rw [fourierCoeffOn, fourierCoeff_eq_intervalIntegral _ _ a, add_sub, add_sub_cancel_left]
congr 1
simp_rw [intervalIntegral.integral_of_le hab.le]
refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_
rw [liftIoc_coe_apply]
rwa [add_sub, add_sub_cancel_left]
