English
Let K be a compact set in E with measurable K. Let f and g be continuous real-valued functions on E. For any ε > 0 and δ > 0 such that |g(x) − f(x)| < δ for all x in K, the difference between the integrals of mulExpNegMulSq(ε, ·) composed with g and with f, over K with respect to P, is bounded by δ times (P(K)) raised to the real part; explicitly, |∫_K mulExpNegMulSq(ε, g(x)) dP − ∫_K mulExpNegMulSq(ε, f(x)) dP| ≤ δ · (P(K)).toReal.
Русский
Пусть K - компактное множество в E, измеримо по мере P. Пусть f, g: E → ℝ непрерывны. При ε > 0 и δ > 0, если для всех x ∈ K выполняется |g(x) − f(x)| < δ, то разность интегралов ∫_K mulExpNegMulSq(ε, g(x)) dP и ∫_K mulExpNegMulSq(ε, f(x)) dP по мере P удовлетворяет неравенству |∫_K mulExpNegMulSq(ε, g(x)) dP − ∫_K mulExpNegMulSq(ε, f(x)) dP| ≤ δ · (P(K)).toReal.
LaTeX
$$$|\\int_K mulExpNegMulSq(\\varepsilon, g(x)) \\, dP - \\int_K mulExpNegMulSq(\\varepsilon, f(x)) \\, dP| \\le \\delta \\cdot (P(K)).toReal$$$
Lean4
theorem abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure {K : Set E} (hK : IsCompact K) (hKmeas : MeasurableSet K)
(f g : C(E, ℝ)) {δ : ℝ} (hε : 0 < ε) (hfg : ∀ x ∈ K, |g x - f x| < δ) :
|∫ x in K, mulExpNegMulSq ε (g x) ∂P - ∫ x in K, mulExpNegMulSq ε (f x) ∂P| ≤ δ * (P K).toReal :=
by
rw [←
(integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
(integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f)),
← norm_eq_abs]
exact
norm_setIntegral_le_of_norm_le_const hK.measure_lt_top
(fun x hxK => le_trans (dist_mulExpNegMulSq_le_dist hε) (hfg x hxK).le)
