lean_workbook_plus_2269

Proved

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

For any two positive numbers u and v, prove that $\left(u+v\right)^2 \geq 4uv$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2269 (u v : ℝ) (hu : u > 0) (hv : v > 0) : (u + v) ^ 2 ≥ 4 * u * v   :=  by sorry

Source