Documentation

Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

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):

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 #

References #

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.

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

    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.

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

    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 }
    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 : 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 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 : GenContFract K} [Field K] (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 : GenContFract K} [LinearOrderedField K] (s_pos : ∀ {gp : GenContFract.Pair K} {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} [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.