norm_sq — Mathlib

English

If f is differentiable within s at x with derivative f', then the derivative of the map t ↦ ‖f(t)‖^2 at x in direction h is 2 ⟪f(x), f'(h)⟫.

Русский

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

LaTeX

$$$$\text{HasDerivWithinAt}$ \|f\|^2\, s x, \; 2 ⟪f(x), f'(h)⟫ $ for h.$$

Lean4

theorem norm_sq {f : ℝ → F} {f' : F} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (‖f ·‖ ^ 2) (2 * ⟪f x, f'⟫) s x := by simpa using hf.hasFDerivWithinAt.norm_sq.hasDerivWithinAt

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