Theorems · Theorem · harmonic analysis

UnitAddTorus.hasSum_mFourier_series_of_summable

∀ {d : Type u_1} [inst : Fintype d] {f : C(UnitAddTorus d, ℂ)},
  Summable (UnitAddTorus.mFourierCoeff ⇑f) →
    HasSum (fun i => UnitAddTorus.mFourierCoeff (⇑f) i • UnitAddTorus.mFourier i) f

If the sequence of Fourier coefficients of f is summable, then the Fourier series converges uniformly to f.

Defined in: Mathlib.Analysis.Fourier.AddCircleMulti
Cited by: 1 results in Mathlib
Foundations: Depth 275 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites26

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement · cited by 25,697
Fintypestatement and proof · cited by 7,736
Complexstatement and proof · cited by 5,565
Norm.normproof · cited by 5,413
mul_oneproof · cited by 3,885
ContinuousMapstatement and proof · cited by 2,491
SummationFilter.unconditionalstatement and proof · cited by 2,068
MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
Summablestatement and proof · cited by 778
HasSumstatement and proof · cited by 518
AddSubgroup.zmultiplesstatement · cited by 493

Cited by1

Results whose statement or proof uses this declaration.

UnitAddTorus.hasSum_mFourier_series_apply_of_summableproof · cited by 0