deriv_negMulLog

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

English

If x ≠ 0, then the derivative of -x log x is - log x − 1.

Русский

Если x ≠ 0, то производная от −x log x равна − log x − 1.

LaTeX

$$$ \frac{d}{dx}\bigl(-x\log x\bigr) = -\log x - 1 \quad (x \neq 0). $$$

Lean4

theorem deriv_negMulLog {x : ℝ} (hx : x ≠ 0) : deriv negMulLog x = -log x - 1 :=
  by
  rw [negMulLog_eq_neg, deriv.fun_neg, deriv_mul_log hx]
  ring

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

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

Разделы

Аффилиация

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