Prove2Me

lean_workbook_plus_8986

Proved

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

prove that (a+bp)2+(b+cp)2+(c+ap)2≥(1+p)22(a2+b2+c2+ab+bc+ca)(a+bp)^2 + (b+cp)^2 + (c+ap)^2\ge \frac{(1+p)^2}{2}(a^2+b^2+c^2+ab+bc+ca) for a,b,c,p≥0a,b,c,p\ge 0

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

View graph