rpow_const — Mathlib

English

If f is differentiable at x with derivative f', and f(x) ≠ 0 or p ≥ 1, then the derivative at x of the function y ↦ f(y)^p is f'(x) · p · f(x)^{p−1}. In symbols, d/dx [f(x)^p] = f'(x) p f(x)^{p−1}.

Русский

Если f дифференцируема в точке x с производной f', и f(x) ≠ 0 или p ≥ 1, то производная в точке x функции y ↦ f(y)^p равна f'(x) p f(x)^{p−1}.

LaTeX

$$$\\displaystyle \\frac{d}{dx}\\bigl(f(x)^p\\bigr) = f'(x) \\cdot p \\cdot f(x)^{\,p-1}$$$

Lean4

theorem rpow_const (hf : HasDerivAt f f' x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
    HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hf.rpow_const hx

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