English
For t ≠ 0, ContDiffAt of the norm at x is equivalent to ContDiffAt at t x.
Русский
Для t ≠ 0 ContDiffAt нормы в x эквивалентна ContDiffAt в t x.
LaTeX
$$$\\text{contDiffAt_norm_smul_iff} (ht: t \\neq 0) : \\; CDiffAt(\\|\\cdot\\|) x \\iff CDiffAt(\\|\\cdot\\|) (t x)$$$
Lean4
theorem fderiv_norm_self {x : E} (h : DifferentiableAt ℝ (‖·‖) x) : fderiv ℝ (‖·‖) x x = ‖x‖ :=
by
rw [← h.lineDeriv_eq_fderiv, lineDeriv]
have this (t : ℝ) : ‖x + t • x‖ = |1 + t| * ‖x‖ := by rw [← norm_eq_abs, ← norm_smul, add_smul, one_smul]
simp_rw [this]
rw [deriv_mul_const]
· conv_lhs => enter [1, 1]; change _root_.abs ∘ (fun t ↦ 1 + t)
rw [deriv_comp, deriv_abs, deriv_const_add]
· simp
· exact differentiableAt_abs (by simp)
· exact differentiableAt_id.const_add _
· exact (differentiableAt_abs (by simp)).comp _ (differentiableAt_id.const_add _)
