A cyclic rational inequality in two positive variables

Proved

WorkbookSource.base_2154

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Given $a=x^2$ , $b=y^2$ where $x>0$ and $y>0$ , prove that $\dfrac{x^2}{y^2}+\dfrac{y^2}{(x+y)^2}+\dfrac{(x+y)^2}{x^2}\geq\dfrac{10(x^4+y^4+(x+y)^4)}{(x^2+y^2+(x+y)^2)^2}$ .

Source: InternLM Lean-Workbook, record lean_workbook_2154 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_2154 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : (x^2 / y^2 + y^2 / (x + y)^2 + (x + y)^2 / x^2) ≥ (10 * (x^4 + y^4 + (x + y)^4)) / (x^2 + y^2 + (x + y)^2)^2  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_2154; Apache-2.0

View graph