lean_workbook_plus_81533

Proved

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

$\frac{\sqrt{a+b}}{\sqrt{2}}\geq\frac{2}{\frac{1}{\sqrt{a}}+\frac{1}{\sqrt{b}}}\Longleftrightarrow\sqrt{a+b}(\frac{1}{\sqrt{a}}+\frac{1}{\sqrt{b}})\geq2\sqrt{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81533 (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : (Real.sqrt (a + b) / Real.sqrt 2) ≥ 2 / (1 / Real.sqrt a + 1 / Real.sqrt b) ↔ Real.sqrt (a + b) * (1 / Real.sqrt a + 1 / Real.sqrt b) ≥ 2 * Real.sqrt 2   :=  by sorry

Source

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

View graph