Documentation

Mathlib.Algebra.ContinuedFractions.Translations

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.

source
theorem GenContFract.terminatedAt_iff_s_terminatedAt {α : Type u_1} {g : GenContFract α} {n : ℕ} :
g.TerminatedAt n ↔ g.s.TerminatedAt n
source
theorem GenContFract.terminatedAt_iff_s_none {α : Type u_1} {g : GenContFract α} {n : ℕ} :
g.TerminatedAt n ↔ g.s.get? n = none
source
theorem GenContFract.partNum_none_iff_s_none {α : Type u_1} {g : GenContFract α} {n : ℕ} :
g.partNums.get? n = none ↔ g.s.get? n = none
source
theorem GenContFract.terminatedAt_iff_partNum_none {α : Type u_1} {g : GenContFract α} {n : ℕ} :
g.TerminatedAt n ↔ g.partNums.get? n = none
source
theorem GenContFract.partDen_none_iff_s_none {α : Type u_1} {g : GenContFract α} {n : ℕ} :
g.partDens.get? n = none ↔ g.s.get? n = none
source
theorem GenContFract.terminatedAt_iff_partDen_none {α : Type u_1} {g : GenContFract α} {n : ℕ} :
g.TerminatedAt n ↔ g.partDens.get? n = none
source
theorem GenContFract.partNum_eq_s_a {α : Type u_1} {g : GenContFract α} {n : ℕ} {gp : GenContFract.Pair α} (s_nth_eq : g.s.get? n = some gp) :
g.partNums.get? n = some gp.a
source
theorem GenContFract.partDen_eq_s_b {α : Type u_1} {g : GenContFract α} {n : ℕ} {gp : GenContFract.Pair α} (s_nth_eq : g.s.get? n = some gp) :
g.partDens.get? n = some gp.b
source
theorem GenContFract.exists_s_a_of_partNum {α : Type u_1} {g : GenContFract α} {n : ℕ} {a : α} (nth_partNum_eq : g.partNums.get? n = some a) :
∃ (gp : GenContFract.Pair α), g.s.get? n = some gp ∧ gp.a = a
source
theorem GenContFract.exists_s_b_of_partDen {α : Type u_1} {g : GenContFract α} {n : ℕ} {b : α} (nth_partDen_eq : g.partDens.get? n = some b) :
∃ (gp : GenContFract.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.

source
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)
source
theorem GenContFract.num_eq_conts_a {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] :
g.nums n = (g.conts n).a
source
theorem GenContFract.den_eq_conts_b {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] :
g.dens n = (g.conts n).b
source
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
source
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
source
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 : GenContFract.Pair K), g.conts n = conts ∧ conts.a = A
source
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 : GenContFract.Pair K), g.conts n = conts ∧ conts.b = B
source
@[simp]
theorem GenContFract.zeroth_contAux_eq_one_zero {K : Type u_1} {g : GenContFract K} [DivisionRing K] :
g.contsAux 0 = { a := 1, b := 0 }
source
@[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 }
source
@[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 }
source
@[simp]
theorem GenContFract.zeroth_num_eq_h {K : Type u_1} {g : GenContFract K} [DivisionRing K] :
g.nums 0 = g.h
source
@[simp]
theorem GenContFract.zeroth_den_eq_one {K : Type u_1} {g : GenContFract K} [DivisionRing K] :
g.dens 0 = 1
source
@[simp]
theorem GenContFract.zeroth_conv_eq_h {K : Type u_1} {g : GenContFract K} [DivisionRing K] :
g.convs 0 = g.h
source
theorem GenContFract.second_contAux_eq {K : Type u_1} {g : GenContFract K} [DivisionRing K] {gp : GenContFract.Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }
source
theorem GenContFract.first_cont_eq {K : Type u_1} {g : GenContFract K} [DivisionRing K] {gp : GenContFract.Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }
source
theorem GenContFract.first_num_eq {K : Type u_1} {g : GenContFract K} [DivisionRing K] {gp : GenContFract.Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.nums 1 = gp.b * g.h + gp.a
source
theorem GenContFract.first_den_eq {K : Type u_1} {g : GenContFract K} [DivisionRing K] {gp : GenContFract.Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
g.dens 1 = gp.b
source
@[simp]
theorem GenContFract.zeroth_conv'Aux_eq_zero {K : Type u_1} [DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)} :
GenContFract.convs'Aux s 0 = 0
source
@[simp]
theorem GenContFract.zeroth_conv'_eq_h {K : Type u_1} {g : GenContFract K} [DivisionRing K] :
g.convs' 0 = g.h
source
theorem GenContFract.convs'Aux_succ_none {K : Type u_1} [DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)} (h : s.head = none) (n : ℕ) :
GenContFract.convs'Aux s (n + 1) = 0
source
theorem GenContFract.convs'Aux_succ_some {K : Type u_1} [DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)} {p : GenContFract.Pair K} (h : s.head = some p) (n : ℕ) :
GenContFract.convs'Aux s (n + 1) = p.a / (p.b + GenContFract.convs'Aux s.tail n)