norm_sq — Mathlib

English

For a function f: R → F differentiable at x with derivative f', the derivative of the real-valued function t ↦ ‖f(t)‖^2 at x is the map h ↦ 2 ⟪f(x), f'(h)⟫.

Русский

Для функции f: ℝ → F, дифференцируемой в точке x с производной f', производная t ↦ ‖f(t)‖^2 в x равна h ↦ 2 ⟪f(x), f'(h)⟫.

LaTeX

$$$$\text{HasFDerivAt}$ \|f\|^2, \; 2 \langle f(x), f'\rangle $ at x.$$

Lean4

theorem norm_sq {f : ℝ → F} {f' : F} {x : ℝ} (hf : HasDerivAt f f' x) : HasDerivAt (‖f ·‖ ^ 2) (2 * ⟪f x, f'⟫) x := by
  simpa using hf.hasFDerivAt.norm_sq.hasDerivAt

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