mathlib documentation

algebra.continued_fractions.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 convergents.
  5. Computation of convergents by directly evaluating the fraction described by the gcf in convergents'.

Implementation notes #

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

References #

Tags #

numerics, number theory, approximations, fractions

Definitions #

structure generalized_continued_fraction.pair (α : Type u_1) :
Type u_1
  • a : α
  • b : α

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

Interlude: define some expected coercions and instances.

@[instance]

Make a gcf.pair printable.

Equations

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

Equations
@[simp]
theorem generalized_continued_fraction.pair.coe_to_generalized_continued_fraction_pair {α : Type u_1} {β : Type u_2} [has_coe α β] {a b : α} :
{a := a, b := b} = {a := a, b := b}
structure generalized_continued_fraction (α : Type u_1) :
Type u_1

A generalised continued fraction (gcf) is a potentially infinite expression of the form

                            a₀
            h + ---------------------------
                              a₁
                  b₀ + --------------------
                                a₂
                        b₁ + --------------
                                    a₃
                              b₂ + --------
                                  b₃ + ...

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 generalized_continued_fraction.pairs s. For convenience, one often writes [h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...].

Constructs a generalized continued fraction without fractional part.

Equations

Returns the sequence of partial numerators aᵢ of g.

Equations

Returns the sequence of partial denominators bᵢ of g.

Equations

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

Equations
@[instance]

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

Equations

A gcf terminates if its sequence terminates.

Equations

Interlude: define some expected coercions.

@[simp]
theorem generalized_continued_fraction.coe_to_generalized_continued_fraction {α : Type u_1} {β : Type u_2} [has_coe α β] {g : generalized_continued_fraction α} :
g = {h := (g.h), s := seq.map coe g.s}

A generalized continued fraction is a simple continued fraction if all partial numerators are equal to one.

                            1
            h + ---------------------------
                              1
                  b₀ + --------------------
                                1
                        b₁ + --------------
                                    1
                              b₂ + --------
                                  b₃ + ...
Equations
def simple_continued_fraction (α : Type u_1) [has_one α] :
Type u_1

A simple continued fraction (scf) is a generalized continued fraction (gcf) whose partial numerators are equal to one.

                            1
            h + ---------------------------
                              1
                  b₀ + --------------------
                                1
                        b₁ + --------------
                                    1
                              b₂ + --------
                                  b₃ + ...

For convenience, one often writes [h; b₀, b₁, b₂,...]. It is encoded as the subtype of gcfs that satisfy generalized_continued_fraction.is_simple_continued_fraction.

Equations

Constructs a simple continued fraction without fractional part.

Equations
@[instance]

Lift a scf to a gcf using the inclusion map.

Equations

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

Equations
def continued_fraction (α : Type u_1) [has_one α] [has_zero α] [has_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 simple_continued_fraction.is_continued_fraction.

Equations

Interlude: define some expected coercions.

def continued_fraction.of_integer {α : Type u_1} [has_one α] [has_zero α] [has_lt α] (a : α) :

Constructs a continued fraction without fractional part.

Equations
@[instance]

Lift a cf to a scf using the inclusion map.

Equations

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.continued_fractions.convergents_equiv.

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*, andBₙthe *nth denominator* ofg. The *nth convergent* ofgis given byAₙ / Bₙ`.

def generalized_continued_fraction.next_numerator {K : Type u_2} [division_ring K] (a b ppredA 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
def generalized_continued_fraction.next_denominator {K : Type u_2} [division_ring K] (aₙ bₙ ppredB predB : K) :
K

Returns the next denominator Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂``, wherepredBisBₙ₋₁andppredBisBₙ₋₂,aisaₙ₋₁, andbisbₙ₋₁`.

Equations

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations
theorem generalized_continued_fraction.ext_iff {α : Type u_1} {g g' : generalized_continued_fraction α} :
g = g' g.h = g'.h g.s = g'.s

Two gcfs g and g' are equal if and only if their components are equal.

@[ext]
theorem generalized_continued_fraction.ext {α : Type u_1} {g g' : generalized_continued_fraction α} (hyp : g.h = g'.h g.s = g'.s) :
g = g'