by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Prove or disprove the following inequalities for positive numbers a, b, and c:\n\ni) a2b2(a−b)4+b2c2(b−c)4+c2a2(c−a)4≥21⋅[ab(a−b)2+bc(b−c)2+ca(c−a)2]2.\nii) a2b2(a−b)4+b2c2(b−c)4+c2a2(c−a)4≥21⋅[ab(a−b)2+bc(b−c)2+ca(c−a)2].
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_32437 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (a - b) ^ 4 / (a ^ 2 * b ^ 2) + (b - c) ^ 4 / (b ^ 2 * c ^ 2) + (c - a) ^ 4 / (c ^ 2 * a ^ 2) ≥ 1 / 2 * ((a - b) ^ 2 / (a * b) + (b - c) ^ 2 / (b * c) + (c - a) ^ 2 / (c * a)) ^ 2 := by sorry