mathlib documentation

algebra.continued_fractions.translations

Basic Translation Lemmas Between Functions Defined for Continued Fractions #

Summary #

Some simple translation lemmas between the different definitions of functions defined in algebra.continued_fractions.basic.

Translations Between General Access Functions #

Here we give some basic translations that hold by definition between the various methods that allow us to access the numerators and denominators of a continued fraction.

theorem generalized_continued_fraction.exists_s_a_of_part_num {α : Type u_1} {g : generalized_continued_fraction α} {n : } {a : α} (nth_part_num_eq : g.partial_numerators.nth n = some a) :
∃ (gp : generalized_continued_fraction.pair α), g.s.nth n = some gp gp.a = a
theorem generalized_continued_fraction.exists_s_b_of_part_denom {α : Type u_1} {g : generalized_continued_fraction α} {n : } {b : α} (nth_part_denom_eq : g.partial_denominators.nth n = some b) :
∃ (gp : generalized_continued_fraction.pair α), g.s.nth n = some gp gp.b = b

Translations Between Computational Functions #

Here we give some basic translations that hold by definition for the computational methods of a continued fraction.

theorem generalized_continued_fraction.exists_conts_a_of_num {K : Type u_1} {g : generalized_continued_fraction K} {n : } [division_ring K] {A : K} (nth_num_eq : g.numerators n = A) :
∃ (conts : generalized_continued_fraction.pair K), g.continuants n = conts conts.a = A
theorem generalized_continued_fraction.exists_conts_b_of_denom {K : Type u_1} {g : generalized_continued_fraction K} {n : } [division_ring K] {B : K} (nth_denom_eq : g.denominators n = B) :
∃ (conts : generalized_continued_fraction.pair K), g.continuants n = conts conts.b = B
theorem generalized_continued_fraction.first_continuant_eq {K : Type u_1} {g : generalized_continued_fraction K} [division_ring K] {gp : generalized_continued_fraction.pair K} (zeroth_s_eq : g.s.nth 0 = some gp) :
g.continuants 1 = {a := (gp.b) * g.h + gp.a, b := gp.b}