A product of shifted ratios bounded by a normalized cubic sum
ProvedWorkbookSource.base_20200lean-workbooksource-checked
Let Prove that {{(\frac{a}{b+c}}+\frac 1{2})(\frac{b}{c+a}}+\frac 1{2})(\frac{c}{a+b}}+\frac 1{2})\le \frac{7}{8}+\frac{a^3+b^3+c^3}{24abc}.
Source: InternLM Lean-Workbook, record lean_workbook_20200 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_20200 (a b c : ℝ) (ha : a > 0) (hb : b > 0) (hc : c > 0) : (a / (b + c) + 1 / 2) * (b / (c + a) + 1 / 2) * (c / (a + b) + 1 / 2) ≤ 7 / 8 + (a^3 + b^3 + c^3) / (24 * a * b * c) := by sorry
Source