A weighted four-variable pair-sum ratio is at least twelve
ProvedWorkbookSource.base_7880lean-workbooksource-checked
Prove that for positive real numbers a, b, c, and d, the following inequality holds: $\frac{c+d+4a}{a+b}+\frac{d+a+4b}{b+c}+\frac{a+b+4c}{c+d}+\frac{b+c+4d}{d+a} \geq 12$
Source: InternLM Lean-Workbook, record lean_workbook_7880 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_7880 (a b c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) : (c + d + 4 * a) / (a + b) + (d + a + 4 * b) / (b + c) + (a + b + 4 * c) / (c + d) + (b + c + 4 * d) / (d + a) ≥ 12 := by sorry
Source