lean_workbook_plus_32608

Proved

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

Prove the inequality $\frac{a^2}{x}+\frac{b^2}{y}+\frac{c^2}{z}\geq \frac{(a+b+c)^2}{x+y+z}$ using Cauchy-Schwarz inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32608 {a b c x y z : ℝ} (hx : x > 0) (hy : y > 0) (hz : z > 0) : (a^2 / x + b^2 / y + c^2 / z) ≥ (a + b + c)^2 / (x + y + z)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph