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 (α : Type u_1) [CommSemiring α] : 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 → α

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

Equations

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

def LinearRecurrence.IsSolution {α : Type u_1} [CommSemiring α] (E : LinearRecurrence α) (u : ℕ → α) : 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 {α : Type u_1} [CommSemiring α] (E : LinearRecurrence α) (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)

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

E.mkSol indeed gives solutions to E.

theorem LinearRecurrence.mkSol_eq_init {α : Type u_1} [CommSemiring α] (E : LinearRecurrence α) (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} [CommSemiring α] (E : LinearRecurrence α) {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} [CommSemiring α] (E : LinearRecurrence α) {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} [CommSemiring α] (E : LinearRecurrence α) : 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' := ⋯ }

theorem LinearRecurrence.is_sol_iff_mem_solSpace {α : Type u_1} [CommSemiring α] (E : LinearRecurrence α) (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} [CommSemiring α] (E : LinearRecurrence α) : ↥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 := ⋯ }

theorem LinearRecurrence.sol_eq_of_eq_init {α : Type u_1} [CommSemiring α] (E : LinearRecurrence α) (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} [CommSemiring α] (E : LinearRecurrence α) : (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.

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

The dimension of E.solSpace is E.order.

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

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