negMulLog_eq_neg

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

English

The function negMulLog equals the negation of x log x, i.e., negMulLog(x) = -(x log x).

Русский

Функция negMulLog равна отрицанию x log x: negMulLog(x) = -(x log x).

LaTeX

$$$\text{negMulLog}(x) = -(x \log x)$$$

Lean4

theorem negMulLog_eq_neg : negMulLog = fun x ↦ -(x * log x) := by simp [negMulLog_def]

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

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

Разделы

Аффилиация

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