Prove2Me

lean_workbook_plus_76588

Proved

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

Due to the symmetry, we may assume WLOG that a≥b≥ca\ge b \ge c . Hence, a+b≥c+a≥b+ca+b \ge c+a \ge b+c and aba+b≥cac+a+bcb+c\frac{ab}{a+b} \ge \frac{ca}{c+a} + \frac{bc}{b+c} . By Chebychev's inequality, we have

(∑cycaba+b)(∑cyca+b)≤3∑cycab\left(\sum_{cyc}\frac{ab}{a+b}\right)\left(\sum_{cyc} a+b\right) \le 3\sum_{cyc} ab

or

∑cycaba+b≤3(ab+bc+ca)2(a+b+c)\sum_{cyc}\frac{ab}{a+b} \le \frac{3(ab+bc+ca)}{2(a+b+c)}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76588  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a ≥ b ∧ b ≥ c) :
  (a * b / (a + b) + b * c / (b + c) + c * a / (c + a)) ≤ (3 * (a * b + b * c + c * a)) / (2 * (a + b + c))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph