English
If t ≠ 0 and f is differentiableAt with respect to the norm, then the derivative of the norm at t x is t times the derivative at x adjusted by the sign of t; explicitly, D‖·‖(t x) = sign(t) D‖·‖(x).
Русский
Если t ≠ 0 и функция нормы дифференцируема, то производная нормы в точке t x равна знаку t, умноженному на производную нормы в x: D‖·‖(t x) = sign(t) D‖·‖(x).
LaTeX
$$$D\\|\\cdot\\|_{t x} = (\\operatorname{sign} t)\\, D\\|\\cdot\\|_{x} \\quad (t \\neq 0)$$$
Lean4
theorem hasStrictFDerivAt_norm_smul (ht : t ≠ 0) (h : HasStrictFDerivAt (‖·‖) f x) :
HasStrictFDerivAt (‖·‖) ((SignType.sign t : ℝ) • f) (t • x) :=
by
have h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x) :=
hasStrictFDerivAt_id (t • x) |>.const_smul t⁻¹
have h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x := h.const_smul |t|
conv at h2 => enter [3]; rw [← one_smul ℝ x, ← inv_mul_cancel₀ ht, mul_smul]
convert h2.comp (t • x) h1 with y
· rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
ext y
simp only [coe_smul', Pi.smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply, comp_id]
rw [eq_inv_mul_iff_mul_eq₀ ht, ← mul_assoc, self_mul_sign]
