concaveOn_negMulLog

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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

English

The function f(x) = -x log x is concave on [0, ∞).

Русский

Функция f(x) = -x log x выпукла по красной оси на [0, ∞).

LaTeX

$$ConcaveOn(\mathbb{R}, [0, \infty), x \mapsto -x\log x)$$

Lean4

theorem concaveOn_negMulLog : ConcaveOn ℝ (Set.Ici (0 : ℝ)) negMulLog :=
  strictConcaveOn_negMulLog.concaveOn

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

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

Разделы

Аффилиация

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