lean_workbook_plus_36562

Proved

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

Derive the inequality $\frac{x}{1+nx^2} \leq \frac{1}{2\sqrt{n}}$ using the AM-GM inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36562 (x : ℝ) (n : ℕ) (hn : n ≠ 0) : (x / (1 + n * x ^ 2)) ≤ (1 / (2 * Real.sqrt n))   :=  by sorry

Source