Prove2Me

A fourth-degree inequality involving cyclic differences

Proved
WorkbookSource.base_39574

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let aa , bb , cc and dd be non-negative numbers. Prove that:

(a2+b2+c2+d2)2≥4(a−b)(b−c)(c−d)(d−a)+16abcd.(a^2+b^2+c^2+d^2)^2\geq4(a-b)(b-c)(c-d)(d-a)+16abcd.

Let (a−b)(b−c)(c−d)(d−a)=A≥0,  abcd=B(a-b)(b-c)(c-d)(d-a)=A\ge 0, \ \ abcd=B .

a2+b2+c2+d2=12((a−b)2+(b−c)2+(c−d)2+(d−a)2)+ab+bc+cd+da≥2A+4Ba^2+b^2+c^2+d^2=\frac{1}{2}((a-b)^2+(b-c)^2+(c-d)^2+(d-a)^2)+ab+bc+cd+da\ge 2\sqrt{A}+4\sqrt{B}

It remains to prove

(2A+4B)2≥4A+16B(2\sqrt{A}+4\sqrt{B})^2\ge 4A+16B

which is obvious.

Source: InternLM Lean-Workbook, record lean_workbook_39574 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_39574  (a b c d : ℝ)
  (h₀ : 0 ≤ a)
  (h₁ : 0 ≤ b)
  (h₂ : 0 ≤ c)
  (h₃ : 0 ≤ d) :
  (a^2 + b^2 + c^2 + d^2)^2 ≥ 4 * (a - b) * (b - c) * (c - d) * (d - a) + 16 * a * b * c * d  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_39574; Apache-2.0

View graph