Applications

TheoremPoisson’s formula#

Poisson's summation formula for Schwartz functions.

SchwartzMap.tsum_eq_tsum_fourier (f : SchwartzMap ℝ ℂ) (x : ℝ) :
  ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), (FourierTransform.fourier f) ↑n * (fourier n) ↑x

Sources

• Mathlib documentation: SchwartzMap.tsum_eq_tsum_fourier
• Source of SchwartzMap.tsum_eq_tsum_fourier in Mathlib/Analysis/Fourier/PoissonSummation.lean
• Mathlib undergraduate list: Distribution calculus › Applications

MathlibSchwartzMap.tsum_eq_tsum_fourier

Uses 8

Statement usesBorel sigma-algebra · Cos (extension of trigonometric functions to the complex plane) · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Schwartz space

Proof usesAbsolutely convergent series in Banach spaces · Fourier Series · Lebesgue measure (Measures and integral calculus)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.