A fourth-order recurrence grows slower than the square of its index
ProvedWorkbookSource.plus_63221lean-workbooksequencessource-checked
Let a₀=a₁=a₃=0 and a₂=−1, with aₙ₊₄+2aₙ₊₃+3aₙ₊₂+2aₙ₊₁+aₙ=0 for every n≥0. Then lim aₙ/n²=0.
Source: InternLM Lean-Workbook, record lean_workbook_plus_63221 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookSource.plus_63221 (a : ℕ → ℝ) (a0 : a 0 = 0) (a1 : a 1 = 0) (a2 : a 2 = -1) (a3 : a 3 = 0) (h : ∀ n, a (n + 4) + 2 * a (n + 3) + 3 * a (n + 2) + 2 * a (n + 1) + a n = 0) : ∀ ε > 0, ∃ N : ℕ, ∀ n > N, |a n / n ^ 2| < ε := by sorry
Source