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),
where u is a sequence, d is the order of the recurrence and the a i
are its coefficients.
In this file, we define the structure linear_recurrence so that
linear_recurrence.mk d a represents the above relation, and we call
a sequence u which verifies it a solution of the linear recurrence.
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 firstdterms builds alinear_equivbetween the solution space andfin d → α, akaα ^ d. As a consequence, two solutions are equal if and only if their firstdterms are equals. - a geometric sequence
q ^ nis solution iffqis a root of a particular polynomial, which we call the characteristic polynomial of the recurrence
Of course, although we can inductively generate solutions (cf mk_sol), the
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 "linear recurrence relation" over a commutative semiring is given by its
order n and n coefficients.
Equations
- linear_recurrence.inhabited α = {default := {order := 0, coeffs := inhabited.default (fin 0 → α) unique.inhabited}}
We say that a sequence u is solution of linear_recurrence order coeffs when we have
u (n + order) = ∑ i : fin order, coeffs i * u (n + i) for any n.
A solution of a linear_recurrence which satisfies certain initial conditions.
We will prove this is the only such solution.
E.mk_sol indeed gives solutions to E.
E.mk_sol init's first E.order terms are init.
If u is a solution to E and init designates its first E.order values,
then ∀ n, u n = E.mk_sol init n.
If u is a solution to E and init designates its first E.order values,
then u = E.mk_sol init. This proves that E.mk_sol init is the only solution
of E whose first E.order values are given by init.
The space of solutions of E, as a submodule over α of the semimodule ℕ → α.
Defining property of the solution space : u is a solution
iff it belongs to the solution space.
The function that maps a solution u of E to its first
E.order terms as a linear_equiv.
Two solutions are equal iff they are equal on range E.order.
E.tuple_succ maps ![s₀, s₁, ..., sₙ] to ![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ],
where n := E.order. This operation is quite useful for determining closed-form
solutions of E.
E.tuple_succ maps ![s₀, s₁, ..., sₙ] to ![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ],
where n := E.order.
The dimension of E.sol_space is E.order.
The characteristic polynomial of E is X ^ E.order - ∑ i : fin E.order, (E.coeffs i) * X ^ i.
Equations
- E.char_poly = polynomial.monomial E.order 1 - finset.univ.sum (λ (i : fin E.order), polynomial.monomial ↑i (E.coeffs i))
The geometric sequence q^n is a solution of E iff
q is a root of E's characteristic polynomial.