norm_sq — Mathlib

English

If f is differentiable at x, then the map y ↦ ‖f(y)‖^2 is differentiable at x.

Русский

Если f дифференцируема в точке x, то y ↦ ‖f(y)‖^2 дифференцируема в x.

LaTeX

$$$$\text{DifferentiableAt}_{\mathbb{R}} f x \Rightarrow \text{DifferentiableAt}_{\mathbb{R}} (\|f\|^2) x.$$$$

Lean4

theorem norm_sq (hf : DifferentiableAt ℝ f x) : DifferentiableAt ℝ (fun y => ‖f y‖ ^ 2) x :=
  ((contDiffAt_id.norm_sq 𝕜).differentiableAt le_rfl).comp x hf

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