English
In Poisson summation, the m-th Fourier coefficient of the periodic sum ∑′ f(x+n) equals the Fourier transform of f evaluated at m.
Русский
В сумме Пуассона m-я фурье-коэффициента периодической суммы ∑′ f(x+n) равна значения Фурье-преобразования f в точке m.
LaTeX
$$$$ \widehat{f}(m) = \mathcal{F} f(m) $$$$
Lean4
theorem tendsto_integral_gaussian_smul (hf : Integrable f) (h'f : Integrable (𝓕 f)) (v : V) :
Tendsto (fun (c : ℝ) ↦ ∫ w : V, ((π * c) ^ (finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * c * ‖v - w‖ ^ 2)) • f w) atTop
(𝓝 (𝓕⁻ (𝓕 f) v)) :=
by
have A :
Tendsto (fun (c : ℝ) ↦ (∫ w : V, cexp (-c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫) • (𝓕 f) w)) atTop (𝓝 (𝓕⁻ (𝓕 f) v)) :=
by
have : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • (𝓕 f) w) :=
by
have B : Continuous fun p : V × V => (-innerₗ V) p.1 p.2 := continuous_inner.neg
simpa using (VectorFourier.fourierIntegral_convergent_iff Real.continuous_fourierChar B v).2 h'f
convert tendsto_integral_cexp_sq_smul this using 4 with c w
· rw [Submonoid.smul_def, Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_comm]
congr 3
simp only [ofReal_mul, ofReal_ofNat]
ring
· simp [fourierIntegralInv_eq]
have B :
Tendsto (fun (c : ℝ) ↦ (∫ w : V, 𝓕 (fun w ↦ cexp (-c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)) w • f w)) atTop
(𝓝 (𝓕⁻ (𝓕 f) v)) :=
by
apply A.congr'
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
have J : Integrable (fun w ↦ cexp (-c⁻¹ * ‖w‖ ^ 2 + 2 * π * I * ⟪v, w⟫)) :=
GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (by simpa) _ _
simpa using
(VectorFourier.integral_fourierIntegral_smul_eq_flip (L := innerₗ V) Real.continuous_fourierChar continuous_inner
J hf).symm
apply B.congr'
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
congr with w
rw [fourierIntegral_gaussian_innerProductSpace' (by simpa)]
congr
· simp
· simp; ring
