Basic Translation Lemmas Between Functions Defined for Continued Fractions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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 = option.some gp) :

g.partial_numerators.nth n = option.some gp.a

source

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 = option.some gp) :

g.partial_denominators.nth n = option.some gp.b

source

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 = option.some a) :

∃ (gp : generalized_continued_fraction.pair α), g.s.nth n = option.some gp ∧ gp.a = a

source

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 = 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.

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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}

source

@[simp]

theorem generalized_continued_fraction.first_continuant_aux_eq_h_one {K : Type u_1} {g : generalized_continued_fraction K} [division_ring K] :

g.continuants_aux 1 = {a := g.h, b := 1}

source

@[simp]

theorem generalized_continued_fraction.zeroth_continuant_eq_h_one {K : Type u_1} {g : generalized_continued_fraction K} [division_ring K] :

g.continuants 0 = {a := g.h, b := 1}

source

@[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

source

@[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

source

@[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

source

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 = option.some gp) :

g.continuants_aux 2 = {a := gp.b * g.h + gp.a, b := gp.b}

source

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 = option.some gp) :

g.continuants 1 = {a := gp.b * g.h + gp.a, b := gp.b}

source

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 = option.some gp) :

g.numerators 1 = gp.b * g.h + gp.a

source

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 = option.some gp) :

g.denominators 1 = gp.b

source

@[simp]

theorem generalized_continued_fraction.zeroth_convergent'_aux_eq_zero {K : Type u_1} [division_ring K] {s : stream.seq (generalized_continued_fraction.pair K)} :

generalized_continued_fraction.convergents'_aux s 0 = 0

source

@[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

source

theorem generalized_continued_fraction.convergents'_aux_succ_none {K : Type u_1} [division_ring K] {s : stream.seq (generalized_continued_fraction.pair K)} (h : s.head = option.none) (n : ℕ) :

generalized_continued_fraction.convergents'_aux s (n + 1) = 0

source

theorem generalized_continued_fraction.convergents'_aux_succ_some {K : Type u_1} [division_ring K] {s : stream.seq (generalized_continued_fraction.pair K)} {p : generalized_continued_fraction.pair K} (h : s.head = option.some p) (n : ℕ) :

generalized_continued_fraction.convergents'_aux s (n + 1) = p.a / (p.b + generalized_continued_fraction.convergents'_aux s.tail n)