A cyclic quartic inequality with asymmetric coefficients
ProvedWorkbookSource.base_5981lean-workbooksource-checked
Prove that for non-negative real numbers x, y, and z, the following inequality holds:
Source: InternLM Lean-Workbook, record lean_workbook_5981 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_5981 (x y z : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : 49 * (x + y + z) ^ 4 - 475 * (x + y + z) ^ 2 * (x*y + x*z + y*z) - 408 * (x + y + z) * x*y*z + 288 * (x + y + z) * (x ^ 2 * y + y ^ 2 * z + z ^ 2 * x) + 832 * (x*y + x*z + y*z) ^ 2 ≥ 0 := by sorry
Source