← Formalpedia
lean_workbook_plus_6040 Proved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Let ( a ; b ; c ) = ( 2 x 2 y z ; 2 y 2 z x ; 2 z 2 x y ) (a;b;c)=(\frac{2x^2}{yz};\frac{2y^2}{zx};\frac{2z^2}{xy}) ( a ; b ; c ) = ( y z 2 x 2 ; z x 2 y 2 ; x y 2 z 2 )
4 y 2 z 2 x 2 ( x + y + z ) 2 ( x 2 − x y − z x + y 2 − y z + z 2 ) 2 ( 2 x 2 + y z ) 2 ( z x + 2 y 2 ) 2 ( x y + 2 z 2 ) 2 ≧ 0 4\,{\frac {{y}^{2}{z}^{2}{x}^{2} \left( x+y+z \right) ^{2} \left( {x}^{2}-xy-zx+{y}^{2}-yz+{z}^{2} \right) ^{2}}{ \left( 2\,{x}^{2}+yz \right) ^{2} \left( zx+2\,{y}^{2} \right) ^{2} \left( xy+2\,{z}^{2} \right) ^{2}}} \geqq 0 4 ( 2 x 2 + y z ) 2 ( z x + 2 y 2 ) 2 ( x y + 2 z 2 ) 2 y 2 z 2 x 2 ( x + y + z ) 2 ( x 2 − x y − z x + y 2 − y z + z 2 ) 2 ≧ 0 Done.
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_6040 : ∀ x y z : ℝ, (4 * (y^2 * z^2 * x^2 * (x + y + z)^2 * (x^2 - x * y - x * z + y^2 - y * z + z^2)^2) / ((2 * x^2 + y * z)^2 * (z * x + 2 * y^2)^2 * (x * y + 2 * z^2)^2)) ≥ 0 := by sorry View graph