log_mul_self_monotoneOn — Mathlib

English

The function f(t) = t log t is increasing on [1, ∞). In particular, if 1 ≤ x ≤ y, then x log x ≤ y log y.

Русский

Функция f(t) = t log t возрастает на интервале [1, ∞). В частности, при 1 ≤ x ≤ y выполняется x log x ≤ y log y.

LaTeX

$$$\forall x,y \in \mathbb{R},\ 1 \le x \le y \Rightarrow x \log x \le y \log y$$$

Lean4

theorem log_mul_self_monotoneOn : MonotoneOn (fun x : ℝ => log x * x) {x | 1 ≤ x} := by
  -- TODO: can be strengthened to exp (-1) ≤ x

  simp only [MonotoneOn, mem_setOf_eq]
  intro x hex y hey hxy
  have y_pos : 0 < y := lt_of_lt_of_le zero_lt_one hey
  gcongr
  rwa [le_log_iff_exp_le y_pos, Real.exp_zero]

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