Theorems · Theorem · harmonic analysis

UnitAddTorus.hasSum_sq_mFourierCoeff

∀ {d : Type u_1} [inst : Fintype d] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)),
  HasSum (fun i => ‖UnitAddTorus.mFourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : UnitAddTorus d), ‖↑↑f t‖ ^ 2)

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.

Defined in

Mathlib.Analysis.Fourier.AddCircleMulti

Cited by

0 results in Mathlib

Foundations

Depth 276 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype