Recurrence Lemmas for the Continuants (conts
) Function of Continued Fractions #
Summary #
Given a generalized continued fraction g
, for all n ≥ 1
, we prove that the continuants (conts
)
function indeed satisfies the following recurrences:
Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂
, andBₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂
.
theorem
GenContFract.contsAux_recurrence
{K : Type u_1}
{g : GenContFract K}
{n : ℕ}
[DivisionRing K]
{gp ppred pred : GenContFract.Pair K}
(nth_s_eq : g.s.get? n = some gp)
(nth_contsAux_eq : g.contsAux n = ppred)
(succ_nth_contsAux_eq : g.contsAux (n + 1) = pred)
:
theorem
GenContFract.conts_recurrenceAux
{K : Type u_1}
{g : GenContFract K}
{n : ℕ}
[DivisionRing K]
{gp ppred pred : GenContFract.Pair K}
(nth_s_eq : g.s.get? n = some gp)
(nth_contsAux_eq : g.contsAux n = ppred)
(succ_nth_contsAux_eq : g.contsAux (n + 1) = pred)
:
theorem
GenContFract.conts_recurrence
{K : Type u_1}
{g : GenContFract K}
{n : ℕ}
[DivisionRing K]
{gp ppred pred : GenContFract.Pair K}
(succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_conts_eq : g.conts n = ppred)
(succ_nth_conts_eq : g.conts (n + 1) = pred)
:
Shows that Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂
and Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂
.
theorem
GenContFract.nums_recurrence
{K : Type u_1}
{g : GenContFract K}
{n : ℕ}
[DivisionRing K]
{gp : GenContFract.Pair K}
{ppredA predA : K}
(succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_num_eq : g.nums n = ppredA)
(succ_nth_num_eq : g.nums (n + 1) = predA)
:
Shows that Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂
.
theorem
GenContFract.dens_recurrence
{K : Type u_1}
{g : GenContFract K}
{n : ℕ}
[DivisionRing K]
{gp : GenContFract.Pair K}
{ppredB predB : K}
(succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_den_eq : g.dens n = ppredB)
(succ_nth_den_eq : g.dens (n + 1) = predB)
:
Shows that Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂
.