Limit of a recurrence with squared reciprocal weights
ProvedWorkbookCorrected.plus_42198corrected-formalizationlean-workbooksequencessource-checked
Let aₙ₊₁ = (1−1/n)²aₙ+1/n for every positive integer n. Then aₙ converges to 1/2, regardless of a₁.
Formalization Note: Uses the source’s positive recurrence indices, removes an initial condition absent from the source, and identifies the exact requested limit.
Source: InternLM Lean-Workbook, record lean_workbook_plus_42198 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_42198 (a : ℕ → ℝ)
(h : ∀ n : ℕ, 1 ≤ n → a (n+1)=(1-1/(n:ℝ))^2*a n+1/(n:ℝ)) :
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |a n-1/2| < ε := by sorrySource