lean_workbook_plus_51978

Proved

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

By the AM-GM Inequality, we have \n $\frac{(2a+b)^2}{b}+\frac{81a^2b}{(2a+b)^2} \ge 18a.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51978 (a b : ℝ) (ha : a > 0) (hb : b > 0) : (2 * a + b) ^ 2 / b + 81 * a ^ 2 * b / (2 * a + b) ^ 2 ≥ 18 * a   :=  by sorry

Source