← Formalpedia
lean_workbook_plus_81130 Proved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Prove that for positive reals x, y, z, the following inequality holds:\n\n9 4 − ( x x + y + y y + z + z z + x ) ( y x + y + z y + z + x z + x ) = 1 4 ( y − z ) 2 ( x − z ) 2 ( x − y ) 2 ( x + y ) 2 ( y + z ) 2 ( z + x ) 2 ≥ 0 \frac{9}{4}- \left( {\frac {x}{x+y}}+{\frac {y}{y+z}}+{\frac {z}{z+x}} \right) \left( {\frac {y}{x+y}}+{\frac {z}{y+z}}+{\frac {x}{z+x}} \right) =\frac{1}{4}\,{\frac { \left( y-z \right) ^{2} \left( x-z \right) ^{2} \left( x-y \right) ^{2}}{ \left( x+y \right) ^{2} \left( y+z \right) ^{2} \left( z+x \right) ^{2}}}\geq 0 4 9 − ( x + y x + y + z y + z + x z ) ( x + y y + y + z z + z + x x ) = 4 1 ( x + y ) 2 ( y + z ) 2 ( z + x ) 2 ( y − z ) 2 ( x − z ) 2 ( x − y ) 2 ≥ 0
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_81130 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (9 / 4 - (x / (x + y) + y / (y + z) + z / (z + x)) * (y / (x + y) + z / (y + z) + x / (z + x))) = (1 / 4) * ((y - z) ^ 2 * (x - z) ^ 2 * (x - y) ^ 2) / ((x + y) ^ 2 * (y + z) ^ 2 * (z + x) ^ 2) := by sorry View graph