clog — Mathlib

English

If z ∈ slitPlane and h is HasStrictDerivAt f at x, then derivative of log ∘ f at x is f'(x)/f(x).

Русский

Если z ∈ slitPlane и есть строгая производная log ∘ f в точке x, то производная равна f'(x)/f(x).

LaTeX

$$$$ D(\log \circ f)(x) = \frac{f'(x)}{f(x)}, \quad f(x) \in \mathrm{slitPlane}. $$$$

Lean4

theorem clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : HasStrictDerivAt f f' x) (h₂ : f x ∈ slitPlane) :
    HasStrictDerivAt (fun t => log (f t)) (f' / f x) x := by rw [div_eq_inv_mul];
  exact (hasStrictDerivAt_log h₂).comp x h₁

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