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 equal.
• 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 determine closed-forms for the solutions. This is currently not implemented, as we are waiting for definition and properties of eigenvalues and eigenvectors.

structure LinearRecurrence (R : Type u_1) [CommSemiring R] : Type u_1

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

• order : ℕ

  Order of the linear recurrence

• coeffs : Fin self.order → R

  Coefficients of the linear recurrence

instance instInhabitedLinearRecurrence (R : Type u_1) [CommSemiring R] : Inhabited (LinearRecurrence R)

def LinearRecurrence.IsSolution {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (u : ℕ → R) : Prop

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.

@[irreducible]

def LinearRecurrence.mkSol {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (init : Fin E.order → R) : ℕ → R

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

theorem LinearRecurrence.is_sol_mkSol {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (init : Fin E.order → R) : E.IsSolution (E.mkSol init)

E.mkSol indeed gives solutions to E.

theorem LinearRecurrence.mkSol_eq_init {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (init : Fin E.order → R) (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 {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) {u : ℕ → R} {init : Fin E.order → R} (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' {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) {u : ℕ → R} {init : Fin E.order → R} (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 {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) : Submodule R (ℕ → R)

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

theorem LinearRecurrence.is_sol_iff_mem_solSpace {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (u : ℕ → R) : 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 {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) : ↥E.solSpace ≃ₗ[R] Fin E.order → R

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

theorem LinearRecurrence.sol_eq_of_eq_init {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) (u v : ℕ → R) (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 {R : Type u_1} [CommSemiring R] (E : LinearRecurrence R) : (Fin E.order → R) →ₗ[R] Fin E.order → R

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

theorem LinearRecurrence.solSpace_rank {R : Type u_1} [CommRing R] [StrongRankCondition R] (E : LinearRecurrence R) : Module.rank R ↥E.solSpace = ↑E.order

The dimension of E.solSpace is E.order.

def LinearRecurrence.charPoly {R : Type u_1} [CommRing R] (E : LinearRecurrence R) : Polynomial R

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

theorem LinearRecurrence.geom_sol_iff_root_charPoly {R : Type u_1} [CommRing R] (E : LinearRecurrence R) (q : R) : (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.