contDiff_norm_sq — Mathlib

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

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