Nonnegativity of an expanded sextic polynomial
ProvedWorkbookSource.base_15179lean-workbooksource-checked
Prove that .
Source: InternLM Lean-Workbook, record lean_workbook_15179 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_15179 {a u v : ℝ} : (3 * a^6 + a^5 * (15 * u + 12 * v) + a^4 * (33 * u^2 + 48 * u * v + 15 * v^2) + a^3 * (39 * u^3 + 81 * u^2 * v + 48 * u * v^2 + 6 * v^3) + a^2 * (25 * u^4 + 68 * u^3 * v + 60 * u^2 * v^2 + 17 * u * v^3 + v^4) + a * (8 * u^5 + 27 * u^4 * v + 32 * u^3 * v^2 + 15 * u^2 * v^3 + 2 * u * v^4) + u^6 + 4 * u^5 * v + 6 * u^4 * v^2 + 4 * u^3 * v^3 + u^2 * v^4) ≥ 0 := by sorrySource