clog — Mathlib

English

If f: E → ℂ is differentiable and f(x) ∈ slitPlane, then the derivative of log(f) is (f(x))^{-1} · f'.

Русский

Если f: E → ℂ дифференцируема и f(x) ∈ slitPlane, то производная log(f) равна (f(x))^{-1} · f'.

LaTeX

$$$$ \text{If } f: E \to \mathbb{C},\; f' = Df(x),\; f(x) \in \mathrm{slitPlane},\quad D(\log \circ f)(x) = (f(x))^{-1} \cdot f'. $$$$

Lean4

theorem clog {f : E → ℂ} {f' : StrongDual ℂ E} {x : E} (h₁ : HasStrictFDerivAt f f' x) (h₂ : f x ∈ slitPlane) :
    HasStrictFDerivAt (fun t => log (f t)) ((f x)⁻¹ • f') x :=
  (hasStrictDerivAt_log h₂).comp_hasStrictFDerivAt x h₁

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