mathlib3 documentation

algebra.continued_fractions.computation.translations

Basic Translation Lemmas Between Structures Defined for Computing Continued Fractions #

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

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.

The stream of int_fract_pairs of an integer stops after the first term.

A recurrence relation that expresses the (n+1)th term of the stream of int_fract_pairs of v for non-integer v in terms of the nth term of the stream associated to the inverse of the fractional part of v.

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.

This gives the first pair of coefficients of the continued fraction of a non-integer v.

If a is an integer, then the coefficient sequence of its continued fraction is empty.

Recurrence for the generalized_continued_fraction.of an element v of K in terms of that of the inverse of the fractional part of v.

This expresses the tail of the coefficient sequence of the generalized_continued_fraction.of an element v of K as the coefficient sequence of that of the inverse of the fractional part of v.

If a is an integer, then the convergents' of its continued fraction expansion are all equal to a.

The recurrence relation for the convergents' of the continued fraction expansion of an element v of K in terms of the convergents of the inverse of its fractional part.