deriv_mulExpNegMulSq — Mathlib

English

For all ε ∈ ℝ and y ∈ ℝ, the derivative equals exp (−ε y^2) + y (exp (−ε y^2) (−2 ε y)).

Русский

Для всех ε ∈ ℝ и y ∈ ℝ производная равна exp(−ε y^2) + y (exp(−ε y^2) (−2 ε y)).

LaTeX

$$$\\forall \\varepsilon \\in \\mathbb{R},\\; \\frac{d}{dy} (mulExpNegMulSq\\,\\varepsilon\\, y) = exp(-\\varepsilon y^2) + y ( exp(-\\varepsilon y^2) ( -2 \\varepsilon y))$$$

Lean4

theorem deriv_mulExpNegMulSq (y : ℝ) :
    deriv (mulExpNegMulSq ε) y = exp (-(ε * y * y)) + y * (exp (-(ε * y * y)) * (-2 * ε * y)) :=
  HasDerivAt.deriv (hasDerivAt_mulExpNegMulSq y)

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