LinearRecurrence.geom_sol_iff_root_charPoly
theorem LinearRecurrence.geom_sol_iff_root_charPoly :
∀ {α : Type u_1} [inst : CommRing α] (E : LinearRecurrence α) (q : α),
(E.IsSolution fun n => q ^ n) ↔ E.charPoly.IsRoot q
This theorem states that for all types `α` in the universe `u_1`, where `α` is a commutative ring, and for a linear recurrence `E` and a value `q` of type `α`, the geometric sequence `q^n` is a solution of `E` if and only if `q` is a root of `E`'s characteristic polynomial. In other words, a particular value `q` enables the sequence `q^n` to satisfy the linear recurrence `E` precisely when `q` is a root of the polynomial that characterizes `E`.
More concisely: For a commutative ring type `α` and a linear recurrence `E` over `α`, a value `q` in `α` is a root of `E`'s characteristic polynomial if and only if `q^n` is a solution of `E` for all `n`.
|
LinearRecurrence.is_sol_iff_mem_solSpace
theorem LinearRecurrence.is_sol_iff_mem_solSpace :
∀ {α : Type u_1} [inst : CommSemiring α] (E : LinearRecurrence α) (u : ℕ → α), E.IsSolution u ↔ u ∈ E.solSpace := by
sorry
This theorem states that for any type `α` that is a commutative semiring, a sequence `u` of elements of `α` indexed by natural numbers is a solution to a given linear recurrence `E` if and only if `u` belongs to the solution space of `E`. In other words, the theorem is expressing the defining property of a solution space in the context of linear recurrences: a sequence is a solution to the recurrence if and only if it is a member of the set of all solutions.
More concisely: A sequence `u` of elements from a commutative semiring `α` is a solution to a linear recurrence `E` if and only if `u` is an element of the solution space of `E`.
|
LinearRecurrence.solSpace_rank
theorem LinearRecurrence.solSpace_rank :
∀ {α : Type u_1} [inst : CommRing α] [inst_1 : StrongRankCondition α] (E : LinearRecurrence α),
Module.rank α ↥E.solSpace = ↑E.order
This theorem states that for any Linear Recurrence `E` over a Type `α` (where `α` is a commutative ring with a strong rank condition), the rank (dimension) of the solution space (`E.solSpace`) of the Linear Recurrence is equal to the order of the Linear Recurrence (`E.order`). In other words, the number of linearly independent solutions of the Linear Recurrence is equal to its order.
More concisely: The rank of the solution space of a linear recurrence over a commutative ring with a strong rank condition equals its order.
|
LinearRecurrence.eq_mk_of_is_sol_of_eq_init
theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init :
∀ {α : Type u_1} [inst : CommSemiring α] (E : LinearRecurrence α) {u : ℕ → α} {init : Fin E.order → α},
E.IsSolution u → (∀ (n : Fin E.order), u ↑n = init n) → ∀ (n : ℕ), u n = E.mkSol init n
This theorem states that if `u` is a solution to a linear recurrence `E` and `init` represents the first `E.order` values of `u`, then for all natural numbers `n`, the `n`-th value of `u` equals to `E.mkSol init n`. This means, given a linear recurrence and a sequence satisfying it, if the initial values of the sequence match a certain pattern, then the entire sequence can be generated by the method `E.mkSol` applied to those initial values. Here, `α` is a type with Commutative Semiring structure.
More concisely: If `u` is a solution to a linear recurrence `E` and `init` are the first `E.order` values of `u`, then for all natural numbers `n`, `u(n) = E.mkSol init n`.
|
LinearRecurrence.is_sol_mkSol
theorem LinearRecurrence.is_sol_mkSol :
∀ {α : Type u_1} [inst : CommSemiring α] (E : LinearRecurrence α) (init : Fin E.order → α),
E.IsSolution (E.mkSol init)
This theorem states that for any type `α` that forms a commutative semiring and any Linear Recurrence `E` of this type, if you provide initial values (expressed as a function from finite ordinals less than `E.order` to `α`), the method `E.mkSol init` will produce a solution to the Linear Recurrence `E`. In mathematical terms, for a given sequence defined by a linear recurrence, if you specify its initial values, you can obtain the entire sequence, which will satisfy the defining linear recurrence.
More concisely: For any commutative semiring type `α` and linear recurrence `E` over `α`, given initial values `init : ℕ → α`, there exists a unique solution `s : ℕ → α` to `E` such that `s 0 = init 0` and for all `n`, `s (n + 1) = E.next s n`.
|
LinearRecurrence.sol_eq_of_eq_init
theorem LinearRecurrence.sol_eq_of_eq_init :
∀ {α : Type u_1} [inst : CommSemiring α] (E : LinearRecurrence α) (u v : ℕ → α),
E.IsSolution u → E.IsSolution v → (u = v ↔ Set.EqOn u v ↑(Finset.range E.order))
This theorem states that for any type `α` which forms a commutative semiring, given a linear recurrence `E` and two functions `u` and `v` from natural numbers to `α`, if both `u` and `v` are solutions to the linear recurrence, then `u` and `v` are equal if and only if they are equal on the set of natural numbers less than the order of `E`. In simpler terms, two solutions to a linear recurrence are identical if they coincide on the initial segment of natural numbers up to the order of the recurrence.
More concisely: For any commutative semiring type `α` and linear recurrence `E`, if `u` and `v` are solutions to `E` and their domains contain the natural numbers less than `E`'s order, then `u` and `v` are equal if and only if they agree on these natural numbers.
|
LinearRecurrence.eq_mk_of_is_sol_of_eq_init'
theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init' :
∀ {α : Type u_1} [inst : CommSemiring α] (E : LinearRecurrence α) {u : ℕ → α} {init : Fin E.order → α},
E.IsSolution u → (∀ (n : Fin E.order), u ↑n = init n) → u = E.mkSol init
This theorem states that if `u` is a solution to a linear recurrence `E`, and the first `E.order` values of `u` are specified by `init`, then `u` is equivalent to `E.mkSol init`. This effectively proves that `E.mkSol init` is the only solution to `E` whose first `E.order` values are provided by `init`. It applies to any commutative semiring `α`.
More concisely: If `u` is a solution to a linear recurrence `E` of order `n` with initial values given by `init`, then `u` is equal to the solution `E.mkSol init` obtained from the recurrence equation.
|
LinearRecurrence.mkSol_eq_init
theorem LinearRecurrence.mkSol_eq_init :
∀ {α : Type u_1} [inst : CommSemiring α] (E : LinearRecurrence α) (init : Fin E.order → α) (n : Fin E.order),
E.mkSol init ↑n = init n
This theorem states that for any instance of a type `α` (where `α` is a commutative semiring), any instance of `LinearRecurrence α`, and any function `init` from a finite set of size `E.order` into `α`, the first `E.order` terms of `E.mkSol init` are equal to `init`. In other words, when you create a solution to a linear recurrence relation using `E.mkSol init`, the initial terms of the solution are exactly those provided by the `init` function.
More concisely: For any commutative semiring `α`, any `LinearRecurrence α` instance, and finite set `E` of size `E.order`, the first `E.order` terms of the solution `E.mkSol init` to a linear recurrence relation with initial condition `init` are equal to `init`.
|