differentiableAt_norm_smul — Mathlib

English

There is no differentiability of the norm at the origin in a nontrivial space.

Русский

В ненулевом нормированном пространстве норма в точке ноль не дифференцируема.

LaTeX

$$$\\neg \\text{DifferentiableAt}_{\\mathbb{R}}(\\|\\cdot\\|)(0)$$$

Lean4

theorem differentiableAt_norm_smul (ht : t ≠ 0) : DifferentiableAt ℝ (‖·‖) x ↔ DifferentiableAt ℝ (‖·‖) (t • x)
    where
  mp hd := (hd.hasFDerivAt.hasFDerivAt_norm_smul ht).differentiableAt
  mpr
    hd := by
    convert (hd.hasFDerivAt.hasFDerivAt_norm_smul (inv_ne_zero ht)).differentiableAt
    rw [smul_smul, inv_mul_cancel₀ ht, one_smul]

Похожие утверждения