lean_workbook_plus_27379

Proved

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

Let $1\leq a,b\leq 2$ be real numbers. Prove that \n\n $2(a + b)^2\leq 9ab$ \nBecause $(2a-b)(2b-a)\geq0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27379 (a b : ℝ) (ha : 1 ≤ a ∧ a ≤ 2) (hb : 1 ≤ b ∧ b ≤ 2): 2 * (a + b) ^ 2 ≤ 9 * a * b   :=  by sorry

Source