clog — Mathlib

English

For f: E → ℂ, f' is the Fréchet derivative inside set s at x, if f(x) ∈ slitPlane, then (log ∘ f) has derivative (f(x))^{-1} · f' within s at x.

Русский

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

LaTeX

$$$$ \text{If } h_1 : \mathrm{HasFDerivWithinAt}(f, f', s, x) \\text{ and } f(x) \in \mathrm{slitPlane}, \\; \mathrm{HasFDerivWithinAt}(\log \circ f, (f(x))^{-1} \cdot f', s, x). $$$$

Lean4

theorem clog {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ} (h₁ : HasDerivWithinAt f f' s x) (h₂ : f x ∈ slitPlane) :
    HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x :=
  by
  rw [div_eq_inv_mul]
  exact (hasStrictDerivAt_log h₂).hasDerivAt.comp_hasDerivWithinAt x h₁

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