lean_workbook_plus_12137

Proved

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

We can also write $M(x,y)=(|x|y^2-x^2|y|)^2+(2|xy|+1)(|xy|-1)^2\ge 0,$ with equality when $|x|=|y|=1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12137 (x y : ℝ) : (abs x * y ^ 2 - x ^ 2 * abs y) ^ 2 + (2 * abs (x * y) + 1) * (abs (x * y) - 1) ^ 2 ≥ 0   :=  by sorry

Source