English
Let f: ℝ → ℂ be continuous with decay |x|^{-b} (b>1) and assume its Fourier transform 𝓕f is summable. Then for every x, the Poisson summation holds: the sum of f(x+n) over n ∈ ℤ equals the sum over n ∈ ℤ of the Fourier coefficient times the Fourier kernel.
Русский
Пуассонова сумма при распаде F.rpow: пусть f непрерывна и удовлетворяет распаду|x|^{-b} (b>1), а 𝓕f суммируема. Тогда для любого x выполняется формула Пуассона.
LaTeX
$$$\\forall x \\in \\mathbb{R},\\quad \\sum_{n\\in\\mathbb{Z}}' f(x+n) = \\sum_{n\\in\\mathbb{Z}}' \\mathcal{F}f(n) \\; \\mathrm{fourier}_n(x).$$$
Lean4
/-- **Poisson's summation formula**, assuming that `f` decays as
`|x| ^ (-b)` for some `1 < b` and its Fourier transform is summable. -/
theorem tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b)
(hf : IsBigO (cocompact ℝ) f fun x : ℝ => |x| ^ (-b)) (hFf : Summable fun n : ℤ => 𝓕 f n) (x : ℝ) :
∑' n : ℤ, f (x + n) = ∑' n : ℤ, 𝓕 f n * fourier n (x : UnitAddCircle) :=
Real.tsum_eq_tsum_fourierIntegral
(fun K =>
summable_of_isBigO (Real.summable_abs_int_rpow hb)
((isBigO_norm_restrict_cocompact ⟨_, hc⟩ (zero_lt_one.trans hb) hf K).comp_tendsto Int.tendsto_coe_cofinite))
hFf x
