Closed form of a second-order linear recurrence
ProvedWorkbookCorrected.plus_34888corrected-formalizationlean-workbooksequencessource-checked
Let a₀ = 1, a₁ = 2, and aₙ₊₂ = 4aₙ₊₁+aₙ for every natural number n. Then aₙ = ((2+√5)ⁿ+(2−√5)ⁿ)/2 for every natural number n.
Formalization Note: Supplies the explicit closed form requested in the source; the original formalization merely asserted the existence of a function equal to the sequence.
Source: InternLM Lean-Workbook, record lean_workbook_plus_34888 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_34888 (a : ℕ → ℝ) (h0 : a 0=1) (h1 : a 1=2)
(h : ∀ n : ℕ, a (n+2)=4*a (n+1)+a n) :
∀ n : ℕ, a n=((2+Real.sqrt 5)^n+(2-Real.sqrt 5)^n)/2 := by sorrySource