lean_workbook_plus_57672

Proved

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

Since $xy\le (x+y)^2/4$ (which follows easily from AM-GM), \n\n $(db+c)(dc+b)\le\frac14((db+c)+(dc+b))^2=\frac14(d+1)^2(b+c)^2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57672  (b d c : ℝ) :
  (b * d + c) * (d * c + b) ≤ (1 / 4) * (d + 1)^2 * (b + c)^2   :=  by sorry

Source