Recurrence Lemmas for the Continuants (conts) Function of Continued Fractions

Summary

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

• Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂, and
• Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂.

theorem GenContFract.contsAux_recurrence {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] {gp ppred pred : GenContFract.Pair K} (nth_s_eq : g.s.get? n = some gp) (nth_contsAux_eq : g.contsAux n = ppred) (succ_nth_contsAux_eq : g.contsAux (n + 1) = pred) : g.contsAux (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

theorem GenContFract.conts_recurrenceAux {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] {gp ppred pred : GenContFract.Pair K} (nth_s_eq : g.s.get? n = some gp) (nth_contsAux_eq : g.contsAux n = ppred) (succ_nth_contsAux_eq : g.contsAux (n + 1) = pred) : g.conts (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

theorem GenContFract.conts_recurrence {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] {gp ppred pred : GenContFract.Pair K} (succ_nth_s_eq : g.s.get? (n + 1) = some gp) (nth_conts_eq : g.conts n = ppred) (succ_nth_conts_eq : g.conts (n + 1) = pred) : g.conts (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ₙ₋₂.

theorem GenContFract.nums_recurrence {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] {gp : GenContFract.Pair K} {ppredA predA : K} (succ_nth_s_eq : g.s.get? (n + 1) = some gp) (nth_num_eq : g.nums n = ppredA) (succ_nth_num_eq : g.nums (n + 1) = predA) : g.nums (n + 2) = gp.b * predA + gp.a * ppredA

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

theorem GenContFract.dens_recurrence {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] {gp : GenContFract.Pair K} {ppredB predB : K} (succ_nth_s_eq : g.s.get? (n + 1) = some gp) (nth_den_eq : g.dens n = ppredB) (succ_nth_den_eq : g.dens (n + 1) = predB) : g.dens (n + 2) = gp.b * predB + gp.a * ppredB

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