English
Assume f and its Fourier transform decay like |x|^{-b} with b>1. If both f and 𝓕f decay that way and the Fourier series ∑ 𝓕f(n) converges, then the Poisson summation holds for all x.
Русский
Предположим, что и f, и его преобразование Фурье распадаются как |x|^{-b} (b>1). Если оба ряда сходятся, то формула Пуассона выполняется для каждого x.
LaTeX
$$$\\forall x\\in\\mathbb{R},\\; \\sum_{n\\in\\mathbb{Z}}' f(x+n) = \\sum_{n\\in\\mathbb{Z}}' 𝓕f(n) \\; \\mathrm{fourier}_n(x).$$$
Lean4
/-- **Poisson's summation formula**, assuming that both `f` and its Fourier transform decay as
`|x| ^ (-b)` for some `1 < b`. (This is the one-dimensional case of Corollary VII.2.6 of Stein and
Weiss, *Introduction to Fourier analysis on Euclidean spaces*.) -/
theorem tsum_eq_tsum_fourierIntegral_of_rpow_decay {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b)
(hf : f =O[cocompact ℝ] (|·| ^ (-b))) (hFf : (𝓕 f) =O[cocompact ℝ] (|·| ^ (-b))) (x : ℝ) :
∑' n : ℤ, f (x + n) = ∑' n : ℤ, 𝓕 f n * fourier n (x : UnitAddCircle) :=
Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable hc hb hf
(summable_of_isBigO (Real.summable_abs_int_rpow hb) (hFf.comp_tendsto Int.tendsto_coe_cofinite)) x
