norm_sq — Mathlib

English

If f is differentiable within a set s at x, then y ↦ ‖f(y)‖^2 is differentiable within s at x.

Русский

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

LaTeX

$$$\text{DifferentiableWithinAt}_{\mathbb{R}}(f,s,x) \Rightarrow \text{DifferentiableWithinAt}_{\mathbb{R}}(y \mapsto \|f(y)\|^2, s, x).$$$

Lean4

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

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