lean_workbook_plus_14997

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $1/2\,{\frac { \left( x+y \right) ^{2}}{xy}}+2-8\,{\frac {xy}{ \left( x+y \right) ^{2}}}\leq {\frac {x}{y}}+{\frac {y}{x}}$ given $x,y>0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14997 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : 1 / 2 * (x + y) ^ 2 / (x * y) + 2 - 8 * (x * y) / (x + y) ^ 2 ≤ x / y + y / x   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph