lean_workbook_plus_80054

Proved

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

Using the Cauchy inequality, show that if $u+2v>4$ , then $u^2+4v^2>8$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80054 (u v : ℝ) (h : u + 2 * v > 4) : u ^ 2 + 4 * v ^ 2 > 8   :=  by sorry

Source