English
For any ε ∈ ℝ and any f: α → ℝ continuous, the composition x ↦ mulExpNegMulSq ε (f(x)) is continuous.
Русский
Для любого ε ∈ ℝ и любой непрерывной функции f: α → ℝ композиция x ↦ mulExpNegMulSq ε (f(x)) непрерывна.
LaTeX
$$$\\forall \\varepsilon \\in \\mathbb{R},\\; \\forall f:\\u00A0\\alpha \\to \\mathbb{R},\\; f\\text{ continuous} \\Rightarrow (x \\mapsto mulExpNegMulSq\\,\\varepsilon\\,(f(x)))\\text{ is continuous}$$$
Lean4
/-- For fixed `ε > 0`, the mapping `x ↦ mulExpNegMulSq ε x` is bounded by `(√ε)⁻¹ -/
theorem abs_mulExpNegMulSq_le (hε : 0 < ε) {x : ℝ} : |mulExpNegMulSq ε x| ≤ (√ε)⁻¹ :=
by
rw [mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one hε x, abs_mul, abs_of_pos (by positivity)]
apply mul_le_of_le_one_right
· positivity
· exact abs_mulExpNegMulSq_one_le_one (√ε * x)
