Prove2Me

lean_workbook_plus_42270

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that 22a⋅aa⋅bb<(a+b)a+b(1)⟺2aln⁡2+aln⁡a+bln⁡b−(a+b)ln⁡(a+b)<0(2)2^{2a}\cdot a^a\cdot b^b<(a+b)^{a+b}\quad(1)\Longleftrightarrow 2a\ln 2+a\ln a+b\ln b-(a+b)\ln(a+b)<0\quad(2).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_42270 (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : (2:ℝ) ^ (2 * a) * a ^ a * b ^ b < (a + b) ^ (a + b) ↔ 2 * a * Real.log 2 + a * Real.log a + b * Real.log b - (a + b) * Real.log (a + b) < 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph