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)
:
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)
:
theorem
GenContFract.convs'Aux_stable_step_of_terminated
{K : Type u_1}
{n : ℕ}
[DivisionRing K]
{s : Stream'.Seq (GenContFract.Pair K)}
(terminatedAt_n : s.TerminatedAt n)
:
GenContFract.convs'Aux s (n + 1) = GenContFract.convs'Aux s n
theorem
GenContFract.convs'Aux_stable_of_terminated
{K : Type u_1}
{n m : ℕ}
[DivisionRing K]
{s : Stream'.Seq (GenContFract.Pair K)}
(n_le_m : n ≤ m)
(terminatedAt_n : s.TerminatedAt 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