log — Mathlib

English

If f has a strict Fréchet derivative f' at x and f(x) ≠ 0, log ∘ f has strict Fréchet derivative (f x)^{-1} • f'.

Русский

Если f имеет строгую производную Фреше в x и f(x) ≠ 0, то log ∘ f имеет строгую производную (f x)^{-1} • f'.

LaTeX

$$HasStrictFDerivAt log (f x) ((f x)^{-1} • f')$$

Lean4

theorem log (hf : HasStrictFDerivAt f f' x) (hx : f x ≠ 0) : HasStrictFDerivAt (fun x => log (f x)) ((f x)⁻¹ • f') x :=
  (hasStrictDerivAt_log hx).comp_hasStrictFDerivAt x hf

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