Prove2Me

A cyclic quadratic-product ratio upper bound

Proved
WorkbookSource.base_12714

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

lean-workbooksource-checked

Let x,y,z>0x,y,z>0 .Prove that: x2(y+z)x2+2yz+y2(z+x)y2+2zx+z2(x+y)z2+2xy≤2(x2+y2+z2)x+y+z\frac{x^2(y+z)}{x^2+2yz}+\frac{y^2(z+x)}{y^2+2zx}+\frac{z^2(x+y)}{z^2+2xy}\leq\frac{2(x^2+y^2+z^2)}{x+y+z} .

Source: InternLM Lean-Workbook, record lean_workbook_12714 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_12714 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x^2 * (y + z) / (x^2 + 2 * y * z) + y^2 * (z + x) / (y^2 + 2 * z * x) + z^2 * (x + y) / (z^2 + 2 * x * y)) ≤ (2 * (x^2 + y^2 + z^2)) / (x + y + z)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_12714; Apache-2.0

View graph