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.

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.

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.