The scaled limit of an index-dependent square-root recurrence
ProvedWorkbookCorrected.plus_63871corrected-formalizationlean-workbooksequencessource-checked
Let x₁=1 and xₙ₊₁=√(1+nxₙ) for every integer n≥1. Then lim xₙ/n=1.
Formalization Note: Restores the source’s initial index and positive recurrence indices, and specifies the exact limit.
Source: InternLM Lean-Workbook, record lean_workbook_plus_63871 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_63871 (x : ℕ → ℝ) (x1 : x 1 = 1) (h : ∀ n : ℕ, 1 ≤ n → x (n+1)=Real.sqrt (1+(n:ℝ)*x n)) : ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |x n / (n:ℝ)-1| < ε := by sorry
Source