lean_workbook_plus_74106

Proved

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

Show that the simplified inequality $\sqrt{(a^2 + b^2)(4b^2 + a^2)} \geq 3ab$ follows from the Cauchy-Schwarz inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74106 (a b : ℝ) : Real.sqrt ((a^2 + b^2) * (4 * b^2 + a^2)) ≥ 3 * a * b   :=  by sorry

Source