not_DifferentiableAt_log_mul_zero

English

The function x ↦ x log x is not differentiable at x = 0.

Русский

Функция f(x) = x log x не дифференцируема в точке x = 0.

LaTeX

$$$\neg \text{DifferentiableAt} \left( x \mapsto x \log x \right)\, 0$$$

Lean4

/-- At `x=0`, `(fun x ↦ x * log x)` is not differentiable
(but note that it is continuous, see `continuous_mul_log`). -/
theorem not_DifferentiableAt_log_mul_zero : ¬DifferentiableAt ℝ (fun x ↦ x * log x) 0 := fun h ↦
  (not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi (fun x : ℝ ↦ x * log x) (a := 0))
    tendsto_deriv_mul_log_nhdsWithin_zero (h.differentiableWithinAt (s := Set.Ioi 0))

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