cexp — Mathlib

English

If f: E → C has a Fréchet derivative f' at x, then exp ∘ f has Fréchet derivative exp(f(x))·f' at x.

Русский

Если f: E → ℂ имеет производную Фрете в x, то exp ∘ f имеет производную exp(f(x))·f' в x.

LaTeX

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

Lean4

theorem cexp (hf : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (fun x => Complex.exp (f x)) s x :=
  hf.hasFDerivWithinAt.cexp.differentiableWithinAt

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