Stabilisation of gcf Computations Under Termination #
Summary #
We show that the continuants and convergents of a gcf stabilise once the gcf terminates.
theorem
GeneralizedContinuedFraction.terminated_stable
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
{m : ℕ}
(n_le_m : n ≤ m)
(terminated_at_n : g.TerminatedAt n)
:
g.TerminatedAt m
If a gcf terminated at position n, it also terminated at m ≥ n.
theorem
GeneralizedContinuedFraction.continuantsAux_stable_step_of_terminated
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
[DivisionRing K]
(terminated_at_n : g.TerminatedAt n)
:
theorem
GeneralizedContinuedFraction.continuantsAux_stable_of_terminated
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
{m : ℕ}
[DivisionRing K]
(n_lt_m : n < m)
(terminated_at_n : g.TerminatedAt n)
:
theorem
GeneralizedContinuedFraction.convergents'Aux_stable_step_of_terminated
{K : Type u_1}
{n : ℕ}
[DivisionRing K]
{s : Stream'.Seq (GeneralizedContinuedFraction.Pair K)}
(terminated_at_n : s.TerminatedAt n)
:
theorem
GeneralizedContinuedFraction.convergents'Aux_stable_of_terminated
{K : Type u_1}
{n : ℕ}
{m : ℕ}
[DivisionRing K]
{s : Stream'.Seq (GeneralizedContinuedFraction.Pair K)}
(n_le_m : n ≤ m)
(terminated_at_n : s.TerminatedAt n)
:
theorem
GeneralizedContinuedFraction.continuants_stable_of_terminated
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
{m : ℕ}
[DivisionRing K]
(n_le_m : n ≤ m)
(terminated_at_n : g.TerminatedAt n)
:
g.continuants m = g.continuants n
theorem
GeneralizedContinuedFraction.numerators_stable_of_terminated
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
{m : ℕ}
[DivisionRing K]
(n_le_m : n ≤ m)
(terminated_at_n : g.TerminatedAt n)
:
g.numerators m = g.numerators n
theorem
GeneralizedContinuedFraction.denominators_stable_of_terminated
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
{m : ℕ}
[DivisionRing K]
(n_le_m : n ≤ m)
(terminated_at_n : g.TerminatedAt n)
:
g.denominators m = g.denominators n
theorem
GeneralizedContinuedFraction.convergents_stable_of_terminated
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
{m : ℕ}
[DivisionRing K]
(n_le_m : n ≤ m)
(terminated_at_n : g.TerminatedAt n)
:
g.convergents m = g.convergents n
theorem
GeneralizedContinuedFraction.convergents'_stable_of_terminated
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
{m : ℕ}
[DivisionRing K]
(n_le_m : n ≤ m)
(terminated_at_n : g.TerminatedAt n)
:
g.convergents' m = g.convergents' n