hasDerivAt_norm_rpow — Mathlib

English

In one dimension, the derivative of x ↦ ‖x‖^p equals p|x|^(p−2)x.

Русский

В одномерном случае производная функции x ↦ |x|^p равна p|x|^(p−2)x.

LaTeX

$$$\\text{HasDerivAt}(x \\mapsto \\|x\\|^p, p\\|x\\|^{p-2}x, x)$$$

Lean4

theorem hasDerivAt_norm_rpow (x : ℝ) {p : ℝ} (hp : 1 < p) :
    HasDerivAt (fun x : ℝ ↦ ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x := by
  convert hasFDerivAt_norm_rpow x hp |>.hasDerivAt using 1; simp

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