# 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 `LinearRecurrence`

so that
`LinearRecurrence.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
`u`

to its first`d`

terms builds a`LinearEquiv`

between the solution space and`Fin d → α`

, aka`α ^ d`

. As a consequence, two solutions are equal if and only if their first`d`

terms are equals. - a geometric sequence
`q ^ n`

is solution iff`q`

is a root of a particular polynomial, which we call the*characteristic polynomial*of the recurrence

Of course, although we can inductively generate solutions (cf `mkSol`

), 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.

## Instances For

## Equations

- instInhabitedLinearRecurrence α = { default := { order := 0, coeffs := default } }

We say that a sequence `u`

is solution of `LinearRecurrence order coeffs`

when we have
`u (n + order) = ∑ i : Fin order, coeffs i * u (n + i)`

for any `n`

.

## Instances For

A solution of a `LinearRecurrence`

which satisfies certain initial conditions.
We will prove this is the only such solution.

## Equations

## Instances For

`E.mkSol`

indeed gives solutions to `E`

.

If `u`

is a solution to `E`

and `init`

designates its first `E.order`

values,
then `∀ n, u n = E.mkSol init n`

.

If `u`

is a solution to `E`

and `init`

designates its first `E.order`

values,
then `u = E.mkSol init`

. This proves that `E.mkSol 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 module `ℕ → α`

.

## Equations

## Instances For

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 `LinearEquiv`

.

## Equations

## Instances For

Two solutions are equal iff they are equal on `range E.order`

.

`E.tupleSucc`

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.tupleSucc`

maps `![s₀, s₁, ..., sₙ]`

to `![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ]`

,
where `n := E.order`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The characteristic polynomial of `E`

is
`X ^ E.order - ∑ i : Fin E.order, (E.coeffs i) * X ^ i`

.

## Equations

- E.charPoly = (Polynomial.monomial E.order) 1 - ∑ i : Fin E.order, (Polynomial.monomial ↑i) (E.coeffs i)

## Instances For

The geometric sequence `q^n`

is a solution of `E`

iff
`q`

is a root of `E`

's characteristic polynomial.