# Correctness of Terminating Continued Fraction Computations (`GeneralizedContinuedFraction.of`

) #

## Summary #

We show the correctness of the
algorithm computing continued fractions (`GeneralizedContinuedFraction.of`

) in case of termination
in the following sense:

At every step `n : ℕ`

, we can obtain the value `v`

by adding a specific residual term to the last
denominator of the fraction described by `(GeneralizedContinuedFraction.of v).convergents' n`

.
The residual term will be zero exactly when the continued fraction terminated; otherwise, the
residual term will be given by the fractional part stored in
`GeneralizedContinuedFraction.IntFractPair.stream v n`

.

For an example, refer to
`GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some`

and for more
information about the computation process, refer to `Algebra.ContinuedFractions.Computation.Basic`

.

## Main definitions #

`GeneralizedContinuedFraction.compExactValue`

can be used to compute the exact value approximated by the continued fraction`GeneralizedContinuedFraction.of v`

by adding a residual term as described in the summary.

## Main Theorems #

`GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some`

shows that`GeneralizedContinuedFraction.compExactValue`

indeed returns the value`v`

when given the convergent and fractional part as described in the summary.`GeneralizedContinuedFraction.of_correctness_of_terminatedAt`

shows the equality`v = (GeneralizedContinuedFraction.of v).convergents n`

if`GeneralizedContinuedFraction.of v`

terminated at position`n`

.

Given two continuants `pconts`

and `conts`

and a value `fr`

, this function returns

`conts.a / conts.b`

if`fr = 0`

`exact_conts.a / exact_conts.b`

where`exact_conts = nextContinuants 1 fr⁻¹ pconts conts`

otherwise.

This function can be used to compute the exact value approximated by a continued fraction
`GeneralizedContinuedFraction.of v`

as described in lemma
`compExactValue_correctness_of_stream_eq_some`

.

## Instances For

Just a computational lemma we need for the next main proof.

Shows the correctness of `compExactValue`

in case the continued fraction
`GeneralizedContinuedFraction.of v`

did not terminate at position `n`

. That is, we obtain the
value `v`

if we pass the two successive (auxiliary) continuants at positions `n`

and `n + 1`

as well
as the fractional part at `IntFractPair.stream n`

to `compExactValue`

.

The correctness might be seen more readily if one uses `convergents'`

to evaluate the continued
fraction. Here is an example to illustrate the idea:

Let `(v : ℚ) := 3.4`

. We have

`GeneralizedContinuedFraction.IntFractPair.stream v 0 = some ⟨3, 0.4⟩`

, and`GeneralizedContinuedFraction.IntFractPair.stream v 1 = some ⟨2, 0.5⟩`

. Now`(GeneralizedContinuedFraction.of v).convergents' 1 = 3 + 1/2`

, and our fractional term at position`2`

is`0.5`

. We hence have`v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4`

. This computation corresponds exactly to the one using the recurrence equation in`compExactValue`

.

The convergent of `GeneralizedContinuedFraction.of v`

at step `n - 1`

is exactly `v`

if the
`IntFractPair.stream`

of the corresponding continued fraction terminated at step `n`

.

If `GeneralizedContinuedFraction.of v`

terminated at step `n`

, then the `n`

th convergent is
exactly `v`

.

If `GeneralizedContinuedFraction.of v`

terminates, then there is `n : ℕ`

such that the `n`

th
convergent is exactly `v`

.

If `GeneralizedContinuedFraction.of v`

terminates, then its convergents will eventually always
be `v`

.