norm_sq — Mathlib

English

If f has derivative f' within s at x, then y ↦ ‖f(y)‖^2 has derivative 2 ⟪f(x), f'(·)⟫ within s at x.

Русский

Если у f внутри s в x есть производная f', то y ↦ ‖f(y)‖^2 имеет внутри s в x производную 2 ⟪f(x), f'(·)⟫.

LaTeX

$$$$\text{HasFDerivWithinAt}$ \|f\|^2, \; 2 ⟪f(x), f'\rangle $ s x.$$$$

Lean4

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

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