English
In the L^2 setting on AddCircle, the Fourier series of an L^2-function f converges in the Hilbert space to f; equivalently, the squared-norm of f equals the sum of squared magnitudes of its Fourier coefficients.
Русский
Для функции f в L^2(AddCircle) ряд Фурье сходится к f в пространстве Гильберта; сумма квадратов модулей коэффициентов Фурье равна норме L^2(f)^2.
LaTeX
$$$$ \\|f\\|_{L^2}^2 = \\sum_{i\\in\\mathbb{Z}} |\\widehat{f}(i)|^{2} $$$$
Lean4
/-- The Fourier series of an `L2` function `f` sums to `f`, in the `L²` space of `AddCircle T`. -/
theorem hasSum_fourier_series_L2 (f : Lp ℂ 2 <| @haarAddCircle T hT) :
HasSum (fun i => fourierCoeff f i • fourierLp 2 i) f :=
by
simp_rw [← fourierBasis_repr]; rw [← coe_fourierBasis]
exact HilbertBasis.hasSum_repr fourierBasis f
