Prove2Me

lean_workbook_plus_14201

Proved

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

f(a)+f(b)2+f(b)+f(c)2+f(c)+f(a)2≥f(a+b2)+f(b+c2)+f(c+a2)⇒1a+1b+1c≥2a+b+2b+c+2c+a\frac{f(a)+f(b)}{2}+\frac{f(b)+f(c)}{2}+\frac{f(c)+f(a)}{2}\geq f(\frac{a+b}{2})+f(\frac{b+c}{2})+f(\frac{c+a}{2})\Rightarrow \frac{1}{a}+\frac{1}{b}+\frac{1}{c}\geq \frac{2}{a+b}+\frac{2}{b+c}+\frac{2}{c+a}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14201 (f : ℝ → ℝ) (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (f a + f b) / 2 + (f b + f c) / 2 + (f c + f a) / 2 ≥ f (a + b) / 2 + f (b + c) / 2 + f (c + a) / 2 → 1 / a + 1 / b + 1 / c ≥ 2 / (a + b) + 2 / (b + c) + 2 / (c + a)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph