hasSum_mFourier_series_of_summable

English

If the Fourier coefficients are summable, then the Fourier series converges to f in the sup norm.

Русский

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

LaTeX

$$$$\\text{HasSum}(f) = \\sum_i mFourierCoeff(f,i) \\cdot mFourier(i) \\text{ и сх. в } \\|\\cdot\\|_\\infty.$$$$

Lean4

/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series converges
uniformly to `f`. -/
theorem hasSum_mFourier_series_of_summable (h : Summable (mFourierCoeff f)) :
    HasSum (fun i ↦ mFourierCoeff f i • mFourier i) f :=
  by
  have sum_L2 := hasSum_mFourier_series_L2 (ContinuousMap.toLp 2 volume ℂ f)
  simp only [mFourierCoeff_toLp] at sum_L2
  refine ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2
  simpa only [norm_smul, mFourier_norm, mul_one] using h.norm

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