A weighted cyclic linear ratio sum is at least nine quarters
ProvedWorkbookSource.base_52965lean-workbooksource-checked
Let and are positive numbers. Prove that: $ \frac {2a + b}{a + c + 2b} + \frac {2b + c}{b + a + 2c} + \frac {2c + a}{c + b + 2a}\geq\frac {9}{4} There is a nice proof.
Source: InternLM Lean-Workbook, record lean_workbook_52965 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_52965 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (2 * a + b) / (a + c + 2 * b) + (2 * b + c) / (b + a + 2 * c) + (2 * c + a) / (c + b + 2 * a) ≥ 9 / 4 := by sorry
Source