A cyclic cubic-product inequality

Proved

WorkbookSource.base_3844

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

lean-workbooksource-checked

The inequality $3(x^3y+y^3z+z^3x)\leq(x+y+z)(x^3+y^3+z^3)$ can be proved for any real $x,y,z$ using the same method as above.

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_3844 (x y z : ℝ) : 3 * (x^3 * y + y^3 * z + z^3 * x) ≤ (x + y + z) * (x^3 + y^3 + z^3)  :=  by sorry

Source