Prove2Me

lean_workbook_plus_16739

Proved

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

Follow schur: r≥ p(4q−p2)9→q≤ p3+364p+9 r \ge\ \frac {p(4q - p^2)}{9} \rightarrow q \le\ \frac {p^3 + 36}{4p + 9}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16739 (p q r : ℝ) (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (hpq : p + q + r = 1) (hpqr : p * q * r = 1) (h : r ≥ p * (4 * q - p ^ 2) / 9) : q ≤ p ^ 3 + 36 / (4 * p + 9)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph