norm_sq

Mathlib.Analysis.InnerProductSpace.Calculus

URI: https://scilib.ai/kg/mathlib#HasFDerivAt.norm_sq

← MathLib Explorer

English

See 51060 (duplicate): derivative of squared norm property.

Русский

См. 51060 (повторение): свойство производной квадрата нормы.

LaTeX

$$$$ \\text{HasFDerivAt}\\; (\\|f\\|^2) = 2 \\cdot (\\dots) $$$$

Lean4

theorem norm_sq {f : G → F} {f' : G →L[ℝ] F} (hf : HasFDerivAt f f' x) :
    HasFDerivAt (‖f ·‖ ^ 2) (2 • (innerSL ℝ (f x)).comp f') x :=
  (hasStrictFDerivAt_norm_sq _).hasFDerivAt.comp x hf

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

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

Разделы

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

Аффилиация

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