Recurrence Lemmas for the continuants
Function of Continued Fractions. #
Summary #
Given a generalized continued fraction g
, for all n ≥ 1
, we prove that the continuants
function indeed satisfies the following recurrences:
Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂
, andBₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂
.
theorem
GeneralizedContinuedFraction.continuantsAux_recurrence
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
[DivisionRing K]
{gp : GeneralizedContinuedFraction.Pair K}
{ppred : GeneralizedContinuedFraction.Pair K}
{pred : GeneralizedContinuedFraction.Pair K}
(nth_s_eq : g.s.get? n = some gp)
(nth_conts_aux_eq : g.continuantsAux n = ppred)
(succ_nth_conts_aux_eq : g.continuantsAux (n + 1) = pred)
:
theorem
GeneralizedContinuedFraction.continuants_recurrenceAux
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
[DivisionRing K]
{gp : GeneralizedContinuedFraction.Pair K}
{ppred : GeneralizedContinuedFraction.Pair K}
{pred : GeneralizedContinuedFraction.Pair K}
(nth_s_eq : g.s.get? n = some gp)
(nth_conts_aux_eq : g.continuantsAux n = ppred)
(succ_nth_conts_aux_eq : g.continuantsAux (n + 1) = pred)
:
theorem
GeneralizedContinuedFraction.continuants_recurrence
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
[DivisionRing K]
{gp : GeneralizedContinuedFraction.Pair K}
{ppred : GeneralizedContinuedFraction.Pair K}
{pred : GeneralizedContinuedFraction.Pair K}
(succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_conts_eq : g.continuants n = ppred)
(succ_nth_conts_eq : g.continuants (n + 1) = pred)
:
Shows that Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂
and Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂
.
theorem
GeneralizedContinuedFraction.numerators_recurrence
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
[DivisionRing K]
{gp : GeneralizedContinuedFraction.Pair K}
{ppredA : K}
{predA : K}
(succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_num_eq : g.numerators n = ppredA)
(succ_nth_num_eq : g.numerators (n + 1) = predA)
:
Shows that Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂
.
theorem
GeneralizedContinuedFraction.denominators_recurrence
{K : Type u_1}
{g : GeneralizedContinuedFraction K}
{n : ℕ}
[DivisionRing K]
{gp : GeneralizedContinuedFraction.Pair K}
{ppredB : K}
{predB : K}
(succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_denom_eq : g.denominators n = ppredB)
(succ_nth_denom_eq : g.denominators (n + 1) = predB)
:
Shows that Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂
.