lean_workbook_plus_27731

Proved

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

Use the inequality $ab\le\frac{(a+b)^2}{4}$ for $a=4x^2-f(x)$ and $b=f(x).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27731 (f : ℝ → ℝ) (x : ℝ) : (4 * x ^ 2 - f x) * f x ≤ (4 * x ^ 2 - f x + f x) ^ 2 / 4   :=  by sorry

Source