mathlib documentation

algebra.​linear_recurrence

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.

We prove a few basic lemmas about this concept, such as :

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) [comm_semiring α] :
Type u_1

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

def linear_recurrence.​is_solution {α : Type u_1} [comm_semiring α] :
linear_recurrence α( → α) → 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} [comm_semiring α] (E : linear_recurrence α) :
(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} [comm_semiring α] (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} [comm_semiring α] (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} [comm_semiring α] (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} [comm_semiring α] (E : linear_recurrence α) {u : → α} {init : fin E.order → α} :
E.is_solution u(∀ (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} [comm_semiring α] :
linear_recurrence αsubmodule α ( → α)

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

Equations
theorem linear_recurrence.​is_sol_iff_mem_sol_space {α : Type u_1} [comm_semiring α] (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} [comm_semiring α] (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} [comm_semiring α] (E : linear_recurrence α) (u 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} [comm_semiring α] (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

The dimension of E.sol_space is E.order.

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.