deriv_mul_log_zero

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

URI: https://scilib.ai/kg/mathlib#Real.deriv_mul_log_zero

← MathLib Explorer

English

The derivative at 0 of f(x) = x log x is 0 (junk value).

Русский

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

LaTeX

$$$\dfrac{d}{dx}\bigl(x \log x\bigr)\Big|_{x=0} = 0$$$

Lean4

/-- Not differentiable, hence `deriv` has junk value zero. -/
theorem deriv_mul_log_zero : deriv (fun x ↦ x * log x) 0 = 0 :=
  deriv_zero_of_not_differentiableAt not_DifferentiableAt_log_mul_zero

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru