lean_workbook_plus_13067

Proved

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

Prove the inequality using the AM-HM inequality: $\frac {1}{a + b}\leq \frac {1}{4a} + \frac {1}{4b}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13067 (a b : ℝ) (ha : a > 0) (hb : b > 0) : 1 / (a + b) ≤ 1 / (4 * a) + 1 / (4 * b)   :=  by sorry

Source