lean_workbook_plus_16937
Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Let f(x)=2x(1−x)2 , then the max occurs when f′(x)=6x2−8x+2=0 , which has roots x=31 and x=1 . Hence, \n\n f(x)≤f(31)=2(31)(32)2=278 .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16937 :
IsGreatest {y : ℝ | ∃ x, 0 ≤ x ∧ x ≤ 1 ∧ y = 2 * x * (1 - x)^2} (8 / 27) := by sorryView graph