not_differentiableAt_abs_zero — Mathlib

English

The absolute value function is not differentiable at 0.

Русский

Функция абсолютного значения не дифференцируема в точке 0.

LaTeX

$$$\neg\operatorname{DifferentiableAt} (|\cdot|) (0)$$$

Lean4

theorem not_differentiableAt_abs_zero : ¬DifferentiableAt ℝ (abs : ℝ → ℝ) 0 :=
  by
  intro h
  have h₁ : deriv abs (0 : ℝ) = 1 :=
    (uniqueDiffOn_Ici _ _ Set.left_mem_Ici).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
      (hasDerivWithinAt_id _ _).congr_of_mem (fun _ h ↦ abs_of_nonneg h) Set.left_mem_Ici
  have h₂ : deriv abs (0 : ℝ) = -1 :=
    (uniqueDiffOn_Iic _ _ Set.right_mem_Iic).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
      (hasDerivWithinAt_neg _ _).congr_of_mem (fun _ h ↦ abs_of_nonpos h) Set.right_mem_Iic
  linarith

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