lean_workbook_plus_19437

Proved

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

Let $a > 0$ , $b > 0$ and $ab=1$ . Prove that $\frac{a}{a^2+3}+\frac{b}{b^2+3}\leq\frac{1}{2}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19437 (a b : ℝ) (hab : a * b = 1) : a / (a ^ 2 + 3) + b / (b ^ 2 + 3) ≤ 1 / 2   :=  by sorry

Source