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:

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

theorem GeneralizedContinuedFraction.continuantsAux_recurrence {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K] {gp : GeneralizedContinuedFraction.Pair K} {ppred : GeneralizedContinuedFraction.Pair K} {pred : GeneralizedContinuedFraction.Pair K} (nth_s_eq : Stream'.Seq.get? g.s n = some gp) (nth_conts_aux_eq : GeneralizedContinuedFraction.continuantsAux g n = ppred) (succ_nth_conts_aux_eq : GeneralizedContinuedFraction.continuantsAux g (n + 1) = pred) : GeneralizedContinuedFraction.continuantsAux g (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

theorem GeneralizedContinuedFraction.continuants_recurrenceAux {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K] {gp : GeneralizedContinuedFraction.Pair K} {ppred : GeneralizedContinuedFraction.Pair K} {pred : GeneralizedContinuedFraction.Pair K} (nth_s_eq : Stream'.Seq.get? g.s n = some gp) (nth_conts_aux_eq : GeneralizedContinuedFraction.continuantsAux g n = ppred) (succ_nth_conts_aux_eq : GeneralizedContinuedFraction.continuantsAux g (n + 1) = pred) : GeneralizedContinuedFraction.continuants g (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

theorem GeneralizedContinuedFraction.continuants_recurrence {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K] {gp : GeneralizedContinuedFraction.Pair K} {ppred : GeneralizedContinuedFraction.Pair K} {pred : GeneralizedContinuedFraction.Pair K} (succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp) (nth_conts_eq : GeneralizedContinuedFraction.continuants g n = ppred) (succ_nth_conts_eq : GeneralizedContinuedFraction.continuants g (n + 1) = pred) : GeneralizedContinuedFraction.continuants g (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 GeneralizedContinuedFraction.numerators_recurrence {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K] {gp : GeneralizedContinuedFraction.Pair K} {ppredA : K} {predA : K} (succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp) (nth_num_eq : GeneralizedContinuedFraction.numerators g n = ppredA) (succ_nth_num_eq : GeneralizedContinuedFraction.numerators g (n + 1) = predA) : GeneralizedContinuedFraction.numerators g (n + 2) = gp.b * predA + gp.a * ppredA

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

theorem GeneralizedContinuedFraction.denominators_recurrence {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K] {gp : GeneralizedContinuedFraction.Pair K} {ppredB : K} {predB : K} (succ_nth_s_eq : Stream'.Seq.get? g.s (n + 1) = some gp) (nth_denom_eq : GeneralizedContinuedFraction.denominators g n = ppredB) (succ_nth_denom_eq : GeneralizedContinuedFraction.denominators g (n + 1) = predB) : GeneralizedContinuedFraction.denominators g (n + 2) = gp.b * predB + gp.a * ppredB

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