log — Mathlib

English

If f has a differentiable map with nonzero values, then log ∘ f has the appropriate Fréchet derivative given by (f x)^{-1} times the derivative of f.

Русский

Если f имеет производную с ненулевыми значениями, то log ∘ f имеет соответствующую производную Фреше: (f(x))^{-1} умножает производную f.

LaTeX

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

Lean4

theorem log (hf : HasFDerivAt f f' x) (hx : f x ≠ 0) : HasFDerivAt (fun x => log (f x)) ((f x)⁻¹ • f') x :=
  (hasDerivAt_log hx).comp_hasFDerivAt x hf

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