English
For differentiable f and integer n, logDeriv of f(z) raised to n equals n times logDeriv f at x.
Русский
Для дифференцируемой f и целого n логарифмическая производная f(z)^n в точке x равна n умножить на logDeriv f x.
LaTeX
$$$\forall f:\; \mathbb{K}\to\mathbb{K}',\; x:\mathbb{K},\; \text{DifferentiableAt } f x\Rightarrow\forall n\in\mathbb{Z},\; \logDeriv\,(f\cdot^n)(x) = n\cdot \logDeriv f x$$$
Lean4
theorem logDeriv_fun_zpow {f : 𝕜 → 𝕜'} {x : 𝕜} (hdf : DifferentiableAt 𝕜 f x) (n : ℤ) :
logDeriv (f · ^ n) x = n * logDeriv f x :=
by
rcases eq_or_ne n 0 with rfl | hn; · simp
rcases eq_or_ne (f x) 0 with hf | hf
· simp [logDeriv_apply, zero_zpow, *]
· rw [logDeriv_apply, ← comp_def (· ^ n), deriv_comp _ (differentiableAt_zpow.2 <| .inl hf) hdf, deriv_zpow,
logDeriv_apply]
simp [field, zpow_sub_one₀ hf]
