lean_workbook_plus_68083

Proved

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

For $x>0$ , we have $\displaystyle \frac{x}{4+x^2} \leq \frac{1}{20}\left(1+\frac{15}{1+x}\right)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68083 (x : ℝ) (hx : 0 < x) : (x / (4 + x ^ 2) ≤ (1 / 20) * (1 + 15 / (1 + x)))   :=  by sorry

Source