lean_workbook_plus_2428

Proved

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

Let $a$ and $b$ be two positive real numbers with $a \le 2b \le 3a.$ Prove that $a^2+ b^2\le \frac{5}{2} ab$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2428 (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a ≤ 2 * b) (h : 2 * b ≤ 3 * a) : a^2 + b^2 ≤ 5 / 2 * a * b   :=  by sorry

Source