Theorems · Theorem · harmonic analysis

Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable

∀ {f : ℝ → ℂ},
  Continuous f →
    ∀ {b : ℝ},
      1 < b →
        (f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) →
          (Summable fun n => FourierTransform.fourier f ↑n) →
            ∀ (x : ℝ), ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier f ↑n * (fourier n) ↑x

Poisson's summation formula, assuming that f decays as |x| ^ (-b) for some 1 < b and its Fourier transform is summable.

Defined in

Mathlib.Analysis.Fourier.PoissonSummation

Cited by

1 results in Mathlib

Foundations

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