A sharp bound with a fixed sum

Proved

WorkbookSource.problem_12814

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalitieslean-workbooksource-checked

If $x,y\ge0$ and $x+y=1$ , then

x^2+y^2+x^2y^2\ge\frac9{16}.

Source: InternLM Lean-Workbook, record lean_workbook_12814 (Apache-2.0). The complete source proposition is preserved.

Preamble

import Mathlib

Formal statement

theorem WorkbookSource.problem_12814 (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x + y = 1) : x^2 + y^2 + x^2 * y^2 ≥ 9 / 16  :=  by sorry

Source