differentiable_norm_rpow

Mathlib.Analysis.InnerProductSpace.NormPow

URI: https://scilib.ai/kg/mathlib#differentiable_norm_rpow

← MathLib Explorer

English

The derivative of x ↦ |x|^p is the same as for ‖x‖^p, i.e. p|x|^(p−2)x.

Русский

Производная функции x ↦ |x|^p совпадает с производной ‖x‖^p, т.е. p|x|^(p−2)x.

LaTeX

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

Lean4

theorem differentiable_norm_rpow {p : ℝ} (hp : 1 < p) : Differentiable ℝ (fun x : E ↦ ‖x‖ ^ p) := fun x ↦
  hasFDerivAt_norm_rpow x hp |>.differentiableAt

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru