# Equivalence of Recursive and Direct Computations of Convergents of Generalized Continued Fractions #

## Summary #

We show the equivalence of two computations of convergents (recurrence relation (convs) vs. direct evaluation (convs')) for generalized continued fractions (GenContFracts) on linear ordered fields. We follow the proof from [HWHBS08], Chapter 10. Here's a sketch:

Let c be a continued fraction [h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...], visually: $$c = h + \dfrac{a_0} {b_0 + \dfrac{a_1} {b_1 + \dfrac{a_2} {b_2 + \dfrac{a_3} {b_3 + \dots}}}}$$ One can compute the convergents of c in two ways:

1. Directly evaluating the fraction described by c up to a given n (convs')
2. Using the recurrence (convs):
• A₋₁ = 1, A₀ = h, Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂, and
• B₋₁ = 0, B₀ = 1, Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂.

To show the equivalence of the computations in the main theorem of this file convs_eq_convs', we proceed by induction. The case n = 0 is trivial.

For n + 1, we first "squash" the n + 1th position of c into the nth position to obtain another continued fraction c' := [h; (a₀, b₀),..., (aₙ-₁, bₙ-₁), (aₙ, bₙ + aₙ₊₁ / bₙ₊₁), (aₙ₊₁, bₙ₊₁),...]. This squashing process is formalised in section Squash. Note that directly evaluating c up to position n + 1 is equal to evaluating c' up to n. This is shown in lemma succ_nth_conv'_eq_squashGCF_nth_conv'.

By the inductive hypothesis, the two computations for the nth convergent of c coincide. So all that is left to show is that the recurrence relation for c at n + 1 and c' at n coincide. This can be shown by another induction. The corresponding lemma in this file is succ_nth_conv_eq_squashGCF_nth_conv.

## Main Theorems #

• GenContFract.convs_eq_convs' shows the equivalence under a strict positivity restriction on the sequence.
• ContFract.convs_eq_convs' shows the equivalence for regular continued fractions.

## Tags #

fractions, recurrence, equivalence

We will show the equivalence of the computations by induction. To make the induction work, we need to be able to squash the nth and (n + 1)th value of a sequence. This squashing itself and the lemmas about it are not very interesting. As a reader, you hence might want to skip this section.

def GenContFract.squashSeq {K : Type u_1} [] (s : ) (n : ) :

Given a sequence of GenContFract.Pairs s = [(a₀, bₒ), (a₁, b₁), ...], squashSeq s n combines ⟨aₙ, bₙ⟩ and ⟨aₙ₊₁, bₙ₊₁⟩ at position n to ⟨aₙ, bₙ + aₙ₊₁ / bₙ₊₁⟩. For example, squashSeq s 0 = [(a₀, bₒ + a₁ / b₁), (a₁, b₁),...]. If s.TerminatedAt (n + 1), then squashSeq s n = s.

Equations
• One or more equations did not get rendered due to their size.
Instances For

We now prove some simple lemmas about the squashed sequence

theorem GenContFract.squashSeq_eq_self_of_terminated {K : Type u_1} {n : } {s : } [] (terminatedAt_succ_n : s.TerminatedAt (n + 1)) :

If the sequence already terminated at position n + 1, nothing gets squashed.

theorem GenContFract.squashSeq_nth_of_not_terminated {K : Type u_1} {n : } {s : } [] {gp_n : } {gp_succ_n : } (s_nth_eq : s.get? n = some gp_n) (s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n) :
.get? n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }

If the sequence has not terminated before position n + 1, the value at n + 1 gets squashed into position n.

theorem GenContFract.squashSeq_nth_of_lt {K : Type u_1} {n : } {s : } [] {m : } (m_lt_n : m < n) :
.get? m = s.get? m

The values before the squashed position stay the same.

Squashing at position n + 1 and taking the tail is the same as squashing the tail of the sequence at position n.

The auxiliary function convs'Aux returns the same value for a sequence and the corresponding squashed sequence at the squashed position.

Let us now lift the squashing operation to gcfs.

def GenContFract.squashGCF {K : Type u_1} [] (g : ) :

Given a gcf g = [h; (a₀, bₒ), (a₁, b₁), ...], we have

• squashGCF g 0 = [h + a₀ / b₀); (a₀, bₒ), ...],
• squashGCF g (n + 1) = ⟨g.h, squashSeq g.s n⟩
Equations
• g.squashGCF 0 = match g.s.get? 0 with | none => g | some gp => { h := g.h + gp.a / gp.b, s := g.s }
• g.squashGCF n.succ = { h := g.h, s := }
Instances For

Again, we derive some simple lemmas that are not really of interest. This time for the squashed gcf.

theorem GenContFract.squashGCF_eq_self_of_terminated {K : Type u_1} {n : } {g : } [] (terminatedAt_n : g.TerminatedAt n) :
g.squashGCF n = g

If the gcf already terminated at position n, nothing gets squashed.

theorem GenContFract.squashGCF_nth_of_lt {K : Type u_1} {n : } {g : } [] {m : } (m_lt_n : m < n) :
(g.squashGCF (n + 1)).s.get? m = g.s.get? m

The values before the squashed position stay the same.

theorem GenContFract.succ_nth_conv'_eq_squashGCF_nth_conv' {K : Type u_1} {n : } {g : } [] :
g.convs' (n + 1) = (g.squashGCF n).convs' n

convs' returns the same value for a gcf and the corresponding squashed gcf at the squashed position.

theorem GenContFract.contsAux_eq_contsAux_squashGCF_of_le {K : Type u_1} {n : } {g : } [] {m : } :
m ng.contsAux m = (g.squashGCF n).contsAux m

The auxiliary continuants before the squashed position stay the same.

theorem GenContFract.succ_nth_conv_eq_squashGCF_nth_conv {K : Type u_1} {n : } {g : } [] (nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some bb 0) :
g.convs (n + 1) = (g.squashGCF n).convs n

The convergents coincide in the expected way at the squashed position if the partial denominator at the squashed position is not zero.

theorem GenContFract.convs_eq_convs' {K : Type u_1} {n : } {g : } (s_pos : ∀ {gp : } {m : }, m < ng.s.get? m = some gp0 < gp.a 0 < gp.b) :
g.convs n = g.convs' n

Shows that the recurrence relation (convs) and direct evaluation (convs') of the generalized continued fraction coincide at position n if the sequence of fractions contains strictly positive values only. Requiring positivity of all values is just one possible condition to obtain this result. For example, the dual - sequences with strictly negative values only - would also work.

In practice, one most commonly deals with regular continued fractions, which satisfy the positivity criterion required here. The analogous result for them (see ContFract.convs_eq_convs) hence follows directly from this theorem.

theorem ContFract.convs_eq_convs' {K : Type u_1} {c : } :
(↑c).convs = (↑c).convs'

Shows that the recurrence relation (convs) and direct evaluation (convs') of a (regular) continued fraction coincide.