hasSum_sq_mFourierCoeff — Mathlib

English

The sum of squared norms of Fourier coefficients equals the L2-norm of f.

Русский

Сумма квадратов норм коэффициентов Фурье равна норме L2 функции.

LaTeX

$$$$\\sum_i \\|mFourierCoeff(f,i)\\|^2 = \\|f\\|_2^2.$$$$

Lean4

/-- **Parseval's identity** for norms: for an `L²` function `f` on `UnitAddTorus d`, the sum of the
squared norms of the Fourier coefficients equals the `L²` norm of `f`. -/
theorem hasSum_sq_mFourierCoeff (f : L²(UnitAddTorus d)) : HasSum (fun i ↦ ‖mFourierCoeff f i‖ ^ 2) (∫ t, ‖f t‖ ^ 2) :=
  by
  simpa only [← RCLike.inner_apply', inner_self_eq_norm_sq, ← integral_re (L2.integrable_inner f f)] using
    RCLike.hasSum_re ℂ (hasSum_prod_mFourierCoeff f f)

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