Prove2Me

lean_workbook_plus_70562

Proved

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

It follows form following 2 inequalities:\n\n ab(a2+b22)≤(a+b2)2\sqrt{ab\left(\frac{a^2+b^2}{2}\right)} \leq \left(\frac{a+b}{2}\right)^2 \n\nand:\n\n (a2−ab+b2)(a+b)2≥(a2+b2)2(a^2-ab+b^2)(a+b)^2 \ge (a^2+b^2)^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70562  (a b : ℝ) :
  Real.sqrt (a * b * ((a^2 + b^2) / 2)) ≤ ((a + b) / 2)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph