hasDerivAt_abs_rpow — Mathlib

English

For p>1, the function x ↦ |x|^p is differentiable with derivative p|x|^{p-2}x.

Русский

При p>1 функция x ↦ |x|^p дифференцируема и имеет производную p|x|^{p-2}x.

LaTeX

$$$\\text{Differentiable}(x \\mapsto |x|^p)\\Rightarrow \\text{derivative}=p|x|^{p-2}x$$$

Lean4

theorem hasDerivAt_abs_rpow (x : ℝ) {p : ℝ} (hp : 1 < p) : HasDerivAt (fun x : ℝ ↦ |x| ^ p) (p * |x| ^ (p - 2) * x) x :=
  by simpa using hasDerivAt_norm_rpow x hp

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