# mathlibdocumentation

algebra.continued_fractions.computation.translations

# Basic Translation Lemmas Between Structures Defined for Computing Continued Fractions #

## Summary #

This is a collection of simple lemmas between the different structures used for the computation of continued fractions defined in algebra.continued_fractions.computation.basic. The file consists of three sections:

1. Recurrences and inversion lemmas for int_fract_pair.stream: these lemmas give us inversion rules and recurrences for the computation of the stream of integer and fractional parts of a value.
2. Translation lemmas for the head term: these lemmas show us that the head term of the computed continued fraction of a value v is ⌊v⌋ and how this head term is moved along the structures used in the computation process.
3. Translation lemmas for the sequence: these lemmas show how the sequences of the involved structures (int_fract_pair.stream, int_fract_pair.seq1, and generalized_continued_fraction.of) are connected, i.e. how the values are moved along the structures and the termination of one sequence implies the termination of another sequence.

## Main Theorems #

• succ_nth_stream_eq_some_iff gives as a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of non-termination.
• succ_nth_stream_eq_none_iff gives as a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of termination.
• nth_of_eq_some_of_succ_nth_int_fract_pair_stream and nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero show how the entries of the sequence of the computed continued fraction can be obtained from the stream of integer and fractional parts.

### Recurrences and Inversion Lemmas for int_fract_pair.stream#

Here we state some lemmas that give us inversion rules and recurrences for the computation of the stream of integer and fractional parts of a value.

theorem generalized_continued_fraction.int_fract_pair.stream_eq_none_of_fr_eq_zero {K : Type u_1} [floor_ring K] {v : K} {n : } (stream_nth_eq : = option.some ifp_n) (nth_fr_eq_zero : ifp_n.fr = 0) :

Gives a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of termination.

theorem generalized_continued_fraction.int_fract_pair.succ_nth_stream_eq_some_iff {K : Type u_1} [floor_ring K] {v : K} {n : } {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} :
= option.some ifp_succ_n ∃ (ifp_n : , ifp_n.fr 0 = ifp_succ_n

Gives a recurrence to compute the n + 1th value of the sequence of integer and fractional parts of a value in case of non-termination.

theorem generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_fr_zero {K : Type u_1} [floor_ring K] {v : K} {n : } {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (stream_succ_nth_eq : = option.some ifp_succ_n) (succ_nth_fr_eq_zero : ifp_succ_n.fr = 0) :
∃ (ifp_n : , (ifp_n.fr)⁻¹ = (ifp_n.fr)⁻¹

### Translation of the Head Term #

Here we state some lemmas that show us that the head term of the computed continued fraction of a value v is ⌊v⌋ and how this head term is moved along the structures used in the computation process.

@[simp]

The head term of the sequence with head of v is just the integer part of v.

@[simp]
theorem generalized_continued_fraction.of_h_eq_floor {K : Type u_1} [floor_ring K] {v : K} :

The head term of the gcf of v is ⌊v⌋.

### Translation of the Sequences #

Here we state some lemmas that show how the sequences of the involved structures (int_fract_pair.stream, int_fract_pair.seq1, and generalized_continued_fraction.of) are connected, i.e. how the values are moved along the structures and how the termination of one sequence implies the termination of another sequence.

#### Translation of the Termination of the Sequences #

Let's first show how the termination of one sequence implies the termination of another sequence.

#### Translation of the Values of the Sequence #

Now let's show how the values of the sequences correspond to one another.

theorem generalized_continued_fraction.nth_of_eq_some_of_succ_nth_int_fract_pair_stream {K : Type u_1} [floor_ring K] {v : K} {n : } {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (stream_succ_nth_eq : = option.some ifp_succ_n) :
= option.some {a := 1, b := (ifp_succ_n.b)}

Shows how the entries of the sequence of the computed continued fraction can be obtained by the integer parts of the stream of integer and fractional parts.

theorem generalized_continued_fraction.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero {K : Type u_1} [floor_ring K] {v : K} {n : } (stream_nth_eq : = option.some ifp_n) (nth_fr_ne_zero : ifp_n.fr 0) :
= option.some {a := 1, b := .b)}

Shows how the entries of the sequence of the computed continued fraction can be obtained by the fractional parts of the stream of integer and fractional parts.