hasSum_mFourier_series_L2 — Mathlib

English

The Fourier series of an L2 function converges to the function in L2-norm.

Русский

Ряд Фурье функции в L2 сходится к самой функции в норме L2.

LaTeX

$$$$ \\text{HasSum}(\\sum_i mFourierCoeff(f,i) \\cdot mFourierLp(2,i)) = f $$ в L2.$$

Lean4

/-- The Fourier series of an `L2` function `f` sums to `f` in the `L²` norm. -/
theorem hasSum_mFourier_series_L2 (f : L²(UnitAddTorus d)) : HasSum (fun i ↦ mFourierCoeff f i • mFourierLp 2 i) f := by
  simpa [← coe_mFourierBasis, mFourierBasis_repr] using mFourierBasis.hasSum_repr f

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