Stabilisation of gcf Computations Under Termination

Summary

We show that the continuants and convergents of a gcf stabilise once the gcf terminates.

theorem GenContFract.terminated_stable {K : Type u_1} {g : GenContFract K} {n m : ℕ} (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.TerminatedAt m

If a gcf terminated at position n, it also terminated at m ≥ n.

theorem GenContFract.contsAux_stable_step_of_terminated {K : Type u_1} {g : GenContFract K} {n : ℕ} [DivisionRing K] (terminatedAt_n : g.TerminatedAt n) : g.contsAux (n + 2) = g.contsAux (n + 1)

theorem GenContFract.contsAux_stable_of_terminated {K : Type u_1} {g : GenContFract K} {n m : ℕ} [DivisionRing K] (n_lt_m : n < m) (terminatedAt_n : g.TerminatedAt n) : g.contsAux m = g.contsAux (n + 1)

theorem GenContFract.convs'Aux_stable_step_of_terminated {K : Type u_1} {n : ℕ} [DivisionRing K] {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.TerminatedAt n) : convs'Aux s (n + 1) = convs'Aux s n

theorem GenContFract.convs'Aux_stable_of_terminated {K : Type u_1} {n m : ℕ} [DivisionRing K] {s : Stream'.Seq (Pair K)} (n_le_m : n ≤ m) (terminatedAt_n : s.TerminatedAt n) : convs'Aux s m = convs'Aux s n

theorem GenContFract.conts_stable_of_terminated {K : Type u_1} {g : GenContFract K} {n m : ℕ} [DivisionRing K] (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.conts m = g.conts n

theorem GenContFract.nums_stable_of_terminated {K : Type u_1} {g : GenContFract K} {n m : ℕ} [DivisionRing K] (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.nums m = g.nums n

theorem GenContFract.dens_stable_of_terminated {K : Type u_1} {g : GenContFract K} {n m : ℕ} [DivisionRing K] (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.dens m = g.dens n

theorem GenContFract.convs_stable_of_terminated {K : Type u_1} {g : GenContFract K} {n m : ℕ} [DivisionRing K] (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.convs m = g.convs n

theorem GenContFract.convs'_stable_of_terminated {K : Type u_1} {g : GenContFract K} {n m : ℕ} [DivisionRing K] (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.convs' m = g.convs' n