lean_workbook_plus_20326

Proved

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

Prove that $0\le x(1-x)\le\frac14$ for all $x\in [0,1]$ using the Arithmetic Mean-Geometric Mean (AM-GM) inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20326 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ 1) :
  0 ≤ x * (1 - x) ∧ x * (1 - x) ≤ 1 / 4   :=  by sorry

Source