has_pointwise_sum_fourier_series_of_summable

English

Similarly for LiftIco, the Fourier coefficients of AddCircle.liftIco T a f equal the interval Fourier coefficients of f on the corresponding interval.

Русский

Аналогично LiftIco: коэффициенты Фурье AddCircle.liftIco T a f равны коэффициентам Фурье на соответствующем интервале.

LaTeX

$$$$ \\widehat{\\mathrm{liftIco}(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 of `f`
converges everywhere pointwise to `f`. -/
theorem has_pointwise_sum_fourier_series_of_summable (h : Summable (fourierCoeff f)) (x : AddCircle T) :
    HasSum (fun i => fourierCoeff f i • fourier i x) (f x) := by
  convert (ContinuousMap.evalCLM ℂ x).hasSum (hasSum_fourier_series_of_summable h)

Похожие утверждения