Three fourth powers of pairwise sums bound the fourth-power sum

Proved

WorkbookSource.base_24200

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

lean-workbooksource-checked

If a, b, c are real number then: $(a+b)^4+(b+c)^4+(c+a)^4 \ge \frac{4(a^4+b^4+c^4)}{7}$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_24200 (a b c: ℝ) : (a + b) ^ 4 + (b + c) ^ 4 + (c + a) ^ 4 ≥ (4 / 7) * (a ^ 4 + b ^ 4 + c ^ 4)  :=  by sorry

Source