exp — Mathlib

English

If f has a Fréchet derivative f' at x, then exp(f) has derivative exp(f(x)) times f' at x.

Русский

Если у f есть производная Фреше в точке x, то у exp(f) производная равна exp(f(x)) умноженному на f' в x.

LaTeX

$$$$ \HasFDerivAt(f, f', x) \Rightarrow \HasFDerivAt(\lambda y. \exp(f(y)), \exp(f(x)) \cdot f', x) $$$$

Lean4

theorem exp (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') x :=
  (Real.hasDerivAt_exp (f x)).comp_hasFDerivAt x hf

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