lean_workbook_plus_67214

Proved

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

prove that \n $\frac{x^2}{a}+\frac{y^2}{b}\geq\frac{(x+y)^2}{a+b}$ \n \n (where $a,b,x,y$ are positive Real no.)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67214 (a b x y : ℝ) (hx: a > 0 ∧ b > 0 ∧ x > 0 ∧ y > 0) : (x ^ 2 / a + y ^ 2 / b) ≥ (x + y) ^ 2 / (a + b)   :=  by sorry

Source