English
Similarly to liftIoc, Fourier coefficients of AddCircle.liftIco T a f coincide with Fourier coefficients on the corresponding interval: fourierCoeff (AddCircle.liftIco T a f) n = fourierCoeffOn (lt_add_of_pos_right a hT.out) f n.
Русский
Аналогично liftIoc, коэффициенты Фурье AddCircle.liftIco совпадают с коэффициентами на соответствующем интервале.
LaTeX
$$$$ \\widehat{\\mathrm{liftIco}(T,a)f}_n = \\widehat{f}_{\\,[a,\\,a+T],n} $$$$
Lean4
theorem fourierCoeff_liftIco_eq {a : ℝ} (f : ℝ → ℂ) (n : ℤ) :
fourierCoeff (AddCircle.liftIco T a f) n = fourierCoeffOn (lt_add_of_pos_right a hT.out) f n :=
by
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral _ _ a, add_sub_cancel_left a T]
congr 1
simp_rw [intervalIntegral.integral_of_le (lt_add_of_pos_right a hT.out).le]
iterate 2 rw [integral_Ioc_eq_integral_Ioo]
refine setIntegral_congr_fun measurableSet_Ioo fun x hx => ?_
rw [liftIco_coe_apply (Ioo_subset_Ico_self hx)]
