lean_workbook_plus_7901

Proved

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

Prove that $\frac{1}{2}(a^2+b^2) \ge ab$ , $\frac{1}{2}(b^2+c^2) \ge bc$ , and $\frac{1}{2}(a^2+c^2) \ge ac$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7901 (a b c : ℝ) : (a^2 + b^2)/2 ≥ a * b ∧ (b^2 + c^2)/2 ≥ b * c ∧ (c^2 + a^2)/2 ≥ c * a   :=  by sorry

Source