hasSum_mFourier_series_apply_of_summable

English

If Fourier coefficients are summable, then the Fourier series converges pointwise to f at every x.

Русский

Если коэффициенты Фурье суммируемы, ряд Фурье сходится в каждой точке к f.

LaTeX

$$$$\\forall x,\\ HasSum\\Big( mFourierCoeff(f,i) \\cdot mFourier(i)(x) \\Big) = f(x). $$$$

Lean4

/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series of `f`
converges everywhere pointwise to `f`. -/
theorem hasSum_mFourier_series_apply_of_summable (h : Summable (mFourierCoeff f)) (x : UnitAddTorus d) :
    HasSum (fun i ↦ mFourierCoeff f i • mFourier i x) (f x) := by
  simpa only [map_smul] using (ContinuousMap.evalCLM ℂ x).hasSum (hasSum_mFourier_series_of_summable h)

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