English
For a bounded continuous function g: E → ℝ and hε ≥ 0, |(mulExpNegMulSq ε ∘ g)(x)| ≤ ||g|| for all x.
Русский
Пусть g: E → ℝ ограничена и непрерывна; тогда для всех x выполняется |mulExpNegMulSq ε (g(x))| ≤ ||g||, при ε ≥ 0.
LaTeX
$$$\\forall E \\text{ with } \\text{TopologicalSpace}, \\; g:\\u00A0E \\to \\mathbb{R},\\; g\\text{ bounded},\\; \\forall x,\\; |mulExpNegMulSq\\,\\varepsilon\\,(g(x))| \\le \\|g\\|$$$
Lean4
/-- For a fixed bounded function `g`, `mulExpNegMulSq ε ∘ g` is bounded by `norm g`,
uniformly in `ε ≥ 0`. -/
theorem abs_mulExpNegMulSq_comp_le_norm {E : Type*} [TopologicalSpace E] {x : E} (g : BoundedContinuousFunction E ℝ)
(hε : 0 ≤ ε) : |(mulExpNegMulSq ε ∘ g) x| ≤ ‖g‖ :=
by
simp only [Function.comp_apply, mulExpNegMulSq, abs_mul, abs_exp]
apply le_trans (mul_le_of_le_one_right (abs_nonneg (g x)) _) (g.norm_coe_le_norm x)
rw [exp_le_one_iff, Left.neg_nonpos_iff, mul_assoc]
exact mul_nonneg hε (mul_self_nonneg (g x))
