clog_real — Mathlib

English

For f: ℝ → ℂ, s ⊆ ℝ, x ∈ s with f(x) ∈ slitPlane, HasDerivWithinAt log(f(t)) derivative is f' / f(x) inside s.

Русский

Для f: ℝ → ℂ, s ⊆ ℝ, x ∈ s, если f(x) ∈ slitPlane, то производная log(f) внутри s равна f'(x)/f(x).

LaTeX

$$$$ \text{If } h_1 : \mathrm{HasDerivWithinAt}(f, f', s, x)\text{ and } f(x) \in \mathrm{slitPlane},\; \frac{d}{dt}\log(f(t))\Big|_{t=x} = \frac{f'(x)}{f(x)}. $$$$

Lean4

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

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