English
For any x and t, the derivative of the norm at t x satisfies f'(t x) = sign(t) f'(x). If E is trivial, the statement trivializes.
Русский
Для любых x и t производная функции нормы удовлетворяет f'(t x) = sign(t) f'(x).
LaTeX
$$$fderiv_{\\mathbb{R}}(\\|\\cdot\\|)\\bigl(t x\\bigr) = (\\operatorname{sign} t) \\cdot fderiv_{\\mathbb{R}}(\\|\\cdot\\|)\\bigl(x\\bigr)$$$
Lean4
theorem fderiv_norm_smul : fderiv ℝ (‖·‖) (t • x) = (SignType.sign t : ℝ) • (fderiv ℝ (‖·‖) x) :=
by
cases subsingleton_or_nontrivial E
· simp_rw [(hasFDerivAt_of_subsingleton _ _).fderiv, smul_zero]
· by_cases hd : DifferentiableAt ℝ (‖·‖) x
· obtain rfl | ht := eq_or_ne t 0
· simp only [zero_smul, _root_.sign_zero, SignType.coe_zero]
exact fderiv_zero_of_not_differentiableAt <| not_differentiableAt_norm_zero E
· rw [(hd.hasFDerivAt.hasFDerivAt_norm_smul ht).fderiv]
· rw [fderiv_zero_of_not_differentiableAt hd, fderiv_zero_of_not_differentiableAt]
· simp
· exact mt DifferentiableAt.differentiableAt_norm_of_smul hd
