A symmetric product inequality

Proved

WorkbookSource.problem_26366

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let $x, y\in R, a,b>0$ . Prove that

(ax+by)(bx+ay) \ge (a+b)^2xy.

Source: InternLM Lean-Workbook, record lean_workbook_26366 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.

Preamble

import Mathlib
open Real

Formal statement

theorem WorkbookSource.problem_26366 (x y a b : ℝ) (ha : 0 < a) (hb : 0 < b) : (a * x + b * y) * (b * x + a * y) ≥ (a + b) ^ 2 * x * y  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_26366; Apache-2.0

View graph