Prove2Me

lean_workbook_plus_44927

Proved

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

By Cauchy-Schwarz's inequality, we have \n

(a2b+b2c+c2a)2≤(a2+b2+c2)(a2b2+b2c2+c2a2).(a^2b+b^2c+c^2a)^2 \le (a^2+b^2+c^2)(a^2b^2+b^2c^2+c^2a^2).

The rest is to prove that 3(a2b2+b2c2+c2a2)≤(a2+b2+c2)2,3(a^2b^2+b^2c^2+c^2a^2) \le (a^2+b^2+c^2)^2, which is true because \n

RHS−LHS=12[(a2−b2)2+(b2−c2)2+(c2−a2)2]≥0.RHS-LHS = \frac{1}{2}[(a^2-b^2)^2+(b^2-c^2)^2+(c^2-a^2)^2] \ge 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44927  (a b c : ℝ) :
  (a^2 * b + b^2 * c + c^2 * a)^2 ≤ (a^2 + b^2 + c^2) * (a^2 * b^2 + b^2 * c^2 + c^2 * a^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph