Three quadratic forms bound a cubed pairwise sum and squared differences
ProvedWorkbookSource.base_1815lean-workbooksource-checked
The following inequality is also true. For all reals , and prove that: $ (a^2 + ab + b^2)(b^2 + bc + c^2)(c^2 + ca + a^2)\ge (ab + bc + ca)^3+\frac{1}{6}(a-b)^2(a-c)^2(b-c)^2
Source: InternLM Lean-Workbook, record lean_workbook_1815 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_1815 (a b c : ℝ) : (a^2 + a * b + b^2) * (b^2 + b * c + c^2) * (c^2 + c * a + a^2) ≥ (a * b + b * c + c * a)^3 + (1/6) * (a - b)^2 * (a - c)^2 * (b - c)^2 := by sorry
Source