Theorems · Theorem · harmonic analysis

Real.tsum_eq_tsum_fourier

∀ {f : C(ℝ, ℂ)},
  (∀ (K : TopologicalSpace.Compacts ℝ),
      Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖) →
    (Summable fun n => FourierTransform.fourier ⇑f ↑n) →
      ∀ (x : ℝ), ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier ⇑f ↑n * (fourier n) ↑x

Poisson's summation formula, most general form.

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites38

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
Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
AddCommMonoidproof · cited by 12,281
SetLike.coestatement and proof · cited by 8,199
Set.Elemstatement · cited by 7,166
Complexstatement and proof · cited by 5,565
Norm.normstatement and proof · cited by 5,413
ContinuousMapstatement and proof · cited by 2,491
SummationFilter.unconditionalstatement and proof · cited by 2,068
tsumstatement and proof · cited by 1,148

Cited by1

Results whose statement or proof uses this declaration.

Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summableproof · cited by 1