English
As with liftIoc, the Fourier coefficients of AddCircle.liftIoc T a f match those of f on the corresponding interval.
Русский
Как и liftIoc, коэффициенты Фурье AddCircle.liftIoc T a f совпадают сcoefficients f на соответствующем интервале.
LaTeX
$$$$ \\widehat{\\mathrm{liftIoc}(T,a)f}_n = \\widehat{f}_{\\text{[a,a+T]},n} $$$$
Lean4
/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series converges
uniformly to `f`. -/
theorem hasSum_fourier_series_of_summable (h : Summable (fourierCoeff f)) :
HasSum (fun i => fourierCoeff f i • fourier i) f :=
by
have sum_L2 := hasSum_fourier_series_L2 (toLp (E := ℂ) 2 haarAddCircle ℂ f)
simp_rw [fourierCoeff_toLp] at sum_L2
refine ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2
simp_rw [norm_smul, fourier_norm, mul_one]
exact h.norm
