A bilinear inequality with a circle constraint

Proved

WorkbookSource.base_20583

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

lean-workbooksource-checked

For $a,b\in R$ , and $x,y\in R$ , such that $x^2 + y^2 = 4$ , prove the following inequality $(a + b)^2 - (x + ay)(x + by) + 4\geq0$

Source: InternLM Lean-Workbook, record lean_workbook_20583 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_20583 (a b x y : ℝ) (h : x^2 + y^2 = 4) : (a + b)^2 - (x + a*y)*(x + b*y) + 4 ≥ 0  :=  by sorry

Source