A cyclic sixth-power inequality with mixed terms
ProvedWorkbookSource.plus_62922lean-workbooksource-checked
prove that
Source: InternLM Lean-Workbook, record lean_workbook_plus_62922 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_62922 (x y z : ℝ) : (4 * x ^ 6 + x ^ 4 * y ^ 2 + x ^ 4 * z ^ 2 - 6 * x ^ 3 * y ^ 3) + (4 * y ^ 6 + y ^ 4 * z ^ 2 + y ^ 4 * x ^ 2 - 6 * y ^ 3 * z ^ 3) + (4 * z ^ 6 + z ^ 4 * x ^ 2 + z ^ 4 * y ^ 2 - 6 * z ^ 3 * x ^ 3) ≥ 0 := by sorry
Source