English
For a function f in L^2(AddCircle), the sum over i of the squared norm of the Fourier coefficient equals the L^2-norm squared of f.
Русский
Для функции f в L^2(AddCircle) сумма по i квадратов модулей коэффициентов Фурье равна квадрату нормы L^2(f).
LaTeX
$$$$ \\sum_{i\\in\\mathbb{Z}} \\|\\widehat{f}(i)\\|^2 = \\|f\\|_{L^2}^2 $$$$
Lean4
/-- **Parseval's identity**: for an `L²` function `f` on `AddCircle T`, the sum of the squared
norms of the Fourier coefficients equals the `L²` norm of `f`. -/
theorem tsum_sq_fourierCoeff (f : Lp ℂ 2 <| @haarAddCircle T hT) :
∑' i : ℤ, ‖fourierCoeff f i‖ ^ 2 = ∫ t : AddCircle T, ‖f t‖ ^ 2 ∂haarAddCircle :=
by
simp_rw [← fourierBasis_repr]
have H₁ : ‖fourierBasis.repr f‖ ^ 2 = ∑' i, ‖fourierBasis.repr f i‖ ^ 2 :=
by
apply_mod_cast lp.norm_rpow_eq_tsum ?_ (fourierBasis.repr f)
simp
have H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp
have H₃ := congr_arg RCLike.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ _ f f)
rw [← integral_re] at H₃
· simp only [← norm_sq_eq_re_inner] at H₃
rw [← H₁, H₂, H₃]
· exact L2.integrable_inner f f
