lean_workbook_plus_22326
Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Apply Cauchy-schwarz inequality on (ax,a) and similarly, y,b instead of x,a \n (ax2+by2)(a+b)≥(x+y)2⟹ax2+by2≥a+b(x+y)2
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22326 {x y : ℝ} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : (x ^ 2 / a + y ^ 2 / b) * (a + b) ≥ (x + y) ^ 2 := by sorryView graph