A product and linear bound on an ellipse

Proved

WorkbookSource.plus_8085

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

lean-workbooksource-checked

It is known that $x$ and $y$ are reals satisfying $x^2 + 2xy + 3y^2 = 4$ . Prove that $xy - 2x + 4y \leq \frac{20}{3}$ .

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_8085 (x y : ℝ) (h : x ^ 2 + 2 * x * y + 3 * y ^ 2 = 4) : x * y - 2 * x + 4 * y ≤ 20 / 3   :=  by sorry

Source