lean_workbook_plus_1320

Proved

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

Using the Arithmetic Mean-Geometric Mean (AM-GM) inequality, show that $2(a+c)^{2}+2(b+d)^{2} \geq 8(ac+bd)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1320 (a b c d : ℝ) : 2 * (a + c) ^ 2 + 2 * (b + d) ^ 2 ≥ 8 * (a * c + b * d)   :=  by sorry

Source