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.terminated_at_iff_s_terminated_at
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
g.terminated_at n ↔ g.s.terminated_at n
theorem
generalized_continued_fraction.terminated_at_iff_s_none
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
theorem
generalized_continued_fraction.part_num_none_iff_s_none
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
theorem
generalized_continued_fraction.terminated_at_iff_part_num_none
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
g.terminated_at n ↔ g.partial_numerators.nth n = none
theorem
generalized_continued_fraction.part_denom_none_iff_s_none
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
theorem
generalized_continued_fraction.terminated_at_iff_part_denom_none
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
g.terminated_at n ↔ g.partial_denominators.nth n = none
theorem
generalized_continued_fraction.part_num_eq_s_a
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ}
{gp : generalized_continued_fraction.pair α}
(s_nth_eq : g.s.nth n = some gp) :
g.partial_numerators.nth n = some gp.a
theorem
generalized_continued_fraction.part_denom_eq_s_b
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ}
{gp : generalized_continued_fraction.pair α}
(s_nth_eq : g.s.nth n = some gp) :
g.partial_denominators.nth n = some gp.b
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) :
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) :
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.nth_cont_eq_succ_nth_cont_aux
{K : Type u_1}
{g : generalized_continued_fraction K}
{n : ℕ}
[division_ring K] :
g.continuants n = g.continuants_aux (n + 1)
theorem
generalized_continued_fraction.num_eq_conts_a
{K : Type u_1}
{g : generalized_continued_fraction K}
{n : ℕ}
[division_ring K] :
g.numerators n = (g.continuants n).a
theorem
generalized_continued_fraction.denom_eq_conts_b
{K : Type u_1}
{g : generalized_continued_fraction K}
{n : ℕ}
[division_ring K] :
g.denominators n = (g.continuants n).b
theorem
generalized_continued_fraction.convergent_eq_num_div_denom
{K : Type u_1}
{g : generalized_continued_fraction K}
{n : ℕ}
[division_ring K] :
g.convergents n = g.numerators n / g.denominators n
theorem
generalized_continued_fraction.convergent_eq_conts_a_div_conts_b
{K : Type u_1}
{g : generalized_continued_fraction K}
{n : ℕ}
[division_ring K] :
g.convergents n = (g.continuants n).a / (g.continuants n).b
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
@[simp]
theorem
generalized_continued_fraction.zeroth_continuant_aux_eq_one_zero
{K : Type u_1}
{g : generalized_continued_fraction K}
[division_ring K] :
g.continuants_aux 0 = {a := 1, b := 0}
@[simp]
theorem
generalized_continued_fraction.first_continuant_aux_eq_h_one
{K : Type u_1}
{g : generalized_continued_fraction K}
[division_ring K] :
@[simp]
theorem
generalized_continued_fraction.zeroth_continuant_eq_h_one
{K : Type u_1}
{g : generalized_continued_fraction K}
[division_ring K] :
@[simp]
theorem
generalized_continued_fraction.zeroth_numerator_eq_h
{K : Type u_1}
{g : generalized_continued_fraction K}
[division_ring K] :
g.numerators 0 = g.h
@[simp]
theorem
generalized_continued_fraction.zeroth_denominator_eq_one
{K : Type u_1}
{g : generalized_continued_fraction K}
[division_ring K] :
g.denominators 0 = 1
@[simp]
theorem
generalized_continued_fraction.zeroth_convergent_eq_h
{K : Type u_1}
{g : generalized_continued_fraction K}
[division_ring K] :
g.convergents 0 = g.h
theorem
generalized_continued_fraction.second_continuant_aux_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) :
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) :
theorem
generalized_continued_fraction.first_numerator_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) :
theorem
generalized_continued_fraction.first_denominator_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.denominators 1 = gp.b
@[simp]
theorem
generalized_continued_fraction.zeroth_convergent'_aux_eq_zero
{K : Type u_1}
[division_ring K]
{s : seq (generalized_continued_fraction.pair K)} :
@[simp]
theorem
generalized_continued_fraction.zeroth_convergent'_eq_h
{K : Type u_1}
{g : generalized_continued_fraction K}
[division_ring K] :
g.convergents' 0 = g.h