# Termination of Continued Fraction Computations (GeneralizedContinuedFraction.of) #

## Summary #

We show that the continued fraction for a value v, as defined in Mathlib.Algebra.ContinuedFractions.Basic, terminates if and only if v corresponds to a rational number, that is ↑v = q for some q : ℚ.

## Main Theorems #

• GeneralizedContinuedFraction.coe_of_rat_eq shows that GeneralizedContinuedFraction.of v = GeneralizedContinuedFraction.of q for v : α given that ↑v = q and q : ℚ.
• GeneralizedContinuedFraction.terminates_iff_rat shows that GeneralizedContinuedFraction.of v terminates if and only if ↑v = q for some q : ℚ.

## Tags #

rational, continued fraction, termination

### Terminating Continued Fractions Are Rational #

We want to show that the computation of a continued fraction GeneralizedContinuedFraction.of v 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 (of_correctness_of_terminates) of GeneralizedContinuedFraction.of to show that v = ↑q.

theorem GeneralizedContinuedFraction.exists_gcf_pair_rat_eq_of_nth_conts_aux {K : Type u_1} [] (v : K) (n : ) :
∃ (conts : ), .continuantsAux n = GeneralizedContinuedFraction.Pair.map Rat.cast conts
theorem GeneralizedContinuedFraction.exists_gcf_pair_rat_eq_nth_conts {K : Type u_1} [] (v : K) (n : ) :
∃ (conts : ), .continuants n = GeneralizedContinuedFraction.Pair.map Rat.cast conts
theorem GeneralizedContinuedFraction.exists_rat_eq_nth_numerator {K : Type u_1} [] (v : K) (n : ) :
∃ (q : ), .numerators n = q
theorem GeneralizedContinuedFraction.exists_rat_eq_nth_denominator {K : Type u_1} [] (v : K) (n : ) :
∃ (q : ), .denominators n = q
theorem GeneralizedContinuedFraction.exists_rat_eq_nth_convergent {K : Type u_1} [] (v : K) (n : ) :
∃ (q : ), .convergents n = q

Every finite convergent corresponds to a rational number.

theorem GeneralizedContinuedFraction.exists_rat_eq_of_terminates {K : Type u_1} [] {v : K} (terminates : .Terminates) :
∃ (q : ), v = q

Every terminating continued fraction corresponds to a rational number.

### 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 number q : ℚ and value v : K with v = ↑q, the continued fraction of q and v coincide. In particular, we show that

    (↑(GeneralizedContinuedFraction.of q : GeneralizedContinuedFraction ℚ) :
GeneralizedContinuedFraction K)
= GeneralizedContinuedFraction.of v


in GeneralizedContinuedFraction.coe_of_rat_eq.

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 GeneralizedContinuedFraction.IntFractPair.

theorem GeneralizedContinuedFraction.IntFractPair.coe_of_rat_eq {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) :
theorem GeneralizedContinuedFraction.IntFractPair.coe_stream_nth_rat_eq {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) (n : ) :
theorem GeneralizedContinuedFraction.IntFractPair.coe_stream'_rat_eq {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) :

Now we lift the coercion results to the continued fraction computation.

theorem GeneralizedContinuedFraction.coe_of_h_rat_eq {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) :
theorem GeneralizedContinuedFraction.coe_of_s_get?_rat_eq {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) (n : ) :
Option.map () (.get? n) = .get? n
theorem GeneralizedContinuedFraction.coe_of_s_rat_eq {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) :
theorem GeneralizedContinuedFraction.coe_of_rat_eq {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) :
{ h := , s := } =

Given (v : K), (q : ℚ), and v = q, we have that of q = of v

theorem GeneralizedContinuedFraction.of_terminates_iff_of_rat_terminates {K : Type u_1} [] {v : K} {q : } (v_eq_q : v = q) :
.Terminates .Terminates

### 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 v and 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 IntFractPair.of q⁻¹ is smaller than the numerator of q.

theorem GeneralizedContinuedFraction.IntFractPair.stream_succ_nth_fr_num_lt_nth_fr_num_rat {q : } {n : } {ifp_succ_n : } (stream_nth_eq : ) (stream_succ_nth_eq : = some ifp_succ_n) :
ifp_succ_n.fr.num < ifp_n.fr.num

Shows that the sequence of numerators of the fractional parts of the stream is strictly antitone.

The continued fraction of a rational number terminates.

theorem GeneralizedContinuedFraction.terminates_iff_rat {K : Type u_1} [] (v : K) :
.Terminates ∃ (q : ), v = q

The continued fraction GeneralizedContinuedFraction.of v terminates if and only if v ∈ ℚ`.