clog_real — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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