English
For all y ∈ ℝ, HasDerivAt mulExpNegMulSq ε at y with the explicit derivative formula: exp (−ε y^2) + y (exp (−ε y^2) (−2 ε y)).
Русский
Для всех y ∈ ℝ функция mulExpNegMulSq ε имеет производную по x в точке y, равную exp(−ε y^2) + y exp(−ε y^2)(−2 ε y).
LaTeX
$$$\\forall y \\in \\mathbb{R},\\; HasDerivAt( mulExpNegMulSq\\,\\varepsilon)\\,\\bigl( exp(-\\varepsilon y^2) + y \\bigl( exp(-\\varepsilon y^2) ( -2 \\varepsilon y) \\bigr) \\bigr)\\, y$$$
Lean4
theorem hasDerivAt_mulExpNegMulSq (y : ℝ) :
HasDerivAt (mulExpNegMulSq ε) (exp (-(ε * y * y)) + y * (exp (-(ε * y * y)) * (-2 * ε * y))) y :=
by
nth_rw 1 [← one_mul (exp (-(ε * y * y)))]
apply HasDerivAt.mul (hasDerivAt_id' y)
apply
HasDerivAt.exp
(HasDerivAt.congr_deriv
(HasDerivAt.neg (HasDerivAt.mul (HasDerivAt.const_mul ε (hasDerivAt_id' y)) (hasDerivAt_id' y))) (by ring))
