log — Mathlib

English

If f is differentiable at x and f(x) ≠ 0, then the derivative of log(f(x)) equals the logarithmic derivative logDeriv f at x.

Русский

Если f дифференцируема в x и f(x) ≠ 0, то производная log(f(x)) равна логарифмическому производному logDeriv f в x.

LaTeX

$$deriv (log ∘ f) x = logDeriv f x$$

Lean4

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

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