lean_workbook_plus_49431

Proved

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

If $x, y \in \mathbb{R}$ and $y > 0$ , prove that $4(x^2 + y^2)^2 \ge y^2(7x^2 + 3xy + 3y^2)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49431 (x y : ℝ) (hy : 0 < y) : 4 * (x ^ 2 + y ^ 2) ^ 2 ≥ y ^ 2 * (7 * x ^ 2 + 3 * x * y + 3 * y ^ 2)   :=  by sorry

Source