lean_workbook_plus_13590

Proved

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

One method: Use the inequality $xy \leq \frac{(x+y)^2}{4}$ and express $x^ny^n(x^2+y^2)$ as $x^ny^n((x+y)^2-2xy)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13590 (x y n : ℕ) :
  x^n * y^n * (x^2 + y^2) ≤ x^n * y^n * ((x + y)^2 - 2 * x * y)   :=  by sorry

Source