A cyclic mixed quadratic ratio sum is at most one
ProvedWorkbookSource.base_35726lean-workbooksource-checked
Prove that if then,
Source: InternLM Lean-Workbook, record lean_workbook_35726 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_35726 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x * y) / (x ^ 2 + x * y + y * z) + (y * z) / (y ^ 2 + y * z + z * x) + (z * x) / (z ^ 2 + z * x + x * y) ≤ 1 := by sorry
Source