dist_mulExpNegMulSq_le_two_mul_sqrt

English

For any ε > 0, the map x ↦ mulExpNegMulSq ε x is 1-Lipschitz.

Русский

Для любого ε > 0 отображение x ↦ mulExpNegMulSq ε x является 1-липшицевой.

LaTeX

$$$\\forall \\varepsilon > 0,\\; LipschitzWith\\,1\\, (mulExpNegMulSq\\,\\varepsilon)$$$

Lean4

theorem dist_mulExpNegMulSq_le_two_mul_sqrt (hε : 0 < ε) (x y : ℝ) :
    dist (mulExpNegMulSq ε x) (mulExpNegMulSq ε y) ≤ 2 * (√ε)⁻¹ :=
  by
  apply le_trans (dist_triangle (mulExpNegMulSq ε x) 0 (mulExpNegMulSq ε y))
  simp only [dist_zero_right, norm_eq_abs, dist_zero_left, two_mul]
  exact add_le_add (abs_mulExpNegMulSq_le hε) (abs_mulExpNegMulSq_le hε)

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