Termination of Continued Fraction Computations (GenContFract.of)

Summary

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

Main Theorems

• GenContFract.coe_of_rat_eq shows that GenContFract.of v = GenContFract.of q for v : α given that ↑v = q and q : ℚ.
• GenContFract.terminates_iff_rat shows that GenContFract.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 GenContFract.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 GenContFract.of to show that v = ↑q.

theorem GenContFract.exists_gcf_pair_rat_eq_of_nth_contsAux {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] (v : K) (n : ℕ) : ∃ (conts : Pair ℚ), (GenContFract.of v).contsAux n = Pair.map Rat.cast conts

theorem GenContFract.exists_gcf_pair_rat_eq_nth_conts {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] (v : K) (n : ℕ) : ∃ (conts : Pair ℚ), (GenContFract.of v).conts n = Pair.map Rat.cast conts

theorem GenContFract.exists_rat_eq_nth_num {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] (v : K) (n : ℕ) : ∃ (q : ℚ), (GenContFract.of v).nums n = ↑q

theorem GenContFract.exists_rat_eq_nth_den {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] (v : K) (n : ℕ) : ∃ (q : ℚ), (GenContFract.of v).dens n = ↑q

theorem GenContFract.exists_rat_eq_nth_conv {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] (v : K) (n : ℕ) : ∃ (q : ℚ), (GenContFract.of v).convs n = ↑q

Every finite convergent corresponds to a rational number.

theorem GenContFract.exists_rat_eq_of_terminates {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] {v : K} (terminates : (GenContFract.of v).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

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

in GenContFract.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 GenContFract.IntFractPair.

theorem GenContFract.IntFractPair.coe_of_rat_eq {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) : mapFr Rat.cast (IntFractPair.of q) = IntFractPair.of v

theorem GenContFract.IntFractPair.coe_stream_nth_rat_eq {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) (n : ℕ) : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n

theorem GenContFract.IntFractPair.coe_stream'_rat_eq {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) : Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v

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

theorem GenContFract.coe_of_h_rat_eq {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) : ↑(GenContFract.of q).h = (GenContFract.of v).h

theorem GenContFract.coe_of_s_get?_rat_eq {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) (n : ℕ) : Option.map (Pair.map Rat.cast) ((GenContFract.of q).s.get? n) = (GenContFract.of v).s.get? n

theorem GenContFract.coe_of_s_rat_eq {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) : Stream'.Seq.map (Pair.map Rat.cast) (GenContFract.of q).s = (GenContFract.of v).s

theorem GenContFract.coe_of_rat_eq {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) : { h := ↑(GenContFract.of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (GenContFract.of q).s } = GenContFract.of v

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

theorem GenContFract.of_terminates_iff_of_rat_terminates {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] {v : K} {q : ℚ} (v_eq_q : v = ↑q) : (GenContFract.of v).Terminates ↔ (GenContFract.of q).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.

theorem GenContFract.IntFractPair.of_inv_fr_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) : (IntFractPair.of q⁻¹).fr.num < q.num

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 GenContFract.IntFractPair.stream_succ_nth_fr_num_lt_nth_fr_num_rat {q : ℚ} {n : ℕ} {ifp_n ifp_succ_n : IntFractPair ℚ} (stream_nth_eq : IntFractPair.stream q n = some ifp_n) (stream_succ_nth_eq : IntFractPair.stream q (n + 1) = 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.

theorem GenContFract.IntFractPair.stream_nth_fr_num_le_fr_num_sub_n_rat {q : ℚ} {n : ℕ} {ifp_n : IntFractPair ℚ} : IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n

theorem GenContFract.IntFractPair.exists_nth_stream_eq_none_of_rat (q : ℚ) : ∃ (n : ℕ), IntFractPair.stream q n = none

theorem GenContFract.terminates_of_rat (q : ℚ) : (GenContFract.of q).Terminates

The continued fraction of a rational number terminates.

theorem GenContFract.terminates_iff_rat {K : Type u_1} [Field K] [LinearOrder K] [FloorRing K] [IsStrictOrderedRing K] (v : K) : (GenContFract.of v).Terminates ↔ ∃ (q : ℚ), v = ↑q

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