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 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 (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)

Equations

• instInhabitedLinearRecurrence R = { default := { order := 0, coeffs := default } }

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.

Equations

• E.IsSolution u = ∀ (n : ℕ), u (n + E.order) = ∑ i : Fin E.order, E.coeffs i * u (n + ↑i)

@[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.

Equations

• E.mkSol init x✝ = if h : x✝ < E.order then init ⟨x✝, h⟩ else ∑ k : Fin E.order, have x := ⋯; E.coeffs k * E.mkSol init (x✝ - E.order + ↑k)

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.

Equations

• E.solSpace = { carrier := {u : ℕ → R | E.IsSolution u}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

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.

Equations

• E.toInit = { toFun := fun (u : ↥E.solSpace) (x : Fin E.order) => ↑u ↑x, map_add' := ⋯, map_smul' := ⋯, invFun := fun (u : Fin E.order → R) => ⟨E.mkSol u, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• E.charPoly = (Polynomial.monomial E.order) 1 - ∑ i : Fin E.order, (Polynomial.monomial ↑i) (E.coeffs 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.