lean_workbook_plus_54915

Proved

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

It is easy to see that $\frac{1}{a^2}+\frac{1}{b^2}\geqslant \frac{8}{(a+b)^2} , a>0,b>0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54915  (a b : ℝ)
  (h₀ : 0 < a ∧ 0 < b) :
  1 / a^2 + 1 / b^2 ≥ 8 / (a + b)^2   :=  by sorry

Source