A cubic product bound involving an absolute value

Proved

WorkbookSource.plus_45827

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

lean-workbooksource-checked

Prove that $(1+|a|+a^2)^3 \geq (1+|a|)^3(1+|a|^3)$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_45827 (a : ℝ) : (1 + |a| + a^2)^3 ≥ (1 + |a|)^3 * (1 + |a|^3)   :=  by sorry

Source