English
As a parameter c tends to infinity, a Gaussian-weighted integral of f tends to the plain integral of f, i.e., localization by Gaussian weights recovers the total integral.
Русский
При стремлении параметра c к бесконечности гауссов весовой интеграл от f стремится к обычному интегралу от f.
LaTeX
$$$$ \lim_{c\to\infty} \int_V e^{-c^{-1}\|v\|^{2}} f(v) \, dv = \int_V f(v) \, dv $$$$
Lean4
theorem tendsto_integral_cexp_sq_smul (hf : Integrable f) :
Tendsto (fun (c : ℝ) ↦ (∫ v : V, cexp (-c⁻¹ * ‖v‖ ^ 2) • f v)) atTop (𝓝 (∫ v : V, f v)) :=
by
apply tendsto_integral_filter_of_dominated_convergence _ _ _ hf.norm
· filter_upwards with v
nth_rewrite 2 [show f v = cexp (-(0 : ℝ) * ‖v‖ ^ 2) • f v by simp]
apply (Tendsto.cexp _).smul_const
exact tendsto_inv_atTop_zero.ofReal.neg.mul_const _
· filter_upwards with c using AEStronglyMeasurable.smul (Continuous.aestronglyMeasurable (by fun_prop)) hf.1
· filter_upwards [Ici_mem_atTop (0 : ℝ)] with c (hc : 0 ≤ c)
filter_upwards with v
simp only [ofReal_inv, neg_mul, norm_smul]
norm_cast
conv_rhs => rw [← one_mul (‖f v‖)]
gcongr
simp only [norm_eq_abs, abs_exp, exp_le_one_iff, Left.neg_nonpos_iff]
positivity
