# Basic Translation Lemmas Between Functions Defined for Continued Fractions #

## Summary #

Some simple translation lemmas between the different definitions of functions defined in Algebra.ContinuedFractions.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 GenContFract.terminatedAt_iff_s_terminatedAt {α : Type u_1} {g : } {n : } :
g.TerminatedAt n g.s.TerminatedAt n
theorem GenContFract.terminatedAt_iff_s_none {α : Type u_1} {g : } {n : } :
g.TerminatedAt n g.s.get? n = none
theorem GenContFract.partNum_none_iff_s_none {α : Type u_1} {g : } {n : } :
g.partNums.get? n = none g.s.get? n = none
theorem GenContFract.terminatedAt_iff_partNum_none {α : Type u_1} {g : } {n : } :
g.TerminatedAt n g.partNums.get? n = none
theorem GenContFract.partDen_none_iff_s_none {α : Type u_1} {g : } {n : } :
g.partDens.get? n = none g.s.get? n = none
theorem GenContFract.terminatedAt_iff_partDen_none {α : Type u_1} {g : } {n : } :
g.TerminatedAt n g.partDens.get? n = none
theorem GenContFract.partNum_eq_s_a {α : Type u_1} {g : } {n : } {gp : } (s_nth_eq : g.s.get? n = some gp) :
g.partNums.get? n = some gp.a
theorem GenContFract.partDen_eq_s_b {α : Type u_1} {g : } {n : } {gp : } (s_nth_eq : g.s.get? n = some gp) :
g.partDens.get? n = some gp.b
theorem GenContFract.exists_s_a_of_partNum {α : Type u_1} {g : } {n : } {a : α} (nth_partNum_eq : g.partNums.get? n = some a) :
∃ (gp : ), g.s.get? n = some gp gp.a = a
theorem GenContFract.exists_s_b_of_partDen {α : Type u_1} {g : } {n : } {b : α} (nth_partDen_eq : g.partDens.get? n = some b) :
∃ (gp : ), g.s.get? 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 GenContFract.nth_cont_eq_succ_nth_contAux {K : Type u_1} {g : } {n : } [] :
g.conts n = g.contsAux (n + 1)
theorem GenContFract.num_eq_conts_a {K : Type u_1} {g : } {n : } [] :
g.nums n = (g.conts n).a
theorem GenContFract.den_eq_conts_b {K : Type u_1} {g : } {n : } [] :
g.dens n = (g.conts n).b
theorem GenContFract.conv_eq_num_div_den {K : Type u_1} {g : } {n : } [] :
g.convs n = g.nums n / g.dens n
theorem GenContFract.conv_eq_conts_a_div_conts_b {K : Type u_1} {g : } {n : } [] :
g.convs n = (g.conts n).a / (g.conts n).b
theorem GenContFract.exists_conts_a_of_num {K : Type u_1} {g : } {n : } [] {A : K} (nth_num_eq : g.nums n = A) :
∃ (conts : ), g.conts n = conts conts.a = A
theorem GenContFract.exists_conts_b_of_den {K : Type u_1} {g : } {n : } [] {B : K} (nth_denom_eq : g.dens n = B) :
∃ (conts : ), g.conts n = conts conts.b = B
@[simp]
theorem GenContFract.zeroth_contAux_eq_one_zero {K : Type u_1} {g : } [] :
g.contsAux 0 = { a := 1, b := 0 }
@[simp]
theorem GenContFract.first_contAux_eq_h_one {K : Type u_1} {g : } [] :
g.contsAux 1 = { a := g.h, b := 1 }
@[simp]
theorem GenContFract.zeroth_cont_eq_h_one {K : Type u_1} {g : } [] :
g.conts 0 = { a := g.h, b := 1 }
@[simp]
theorem GenContFract.zeroth_num_eq_h {K : Type u_1} {g : } [] :
g.nums 0 = g.h
@[simp]
theorem GenContFract.zeroth_den_eq_one {K : Type u_1} {g : } [] :
g.dens 0 = 1
@[simp]
theorem GenContFract.zeroth_conv_eq_h {K : Type u_1} {g : } [] :
g.convs 0 = g.h
theorem GenContFract.second_contAux_eq {K : Type u_1} {g : } [] {gp : } (zeroth_s_eq : g.s.get? 0 = some gp) :
g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }
theorem GenContFract.first_cont_eq {K : Type u_1} {g : } [] {gp : } (zeroth_s_eq : g.s.get? 0 = some gp) :
g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }
theorem GenContFract.first_num_eq {K : Type u_1} {g : } [] {gp : } (zeroth_s_eq : g.s.get? 0 = some gp) :
g.nums 1 = gp.b * g.h + gp.a
theorem GenContFract.first_den_eq {K : Type u_1} {g : } [] {gp : } (zeroth_s_eq : g.s.get? 0 = some gp) :
g.dens 1 = gp.b
@[simp]
theorem GenContFract.zeroth_conv'Aux_eq_zero {K : Type u_1} [] {s : } :
@[simp]
theorem GenContFract.zeroth_conv'_eq_h {K : Type u_1} {g : } [] :
g.convs' 0 = g.h
theorem GenContFract.convs'Aux_succ_none {K : Type u_1} [] {s : } (h : s.head = none) (n : ) :
theorem GenContFract.convs'Aux_succ_some {K : Type u_1} [] {s : } {p : } (h : s.head = some p) (n : ) :
GenContFract.convs'Aux s (n + 1) = p.a / (p.b + GenContFract.convs'Aux s.tail n)