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 [hardy2008introduction], 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.

References

• https://en.wikipedia.org/wiki/Generalized_continued_fraction
• [Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph][hardy2008introduction]

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} [DivisionRing K] (s : Stream'.Seq (GenContFract.Pair K)) (n : ℕ) : Stream'.Seq (GenContFract.Pair K)

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.

We now prove some simple lemmas about the squashed sequence

theorem GenContFract.squashSeq_eq_self_of_terminated {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [DivisionRing K] (terminatedAt_succ_n : s.TerminatedAt (n + 1)) : GenContFract.squashSeq s n = s

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 : Stream'.Seq (GenContFract.Pair K)} [DivisionRing K] {gp_n : GenContFract.Pair K} {gp_succ_n : GenContFract.Pair K} (s_nth_eq : s.get? n = some gp_n) (s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n) : (GenContFract.squashSeq s 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 : Stream'.Seq (GenContFract.Pair K)} [DivisionRing K] {m : ℕ} (m_lt_n : m < n) : (GenContFract.squashSeq s n).get? m = s.get? m

The values before the squashed position stay the same.

theorem GenContFract.squashSeq_succ_n_tail_eq_squashSeq_tail_n {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [DivisionRing K] : (GenContFract.squashSeq s (n + 1)).tail = GenContFract.squashSeq s.tail n

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

theorem GenContFract.succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [DivisionRing K] : GenContFract.convs'Aux s (n + 2) = GenContFract.convs'Aux (GenContFract.squashSeq s n) (n + 1)

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} [DivisionRing K] (g : GenContFract K) : ℕ → GenContFract K

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 x = match x with | 0 => match g.s.get? 0 with | none => g | some gp => { h := g.h + gp.a / gp.b, s := g.s } | n.succ => { h := g.h, s := GenContFract.squashSeq g.s n }

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 : GenContFract K} [DivisionRing K] (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 : GenContFract K} [DivisionRing K] {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 : GenContFract K} [DivisionRing K] : 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 : GenContFract K} [DivisionRing K] {m : ℕ} : m ≤ n → g.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 : GenContFract K} [Field K] (nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 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 : GenContFract K} [LinearOrderedField K] (s_pos : ∀ {gp : GenContFract.Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < 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} [LinearOrderedField K] {c : ContFract K} : (↑↑c).convs = (↑↑c).convs'

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