strictConvexOn_mul_log — Mathlib

English

The function f(x) = x log x is strictly convex on [0, ∞).

Русский

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

LaTeX

$$$f(x) = x \log x \quad\text{is strictly convex on } [0, \infty).$$$

Lean4

theorem strictConvexOn_mul_log : StrictConvexOn ℝ (Set.Ici (0 : ℝ)) (fun x ↦ x * log x) :=
  by
  refine strictConvexOn_of_deriv2_pos (convex_Ici 0) (continuous_mul_log.continuousOn) ?_
  intro x hx
  simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx
  rw [deriv2_mul_log]
  positivity

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