lean_workbook_plus_2950
Proved$(a+b+c)^3\geq\frac{9}{4}\cdot ((a+b)^2c+((b+c)^2a+(c+a)^2b) \iff 4(a^3+b^3+c^3)+3(a(b^2+c^2)+b(c^2+a^2)+c(a^2+b^2))\ge 30abc
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2950 (a b c : ℝ) :
(a + b + c) ^ 3 ≥ (9 / 4) * (a * (b + c) ^ 2 + b * (c + a) ^ 2 + c * (a + b) ^ 2) ↔
4 * (a ^ 3 + b ^ 3 + c ^ 3) + 3 * (a * (b ^ 2 + c ^ 2) + b * (c ^ 2 + a ^ 2) + c * (a ^ 2 + b ^ 2)) ≥
30 * a * b * c := by sorrySource