# 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

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

• order :
• coeffs : Fin self.orderα
Instances For
instance instInhabitedLinearRecurrence (α : Type u_1) [] :
Equations
• = { default := { order := 0, coeffs := default } }
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.

Equations
• E.IsSolution u = ∀ (n : ), u (n + E.order) = i : Fin E.order, E.coeffs i * u (n + i)
Instances For
@[irreducible]
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
• E.mkSol init x = if h : x < E.order then init x, h else k : Fin E.order, let_fun x_1 := ; E.coeffs k * E.mkSol init (x - E.order + k)
Instances For
theorem LinearRecurrence.is_sol_mkSol {α : Type u_1} [] (E : ) (init : Fin E.orderα) :
E.IsSolution (E.mkSol init)

E.mkSol indeed gives solutions to E.

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

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

@[irreducible]
theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init {α : Type u_1} [] (E : ) {u : α} {init : Fin E.orderα} (h : E.IsSolution u) (heq : ∀ (n : Fin E.order), u n = init n) (n : ) :
u n = E.mkSol init 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 : E.IsSolution u) (heq : ∀ (n : Fin E.order), u n = init n) :
u = E.mkSol init

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 ℕ → α.

Equations
• E.solSpace = { carrier := {u : α | E.IsSolution u}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
theorem LinearRecurrence.is_sol_iff_mem_solSpace {α : Type u_1} [] (E : ) (u : α) :
E.IsSolution u u E.solSpace

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

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

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

Equations
• E.toInit = { toFun := fun (u : E.solSpace) (x : Fin E.order) => u x, map_add' := , map_smul' := , invFun := fun (u : Fin E.orderα) => E.mkSol u, , left_inv := , right_inv := }
Instances For
theorem LinearRecurrence.sol_eq_of_eq_init {α : Type u_1} [] (E : ) (u : α) (v : α) (hu : E.IsSolution u) (hv : E.IsSolution v) :
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LinearRecurrence.solSpace_rank {α : Type u_1} [] (E : ) :
Module.rank α E.solSpace = 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.

Equations
Instances For
theorem LinearRecurrence.geom_sol_iff_root_charPoly {α : Type u_1} [] (E : ) (q : α) :
(E.IsSolution fun (n : ) => q ^ n) E.charPoly.IsRoot q

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