English
The derivative of log ∘ f equals logDeriv f when f is differentiable and its value lies in the slit plane.
Русский
Производная log ∘ f равна logDeriv f при дифференцируемости f и значении f на slitPlane.
LaTeX
$$$$ \text{If } f: \mathbb{C} \to \mathbb{C},\; x \mapsto \log(f(x)) \text{ is differentiable and } f(x) \in \mathrm{slitPlane}, \\ \text{then } \mathrm{deriv}(\log \circ f)(x) = \logDeriv f(x). $$$$
Lean4
/-- The derivative of `log ∘ f` is the logarithmic derivative provided `f` is differentiable and
we are on the slitPlane. -/
theorem deriv_log_comp_eq_logDeriv {f : ℂ → ℂ} {x : ℂ} (h₁ : DifferentiableAt ℂ f x) (h₂ : f x ∈ Complex.slitPlane) :
deriv (Complex.log ∘ f) x = logDeriv f x :=
by
have A := (HasDerivAt.clog h₁.hasDerivAt h₂).deriv
rw [← h₁.hasDerivAt.deriv] at A
simp only [logDeriv, Pi.div_apply, ← A, Function.comp_def]
