lean_workbook_plus_50321

Proved

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

Prove for positive a, b, and real x, y, \n

\frac{x^2}{a}+\frac{y^2}{b}\geq\frac{(x+y)^2}{a+b}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50321 (x y a b : ℝ) (ha : 0 < a) (hb : 0 < b) : (x ^ 2 / a + y ^ 2 / b) ≥ (x + y) ^ 2 / (a + b)   :=  by sorry

Source