English
For bounded continuous g, the integral ∫ mulExpNegMulSq ε (g) dP converges to ∫ g dP as ε → 0+.
Русский
Пусть g ограничена и непрерывна. Тогда интеграл от mulExpNegMulSq ε (g) по P сходится к интегралу g по P при ε → 0+.
LaTeX
$$$\\text{Tendsto}\\bigl(\\lambda \\varepsilon. \\int_E mulExpNegMulSq(\\varepsilon, g(x))\\, dP\\bigr)\\; (\\mathcal{nhds\\,from\\,above}}) \\to \\int_E g(x)\\, dP$$$
Lean4
/-- The integral of `mulExpNegMulSq ε ∘ g` with respect to a finite measure `P` converges to the
integral of `g`, as `ε → 0` from above. -/
theorem tendsto_integral_mulExpNegMulSq_comp (g : E →ᵇ ℝ) :
Tendsto (fun ε => ∫ x, mulExpNegMulSq ε (g x) ∂P) (𝓝[>] 0) (𝓝 (∫ x, g x ∂P)) :=
by
apply tendsto_of_seq_tendsto
intro u hu
obtain ⟨N, hupos⟩ := eventually_atTop.mp (tendsto_nhdsWithin_iff.mp hu).2
apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
· exact Eventually.of_forall (fun n => g.continuous.mulExpNegMulSq.aestronglyMeasurable)
· use norm g
rw [eventually_atTop]
use N
intro n hn
exact Eventually.of_forall (fun _ => abs_mulExpNegMulSq_comp_le_norm g (le_of_lt (Set.mem_Ioi.mp (hupos n hn))))
· exact Eventually.of_forall (fun _ => (tendsto_nhdsWithin_of_tendsto_nhds tendsto_mulExpNegMulSq).comp hu)
