lean_workbook_plus_34444

Proved

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

Derive the inequality $\sqrt{a^2+b^2}\ge \frac{a+b}{\sqrt{2}}$ from $2(a^2+b^2)\ge (a+b)^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34444 : ∀ a b : ℝ, 2 * (a ^ 2 + b ^ 2) ≥ (a + b) ^ 2 → Real.sqrt (a ^ 2 + b ^ 2) ≥ (a + b) / Real.sqrt 2   :=  by sorry

Source