A sixth-power bound for shifted linear products
ProvedWorkbookSource.plus_50631lean-workbooksource-checked
Prove that for positive numbers $ x, y, z $, $ 27(z + 2x + y)^6 \geq 1024(z + x)(x + y)(y + z + x)^3x $.
Source: InternLM Lean-Workbook, record lean_workbook_plus_50631 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_50631 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : 27 * (z + 2 * x + y) ^ 6 ≥ 1024 * (z + x) * (x + y) * (y + z + x) ^ 3 * x := by sorry
Source