English
For a real a and f:ℝ→ℂ, the Fourier coefficient of AddCircle.liftIoc T a f equals the interval Fourier coefficient of f on an appropriate interval, i.e. fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn (lt_add_of_pos_right a hT.out) f n.
Русский
Для a и f: ℝ→ℂ коэффициент Фурье функции AddCircle.liftIoc T a f совпадает с коэффициентом Фурье функции f на подходящем интервале: fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn (lt_add_of_pos_right a hT.out) f n.
LaTeX
$$$$ \\widehat{\\mathrm{liftIoc}(T,a)f}_n = \\widehat{f}_{\,[a,\\,a+T],n} $$$$
Lean4
theorem fourierCoeff_liftIoc_eq {a : ℝ} (f : ℝ → ℂ) (n : ℤ) :
fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn (lt_add_of_pos_right a hT.out) f n :=
by
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral, add_sub_cancel_left a T]
· congr 1
refine intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => ?_)
rw [liftIoc_coe_apply]
rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx
