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 : GeneralizedContinuedFraction.TerminatedAt g n)
:
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 : GeneralizedContinuedFraction.TerminatedAt g 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 : GeneralizedContinuedFraction.TerminatedAt g 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 : Stream'.Seq.TerminatedAt s 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 : Stream'.Seq.TerminatedAt s 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 : GeneralizedContinuedFraction.TerminatedAt g 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 : GeneralizedContinuedFraction.TerminatedAt g 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 : GeneralizedContinuedFraction.TerminatedAt g 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 : GeneralizedContinuedFraction.TerminatedAt g 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 : GeneralizedContinuedFraction.TerminatedAt g n)
: