Stabilisation of gcf Computations Under Termination
Summary
We show that the continuants and convergents of a gcf stabilise once the gcf terminates.
theorem
generalized_continued_fraction.terminated_stable
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ} :
n ≤ m → g.terminated_at n → g.terminated_at m
If a gcf terminated at position n, it also terminated at m ≥ n.
theorem
generalized_continued_fraction.continuants_aux_stable_step_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n : ℕ}
[division_ring K] :
g.terminated_at n → g.continuants_aux (n + 2) = g.continuants_aux (n + 1)
theorem
generalized_continued_fraction.continuants_aux_stable_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ}
[division_ring K] :
n + 1 ≤ m → g.terminated_at n → g.continuants_aux m = g.continuants_aux (n + 1)
theorem
generalized_continued_fraction.convergents'_aux_stable_step_of_terminated
{K : Type u_1}
{n : ℕ}
[division_ring K]
{s : seq (generalized_continued_fraction.pair K)} :
theorem
generalized_continued_fraction.convergents'_aux_stable_of_terminated
{K : Type u_1}
{n m : ℕ}
[division_ring K]
{s : seq (generalized_continued_fraction.pair K)} :
theorem
generalized_continued_fraction.continuants_stable_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ}
[division_ring K] :
n ≤ m → g.terminated_at n → g.continuants m = g.continuants n
theorem
generalized_continued_fraction.numerators_stable_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ}
[division_ring K] :
n ≤ m → g.terminated_at n → g.numerators m = g.numerators n
theorem
generalized_continued_fraction.denominators_stable_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ}
[division_ring K] :
n ≤ m → g.terminated_at n → g.denominators m = g.denominators n
theorem
generalized_continued_fraction.convergents_stable_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ}
[division_ring K] :
n ≤ m → g.terminated_at n → g.convergents m = g.convergents n
theorem
generalized_continued_fraction.convergents'_stable_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ}
[division_ring K] :
n ≤ m → g.terminated_at n → g.convergents' m = g.convergents' n