English
For HasFDerivAt of the norm, the derivative under a nonzero scalar multiplication scales by the sign of t; i.e., f'(t x) = sign(t) f'(x).
Русский
Если есть производная нормы в точке t x, то она связана со значением производной в x через знак t.
LaTeX
$$$fderiv_{\\mathbb{R}} \\|\\cdot\\|(t x) = (\\operatorname{sign} t) \\cdot fderiv_{\\mathbb{R}} \\|\\cdot\\|(x)$$$
Lean4
theorem hasFDerivAt_norm_smul (ht : t ≠ 0) (h : HasFDerivAt (‖·‖) f x) :
HasFDerivAt (‖·‖) ((SignType.sign t : ℝ) • f) (t • x) :=
by
have h1 : HasFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x) :=
hasFDerivAt_id (t • x) |>.const_smul t⁻¹
have h2 : HasFDerivAt (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 using 2 with y
· simp only [Function.comp_apply]
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]
