clog_real — Mathlib

English

If f: ℝ → ℂ is differentiable and f(x) ∈ slitPlane for all x in domain, then log∘f is differentiable with derivative f'(x)/f(x).

Русский

Если f: ℝ → ℂ дифференцируема и для всех x из области определения f(x) ∈ slitPlane, то log(f(x)) дифференцируема и имеет производную f'(x)/f(x).

LaTeX

$$$$ \forall x,\; f(x) \in \mathrm{slitPlane} \Rightarrow \frac{d}{dx}\log(f(x)) = \frac{f'(x)}{f(x)}. $$$$

Lean4

theorem clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasDerivAt f f' x) (h₂ : f x ∈ slitPlane) :
    HasDerivAt (fun t => log (f t)) (f' / f x) x := by
  simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivAt x h₁

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