English
A construction mkSol(init) defines a sequence by the recurrence E with given initial values init on the first order terms; the rest is defined recursively by the recurrence.
Русский
Конструкция mkSol(init) задаёт последовательность по рекуррентности E с заданными начальными значениями на первых order членов; остальные члены определяются по рекуррентности.
LaTeX
$$$\text{mkSol}(init) : \mathbb{N} \to R\quad\text{with }\; (\text{mkSol}(init))(n) = \begin{cases} init(\langle n, n<\text{order}\rangle) & n<\text{order} \\ \sum_{k : Fin\,\text{order}} E.coeffs\ k \cdot (\text{mkSol}(init))(n-\text{order}+k) & \text{otherwise} \end{cases}$$$
Lean4
/-- A solution of a `LinearRecurrence` which satisfies certain initial conditions.
We will prove this is the only such solution. -/
def mkSol (init : Fin E.order → R) : ℕ → R
| n =>
if h : n < E.order then init ⟨n, h⟩
else
∑ k : Fin E.order,
have _ : n - E.order + k < n := by omega
E.coeffs k * mkSol init (n - E.order + k)
