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) равна (f(x))^{-1} · f'.

LaTeX

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

Lean4

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

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