hasStrictFDerivAt_norm_sq — Mathlib

English

For any x, the derivative of the map z ↦ ‖z‖^2 at x is the linear map h ↦ 2 ⟪x, h⟫.

Русский

Производная отображения z ↦ ‖z‖^2 в точке x равна линейному отображению h ↦ 2 ⟪x, h⟫.

LaTeX

$$$$\text{HasStrictFDerivAt}$ \cdot, \|x\|^2$ $x$ = 2 \cdot \langle x, \cdot \rangle.$$$$

Lean4

theorem hasStrictFDerivAt_norm_sq (x : F) : HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • (innerSL ℝ x)) x :=
  by
  simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]
  convert (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)
  ext y
  simp [two_smul, real_inner_comm]

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