lean_workbook_plus_7207

Proved

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

Let $x,y \in R$ and $x\not= 0, y \not= 0$ . Prove that: $\frac{{4x^2 y^2 }}{{(x^2 + y^2 )^2}} + \frac{{x^2 }}{{y^2 }} + \frac{{y^2 }}{{x^2 }} \ge 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7207 (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) : (4 * x ^ 2 * y ^ 2) / (x ^ 2 + y ^ 2) ^ 2 + x ^ 2 / y ^ 2 + y ^ 2 / x ^ 2 >= 3   :=  by sorry

Source

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

View graph