# mathlibdocumentation

algebra.linear_recurrence

# 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.

• 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 linear_equiv 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 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.

structure linear_recurrence (α : Type u_1)  :
Type u_1

A "linear recurrence relation" over a commutative semiring is given by its order n and n coefficients.

@[protected, instance]
def linear_recurrence.inhabited (α : Type u_1)  :
Equations
def linear_recurrence.is_solution {α : Type u_1} (E : linear_recurrence α) (u : → α) :
Prop

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.

Equations
def linear_recurrence.mk_sol {α : Type u_1} (E : linear_recurrence α) (init : fin E.order → α) :
→ α

A solution of a linear_recurrence which satisfies certain initial conditions. We will prove this is the only such solution.

Equations
theorem linear_recurrence.is_sol_mk_sol {α : Type u_1} (E : linear_recurrence α) (init : fin E.order → α) :
E.is_solution (E.mk_sol init)

E.mk_sol indeed gives solutions to E.

theorem linear_recurrence.mk_sol_eq_init {α : Type u_1} (E : linear_recurrence α) (init : fin E.order → α) (n : fin E.order) :
E.mk_sol init n = init n

E.mk_sol init's first E.order terms are init.

theorem linear_recurrence.eq_mk_of_is_sol_of_eq_init {α : Type u_1} (E : linear_recurrence α) {u : → α} {init : fin E.order → α} (h : E.is_solution u) (heq : ∀ (n : fin E.order), u n = init n) (n : ) :
u n = E.mk_sol init n

If u is a solution to E and init designates its first E.order values, then ∀ n, u n = E.mk_sol init n.

theorem linear_recurrence.eq_mk_of_is_sol_of_eq_init' {α : Type u_1} (E : linear_recurrence α) {u : → α} {init : fin E.order → α} (h : E.is_solution u) (heq : ∀ (n : fin E.order), u n = init n) :
u = E.mk_sol init

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.

def linear_recurrence.sol_space {α : Type u_1} (E : linear_recurrence α) :
( → α)

The space of solutions of E, as a submodule over α of the module ℕ → α.

Equations
theorem linear_recurrence.is_sol_iff_mem_sol_space {α : Type u_1} (E : linear_recurrence α) (u : → α) :

Defining property of the solution space : u is a solution iff it belongs to the solution space.

def linear_recurrence.to_init {α : Type u_1} (E : linear_recurrence α) :

The function that maps a solution u of E to its first E.order terms as a linear_equiv.

Equations
theorem linear_recurrence.sol_eq_of_eq_init {α : Type u_1} (E : linear_recurrence α) (u v : → α) (hu : E.is_solution u) (hv : E.is_solution v) :
u = v v

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.

def linear_recurrence.tuple_succ {α : Type u_1} (E : linear_recurrence α) :
(fin E.order → α) →ₗ[α] fin E.order → α

E.tuple_succ maps ![s₀, s₁, ..., sₙ] to ![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ], where n := E.order.

Equations
theorem linear_recurrence.sol_space_dim {α : Type u_1} [field α] (E : linear_recurrence α) :

The dimension of E.sol_space is E.order.

noncomputable def linear_recurrence.char_poly {α : Type u_1} [comm_ring α] (E : linear_recurrence α) :

The characteristic polynomial of E is X ^ E.order - ∑ i : fin E.order, (E.coeffs i) * X ^ i.

Equations
theorem linear_recurrence.geom_sol_iff_root_char_poly {α : Type u_1} [comm_ring α] (E : linear_recurrence α) (q : α) :
E.is_solution (λ (n : ), q ^ n) E.char_poly.is_root q

The geometric sequence q^n is a solution of E iff q is a root of E's characteristic polynomial.