← Formalpedia
lean_workbook_plus_7624 Disproved by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
We have : \n\n
( x y + y z + z x ) 2 − 3 2 x y z ( x + y + z ) ≤ 1 2 ( x 2 + y 2 + z 2 ) ( x y + y z + z x ) ⇔ ∑ x y ( x − y ) 2 ≥ 0 (xy+yz+zx)^2-\frac{3}{2}xyz(x+y+z)\leq \frac{1}{2}(x^2+y^2+z^2)(xy+yz+zx) \Leftrightarrow \sum xy(x-y)^2 \ge 0 ( x y + y z + z x ) 2 − 2 3 x y z ( x + y + z ) ≤ 2 1 ( x 2 + y 2 + z 2 ) ( x y + y z + z x ) ⇔ ∑ x y ( x − y ) 2 ≥ 0 \n\nL H S = ( x y + y z + z x ) 2 − 3 2 x y z ( x + y + z ) ≤ 1 4 ( x 2 + y 2 + z 2 ) ( 2 x y + 2 y z + 2 z x ) LHS=(xy+yz+zx)^2-\frac{3}{2}xyz(x+y+z)\leq \frac{1}{4}(x^2+y^2+z^2)(2xy+2yz+2zx) L H S = ( x y + y z + z x ) 2 − 2 3 x y z ( x + y + z ) ≤ 4 1 ( x 2 + y 2 + z 2 ) ( 2 x y + 2 y z + 2 z x ) L H S ≤ 1 16 ( x + y + z ) 4 LHS\leq \frac{1}{16}(x+y+z)^4 L H S ≤ 16 1 ( x + y + z ) 4
Preamble
import Mathlib.Analysis.Complex.Basic Formal statement
theorem lean_workbook_plus_7624 : ∀ x y z : ℝ, (x * y + y * z + z * x) ^ 2 - 3 / 2 * x * y * z * (x + y + z) ≤ 1 / 2 * (x ^ 2 + y ^ 2 + z ^ 2) * (x * y + y * z + z * x) := by sorry View graph