nnnorm_deriv_mulExpNegMulSq_le_one

English

If hε > 0 and x ∈ ℝ, then the NN-norm of the derivative is ≤ 1: ‖deriv (mulExpNegMulSq ε) x‖₊ ≤ 1.

Русский

Если hε > 0 и x ∈ ℝ, то NN-норма производной не превосходит 1.

LaTeX

$$$\\forall \\varepsilon > 0, \\; \\forall x \\in \\mathbb{R},\\; \\|\\dfrac{d}{dx} (mulExpNegMulSq\\,\\varepsilon)(x)\\|_{+} \\le 1$$$

Lean4

theorem nnnorm_deriv_mulExpNegMulSq_le_one (hε : 0 < ε) (x : ℝ) : ‖deriv (mulExpNegMulSq ε) x‖₊ ≤ 1 :=
  by
  rw [← NNReal.coe_le_coe, coe_nnnorm]
  exact norm_deriv_mulExpNegMulSq_le_one hε x

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