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 [wall2018analytic], Chapter 1.

Main definitions

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

Implementation notes

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.
We use sequences from data.seq to encode potentially infinite sequences.

References

https://en.wikipedia.org/wiki/Generalized_continued_fraction
[Wall, H.S., Analytic Theory of Continued Fractions][wall2018analytic]

Tags

numerics, number theory, approximations, fractions

source

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ᵢ⟩.

source

@[instance]

def generalized_continued_fraction.pair.inhabited (α : Type u_1) [a : inhabited α] :

inhabited (generalized_continued_fraction.pair α)

source

@[instance]

def generalized_continued_fraction.pair.has_repr (α : Type u_1) [has_repr α] :

has_repr (generalized_continued_fraction.pair α)

Make a gcf.pair printable.

Equations

generalized_continued_fraction.pair.has_repr α = {repr := λ (p : generalized_continued_fraction.pair α), "(a : " ++ repr p.a ++ ", b : " ++ repr p.b ++ ")"}

Interlude: define some expected coercions.

source

@[instance]

def generalized_continued_fraction.pair.has_coe_to_generalized_continued_fraction_pair {α : Type u_1} {β : Type u_2} [has_coe α β] :

has_coe (generalized_continued_fraction.pair α) (generalized_continued_fraction.pair β)

Coerce a pair by elementwise coercion.

Equations

generalized_continued_fraction.pair.has_coe_to_generalized_continued_fraction_pair = {coe := λ (_x : generalized_continued_fraction.pair α), generalized_continued_fraction.pair.has_coe_to_generalized_continued_fraction_pair._match_1 _x}
generalized_continued_fraction.pair.has_coe_to_generalized_continued_fraction_pair._match_1 {a := a, b := b} = {a := ↑a, b := ↑b}

source

@[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}

source

structure generalized_continued_fraction :

Type u_1 → Type u_1

h : α
s : seq (generalized_continued_fraction.pair α)

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₂),...].

source

def generalized_continued_fraction.of_integer {α : Type u_1} :

α → generalized_continued_fraction α

Constructs a generalized continued fraction without fractional part.

Equations

generalized_continued_fraction.of_integer a = {h := a, s := seq.nil (generalized_continued_fraction.pair α)}

source

@[instance]

def generalized_continued_fraction.inhabited {α : Type u_1} [inhabited α] :

inhabited (generalized_continued_fraction α)

Equations

generalized_continued_fraction.inhabited = {default := generalized_continued_fraction.of_integer (inhabited.default α)}

source

def generalized_continued_fraction.partial_numerators {α : Type u_1} :

generalized_continued_fraction α → seq α

Returns the sequence of partial numerators aᵢ of g.

Equations

g.partial_numerators = seq.map generalized_continued_fraction.pair.a g.s

source

def generalized_continued_fraction.partial_denominators {α : Type u_1} :

generalized_continued_fraction α → seq α

Returns the sequence of partial denominators bᵢ of g.

Equations

g.partial_denominators = seq.map generalized_continued_fraction.pair.b g.s

source

def generalized_continued_fraction.terminated_at {α : Type u_1} :

generalized_continued_fraction α → ℕ → Prop

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

Equations

g.terminated_at n = g.s.terminated_at n

source

@[instance]

def generalized_continued_fraction.terminated_at_decidable {α : Type u_1} (g : generalized_continued_fraction α) (n : ℕ) :

decidable (g.terminated_at n)

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

Equations

g.terminated_at_decidable n = _.mpr (g.s.terminated_at_decidable n)

source

def generalized_continued_fraction.terminates {α : Type u_1} :

generalized_continued_fraction α → Prop

A gcf terminates if its sequence terminates.

Equations

g.terminates = g.s.terminates

Interlude: define some expected coercions.

source

def generalized_continued_fraction.seq.coe_to_seq {α : Type u_1} {β : Type u_2} [has_coe α β] :

has_coe (seq α) (seq β)

Coerce a sequence by elementwise coercion.

Equations

generalized_continued_fraction.seq.coe_to_seq = {coe := seq.map (λ (a : α), ↑a)}

source

@[instance]

def generalized_continued_fraction.has_coe_to_generalized_continued_fraction {α : Type u_1} {β : Type u_2} [has_coe α β] :

has_coe (generalized_continued_fraction α) (generalized_continued_fraction β)

Coerce a gcf by elementwise coercion.

Equations

generalized_continued_fraction.has_coe_to_generalized_continued_fraction = {coe := λ (_x : generalized_continued_fraction α), generalized_continued_fraction.has_coe_to_generalized_continued_fraction._match_1 _x}
generalized_continued_fraction.has_coe_to_generalized_continued_fraction._match_1 {h := h, s := s} = {h := ↑h, s := ↑s}

source

@[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 := ↑(g.s)}

source

def generalized_continued_fraction.is_simple_continued_fraction {α : Type u_1} (g : generalized_continued_fraction α) [has_one α] :

Prop

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

g.is_simple_continued_fraction = ∀ (n : ℕ) (aₙ : α), g.partial_numerators.nth n = option.some aₙ → aₙ = 1

source

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

simple_continued_fraction α = {g // g.is_simple_continued_fraction}

source

def simple_continued_fraction.of_integer {α : Type u_1} [has_one α] :

α → simple_continued_fraction α

Constructs a simple continued fraction without fractional part.

Equations

simple_continued_fraction.of_integer a = ⟨generalized_continued_fraction.of_integer a, _⟩

source

@[instance]

def simple_continued_fraction.inhabited {α : Type u_1} [has_one α] :

inhabited (simple_continued_fraction α)

Equations

simple_continued_fraction.inhabited = {default := simple_continued_fraction.of_integer 1}

source

@[instance]

def simple_continued_fraction.has_coe_to_generalized_continued_fraction {α : Type u_1} [has_one α] :

has_coe (simple_continued_fraction α) (generalized_continued_fraction α)

Lift a scf to a gcf using the inclusion map.

Equations

simple_continued_fraction.has_coe_to_generalized_continued_fraction = simple_continued_fraction.has_coe_to_generalized_continued_fraction._proof_1.mpr coe_subtype

source

theorem simple_continued_fraction.coe_to_generalized_continued_fraction {α : Type u_1} [has_one α] {s : simple_continued_fraction α} :

↑s = s.val

source

def simple_continued_fraction.is_regular_continued_fraction {α : Type u_1} [has_one α] [has_zero α] [has_lt α] :

simple_continued_fraction α → Prop

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

Equations

s.is_regular_continued_fraction = ∀ (n : ℕ) (bₙ : α), ↑s.partial_denominators.nth n = option.some bₙ → 0 < bₙ

source

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_regular_continued_fraction.

Equations

continued_fraction α = {s // s.is_regular_continued_fraction}

source

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

α → continued_fraction α

Constructs a continued fraction without fractional part.

Equations

continued_fraction.of_integer a = ⟨simple_continued_fraction.of_integer a, _⟩

source

@[instance]

def continued_fraction.inhabited {α : Type u_1} [has_one α] [has_zero α] [has_lt α] :

inhabited (continued_fraction α)

Equations

continued_fraction.inhabited = {default := continued_fraction.of_integer 0}

source

@[instance]

def continued_fraction.has_coe_to_simple_continued_fraction {α : Type u_1} [has_one α] [has_zero α] [has_lt α] :

has_coe (continued_fraction α) (simple_continued_fraction α)

Lift a cf to a scf using the inclusion map.

Equations

continued_fraction.has_coe_to_simple_continued_fraction = continued_fraction.has_coe_to_simple_continued_fraction._proof_1.mpr coe_subtype

source

theorem continued_fraction.coe_to_simple_continued_fraction {α : Type u_1} [has_one α] [has_zero α] [has_lt α] {c : continued_fraction α} :

↑c = c.val

source

@[instance]

def continued_fraction.has_coe_to_generalized_continued_fraction {α : Type u_1} [has_one α] [has_zero α] [has_lt α] :

has_coe (continued_fraction α) (generalized_continued_fraction α)

Lift a cf to a scf using the inclusion map.

Equations

continued_fraction.has_coe_to_generalized_continued_fraction = {coe := λ (c : continued_fraction α), ↑↑c}

source

theorem continued_fraction.coe_to_generalized_continued_fraction {α : Type u_1} [has_one α] [has_zero α] [has_lt α] {c : continued_fraction α} :

↑c = ↑(c.val)

source

def generalized_continued_fraction.next_numerator {K : Type u_2} [division_ring K] :

K → K → K → 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

generalized_continued_fraction.next_numerator a b ppredA predA = b * predA + a * ppredA

source

def generalized_continued_fraction.next_denominator {K : Type u_2} [division_ring K] :

K → K → K → K → K

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

Equations

generalized_continued_fraction.next_denominator aₙ bₙ ppredB predB = bₙ * predB + aₙ * ppredB

source

def generalized_continued_fraction.next_continuants {K : Type u_2} [division_ring K] :

K → K → generalized_continued_fraction.pair K → generalized_continued_fraction.pair K → generalized_continued_fraction.pair K

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

generalized_continued_fraction.next_continuants a b ppred pred = {a := generalized_continued_fraction.next_numerator a b ppred.a pred.a, b := generalized_continued_fraction.next_denominator a b ppred.b pred.b}

source

def generalized_continued_fraction.continuants_aux {K : Type u_2} [division_ring K] :

generalized_continued_fraction K → stream (generalized_continued_fraction.pair K)

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

Equations

g.continuants_aux (n + 2) = generalized_continued_fraction.continuants_aux._match_1 (g.continuants_aux n.succ) (g.continuants_aux n) (g.continuants_aux n.succ) (g.s.nth n)
g.continuants_aux 1 = {a := g.h, b := 1}
g.continuants_aux 0 = {a := 1, b := 0}
generalized_continued_fraction.continuants_aux._match_1 _f_1 _f_2 _f_3 (option.some gp) = generalized_continued_fraction.next_continuants gp.a gp.b _f_2 _f_3
generalized_continued_fraction.continuants_aux._match_1 _f_1 _f_2 _f_3 option.none = _f_1

source

def generalized_continued_fraction.continuants {K : Type u_2} [division_ring K] :

generalized_continued_fraction K → stream (generalized_continued_fraction.pair K)

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

Equations

g.continuants = g.continuants_aux.tail

source

def generalized_continued_fraction.numerators {K : Type u_2} [division_ring K] :

generalized_continued_fraction K → stream K

Returns the numerators Aₙ of g.

Equations

g.numerators = stream.map generalized_continued_fraction.pair.a g.continuants

source

def generalized_continued_fraction.denominators {K : Type u_2} [division_ring K] :

generalized_continued_fraction K → stream K

Returns the denominators Bₙ of g.

Equations

g.denominators = stream.map generalized_continued_fraction.pair.b g.continuants

source

def generalized_continued_fraction.convergents {K : Type u_2} [division_ring K] :

generalized_continued_fraction K → stream K

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

Equations

g.convergents = λ (n : ℕ), g.numerators n / g.denominators n

source

def generalized_continued_fraction.convergents'_aux {K : Type u_2} [division_ring K] :

seq (generalized_continued_fraction.pair K) → ℕ → K

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

generalized_continued_fraction.convergents'_aux s (n + 1) = generalized_continued_fraction.convergents'_aux._match_1 (generalized_continued_fraction.convergents'_aux s.tail n) s.head
generalized_continued_fraction.convergents'_aux s 0 = 0
generalized_continued_fraction.convergents'_aux._match_1 _f_1 (option.some gp) = gp.a / (gp.b + _f_1)
generalized_continued_fraction.convergents'_aux._match_1 _f_1 option.none = 0

source

def generalized_continued_fraction.convergents' {K : Type u_2} [division_ring K] :

generalized_continued_fraction K → ℕ → K

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