exp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exp (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') x :=
  (Real.hasStrictDerivAt_exp (f x)).comp_hasStrictFDerivAt x hf

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