lean_workbook_plus_35004

Proved

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

Note that for $a,b,c>0$ the sequences $A:=(a,b,c)$ and $B:=(a^2,b^2,c^2)$ . Thus for the rearrangement $C:=(c^2,a^2,b^2)$ of $B$ we have by the REARRANGEMENT inequality: $A \cdot B \geq A \cdot C \Longleftrightarrow aa^2+bb^2+cc^2\geq ac^2+ba^2+cb^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35004 {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a * a^2 + b * b^2 + c * c^2 ≥ a * c^2 + b * a^2 + c * b^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph