Linear recurrence #
Informally, a "linear recurrence" is an assertion of the form
∀ n : ℕ, u (n + d) = a 0 * u n + a 1 * u (n+1) + ... + a (d-1) * u (n+d-1),
u is a sequence,
d is the order of the recurrence and the
are its coefficients.
We prove a few basic lemmas about this concept, such as :
- the space of solutions is a submodule of
(ℕ → α)(i.e a vector space if
αis a field)
- the function that maps a solution
uto its first
dterms builds a
LinearEquivbetween the solution space and
Fin d → α, aka
α ^ d. As a consequence, two solutions are equal if and only if their first
dterms are equals.
- a geometric sequence
q ^ nis solution iff
qis a root of a particular polynomial, which we call the characteristic polynomial of the recurrence
Of course, although we can inductively generate solutions (cf
interesting part would be to determinate closed-forms for the solutions.
This is currently not implemented, as we are waiting for definition and
properties of eigenvalues and eigenvectors.
A solution of a
LinearRecurrence which satisfies certain initial conditions.
We will prove this is the only such solution.
- One or more equations did not get rendered due to their size.
Two solutions are equal iff they are equal on
The geometric sequence
q^n is a solution of
q is a root of
E's characteristic polynomial.