clog — Mathlib

English

For f: ℝ → ℂ differentiable with f(x) ∈ slitPlane, the real-derivative of log(f) at x is f'(x)/f(x).

Русский

Для f: ℝ → ℂ дифференцируемо, и f(x) ∈ slitPlane, производная log(f) по реальной переменной равна f'(x)/f(x).

LaTeX

$$$$ \text{If } f:\mathbb{R}\to\mathbb{C},\; f(x)\in \mathrm{slitPlane},\; \frac{d}{dx}\log(f(x)) = \frac{f'(x)}{f(x)}. $$$$

Lean4

theorem clog {f : E → ℂ} {x : E} (h₁ : DifferentiableAt ℂ f x) (h₂ : f x ∈ slitPlane) :
    DifferentiableAt ℂ (fun t => log (f t)) x :=
  (h₁.hasFDerivAt.clog h₂).differentiableAt

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