A cyclic quartic inequality with a squared pairwise-sum correction
ProvedWorkbookSource.base_22439lean-workbooksource-checked
Given . Show that: a^4+b^4+c^4+\frac{(ab+bc+ca)^2}{3} \geq 2(a^3b+b^3c+c^3a)
Source: InternLM Lean-Workbook, record lean_workbook_22439 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_22439 (a b c : ℝ) : a ^ 4 + b ^ 4 + c ^ 4 + (a * b + b * c + c * a) ^ 2 / 3 ≥ 2 * (a ^ 3 * b + b ^ 3 * c + c ^ 3 * a) := by sorry
Source