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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Summary #

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

theorem generalized_continued_fraction.continuants_aux_recurrence {K : Type u_1} {g : generalized_continued_fraction K} {n : ℕ} [division_ring K] {gp ppred pred : generalized_continued_fraction.pair K} (nth_s_eq : g.s.nth n = option.some gp) (nth_conts_aux_eq : g.continuants_aux n = ppred) (succ_nth_conts_aux_eq : 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}

theorem generalized_continued_fraction.continuants_recurrence_aux {K : Type u_1} {g : generalized_continued_fraction K} {n : ℕ} [division_ring K] {gp ppred pred : generalized_continued_fraction.pair K} (nth_s_eq : g.s.nth n = option.some gp) (nth_conts_aux_eq : g.continuants_aux n = ppred) (succ_nth_conts_aux_eq : 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}

theorem generalized_continued_fraction.continuants_recurrence {K : Type u_1} {g : generalized_continued_fraction K} {n : ℕ} [division_ring K] {gp ppred pred : generalized_continued_fraction.pair K} (succ_nth_s_eq : g.s.nth (n + 1) = option.some gp) (nth_conts_eq : g.continuants n = ppred) (succ_nth_conts_eq : 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ₙ₋₂.

theorem generalized_continued_fraction.numerators_recurrence {K : Type u_1} {g : generalized_continued_fraction K} {n : ℕ} [division_ring K] {gp : generalized_continued_fraction.pair K} {ppredA predA : K} (succ_nth_s_eq : g.s.nth (n + 1) = option.some gp) (nth_num_eq : g.numerators n = ppredA) (succ_nth_num_eq : g.numerators (n + 1) = predA) :

g.numerators (n + 2) = gp.b * predA + gp.a * ppredA

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

theorem generalized_continued_fraction.denominators_recurrence {K : Type u_1} {g : generalized_continued_fraction K} {n : ℕ} [division_ring K] {gp : generalized_continued_fraction.pair K} {ppredB predB : K} (succ_nth_s_eq : g.s.nth (n + 1) = option.some gp) (nth_denom_eq : g.denominators n = ppredB) (succ_nth_denom_eq : g.denominators (n + 1) = predB) :

g.denominators (n + 2) = gp.b * predB + gp.a * ppredB

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