A total sum bounds a product times squared reciprocals
ProvedWorkbookSource.base_15137lean-workbooksource-checked
Prove that for all positive real numbers , the following inequality holds: x + y + z \geq 4xyz \left(\frac{1}{(x+y)^2} + \frac{1}{(x+z)^2} + \frac{1}{(y+z)^2}\right)
Source: InternLM Lean-Workbook, record lean_workbook_15137 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_15137 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : x + y + z ≥ 4*x*y*z * (1/((x+y)^2) + 1/((x+z)^2) + 1/((y+z)^2)) := by sorry
Source