Theorems · Theorem · harmonic analysis

hasSum_sq_fourierCoeff

∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)),
  HasSum (fun i => ‖fourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle)

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.

Defined in

Mathlib.Analysis.Fourier.AddCircle

Cited by

2 results in Mathlib

Foundations

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

Assumes

Fact