lean_workbook_plus_17488

Proved

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

Suppose $u+2v>4$ , use AM-GM inequality to show that $2uv\leq\frac{u^2+4v^2}{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17488 (u v : ℝ) (h : u + 2 * v > 4) : 2 * u * v ≤ (u ^ 2 + 4 * v ^ 2) / 2   :=  by sorry

Source