A cyclic shifted linear ratio sum is at least three
ProvedWorkbookSource.base_17256lean-workbooksource-checked
Let ,prove that;
${\frac {2+y+3,x}{2+x+3,y}}+{\frac {2+z+3,y}{2+y+3,z}}+{\frac {2+x+3,z}{2+z+3,x}}\geq 3.
Source: InternLM Lean-Workbook, record lean_workbook_17256 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_17256 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (2 + y + 3 * x) / (2 + x + 3 * y) + (2 + z + 3 * y) / (2 + y + 3 * z) + (2 + x + 3 * z) / (2 + z + 3 * x) ≥ 3 := by sorry
Source