clog — Mathlib

English

For a map f: E → ℂ and a point x with f(x) ∈ slitPlane, the log-derivative holds with strict derivatives for HasStrictDerivAt or HasFDerivAt contexts.

Русский

Для отображения f: E → ℂ в точке x с f(x) ∈ slitPlane выполняется формула логарифмического производного для строгих производных.

LaTeX

$$$$ \text{If } f: E \to \mathbb{C},\; f(x) \in \mathrm{slitPlane} \Rightarrow D(\log \circ f)(x) = \frac{f'(x)}{f(x)}. $$$$

Lean4

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

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