lean_workbook_plus_79300

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

At first, by Holder inequality, we have $\left(x^3+1\right)\left(1+y^3\right)(1+1) \ge (x+y)^3, \forall x,y \in \mathbb{R^{+}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79300 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : (x^3 + 1) * (1 + y^3) * (1 + 1) ≥ (x + y)^3   :=  by sorry

Source