English
The convergents auxiliary function convs'Aux computes the partial fractions from a stream of pairs and yields a sequence by recursion.
Русский
Вспомогательная функция convs'Aux вычисляет частичные дроби из потока пар и строит последовательность рекурсивно.
LaTeX
$$$convs'Aux : Stream'.Seq (Pair K) \\to \\mathbb{N} \\to K$ with definitional recursion$$
Lean4
/-- Returns the approximation of the fraction described by the given sequence up to a given position n.
For example, `convs'Aux [(1, 2), (3, 4), (5, 6)] 2 = 1 / (2 + 3 / 4)` and
`convs'Aux [(1, 2), (3, 4), (5, 6)] 0 = 0`.
-/
def convs'Aux : Stream'.Seq (Pair K) → ℕ → K
| _, 0 => 0
| s, n + 1 =>
match s.head with
| none => 0
| some gp => gp.a / (gp.b + convs'Aux s.tail n)
