mul_log_nonneg

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

English

If x ≥ 1, then 0 ≤ x log x.

Русский

Если x ≥ 1, то 0 ≤ x log x.

LaTeX

$$$1 \le x \Rightarrow 0 \le x \log x$$$

Lean4

theorem mul_log_nonneg {x : ℝ} (hx : 1 ≤ x) : 0 ≤ x * log x :=
  mul_nonneg (zero_le_one.trans hx) (log_nonneg hx)

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

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

Разделы

Аффилиация

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