log — Mathlib

English

Let f be differentiable at x and f(x) ≠ 0. Then the derivative of log(f(x)) at x is f(x)^{-1} times the derivative of f at x; i.e., D(log∘f)(x) = f(x)^{-1} · Df(x).

Русский

Пусть f дифференцируема в точке x и f(x) ≠ 0. Тогда производная log(f(x)) в точке x равна f(x)^{-1} умноженной на производную f в x; т.е. D(log ∘ f)(x) = f(x)^{-1} · Df(x).

LaTeX

$$$D(\log \circ f)(x) = f(x)^{-1} \cdot Df(x)$$$

Lean4

@[simp]
theorem log (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) : fderiv ℝ (fun x => log (f x)) x = (f x)⁻¹ • fderiv ℝ f x :=
  (hf.hasFDerivAt.log hx).fderiv

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