### Abstract

Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n-1) + f(n - 2) and the quite non-obvious closed form (φn - (-φ)-n) / √5 where φ is the golden ratio.

In this work, I build on existing tools in Isabelle – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Linear_Recurrences

- RatFPS
- Pochhammer_Polynomials
- Linear_Recurrences_Misc
- Partial_Fraction_Decomposition
- Factorizations
- Rational_FPS_Solver
- Linear_Recurrences_Common
- Linear_Homogenous_Recurrences
- Eulerian_Polynomials
- Linear_Inhomogenous_Recurrences
- Rational_FPS_Asymptotics

### Session Linear_Recurrences_Solver

- Linear_Recurrences_Solver
- Linear_Recurrences_Pretty
- Show_RatFPS
- Linear_Recurrences_Test

### Depends on

- Count the Number of Complex Roots
- Polynomial Factorization
- Algebraic Numbers in Isabelle/HOL
- The Factorization Algorithm of Berlekamp and Zassenhaus
- Factorization of Polynomials with Algebraic Coefficients

### Used by

- The Polylogarithm Function

### Auto-related entries

- Formal Puiseux Series

## Cite

×

Linear_Recurrences-AFP

    @article{Linear_Recurrences-AFP,
      author  = {Manuel Eberl},
      title   = {Linear Recurrences},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Linear_Recurrences.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 17, 2017 : Isabelle2017