mathlib documentation

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 #

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.

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.

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]

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.

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.

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.