mathlib3 documentation

algebra.linear_recurrence

Linear recurrence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 :

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

Type u_1

order : ℕ
coeffs : fin self.order → α

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

Instances for linear_recurrence

linear_recurrence.has_sizeof_inst
linear_recurrence.inhabited

@[protected, instance]

def linear_recurrence.inhabited (α : Type u_1) [comm_semiring α] :

inhabited (linear_recurrence α)

Equations

linear_recurrence.inhabited α = {default := {order := 0, coeffs := inhabited.default unique.inhabited}}

def linear_recurrence.is_solution {α : Type u_1} [comm_semiring α] (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

E.is_solution u = ∀ (n : ℕ), u (n + E.order) = finset.univ.sum (λ (i : fin E.order), E.coeffs i * u (n + ↑i))

def linear_recurrence.mk_sol {α : Type u_1} [comm_semiring α] (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

E.mk_sol init n = dite (n < E.order) (λ (h : n < E.order), init ⟨n, h⟩) (λ (h : ¬n < E.order), finset.univ.sum (λ (k : fin E.order), E.coeffs k * E.mk_sol init (n - E.order + ↑k)))

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 → α} (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} [comm_semiring α] (E : linear_recurrence α) :

submodule α (ℕ → α)

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

Equations

E.sol_space = {carrier := {u : ℕ → α | E.is_solution u}, add_mem' := _, zero_mem' := _, smul_mem' := _}

theorem linear_recurrence.is_sol_iff_mem_sol_space {α : Type u_1} [comm_semiring α] (E : linear_recurrence α) (u : ℕ → α) :

E.is_solution u ↔ u ∈ E.sol_space

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 α) :

↥(E.sol_space) ≃ₗ[α] fin E.order → α

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

Equations

E.to_init = {to_fun := λ (u : ↥(E.sol_space)) (x : fin E.order), ↑u ↑x, map_add' := _, map_smul' := _, inv_fun := λ (u : fin E.order → α), ⟨E.mk_sol u, _⟩, left_inv := _, right_inv := _}

theorem linear_recurrence.sol_eq_of_eq_init {α : Type u_1} [comm_semiring α] (E : linear_recurrence α) (u v : ℕ → α) (hu : E.is_solution u) (hv : E.is_solution v) :

u = v ↔ set.eq_on u v ↑(finset.range E.order)

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

E.tuple_succ = {to_fun := λ (X : fin E.order → α) (i : fin E.order), dite (↑i + 1 < E.order) (λ (h : ↑i + 1 < E.order), X ⟨↑i + 1, h⟩) (λ (h : ¬↑i + 1 < E.order), finset.univ.sum (λ (i : fin E.order), E.coeffs i * X i)), map_add' := _, map_smul' := _}

theorem linear_recurrence.sol_space_rank {α : Type u_1} [comm_ring α] [strong_rank_condition α] (E : linear_recurrence α) :

module.rank α ↥(E.sol_space) = ↑(E.order)

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

E.char_poly = ⇑(polynomial.monomial E.order) 1 - finset.univ.sum (λ (i : fin E.order), ⇑(polynomial.monomial ↑i) (E.coeffs i))

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.