lean_workbook_plus_17792

Proved

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

It works because: \n\n

\frac {x+y}{2} \ge \sqrt {xy}

x+y \ge 2\sqrt {xy}

x^2+y^2+2xy \ge 4xy

(x-y)^2 \ge 0

\n\n which is true by the trivial inequality. The equality happens at $x=y$ . We can not have $x,y$ be negative otherwise $\sqrt {xy}$ is not real.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17792  (x y : ℝ)
  (h₀ : 0 ≤ x ∧ 0 ≤ y) :
  (x + y) / 2 ≥ Real.sqrt (x * y) ↔ x^2 + y^2 + 2 * (x * y) ≥ 4 * (x * y)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph