English
For any f ∈ C(E, ℝ), measurable K, ε > 0 with P(K^c) < ε, the difference between the integrals over E and over K of mulExpNegMulSq (ε)∘f is less than √ε.
Русский
Пусть f ∈ C(E, ℝ), K измерима, ε > 0 и P(K^c) < ε, тогда разность интегралов ∫ mulExpNegMulSq(ε)(f) по E и по K меньше √ε.
LaTeX
$$$\\forall f:\\, C(E, \\mathbb{R}),\\; \\forall K:\\, Set E\\; ( MeasurableSet K),\\; ε>0,\\; P(K^c) < ε^{1/2} \\Rightarrow \\, \left| \\int_E mulExpNegMulSq(ε, f) \\, dP - \\int_K mulExpNegMulSq(ε, f) \\, dP\\right| < \\sqrt{ε}$$$
Lean4
theorem abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt (f : C(E, ℝ)) {K : Set E} (hK : MeasurableSet K)
(hε : 0 < ε) (hKP : P Kᶜ < ε.toNNReal) :
|∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (f x) ∂P| < √ε :=
by
apply
lt_of_le_of_lt
(norm_integral_sub_setIntegral_le (Eventually.of_forall (fun _ => abs_mulExpNegMulSq_le hε)) hK
(integrable_mulExpNegMulSq_comp f hε))
rw [mul_inv_lt_iff₀ (sqrt_pos_of_pos hε), mul_self_sqrt (le_of_lt hε)]
exact toReal_lt_of_lt_ofReal hKP
