lean_workbook_plus_9103

Proved

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

prove that $\frac 1{1+x^2}+\frac 1{1+y^2}\geq \frac 2{1+xy}$ for all $x,y>0$ and $xy\geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9103 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (hxy : 1 ≤ x * y) :
  1 / (1 + x^2) + 1 / (1 + y^2) ≥ 2 / (1 + x * y)   :=  by sorry

Source

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

View graph