A rational inequality involving three pairwise sums
ProvedWorkbookSource.base_127lean-workbooksource-checked
Show that we have: .
made by Caragea C.
Here is what I have found:
and so we have that: and we multiply by and we have our ineq!
do you have other solutions? cheers!
Source: InternLM Lean-Workbook, record lean_workbook_127 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_127 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x + y) * (y + z) * (z + x) / (4 * x * y * z) ≥ (x + z) / (y + z) + (y + z) / (x + z) := by sorry
Source