# Documentation

Mathlib.Algebra.LinearRecurrence

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

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

structure LinearRecurrence (α : Type u_1) [] :
Type u_1
• order :
• coeffs : Fin s.orderα

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

Instances For
instance instInhabitedLinearRecurrence (α : Type u_1) [] :
def LinearRecurrence.IsSolution {α : Type u_1} [] (E : ) (u : α) :

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
def LinearRecurrence.mkSol {α : Type u_1} [] (E : ) (init : Fin E.orderα) :
α

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LinearRecurrence.is_sol_mkSol {α : Type u_1} [] (E : ) (init : Fin E.orderα) :

E.mkSol indeed gives solutions to E.

theorem LinearRecurrence.mkSol_eq_init {α : Type u_1} [] (E : ) (init : Fin E.orderα) (n : Fin E.order) :
LinearRecurrence.mkSol E init n = init n

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

theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init {α : Type u_1} [] (E : ) {u : α} {init : Fin E.orderα} (h : ) (heq : ∀ (n : Fin E.order), u n = init n) (n : ) :

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

theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init' {α : Type u_1} [] (E : ) {u : α} {init : Fin E.orderα} (h : ) (heq : ∀ (n : Fin E.order), u n = init n) :
u =

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.

def LinearRecurrence.solSpace {α : Type u_1} [] (E : ) :
Submodule α (α)

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

Instances For
theorem LinearRecurrence.is_sol_iff_mem_solSpace {α : Type u_1} [] (E : ) (u : α) :

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

def LinearRecurrence.toInit {α : Type u_1} [] (E : ) :
{ x // } ≃ₗ[α] Fin E.orderα

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

Instances For
theorem LinearRecurrence.sol_eq_of_eq_init {α : Type u_1} [] (E : ) (u : α) (v : α) (hu : ) (hv : ) :
u = v Set.EqOn u v ↑(Finset.range E.order)

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.

def LinearRecurrence.tupleSucc {α : Type u_1} [] (E : ) :
(Fin E.orderα) →ₗ[α] Fin E.orderα

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

Instances For
theorem LinearRecurrence.solSpace_rank {α : Type u_1} [] (E : ) :
Module.rank α { x // } = E.order

The dimension of E.solSpace is E.order.

def LinearRecurrence.charPoly {α : Type u_1} [] (E : ) :

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

Instances For
theorem LinearRecurrence.geom_sol_iff_root_charPoly {α : Type u_1} [] (E : ) (q : α) :

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