lean_workbook_plus_76960

Proved

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

Prove that $4\left(\frac{(1-q^2)}{3}\right)^2+81\left(\frac{(1+q)^2(1-2q)}{27}\right)^2\ge 15\left(\frac{1-q^2}{3}\right)^3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76960 (q : ℝ) : 4*((1-q^2)/3)^2 + 81*((1+q)^2*(1-2*q)/27)^2 ≥ 15*((1-q^2)/3)^3   :=  by sorry

Source