mathlib documentation


Correctness of Terminating Continued Fraction Computations (gcf.of)


Let us write gcf for generalized_continued_fraction. We show the correctness of the algorithm computing continued fractions (gcf.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 (gcf.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 v n.

For an example, refer to gcf.comp_exact_value_correctness_of_stream_eq_some and for more information about the computation process, refer to algebra.continued_fraction.computation.basic.

Main definitions

Main Theorems

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 = next_continuants 1 fr⁻¹ pconts conts otherwise.

This function can be used to compute the exact value approxmated by a continued fraction gcf.of v as described in lemma comp_exact_value_correctness_of_stream_eq_some.


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

Shows the correctness of comp_exact_value in case the continued fraction gcf.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 n to comp_exact_value.

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

  • v 0 = some ⟨3, 0.4⟩, and
  • v 1 = some ⟨2, 0.5⟩. Now (gcf.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 comp_exact_value.

The convergent of gcf.of v at step n - 1 is exactly v if the of the corresponding continued fraction terminated at step n.

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

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

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