lean_workbook_plus_11641

Proved

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

By $AM-GM$ inequality, we have $a^2+4b^2\ge 2\sqrt{a^2\cdot 4b^2}=4ab\Rightarrow a^2+4b^2-4ab\ge 0.~~~(I)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11641 (a b : ℝ) : a ^ 2 + 4 * b ^ 2 - 4 * a * b ≥ 0   :=  by sorry

Source