lean_workbook_plus_11093

Proved

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

Now, we have $(x-y)^2 \ge 0$ , so $x^2 + y^2 \ge 2xy$ . Thus, $\sqrt{x^2 + xy + y^2} \ge \sqrt{3xy}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11093  (x y : ℝ) :
  Real.sqrt (x^2 + x * y + y^2) ≥ Real.sqrt (3 * x * y)   :=  by sorry

Source