mathlib documentation

algebra.continued_fractions.continuants_recurrence

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:

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} :
g.s.nth n = some gpg.continuants_aux n = ppredg.continuants_aux (n + 1) = predg.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} :
g.s.nth n = some gpg.continuants_aux n = ppredg.continuants_aux (n + 1) = predg.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} :
g.s.nth (n + 1) = some gpg.continuants n = ppredg.continuants (n + 1) = predg.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} :
g.s.nth (n + 1) = some gpg.numerators n = ppredAg.numerators (n + 1) = predAg.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} :
g.s.nth (n + 1) = some gpg.denominators n = ppredBg.denominators (n + 1) = predBg.denominators (n + 2) = (gp.b) * predB + (gp.a) * ppredB

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