English
For any nonzero t, if the norm function is ContDiffAt at x, then it is ContDiffAt at t x; scaling by a nonzero real preserves ContDiffAt of the norm.
Русский
При не нулевом t существование ContDiffAt для нормы в x эквивалентно существованию ContDiffAt в t x; масштабирование сохраняет континуально–дифференцируемость нормы.
LaTeX
$$$\\forall t \\neq 0:\\, \\text{ContDiffAt}_{\\mathbb{R}}(n)(\\|\\cdot\\|)(x) \\Rightarrow \\text{ContDiffAt}_{\\mathbb{R}}(n)(\\|\\cdot\\|)(t x)$$$
Lean4
theorem contDiffAt_norm_smul (ht : t ≠ 0) (h : ContDiffAt ℝ n (‖·‖) x) : ContDiffAt ℝ n (‖·‖) (t • x) :=
by
have h1 : ContDiffAt ℝ n (fun y ↦ t⁻¹ • y) (t • x) := (contDiff_const_smul t⁻¹).contDiffAt
have h2 : ContDiffAt ℝ n (fun y ↦ |t| * ‖y‖) x := h.const_smul |t|
conv at h2 => enter [4]; rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]
convert h2.comp (t • x) h1 using 1
ext y
simp only [Function.comp_apply]
rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
