# Equivalence of Recursive and Direct Computations of `GCF`

Convergents #

## Summary #

We show the equivalence of two computations of convergents (recurrence relation (`convergents`

) vs.
direct evaluation (`convergents'`

)) for `GCF`

s on linear ordered fields. We follow the proof from
[hardy2008introduction], Chapter 10. Here's a sketch:

Let `c`

be a continued fraction `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`

, visually:
$$
c = h + \dfrac{a_0}
{b_0 + \dfrac{a_1}
{b_1 + \dfrac{a_2}
{b_2 + \dfrac{a_3}
{b_3 + \dots}}}}
$$
One can compute the convergents of `c`

in two ways:

- Directly evaluating the fraction described by
`c`

up to a given`n`

(`convergents'`

) - Using the recurrence (
`convergents`

):

`A₋₁ = 1, A₀ = h, Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂`

, and`B₋₁ = 0, B₀ = 1, Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂`

.

To show the equivalence of the computations in the main theorem of this file
`convergents_eq_convergents'`

, we proceed by induction. The case `n = 0`

is trivial.

For `n + 1`

, we first "squash" the `n + 1`

th position of `c`

into the `n`

th position to obtain
another continued fraction
`c' := [h; (a₀, b₀),..., (aₙ-₁, bₙ-₁), (aₙ, bₙ + aₙ₊₁ / bₙ₊₁), (aₙ₊₁, bₙ₊₁),...]`

.
This squashing process is formalised in section `Squash`

. Note that directly evaluating `c`

up to
position `n + 1`

is equal to evaluating `c'`

up to `n`

. This is shown in lemma
`succ_nth_convergent'_eq_squashGCF_nth_convergent'`

.

By the inductive hypothesis, the two computations for the `n`

th convergent of `c`

coincide.
So all that is left to show is that the recurrence relation for `c`

at `n + 1`

and `c'`

at
`n`

coincide. This can be shown by another induction.
The corresponding lemma in this file is `succ_nth_convergent_eq_squashGCF_nth_convergent`

.

## Main Theorems #

`GeneralizedContinuedFraction.convergents_eq_convergents'`

shows the equivalence under a strict positivity restriction on the sequence.`continued_fractions.convergents_eq_convergents'`

shows the equivalence for (regular) continued fractions.

## References #

- https://en.wikipedia.org/wiki/Generalized_continued_fraction
- [
*Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph*][hardy2008introduction]

## Tags #

fractions, recurrence, equivalence

We will show the equivalence of the computations by induction. To make the induction work, we need
to be able to *squash* the nth and (n + 1)th value of a sequence. This squashing itself and the
lemmas about it are not very interesting. As a reader, you hence might want to skip this section.

Given a sequence of `GCF.Pair`

s `s = [(a₀, bₒ), (a₁, b₁), ...]`

, `squashSeq s n`

combines `⟨aₙ, bₙ⟩`

and `⟨aₙ₊₁, bₙ₊₁⟩`

at position `n`

to `⟨aₙ, bₙ + aₙ₊₁ / bₙ₊₁⟩`

. For example,
`squashSeq s 0 = [(a₀, bₒ + a₁ / b₁), (a₁, b₁),...]`

.
If `s.TerminatedAt (n + 1)`

, then `squashSeq s n = s`

.

## Instances For

We now prove some simple lemmas about the squashed sequence

If the sequence already terminated at position `n + 1`

, nothing gets squashed.

If the sequence has not terminated before position `n + 1`

, the value at `n + 1`

gets
squashed into position `n`

.

The values before the squashed position stay the same.

Squashing at position `n + 1`

and taking the tail is the same as squashing the tail of the
sequence at position `n`

.

The auxiliary function `convergents'Aux`

returns the same value for a sequence and the
corresponding squashed sequence at the squashed position.

Let us now lift the squashing operation to gcfs.

Given a gcf `g = [h; (a₀, bₒ), (a₁, b₁), ...]`

, we have

## Instances For

Again, we derive some simple lemmas that are not really of interest. This time for the squashed gcf.

If the gcf already terminated at position `n`

, nothing gets squashed.

The values before the squashed position stay the same.

`convergents'`

returns the same value for a gcf and the corresponding squashed gcf at the
squashed position.

The auxiliary continuants before the squashed position stay the same.

The convergents coincide in the expected way at the squashed position if the partial denominator at the squashed position is not zero.

Shows that the recurrence relation (`convergents`

) and direct evaluation (`convergents'`

) of the
gcf coincide at position `n`

if the sequence of fractions contains strictly positive values only.
Requiring positivity of all values is just one possible condition to obtain this result.
For example, the dual - sequences with strictly negative values only - would also work.

In practice, one most commonly deals with (regular) continued fractions, which satisfy the
positivity criterion required here. The analogous result for them
(see `ContinuedFractions.convergents_eq_convergents`

) hence follows directly from this theorem.

Shows that the recurrence relation (`convergents`

) and direct evaluation (`convergents'`

) of a
(regular) continued fraction coincide.