cexp — Mathlib

English

If f has a strict derivative at x with derivative f', then exp ∘ f has strict derivative exp(f(x))·f' at x.

Русский

Если f имеет строгую производную в x с производной f', то exp(f(x)) умножает эту производную: HasStrictDerivAt(exp ∘ f) = exp(f(x))·f' в точке x.

LaTeX

$$$ \\forall x,\\ HasStrictDerivAt(f,f',x) \\Rightarrow HasStrictDerivAt(\\exp \\circ f, (\\exp( f(x) )) \\cdot f', x)$$$

Lean4

theorem cexp (hf : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') x :=
  (Complex.hasStrictDerivAt_exp (f x)).comp x hf

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