Convergence from bounds between consecutive terms
ProvedWorkbookCorrected.plus_53487corrected-formalizationlean-workbooksequencessource-checked
Let a₀=a₁=1 and aₙ₊₁=aₙ−aₙ₋₁/4 for every integer n ≥ 1. The sequence converges. This proof uses inequalities between consecutive terms, without finding a closed formula.
Formalization Note: Restores the second-order recurrence’s valid indices; the original recurrence at zero contradicted the initial values.
Source: InternLM Lean-Workbook, record lean_workbook_plus_53487 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_53487 (a : ℕ → ℝ) (h0 : a 0=1) (h1 : a 1=1)
(h : ∀ n : ℕ, a (n+2)=a (n+1)-(1/4)*a n) :
∃ l : ℝ, ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |a n-l| < ε := by sorrySource