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 : ℕ} :
g.terminated_at n ↔ g.s.nth n = option.none
theorem
generalized_continued_fraction.part_num_none_iff_s_none
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
g.partial_numerators.nth n = option.none ↔ g.s.nth n = option.none
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 = option.none
theorem
generalized_continued_fraction.part_denom_none_iff_s_none
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ} :
g.partial_denominators.nth n = option.none ↔ g.s.nth n = option.none
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 = option.none
theorem
generalized_continued_fraction.part_num_eq_s_a
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ}
{gp : generalized_continued_fraction.pair α} :
g.s.nth n = option.some gp → g.partial_numerators.nth n = option.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 α} :
g.s.nth n = option.some gp → g.partial_denominators.nth n = option.some gp.b
theorem
generalized_continued_fraction.exists_s_a_of_part_num
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ}
{a : α} :
g.partial_numerators.nth n = option.some a → (∃ (gp : generalized_continued_fraction.pair α), g.s.nth n = option.some gp ∧ gp.a = a)
theorem
generalized_continued_fraction.exists_s_b_of_part_denom
{α : Type u_1}
{g : generalized_continued_fraction α}
{n : ℕ}
{b : α} :
g.partial_denominators.nth n = option.some b → (∃ (gp : generalized_continued_fraction.pair α), g.s.nth n = option.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.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} :
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} :
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} :
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} :
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} :
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} :
g.s.nth 0 = option.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