A quadratic pair-sum ratio bounds a squared square-root sum
ProvedWorkbookSource.base_5580lean-workbooksource-checked
If , , are positive reals, prove that .
Source: InternLM Lean-Workbook, record lean_workbook_5580 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_5580 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (y + z) ^ 2 / (y + z + 2 * x) + (z + x) ^ 2 / (z + x + 2 * y) + (x + y) ^ 2 / (x + y + 2 * z) ≥ (Real.sqrt x + Real.sqrt y + Real.sqrt z) ^ 2 / 3 := by sorry
Source