lean_workbook_plus_16416

Proved

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

For positive real numbers $p,q,r$ with $p+q+r=1$ , prove $p^2+q^2+r^2\ge \frac{1}{3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16416 (p q r : ℝ) (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (hpq: p + q + r = 1) : p^2 + q^2 + r^2 ≥ 1 / 3   :=  by sorry

Source