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

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 ContinuedFractions in the library.
2. We use sequences from Data.Seq to encode potentially infinite sequences.

References

• [Wall, H.S., Analytic Theory of Continued Fractions][wall2018analytic]

Tags

numerics, number theory, approximations, fractions

Definitions

structure GeneralizedContinuedFraction.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

instance GeneralizedContinuedFraction.instInhabitedPair : {a : Type u_2} → [inst : Inhabited a] → Inhabited (GeneralizedContinuedFraction.Pair a)

Equations

• GeneralizedContinuedFraction.instInhabitedPair = { default := { a := default, b := default } }

Interlude: define some expected coercions and instances.

instance GeneralizedContinuedFraction.Pair.instReprPair {α : Type u_1} [Repr α] : Repr (GeneralizedContinuedFraction.Pair α)

Make a GCF.Pair printable.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• GeneralizedContinuedFraction.Pair.map f gp = { a := f gp.a, b := f gp.b }

def GeneralizedContinuedFraction.Pair.coeFn {α : Type u_1} {β : Type u_2} [Coe α β] : GeneralizedContinuedFraction.Pair α → GeneralizedContinuedFraction.Pair β

The coercion between numerator-denominator pairs happens componentwise.

Equations

• GeneralizedContinuedFraction.Pair.coeFn = GeneralizedContinuedFraction.Pair.map Coe.coe

instance GeneralizedContinuedFraction.Pair.instCoePairPair {α : Type u_1} {β : Type u_2} [Coe α β] : Coe (GeneralizedContinuedFraction.Pair α) (GeneralizedContinuedFraction.Pair β)

Coerce a pair by elementwise coercion.

Equations

• GeneralizedContinuedFraction.Pair.instCoePairPair = { coe := GeneralizedContinuedFraction.Pair.coeFn }

@[simp]

theorem GeneralizedContinuedFraction.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 GeneralizedContinuedFraction.ext_iff {α : Type u_1} (x : GeneralizedContinuedFraction α) (y : GeneralizedContinuedFraction α) : x = y ↔ x.h = y.h ∧ x.s = y.s

theorem GeneralizedContinuedFraction.ext {α : Type u_1} (x : GeneralizedContinuedFraction α) (y : GeneralizedContinuedFraction α) (h : x.h = y.h) (s : x.s = y.s) : x = y

structure GeneralizedContinuedFraction (α : 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 GeneralizedContinuedFraction.Pairs s. For convenience, one often writes [h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...].

• h : α

  Head term

• s : Stream'.Seq (GeneralizedContinuedFraction.Pair α)

  Sequence of partial numerator and denominator pairs.

def GeneralizedContinuedFraction.ofInteger {α : Type u_1} (a : α) : GeneralizedContinuedFraction α

Constructs a generalized continued fraction without fractional part.

Equations

• GeneralizedContinuedFraction.ofInteger a = { h := a, s := Stream'.Seq.nil }

instance GeneralizedContinuedFraction.instInhabitedGeneralizedContinuedFraction {α : Type u_1} [Inhabited α] : Inhabited (GeneralizedContinuedFraction α)

Equations

• GeneralizedContinuedFraction.instInhabitedGeneralizedContinuedFraction = { default := GeneralizedContinuedFraction.ofInteger default }

def GeneralizedContinuedFraction.partialNumerators {α : Type u_1} (g : GeneralizedContinuedFraction α) : Stream'.Seq α

Returns the sequence of partial numerators aᵢ of g.

Equations

• GeneralizedContinuedFraction.partialNumerators g = Stream'.Seq.map GeneralizedContinuedFraction.Pair.a g.s

def GeneralizedContinuedFraction.partialDenominators {α : Type u_1} (g : GeneralizedContinuedFraction α) : Stream'.Seq α

Returns the sequence of partial denominators bᵢ of g.

Equations

• GeneralizedContinuedFraction.partialDenominators g = Stream'.Seq.map GeneralizedContinuedFraction.Pair.b g.s

def GeneralizedContinuedFraction.TerminatedAt {α : Type u_1} (g : GeneralizedContinuedFraction α) (n : ℕ) : Prop

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

Equations

• GeneralizedContinuedFraction.TerminatedAt g n = Stream'.Seq.TerminatedAt g.s n

instance GeneralizedContinuedFraction.terminatedAtDecidable {α : Type u_1} (g : GeneralizedContinuedFraction α) (n : ℕ) : Decidable (GeneralizedContinuedFraction.TerminatedAt g n)

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

Equations

• GeneralizedContinuedFraction.terminatedAtDecidable g n = id inferInstance

def GeneralizedContinuedFraction.Terminates {α : Type u_1} (g : GeneralizedContinuedFraction α) : Prop

A gcf terminates if its sequence terminates.

Equations

• GeneralizedContinuedFraction.Terminates g = Stream'.Seq.Terminates g.s

Interlude: define some expected coercions.

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

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

Equations

• ↑g = { h := Coe.coe g.h, s := Stream'.Seq.map GeneralizedContinuedFraction.Pair.coeFn g.s }

instance GeneralizedContinuedFraction.instCoeGeneralizedContinuedFractionGeneralizedContinuedFraction {α : Type u_1} {β : Type u_2} [Coe α β] : Coe (GeneralizedContinuedFraction α) (GeneralizedContinuedFraction β)

Coerce a gcf by elementwise coercion.

Equations

• GeneralizedContinuedFraction.instCoeGeneralizedContinuedFractionGeneralizedContinuedFraction = { coe := GeneralizedContinuedFraction.coeFn }

@[simp]

theorem GeneralizedContinuedFraction.coe_toGeneralizedContinuedFraction {α : Type u_1} {β : Type u_2} [Coe α β] {g : GeneralizedContinuedFraction α} : ↑g = { h := Coe.coe g.h, s := Stream'.Seq.map GeneralizedContinuedFraction.Pair.coeFn g.s }

def GeneralizedContinuedFraction.IsSimpleContinuedFraction {α : Type u_1} (g : GeneralizedContinuedFraction α) [One α] : Prop

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

• GeneralizedContinuedFraction.IsSimpleContinuedFraction g = ∀ (n : ℕ) (aₙ : α), Stream'.Seq.get? (GeneralizedContinuedFraction.partialNumerators g) n = some aₙ → aₙ = 1

def SimpleContinuedFraction (α : 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 GeneralizedContinuedFraction.IsSimpleContinuedFraction.

Equations

• SimpleContinuedFraction α = { g : GeneralizedContinuedFraction α // GeneralizedContinuedFraction.IsSimpleContinuedFraction g }

def SimpleContinuedFraction.ofInteger {α : Type u_1} [One α] (a : α) : SimpleContinuedFraction α

Constructs a simple continued fraction without fractional part.

Equations

• SimpleContinuedFraction.ofInteger a = { val := GeneralizedContinuedFraction.ofInteger a, property := ⋯ }

instance SimpleContinuedFraction.instInhabitedSimpleContinuedFraction {α : Type u_1} [One α] : Inhabited (SimpleContinuedFraction α)

Equations

• SimpleContinuedFraction.instInhabitedSimpleContinuedFraction = { default := SimpleContinuedFraction.ofInteger 1 }

instance SimpleContinuedFraction.instCoeSimpleContinuedFractionGeneralizedContinuedFraction {α : Type u_1} [One α] : Coe (SimpleContinuedFraction α) (GeneralizedContinuedFraction α)

Lift a scf to a gcf using the inclusion map.

Equations

• SimpleContinuedFraction.instCoeSimpleContinuedFractionGeneralizedContinuedFraction = { coe := Subtype.val }

def SimpleContinuedFraction.IsContinuedFraction {α : Type u_1} [One α] [Zero α] [LT α] (s : SimpleContinuedFraction α) : Prop

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

Equations

• SimpleContinuedFraction.IsContinuedFraction s = ∀ (n : ℕ) (bₙ : α), Stream'.Seq.get? (GeneralizedContinuedFraction.partialDenominators ↑s) n = some bₙ → 0 < bₙ

def ContinuedFraction (α : 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 SimpleContinuedFraction.IsContinuedFraction.

Equations

• ContinuedFraction α = { s : SimpleContinuedFraction α // SimpleContinuedFraction.IsContinuedFraction s }

Interlude: define some expected coercions.

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

Constructs a continued fraction without fractional part.

Equations

• ContinuedFraction.ofInteger a = { val := SimpleContinuedFraction.ofInteger a, property := ⋯ }

instance ContinuedFraction.instInhabitedContinuedFraction {α : Type u_1} [One α] [Zero α] [LT α] : Inhabited (ContinuedFraction α)

Equations

• ContinuedFraction.instInhabitedContinuedFraction = { default := ContinuedFraction.ofInteger 0 }

instance ContinuedFraction.instCoeContinuedFractionSimpleContinuedFraction {α : Type u_1} [One α] [Zero α] [LT α] : Coe (ContinuedFraction α) (SimpleContinuedFraction α)

Lift a cf to a scf using the inclusion map.

Equations

• ContinuedFraction.instCoeContinuedFractionSimpleContinuedFraction = { coe := Subtype.val }

instance ContinuedFraction.instCoeContinuedFractionGeneralizedContinuedFraction {α : Type u_1} [One α] [Zero α] [LT α] : Coe (ContinuedFraction α) (GeneralizedContinuedFraction α)

Lift a cf to a scf using the inclusion map.

Equations

• ContinuedFraction.instCoeContinuedFractionGeneralizedContinuedFraction = { coe := fun (c : ContinuedFraction α) => ↑↑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₋₁ = 1, A₀ = h, Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂, and
• B₋₁ = 0, B₀ = 1, Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂.

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 GeneralizedContinuedFraction.nextNumerator {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

• GeneralizedContinuedFraction.nextNumerator a b ppredA predA = b * predA + a * ppredA

def GeneralizedContinuedFraction.nextDenominator {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

• GeneralizedContinuedFraction.nextDenominator aₙ bₙ ppredB predB = bₙ * predB + aₙ * ppredB

def GeneralizedContinuedFraction.nextContinuants {K : Type u_2} [DivisionRing K] (a : K) (b : K) (ppred : GeneralizedContinuedFraction.Pair K) (pred : GeneralizedContinuedFraction.Pair K) : GeneralizedContinuedFraction.Pair K

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

Equations

• One or more equations did not get rendered due to their size.

def GeneralizedContinuedFraction.continuantsAux {K : Type u_2} [DivisionRing K] (g : GeneralizedContinuedFraction K) : Stream' (GeneralizedContinuedFraction.Pair K)

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

Equations

• One or more equations did not get rendered due to their size.
• GeneralizedContinuedFraction.continuantsAux g 0 = { a := 1, b := 0 }
• GeneralizedContinuedFraction.continuantsAux g 1 = { a := g.h, b := 1 }

def GeneralizedContinuedFraction.continuants {K : Type u_2} [DivisionRing K] (g : GeneralizedContinuedFraction K) : Stream' (GeneralizedContinuedFraction.Pair K)

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

Equations

• GeneralizedContinuedFraction.continuants g = Stream'.tail (GeneralizedContinuedFraction.continuantsAux g)

def GeneralizedContinuedFraction.numerators {K : Type u_2} [DivisionRing K] (g : GeneralizedContinuedFraction K) : Stream' K

Returns the numerators Aₙ of g.

Equations

• GeneralizedContinuedFraction.numerators g = Stream'.map GeneralizedContinuedFraction.Pair.a (GeneralizedContinuedFraction.continuants g)

def GeneralizedContinuedFraction.denominators {K : Type u_2} [DivisionRing K] (g : GeneralizedContinuedFraction K) : Stream' K

Returns the denominators Bₙ of g.

Equations

• GeneralizedContinuedFraction.denominators g = Stream'.map GeneralizedContinuedFraction.Pair.b (GeneralizedContinuedFraction.continuants g)

def GeneralizedContinuedFraction.convergents {K : Type u_2} [DivisionRing K] (g : GeneralizedContinuedFraction K) : Stream' K

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

Equations

• GeneralizedContinuedFraction.convergents g n = GeneralizedContinuedFraction.numerators g n / GeneralizedContinuedFraction.denominators g n

def GeneralizedContinuedFraction.convergents'Aux {K : Type u_2} [DivisionRing K] : Stream'.Seq (GeneralizedContinuedFraction.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

• One or more equations did not get rendered due to their size.
• GeneralizedContinuedFraction.convergents'Aux x 0 = 0

def GeneralizedContinuedFraction.convergents' {K : Type u_2} [DivisionRing K] (g : GeneralizedContinuedFraction K) (n : ℕ) : 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

• GeneralizedContinuedFraction.convergents' g n = g.h + GeneralizedContinuedFraction.convergents'Aux g.s n