Prove2Me

lean_workbook_plus_10237

Proved

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

Prove that 2k−12k≤2k−12k+1\frac{2k-1}{2k}\leq\sqrt{\frac{2k-1}{2k+1}} for k=1,2,...,nk=1,2,...,n.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10237 (k : ℕ) (h : 0 < k) :
  ((2 * k - 1 : ℝ) / (2 * k) : ℝ) ≤ Real.sqrt ((2 * k - 1 : ℝ) / (2 * k + 1 : ℝ))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph