dist_mulExpNegMulSq_le_dist — Mathlib

English

For any bounded continuous g, as ε → 0 from above, the integral ∫ mulExpNegMulSq ε (g) dP tends to ∫ g dP.

Русский

Для любой ограниченно непрерывной функции g при ε → 0 сверху интеграл ∫ mulExpNegMulSq ε (g) dP стремится к ∫ g dP.

LaTeX

$$$\\text{As } \\varepsilon \\downarrow 0,\\; \\int_E mulExpNegMulSq(\\varepsilon, g(x))\\, dP \\to \\int_E g(x)\\, dP$$$

Lean4

theorem dist_mulExpNegMulSq_le_dist (hε : 0 < ε) {x y : ℝ} :
    dist (mulExpNegMulSq ε x) (mulExpNegMulSq ε y) ≤ dist x y :=
  by
  have h := lipschitzWith_one_mulExpNegMulSq hε x y
  rwa [ENNReal.coe_one, one_mul, ← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))] at h

Похожие утверждения