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

) #

## Summary #

We show the correctness of the algorithm computing continued fractions (`GenContFract.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 `(GenContFract.of v).convs' 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 `GenContFract.IntFractPair.stream v n`

.

For an example, refer to
`GenContFract.compExactValue_correctness_of_stream_eq_some`

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

.

## Main definitions #

`GenContFract.compExactValue`

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

by adding a residual term as described in the summary.

## Main Theorems #

`GenContFract.compExactValue_correctness_of_stream_eq_some`

shows that`GenContFract.compExactValue`

indeed returns the value`v`

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

shows the equality`v = (GenContFract.of v).convs n`

if`GenContFract.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`

`exactConts.a / exactConts.b`

where`exactConts = nextConts 1 fr⁻¹ pconts conts`

otherwise.

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

as described in lemma `compExactValue_correctness_of_stream_eq_some`

.

## Equations

- GenContFract.compExactValue pconts conts fr = if fr = 0 then conts.a / conts.b else let exactConts := GenContFract.nextConts 1 fr⁻¹ pconts conts; exactConts.a / exactConts.b

## Instances For

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

Shows the correctness of `compExactValue`

in case the continued fraction
`GenContFract.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 `convs'`

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

Let `(v : ℚ) := 3.4`

. We have

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

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

. Now`(GenContFract.of v).convs' 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 `GenContFract.of v`

at step `n - 1`

is exactly `v`

if the
`IntFractPair.stream`

of the corresponding continued fraction terminated at step `n`

.

If `GenContFract.of v`

terminated at step `n`

, then the `n`

th convergent is exactly `v`

.

If `GenContFract.of v`

terminates, then there is `n : ℕ`

such that the `n`

th convergent is
exactly `v`

.

If `GenContFract.of v`

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

.