clog — Mathlib

English

If f: E → ℂ has a Fréchet derivative f' at x and f(x) ∈ slitPlane, then the Fréchet derivative of log(f) at x is (f(x))^{-1} · f'.

Русский

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

LaTeX

$$$$ \text{If } f: E \to \mathbb{C},\; Df(x) = f',\; 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₁ : HasFDerivAt f f' x) (h₂ : f x ∈ slitPlane) :
    HasFDerivAt (fun t => log (f t)) ((f x)⁻¹ • f') x :=
  (hasStrictDerivAt_log h₂).hasDerivAt.comp_hasFDerivAt x h₁

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