English
If f is C^n in the real sense, then the map x ↦ ‖f(x)‖^2 is also C^n.
Русский
Если f является C^n, то отображение x ↦ ‖f(x)‖^2 также принадлежит классу C^n.
LaTeX
$$$$\\text{ContDiff}_{\\mathbb{R}}^n f \\quad\\Rightarrow\\quad \\text{ContDiff}_{\\mathbb{R}}^n \\big( x \\mapsto \\|f(x)\|^2 \\big).$$$$
Lean4
theorem contDiff_norm_sq : ContDiff ℝ n fun x : E => ‖x‖ ^ 2 :=
by
convert (reCLM : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))
exact (inner_self_eq_norm_sq _).symm