lean_workbook_plus_17624

Proved

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

Let $x,y>0$ ,prove that: $2.\frac{1}{x}\geq \frac{4}{(1+x)^2} \Leftrightarrow (1+x)^2\geq 4x$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17624 (x : ℝ) (hx : 0 < x) :
  2 * (1 / x) ≥ 4 / (1 + x) ^ 2 ↔ (1 + x) ^ 2 ≥ 4 * x   :=  by sorry

Source