lean_workbook_plus_53026

Proved

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

Prove that $\sqrt{(1+\alpha)(1+\beta)}\geq 1+\sqrt{\alpha\beta}$ for $\alpha,\beta>0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53026 (α β : ℝ) (hα : 0 < α) (hβ : 0 < β) : Real.sqrt ((1 + α) * (1 + β)) ≥ 1 + Real.sqrt (α * β)   :=  by sorry

Source