Documentation

Mathlib.Algebra.ContinuedFractions.Basic

Basic Definitions/Theorems for Continued Fractions #

Summary #

We define generalised, simple, and regular continued fractions and functions to evaluate their convergents. We follow the naming conventions from Wikipedia and [Wal18], Chapter 1.

Main definitions #

  1. Generalised continued fractions (gcfs)
  2. Simple continued fractions (scfs)
  3. (Regular) continued fractions ((r)cfs)
  4. Computation of convergents using the recurrence relation in convs.
  5. Computation of convergents by directly evaluating the fraction described by the gcf in convs'.

Implementation notes #

  1. The most commonly used kind of continued fractions in the literature are regular continued fractions. We hence just call them ContFract in the library.
  2. We use sequences from Data.Seq to encode potentially infinite sequences.

References #

Tags #

numerics, number theory, approximations, fractions

Definitions #

structure GenContFract.Pair (α : Type u_1) :
Type u_1

We collect a partial numerator aᵢ and partial denominator bᵢ in a pair ⟨aᵢ, bᵢ⟩.

  • a : α

    Partial numerator

  • b : α

    Partial denominator

Instances For
    instance GenContFract.instInhabitedPair :
    {a : Type u_2} → [inst : Inhabited a] → Inhabited (GenContFract.Pair a)
    Equations
    • GenContFract.instInhabitedPair = { default := { a := default, b := default } }

    Interlude: define some expected coercions and instances.

    Make a GenContFract.Pair printable.

    Equations
    def GenContFract.Pair.map {α : Type u_1} {β : Type u_2} (f : αβ) (gp : GenContFract.Pair α) :

    Maps a function f on both components of a given pair.

    Equations
    Instances For
      def GenContFract.Pair.coeFn {α : Type u_1} {β : Type u_2} [Coe α β] :

      The coercion between numerator-denominator pairs happens componentwise.

      Equations
      Instances For
        instance GenContFract.Pair.instCoe {α : Type u_1} {β : Type u_2} [Coe α β] :

        Coerce a pair by elementwise coercion.

        Equations
        • GenContFract.Pair.instCoe = { coe := GenContFract.Pair.coeFn }
        @[simp]
        theorem GenContFract.Pair.coe_toPair {α : Type u_1} {β : Type u_2} [Coe α β] {a : α} {b : α} :
        { a := a, b := b } = { a := Coe.coe a, b := Coe.coe b }
        theorem GenContFract.ext_iff {α : Type u_1} (x : GenContFract α) (y : GenContFract α) :
        x = y x.h = y.h x.s = y.s
        theorem GenContFract.ext {α : Type u_1} (x : GenContFract α) (y : GenContFract α) (h : x.h = y.h) (s : x.s = y.s) :
        x = y
        structure GenContFract (α : Type u_1) :
        Type u_1

        A generalised continued fraction (gcf) is a potentially infinite expression of the form $$ h + \dfrac{a_0} {b_0 + \dfrac{a_1} {b_1 + \dfrac{a_2} {b_2 + \dfrac{a_3} {b_3 + \dots}}}} $$ where h is called the head term or integer part, the aᵢ are called the partial numerators and the bᵢ the partial denominators of the gcf. We store the sequence of partial numerators and denominators in a sequence of GenContFract.Pairs s. For convenience, one often writes [h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...].

        Instances For
          def GenContFract.ofInteger {α : Type u_1} (a : α) :

          Constructs a generalized continued fraction without fractional part.

          Equations
          Instances For
            Equations

            Returns the sequence of partial numerators aᵢ of g.

            Equations
            Instances For

              Returns the sequence of partial denominators bᵢ of g.

              Equations
              Instances For
                def GenContFract.TerminatedAt {α : Type u_1} (g : GenContFract α) (n : ) :

                A gcf terminated at position n if its sequence terminates at position n.

                Equations
                • g.TerminatedAt n = g.s.TerminatedAt n
                Instances For
                  instance GenContFract.terminatedAtDecidable {α : Type u_1} (g : GenContFract α) (n : ) :
                  Decidable (g.TerminatedAt n)

                  It is decidable whether a gcf terminated at a given position.

                  Equations
                  • g.terminatedAtDecidable n = id inferInstance

                  A gcf terminates if its sequence terminates.

                  Equations
                  • g.Terminates = g.s.Terminates
                  Instances For

                    Interlude: define some expected coercions.

                    def GenContFract.coeFn {α : Type u_1} {β : Type u_2} [Coe α β] :

                    The coercion between GenContFract happens on the head term and all numerator-denominator pairs componentwise.

                    Equations
                    Instances For
                      instance GenContFract.instCoe {α : Type u_1} {β : Type u_2} [Coe α β] :

                      Coerce a gcf by elementwise coercion.

                      Equations
                      • GenContFract.instCoe = { coe := GenContFract.coeFn }
                      @[simp]
                      theorem GenContFract.coe_toGenContFract {α : Type u_1} {β : Type u_2} [Coe α β] {g : GenContFract α} :
                      g = { h := Coe.coe g.h, s := Stream'.Seq.map GenContFract.Pair.coeFn g.s }
                      def GenContFract.IsSimpContFract {α : Type u_1} (g : GenContFract α) [One α] :

                      A generalized continued fraction is a simple continued fraction if all partial numerators are equal to one. $$ h + \dfrac{1} {b_0 + \dfrac{1} {b_1 + \dfrac{1} {b_2 + \dfrac{1} {b_3 + \dots}}}} $$

                      Equations
                      • g.IsSimpContFract = ∀ (n : ) (aₙ : α), g.partNums.get? n = some aₙaₙ = 1
                      Instances For
                        def SimpContFract (α : Type u_1) [One α] :
                        Type u_1

                        A simple continued fraction (scf) is a generalized continued fraction (gcf) whose partial numerators are equal to one. $$ h + \dfrac{1} {b_0 + \dfrac{1} {b_1 + \dfrac{1} {b_2 + \dfrac{1} {b_3 + \dots}}}} $$ For convenience, one often writes [h; b₀, b₁, b₂,...]. It is encoded as the subtype of gcfs that satisfy GenContFract.IsSimpContFract.

                        Equations
                        Instances For
                          def SimpContFract.ofInteger {α : Type u_1} [One α] (a : α) :

                          Constructs a simple continued fraction without fractional part.

                          Equations
                          Instances For
                            Equations

                            Lift a scf to a gcf using the inclusion map.

                            Equations
                            • SimpContFract.instCoeGenContFract = { coe := Subtype.val }
                            def SimpContFract.IsContFract {α : Type u_1} [One α] [Zero α] [LT α] (s : SimpContFract α) :

                            A simple continued fraction is a (regular) continued fraction ((r)cf) if all partial denominators bᵢ are positive, i.e. 0 < bᵢ.

                            Equations
                            • s.IsContFract = ∀ (n : ) (bₙ : α), (s).partDens.get? n = some bₙ0 < bₙ
                            Instances For
                              def ContFract (α : Type u_1) [One α] [Zero α] [LT α] :
                              Type u_1

                              A (regular) continued fraction ((r)cf) is a simple continued fraction (scf) whose partial denominators are all positive. It is the subtype of scfs that satisfy SimpContFract.IsContFract.

                              Equations
                              Instances For

                                Interlude: define some expected coercions.

                                def ContFract.ofInteger {α : Type u_1} [One α] [Zero α] [LT α] (a : α) :

                                Constructs a continued fraction without fractional part.

                                Equations
                                Instances For
                                  instance ContFract.instInhabited {α : Type u_1} [One α] [Zero α] [LT α] :
                                  Equations
                                  instance ContFract.instCoeSimpContFract {α : Type u_1} [One α] [Zero α] [LT α] :

                                  Lift a cf to a scf using the inclusion map.

                                  Equations
                                  • ContFract.instCoeSimpContFract = { coe := Subtype.val }
                                  instance ContFract.instCoeGenContFract {α : Type u_1} [One α] [Zero α] [LT α] :

                                  Lift a cf to a scf using the inclusion map.

                                  Equations
                                  • ContFract.instCoeGenContFract = { coe := fun (c : ContFract α) => c }

                                  Computation of Convergents #

                                  We now define how to compute the convergents of a gcf. There are two standard ways to do this: directly evaluating the (infinite) fraction described by the gcf or using a recurrence relation. For (r)cfs, these computations are equivalent as shown in Algebra.ContinuedFractions.ConvergentsEquiv.

                                  We start with the definition of the recurrence relation. Given a gcf g, for all n ≥ 1, we define

                                  Aₙ, Bₙ are called the nth continuants, Aₙ the nth numerator, and Bₙ the nth denominator of g. The nth convergent of g is given by Aₙ / Bₙ.

                                  def GenContFract.nextNum {K : Type u_2} [DivisionRing K] (a : K) (b : K) (ppredA : K) (predA : K) :
                                  K

                                  Returns the next numerator Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂, where predA is Aₙ₋₁, ppredA is Aₙ₋₂, a is aₙ₋₁, and b is bₙ₋₁.

                                  Equations
                                  Instances For
                                    def GenContFract.nextDen {K : Type u_2} [DivisionRing K] (aₙ : K) (bₙ : K) (ppredB : K) (predB : K) :
                                    K

                                    Returns the next denominator Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂, where predB is Bₙ₋₁ and ppredB is Bₙ₋₂, a is aₙ₋₁, and b is bₙ₋₁.

                                    Equations
                                    Instances For
                                      def GenContFract.nextConts {K : Type u_2} [DivisionRing K] (a : K) (b : K) (ppred : GenContFract.Pair K) (pred : GenContFract.Pair K) :

                                      Returns the next continuants ⟨Aₙ, Bₙ⟩ using nextNum and nextDen, where pred is ⟨Aₙ₋₁, Bₙ₋₁⟩, ppred is ⟨Aₙ₋₂, Bₙ₋₂⟩, a is aₙ₋₁, and b is bₙ₋₁.

                                      Equations
                                      Instances For

                                        Returns the continuants ⟨Aₙ₋₁, Bₙ₋₁⟩ of g.

                                        Equations
                                        • g.contsAux 0 = { a := 1, b := 0 }
                                        • g.contsAux 1 = { a := g.h, b := 1 }
                                        • g.contsAux n.succ.succ = match g.s.get? n with | none => g.contsAux (n + 1) | some gp => GenContFract.nextConts gp.a gp.b (g.contsAux n) (g.contsAux (n + 1))
                                        Instances For

                                          Returns the continuants ⟨Aₙ, Bₙ⟩ of g.

                                          Equations
                                          • g.conts = g.contsAux.tail
                                          Instances For

                                            Returns the numerators Aₙ of g.

                                            Equations
                                            Instances For

                                              Returns the denominators Bₙ of g.

                                              Equations
                                              Instances For

                                                Returns the convergents Aₙ / Bₙ of g, where Aₙ, Bₙ are the nth continuants of g.

                                                Equations
                                                • g.convs n = g.nums n / g.dens n
                                                Instances For

                                                  Returns the approximation of the fraction described by the given sequence up to a given position n. For example, convs'Aux [(1, 2), (3, 4), (5, 6)] 2 = 1 / (2 + 3 / 4) and convs'Aux [(1, 2), (3, 4), (5, 6)] 0 = 0.

                                                  Equations
                                                  Instances For
                                                    def GenContFract.convs' {K : Type u_2} [DivisionRing K] (g : GenContFract K) (n : ) :
                                                    K

                                                    Returns the convergents of g by evaluating the fraction described by g up to a given position n. For example, convs' [9; (1, 2), (3, 4), (5, 6)] 2 = 9 + 1 / (2 + 3 / 4) and convs' [9; (1, 2), (3, 4), (5, 6)] 0 = 9

                                                    Equations
                                                    Instances For