lean_workbook_plus_5691

Proved

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

Prove the inequality: $\frac{1}{(1+u)^2} + \frac{1}{(1+v)^2} \geq \frac{1}{1+uv}$ for positive real numbers $u$ and $v$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5691 (u v : ℝ) (hu : u > 0) (hv : v > 0) : (1 / (1 + u) ^ 2 + 1 / (1 + v) ^ 2) ≥ 1 / (1 + u * v)   :=  by sorry

Source