An eighth-degree inequality involving shifted pairwise sums
ProvedWorkbookSource.plus_26437lean-workbooksource-checked
For positive numbers $ x, y, z $, prove that $ 27(2x + z + y)^4((z + x)^2 + (x + y)^2)^2 \geq 256(2(z + x)^2 + 2(x + y)^2 - (y + z)^2)(z + x)^2(x + y)^2(x + y + z)^2 $.
Source: InternLM Lean-Workbook, record lean_workbook_plus_26437 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_26437 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : 27 * (2 * x + z + y) ^ 4 * ((z + x) ^ 2 + (x + y) ^ 2) ^ 2 ≥ 256 * (2 * (z + x) ^ 2 + 2 * (x + y) ^ 2 - (y + z) ^ 2) * (z + x) ^ 2 * (x + y) ^ 2 * (x + y + z) ^ 2 := by sorry
Source