A quartic symmetric expression bounds a difference product
ProvedWorkbookSource.plus_29287lean-workbooksource-checked
Let . Prove that $ \sum_{cyc} a^4 + 3\sum_{cyc} a^2b^2 + 3\ge 2\sum_{cyc} ab(a^2 + b^2 ) + 6(a - b)(a - c)(b - c)
Source: InternLM Lean-Workbook, record lean_workbook_plus_29287 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_29287 (a b c : ℝ) (ha : a + b + c = 3) : a^4 + b^4 + c^4 + 3 * (a^2 * b^2 + b^2 * c^2 + c^2 * a^2) + 3 ≥ 2 * (a * b * (a^2 + b^2) + b * c * (b^2 + c^2) + c * a * (c^2 + a^2)) + 6 * (a - b) * (a - c) * (b - c) := by sorry
Source