Recurrence Lemmas for the `continuants` Function of Continued Fractions.

Summary

Given a generalized continued fraction g, for all n ≥ 1, we prove that the continuants function indeed satisfies the following recurrences:

g.s.nth n = option.some gp → g.continuants_aux n = ppred → g.continuants_aux (n + 1) = pred → g.continuants_aux (n + 2) = {a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b}

g.s.nth n = option.some gp → g.continuants_aux n = ppred → g.continuants_aux (n + 1) = pred → g.continuants (n + 1) = {a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b}

g.s.nth (n + 1) = option.some gp → g.continuants n = ppred → g.continuants (n + 1) = pred → g.continuants (n + 2) = {a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b}

Shows that Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂ and Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂.

g.s.nth (n + 1) = option.some gp → g.numerators n = ppredA → g.numerators (n + 1) = predA → g.numerators (n + 2) = gp.b * predA + gp.a * ppredA

Shows that Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂.

g.s.nth (n + 1) = option.some gp → g.denominators n = ppredB → g.denominators (n + 1) = predB → g.denominators (n + 2) = gp.b * predB + gp.a * ppredB

Shows that Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂.