Vanishing scaled terms of an index-dependent rational recurrence
ProvedWorkbookCorrected.plus_43357corrected-formalizationlean-workbooksequencessource-checked
Let x₁ = 1/2 and xₙ₊₁ = n xₙ²/(1+(n+1)xₙ) for every integer n ≥ 1. Then n xₙ converges to zero.
Formalization Note: Restores the source’s positive recurrence indices; applying the original recurrence at zero contradicted the supplied initial value.
Source: InternLM Lean-Workbook, record lean_workbook_plus_43357 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_43357 (x : ℕ → ℝ) (h1 : x 1=1/2)
(h : ∀ n : ℕ, 1 ≤ n → x (n+1)=(n:ℝ)*x n^2/(1+((n:ℝ)+1)*x n)) :
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |(n:ℝ)*x n| < ε := by sorrySource