English
In any nontrivial normed space, the norm function x ↦ ∥x∥ is not differentiable at 0 (with respect to the base field, typically Real).
Русский
В ненулевом нормированном пространстве норма ∥x∥ не дифференцируема в нуле.
LaTeX
$$$\\neg \\text{DifferentiableAt}_{\\mathbb{R}}(\\|\\cdot\\|)(0)$$$
Lean4
theorem not_differentiableAt_norm_zero [Nontrivial E] : ¬DifferentiableAt ℝ (‖·‖) (0 : E) :=
by
obtain ⟨x, hx⟩ := NormedSpace.exists_lt_norm ℝ E 0
intro h
have : DifferentiableAt ℝ (fun t : ℝ ↦ ‖t • x‖) 0 := DifferentiableAt.comp _ (by simpa) (by simp)
have : DifferentiableAt ℝ (|·|) (0 : ℝ) :=
by
simp_rw [norm_smul, norm_eq_abs] at this
have aux : abs = fun t ↦ (1 / ‖x‖) * (|t| * ‖x‖) := by field_simp
rw [aux]
exact this.const_mul _
exact not_differentiableAt_abs_zero this
