# 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.ContinuedFractions.Computation.Basic`

. The file consists
of three sections:

- Recurrences and inversion lemmas for
`IntFractPair.stream`

: these lemmas give us inversion rules and recurrences for the computation of the stream of integer and fractional parts of a value. - 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. - Translation lemmas for the sequence: these lemmas show how the sequences of the involved
structures (
`IntFractPair.stream`

,`IntFractPair.seq1`

, and`GeneralizedContinuedFraction.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 + 1`

th 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 + 1`

th value of the sequence of integer and fractional parts of a value in case of termination.`get?_of_eq_some_of_succ_get?_intFractPair_stream`

and`get?_of_eq_some_of_get?_intFractPair_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 `IntFractPair.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 + 1`

th value of the sequence of integer and fractional
parts of a value in case of termination.

Gives a recurrence to compute the `n + 1`

th value of the sequence of integer and fractional
parts of a value in case of non-termination.

An easier to use version of one direction of
`GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_eq_some_iff`

.

The stream of `IntFractPair`

s of an integer stops after the first term.

A recurrence relation that expresses the `(n+1)`

th term of the stream of `IntFractPair`

s
of `v`

for non-integer `v`

in terms of the `n`

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

The head term of the sequence with head of `v`

is just the integer part of `v`

.

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
(`IntFractPair.stream`

, `IntFractPair.seq1`

, and `GeneralizedContinuedFraction.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 `GeneralizedContinuedFraction.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 `GeneralizedContinuedFraction.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.