lean_workbook_plus_8232

Proved

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

Show that for nonnegative x, y, and z one has the bound\n $x^2y^3$ + $x^2z^3$ + $y^2x^3$ + $y^2z^3$ + $z^2x^3$ + $z^2y^3$ \n≤ $xy^4$ + $xz^4$ + $yx^4$ + $yz^4$ + $zx^4$ + $zy^4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8232 (x y z : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : x^2*y^3 + x^2*z^3 + y^2*x^3 + y^2*z^3 + z^2*x^3 + z^2*y^3 ≤ x*y^4 + x*z^4 + y*x^4 + y*z^4 + z*x^4 + z*y^4   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph