English
For a Schwartz map f: ℝ → ℂ (rapidly decaying smooth function), Poisson summation holds: the integer-sum of f shifted by x equals the sum of the products of its Fourier transform with the Fourier kernel.
Русский
Для функции Швартца f: ℝ→ℂ выполняется формула Пуассона: сумма f(x+n) по n ∈ ℤ равна сумме 𝓕f(n)·fourier_n(x).
LaTeX
$$$\\sum_{n\\in\\mathbb{Z}}' f(x+n) = \\sum_{n\\in\\mathbb{Z}}' \\widehat{f}(n) \\; \\mathrm{fourier}_n(x),$ где f — SchwartzMap.$$
Lean4
/-- **Poisson's summation formula** for Schwartz functions. -/
theorem tsum_eq_tsum_fourierIntegral (f : SchwartzMap ℝ ℂ) (x : ℝ) :
∑' n : ℤ, f (x + n) = ∑' n : ℤ, fourierTransformCLM ℝ f n * fourier n (x : UnitAddCircle) := by
-- We know that Schwartz functions are `O(‖x ^ (-b)‖)` for *every* `b`; for this argument we take
-- `b = 2` and work with that.
apply
Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay f.continuous one_lt_two (f.isBigO_cocompact_rpow (-2))
((fourierTransformCLM ℝ f).isBigO_cocompact_rpow (-2))
