Theorems · Theorem · harmonic analysis
tsum_sq_fourierCoeffOn
∀ {a b : ℝ} {f : ℝ → ℂ} (hab : a < b),
MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b)) →
∑' (i : ℤ), ‖fourierCoeffOn hab f i‖ ^ 2 = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2- Defined in
- Mathlib.Analysis.Fourier.AddCircle
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 274 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- ENNRealstatement · cited by 9,879
- Complexstatement and proof · cited by 5,565
- Norm.normstatement · cited by 5,413
- SummationFilter.unconditionalstatement · cited by 2,068
- MeasureTheory.Measure.restrictstatement and proof · cited by 1,646
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- tsumstatement · cited by 1,148
- Set.Iocstatement and proof · cited by 971
- intervalIntegralstatement · cited by 546
- MeasureTheory.MemLpstatement and proof · cited by 457
- HasSum.tsum_eqproof · cited by 150
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.