English
Let f be a C(ℝ, ℂ)-valued function on the real line with suitable decay and Fourier-coefficient summability. Then for every x ∈ ℝ the Poisson summation formula holds, equating the sum of shifts of f by integers with a sum over its Fourier coefficients times the corresponding Fourier kernel.
Русский
Пуассонова сумма: пусть f: ℝ → ℂ непрерывна и удовлетворяет соответствующим условиям распадности и суммируемости коэффициентов Фурье; тогда для каждого x ∈ ℝ имеет место равенство суммы сдвигов f по целым числам и суммы по коэффициентам Фурье, умноженным на соответствующий сингулярный ядро Фурье.
LaTeX
$$$\\displaystyle \\forall x \\in \\mathbb{R}\\\\ \\quad \\sum_{n \\in \\mathbb{Z}}' f(x+n) \;=\\; \\sum_{n \\in \\mathbb{Z}}' \\widehat{f}(n) \\cdot \\mathrm{fourier}_n(x).$$$
Lean4
/-- **Poisson's summation formula**, most general form. -/
theorem tsum_eq_tsum_fourierIntegral {f : C(ℝ, ℂ)}
(h_norm : ∀ K : Compacts ℝ, Summable fun n : ℤ => ‖(f.comp <| ContinuousMap.addRight n).restrict K‖)
(h_sum : Summable fun n : ℤ => 𝓕 f n) (x : ℝ) :
∑' n : ℤ, f (x + n) = ∑' n : ℤ, 𝓕 f n * fourier n (x : UnitAddCircle) :=
by
let F : C(UnitAddCircle, ℂ) :=
⟨(f.periodic_tsum_comp_add_zsmul 1).lift, continuous_coinduced_dom.mpr (map_continuous _)⟩
have : Summable (fourierCoeff F) := by
convert h_sum
exact Real.fourierCoeff_tsum_comp_add h_norm _
convert (has_pointwise_sum_fourier_series_of_summable this x).tsum_eq.symm using 1
·
simpa only [F, coe_mk, ← QuotientAddGroup.mk_zero, Periodic.lift_coe, zsmul_one, comp_apply, coe_addRight,
zero_add] using (hasSum_apply (summable_of_locally_summable_norm h_norm).hasSum x).tsum_eq
· simp_rw [← Real.fourierCoeff_tsum_comp_add h_norm, smul_eq_mul, F, coe_mk]
