Termination of Continued Fraction Computations (
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We show that the continued fraction for a value
v, as defined in
algebra.continued_fractions.computation.basic, terminates if and only if
v corresponds to a
rational number, that is
↑v = q for some
q : ℚ.
Main Theorems #
generalized_continued_fraction.of v = generalized_continued_fraction.of qfor
v : αgiven that
↑v = qand
q : ℚ.
generalized_continued_fraction.of vterminates if and only if
↑v = qfor some
q : ℚ.
rational, continued fraction, termination
Terminating Continued Fractions Are Rational #
We want to show that the computation of a continued fraction
terminates if and only if
v ∈ ℚ. In this section, we show the implication from left to right.
We first show that every finite convergent corresponds to a rational number
q and then use the
finite correctness proof (
v = ↑q.
Technical Translation Lemmas #
Before we can show that the continued fraction of a rational number terminates, we have to prove
some technical translation lemmas. More precisely, in this section, we show that, given a rational
q : ℚ and value
v : K with
v = ↑q, the continued fraction of
In particular, we show that
To do this, we proceed bottom-up, showing the correspondence between the basic functions involved in the computation first and then lift the results step-by-step.
First, we show the correspondence for the very basic functions in
Now we lift the coercion results to the continued fraction computation.
(v : K), (q : ℚ), and v = q, we have that
gcf.of q = gcf.of v
Continued Fractions of Rationals Terminate #
Finally, we show that the continued fraction of a rational number terminates.
The crucial insight is that, given any
q : ℚ with
0 < q < 1, the numerator of
int.fract q is
smaller than the numerator of
q. As the continued fraction computation recursively operates on
the fractional part of a value
0 ≤ int.fract v < 1, we infer that the numerator of the
fractional part in the computation decreases by at least one in each step. As
0 ≤ int.fract v,
this process must stop after finite number of steps, and the computation hence terminates.
Shows that for any
q : ℚ with
0 < q < 1, the numerator of the fractional part of
int_fract_pair.of q⁻¹ is smaller than the numerator of
Shows that the sequence of numerators of the fractional parts of the stream is strictly antitone.