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.

def GenContFract.compExactValue {K : Type u_1} [LinearOrderedField K] (pconts : GenContFract.Pair K) (conts : GenContFract.Pair K) (fr : K) : K

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

theorem GenContFract.compExactValue_correctness_of_stream_eq_some_aux_comp {K : Type u_1} [LinearOrderedField K] [FloorRing K] {a : K} (b : K) (c : K) (fract_a_ne_zero : Int.fract a ≠ 0) : (↑⌊a⌋ * b + c) / Int.fract a + b = (b * a + c) / Int.fract a

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

theorem GenContFract.compExactValue_correctness_of_stream_eq_some {K : Type u_1} [LinearOrderedField K] {v : K} {n : ℕ} [FloorRing K] {ifp_n : GenContFract.IntFractPair K} : GenContFract.IntFractPair.stream v n = some ifp_n → v = GenContFract.compExactValue ((GenContFract.of v).contsAux n) ((GenContFract.of v).contsAux (n + 1)) ifp_n.fr

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.

theorem GenContFract.of_correctness_of_nth_stream_eq_none {K : Type u_1} [LinearOrderedField K] {v : K} {n : ℕ} [FloorRing K] (nth_stream_eq_none : GenContFract.IntFractPair.stream v n = none) : v = (GenContFract.of v).convs (n - 1)

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.

theorem GenContFract.of_correctness_of_terminatedAt {K : Type u_1} [LinearOrderedField K] {v : K} {n : ℕ} [FloorRing K] (terminatedAt_n : (GenContFract.of v).TerminatedAt n) : v = (GenContFract.of v).convs n

If GenContFract.of v terminated at step n, then the nth convergent is exactly v.

theorem GenContFract.of_correctness_of_terminates {K : Type u_1} [LinearOrderedField K] {v : K} [FloorRing K] (terminates : (GenContFract.of v).Terminates) : ∃ (n : ℕ), v = (GenContFract.of v).convs n

If GenContFract.of v terminates, then there is n : ℕ such that the nth convergent is exactly v.

theorem GenContFract.of_correctness_atTop_of_terminates {K : Type u_1} [LinearOrderedField K] {v : K} [FloorRing K] (terminates : (GenContFract.of v).Terminates) : ∀ᶠ (n : ℕ) in Filter.atTop, v = (GenContFract.of v).convs n

If GenContFract.of v terminates, then its convergents will eventually always be v.