A cubic bound on the unit interval

Proved

WorkbookSource.problem_13333

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

lean-workbooksource-checked

If $f(y)=y^2-{{2y^3}\over 3}$ then $f'(y)=2y(1-y)\ge 0$ on $[0,1]$ hence $f(y)\le f(1)=1/3$ .

Source: InternLM Lean-Workbook, record lean_workbook_13333 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_13333  (y : ℝ)
  (h₀ : 0 ≤ y)
  (h₁ : y ≤ 1) :
  y^2 - (2 * y^3) / 3 ≤ 1 / 3  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_13333; Apache-2.0

View graph