lean_workbook_plus_54020

Proved

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

By Titu's lemma,\n $\frac{a^2}{x}+\frac{b^2}{y}+\frac{c^2}{z}\ge \frac{(a+b+c)^2}{x+y+z}$ .......(2)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54020 (x y z a b c : ℝ) (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