Prove2Me

lean_workbook_plus_18801

Proved

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

Given q2≥pr,r2≥pq,{p,q,r}∈R+q^2\ge pr, r^2 \ge pq, \{p,q,r\}\in R^{+}, prove that qr≥p\sqrt{qr}\ge p.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18801 (p q r : ℝ) (h : {p,q,r} ⊆ Set.Ioi 0) (hpqr : p * q * r = 1) (hq2 : q^2 ≥ p * r) (hr2 : r^2 ≥ p * q) : √(q * r) ≥ p   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph