deriv_cpow_const — Mathlib

English

If f is differentiable at x and f(x) ∈ slitPlane, then the derivative of x ↦ f(x)^{c} is f(x)^{c} log f(x) · f'(x) scaled by c? (standard form: c f(x)^{c-1} f'(x)).

Русский

Если f дифференцируема в x и f(x) ∈ slitPlane, то производная x ↦ f(x)^{c} равна c f(x)^{c-1} f'(x).

LaTeX

$$$\\text{If }f\\text{ is differentiable at }x\\text{ and }f(x)\\in\\mathrm{slitPlane},\\ \\dfrac{d}{dx} f(x)^{c}= c f(x)^{c-1} f'(x).$$$

Lean4

theorem deriv_cpow_const (hf : DifferentiableAt ℂ f x) (hx : f x ∈ Complex.slitPlane) :
    deriv (fun (x : ℂ) ↦ f x ^ c) x = c * f x ^ (c - 1) * deriv f x :=
  (hf.hasDerivAt.cpow_const hx).deriv

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