lean_workbook_plus_20502

Proved

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

Let $x,y$ be reals such that $xy\geq 1 .$ Prove that\n

\dfrac{1}{1+x^2}+\dfrac{1}{1+y^2}+ \dfrac{1}{8}xy \geq \dfrac{7}{8}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20502 (x y : ℝ) (h : x * y ≥ 1) : 1 / (1 + x ^ 2) + 1 / (1 + y ^ 2) + 1 / 8 * (x * y) ≥ 7 / 8   :=  by sorry

Source