Stabilisation of gcf Computations Under Termination #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_le_m : n ≤ m)
(terminated_at_n : 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]
(terminated_at_n : 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_lt_m : n < m)
(terminated_at_n : 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 : stream.seq (generalized_continued_fraction.pair K)}
(terminated_at_n : s.terminated_at n) :
theorem
generalized_continued_fraction.convergents'_aux_stable_of_terminated
{K : Type u_1}
{n m : ℕ}
[division_ring K]
{s : stream.seq (generalized_continued_fraction.pair K)}
(n_le_m : n ≤ m)
(terminated_at_n : s.terminated_at n) :
theorem
generalized_continued_fraction.continuants_stable_of_terminated
{K : Type u_1}
{g : generalized_continued_fraction K}
{n m : ℕ}
[division_ring K]
(n_le_m : n ≤ m)
(terminated_at_n : 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_le_m : n ≤ m)
(terminated_at_n : 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_le_m : n ≤ m)
(terminated_at_n : 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_le_m : n ≤ m)
(terminated_at_n : 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_le_m : n ≤ m)
(terminated_at_n : g.terminated_at n) :
g.convergents' m = g.convergents' n