English
A variant of the Gaussian limit for the Fourier transform under stronger integrability hypotheses, asserting convergence to pointwise values near v.
Русский
Условия с более сильной интегрируемостью дают сходимость гауссовой аппроксимации к конкретным значениям при фиксированной точке v.
LaTeX
$$$$ \text{tendsto}_{c\to\infty} \int f \to f(v) $$$$
Lean4
theorem tendsto_integral_gaussian_smul' (hf : Integrable f) {v : V} (h'f : ContinuousAt f v) :
Tendsto (fun (c : ℝ) ↦ ∫ w : V, ((π * c : ℂ) ^ (finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * c * ‖v - w‖ ^ 2)) • f w) atTop
(𝓝 (f v)) :=
by
let φ : V → ℝ := fun w ↦ π ^ (finrank ℝ V / 2 : ℝ) * Real.exp (-π ^ 2 * ‖w‖ ^ 2)
have A : Tendsto (fun (c : ℝ) ↦ ∫ w : V, (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v)) :=
by
apply tendsto_integral_comp_smul_smul_of_integrable'
· exact fun x ↦ by positivity
· rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]
nth_rewrite 2 [← pow_one π]
rw [← rpow_natCast, ← rpow_natCast, ← rpow_sub pi_pos, ← rpow_mul pi_nonneg, ← rpow_add pi_pos]
ring_nf
exact rpow_zero _
· have A : Tendsto (fun (w : V) ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop :=
by
rw [tendsto_const_mul_atTop_of_pos (by positivity)]
apply (tendsto_pow_atTop two_ne_zero).comp tendsto_norm_cobounded_atTop
have B :=
tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (finrank ℝ V / 2) 1 zero_lt_one |>.comp A |>.const_mul
(π ^ (-finrank ℝ V / 2 : ℝ))
rw [mul_zero] at B
convert B using 2 with x
simp only [neg_mul, one_mul, Function.comp_apply, ← mul_assoc, ← rpow_natCast, φ]
congr 1
rw [mul_rpow (by positivity) (by positivity), ← rpow_mul pi_nonneg, ← rpow_mul (norm_nonneg _), ← mul_assoc, ←
rpow_add pi_pos, mul_comm]
congr <;> ring
· exact hf
· exact h'f
have B :
Tendsto (fun (c : ℝ) ↦ ∫ w : V, ((c ^ (1 / 2 : ℝ)) ^ finrank ℝ V * φ ((c ^ (1 / 2 : ℝ)) • (v - w))) • f w) atTop
(𝓝 (f v)) :=
A.comp (tendsto_rpow_atTop (by simp))
apply B.congr'
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
congr with w
rw [← coe_smul]
congr
rw [ofReal_mul, ofReal_mul, ofReal_exp, ← mul_assoc]
congr
· rw [mul_cpow_ofReal_nonneg pi_nonneg hc.le, ← rpow_natCast, ← rpow_mul hc.le, mul_comm, ofReal_cpow pi_nonneg,
ofReal_cpow hc.le]
simp [div_eq_inv_mul]
· norm_cast
simp only [one_div, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, neg_mul, neg_inj, ← rpow_natCast,
← rpow_mul hc.le, mul_assoc]
simp
