An inequality with two variables in the unit interval

Proved

WorkbookSource.problem_190

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

inequalitieslean-workbooksource-checked

For $x,y\in[0,1]$ , $x+y\le1$ and $z\ge1$ ,

8x^2y^2+z(x+y)^2\ge4xyz.

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

Preamble

import Mathlib

Formal statement

theorem WorkbookSource.problem_190 (x y z : ℝ) (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) (hxy : x + y ≤ 1) (hz : z ≥ 1) : 8 * x ^ 2 * y ^ 2 + z * (x + y) ^ 2 ≥ 4 * x * y * z  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_190; Apache-2.0

View graph