A cyclic cubic ratio sum bounds eight sevenths of the total
ProvedWorkbookSource.plus_49894lean-workbooksource-checked
Show that if a,b,c are positive, then follows directly from:
Source: InternLM Lean-Workbook, record lean_workbook_plus_49894 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_49894 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (a + b) ^ 3 / (3 * a ^ 2 + 3 * a * b + b ^ 2) + (b + c) ^ 3 / (3 * b ^ 2 + 3 * b * c + c ^ 2) + (c + a) ^ 3 / (3 * c ^ 2 + 3 * c * a + a ^ 2) ≥ 8 / 7 * (a + b + c) := by sorry
Source