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 : GenContFract α} {n : ℕ} : g.TerminatedAt n ↔ g.s.TerminatedAt n

theorem GenContFract.terminatedAt_iff_s_none {α : Type u_1} {g : GenContFract α} {n : ℕ} : g.TerminatedAt n ↔ g.s.get? n = none

theorem GenContFract.partNum_none_iff_s_none {α : Type u_1} {g : GenContFract α} {n : ℕ} : g.partNums.get? n = none ↔ g.s.get? n = none

theorem GenContFract.terminatedAt_iff_partNum_none {α : Type u_1} {g : GenContFract α} {n : ℕ} : g.TerminatedAt n ↔ g.partNums.get? n = none

theorem GenContFract.partDen_none_iff_s_none {α : Type u_1} {g : GenContFract α} {n : ℕ} : g.partDens.get? n = none ↔ g.s.get? n = none

theorem GenContFract.terminatedAt_iff_partDen_none {α : Type u_1} {g : GenContFract α} {n : ℕ} : g.TerminatedAt n ↔ g.partDens.get? n = none

theorem GenContFract.partNum_eq_s_a {α : Type u_1} {g : GenContFract α} {n : ℕ} {gp : Pair α} (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 : GenContFract α} {n : ℕ} {gp : Pair α} (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 : GenContFract α} {n : ℕ} {a : α} (nth_partNum_eq : g.partNums.get? n = some a) : ∃ (gp : Pair α), g.s.get? n = some gp ∧ gp.a = a

theorem GenContFract.exists_s_b_of_partDen {α : Type u_1} {g : GenContFract α} {n : ℕ} {b : α} (nth_partDen_eq : g.partDens.get? n = some b) : ∃ (gp : Pair α), 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 : GenContFract K} {n : ℕ} [DivisionRing K] : g.conts n = g.contsAux (n + 1)

theorem GenContFract.num_eq_conts_a {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] : g.nums n = (g.conts n).a

theorem GenContFract.den_eq_conts_b {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] : g.dens n = (g.conts n).b

theorem GenContFract.conv_eq_num_div_den {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] : g.convs n = g.nums n / g.dens n

theorem GenContFract.conv_eq_conts_a_div_conts_b {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] : g.convs n = (g.conts n).a / (g.conts n).b

theorem GenContFract.exists_conts_a_of_num {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] {A : K} (nth_num_eq : g.nums n = A) : ∃ (conts : Pair K), g.conts n = conts ∧ conts.a = A

theorem GenContFract.exists_conts_b_of_den {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] {B : K} (nth_denom_eq : g.dens n = B) : ∃ (conts : Pair K), g.conts n = conts ∧ conts.b = B

@[simp]

theorem GenContFract.zeroth_contAux_eq_one_zero {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.contsAux 0 = { a := 1, b := 0 }

@[simp]

theorem GenContFract.first_contAux_eq_h_one {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.contsAux 1 = { a := g.h, b := 1 }

@[simp]

theorem GenContFract.zeroth_cont_eq_h_one {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.conts 0 = { a := g.h, b := 1 }

@[simp]

theorem GenContFract.zeroth_num_eq_h {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.nums 0 = g.h

@[simp]

theorem GenContFract.zeroth_den_eq_one {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.dens 0 = 1

@[simp]

theorem GenContFract.zeroth_conv_eq_h {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.convs 0 = g.h

theorem GenContFract.second_contAux_eq {K : Type u_1} {g : GenContFract K} [DivisionRing K] {gp : Pair K} (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 : GenContFract K} [DivisionRing K] {gp : Pair K} (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 : GenContFract K} [DivisionRing K] {gp : Pair K} (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 : GenContFract K} [DivisionRing K] {gp : Pair K} (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} [DivisionRing K] {s : Stream'.Seq (Pair K)} : convs'Aux s 0 = 0

@[simp]

theorem GenContFract.zeroth_conv'_eq_h {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.convs' 0 = g.h

theorem GenContFract.convs'Aux_succ_none {K : Type u_1} [DivisionRing K] {s : Stream'.Seq (Pair K)} (h : s.head = none) (n : ℕ) : convs'Aux s (n + 1) = 0

theorem GenContFract.convs'Aux_succ_some {K : Type u_1} [DivisionRing K] {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p) (n : ℕ) : convs'Aux s (n + 1) = p.a / (p.b + convs'Aux s.tail n)