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 #
- Generalised continued fractions (gcfs)
- Simple continued fractions (scfs)
- (Regular) continued fractions ((r)cfs)
- Computation of convergents using the recurrence relation in
convs
. - Computation of convergents by directly evaluating the fraction described by the gcf in
convs'
.
Implementation notes #
- The most commonly used kind of continued fractions in the literature are regular continued
fractions. We hence just call them
ContFract
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
Tags #
numerics, number theory, approximations, fractions
Definitions #
We collect a partial numerator aᵢ
and partial denominator bᵢ
in a pair ⟨aᵢ, bᵢ⟩
.
- a : α
Partial numerator
- b : α
Partial denominator
Instances For
Equations
- GenContFract.instInhabitedPair = { default := { a := default, b := default } }
Interlude: define some expected coercions and instances.
Make a GenContFract.Pair
printable.
Equations
- GenContFract.Pair.instRepr = { reprPrec := fun (p : GenContFract.Pair α) (x : ℕ) => Std.Format.text "(a : " ++ repr p.a ++ Std.Format.text ", b : " ++ repr p.b ++ Std.Format.text ")" }
Maps a function f
on both components of a given pair.
Equations
- GenContFract.Pair.map f gp = { a := f gp.a, b := f gp.b }
Instances For
The coercion between numerator-denominator pairs happens componentwise.
Equations
- GenContFract.Pair.coeFn = GenContFract.Pair.map Coe.coe
Instances For
Coerce a pair by elementwise coercion.
Equations
- GenContFract.Pair.instCoe = { coe := GenContFract.Pair.coeFn }
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.Pair
s
s
.
For convenience, one often writes [h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]
.
- h : α
Head term
- s : Stream'.Seq (GenContFract.Pair α)
Sequence of partial numerator and denominator pairs.
Instances For
Constructs a generalized continued fraction without fractional part.
Equations
- GenContFract.ofInteger a = { h := a, s := Stream'.Seq.nil }
Instances For
Equations
- GenContFract.instInhabited = { default := GenContFract.ofInteger default }
Returns the sequence of partial numerators aᵢ
of g
.
Equations
- g.partNums = Stream'.Seq.map GenContFract.Pair.a g.s
Instances For
Returns the sequence of partial denominators bᵢ
of g
.
Equations
- g.partDens = Stream'.Seq.map GenContFract.Pair.b g.s
Instances For
A gcf terminated at position n
if its sequence terminates at position n
.
Equations
- g.TerminatedAt n = g.s.TerminatedAt n
Instances For
It is decidable whether a gcf terminated at a given position.
Interlude: define some expected coercions.
The coercion between GenContFract
happens on the head term
and all numerator-denominator pairs componentwise.
Equations
- ↑g = { h := Coe.coe g.h, s := Stream'.Seq.map GenContFract.Pair.coeFn g.s }
Instances For
Coerce a gcf by elementwise coercion.
Equations
- GenContFract.instCoe = { coe := GenContFract.coeFn }
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}}}} $$
Instances For
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
- SimpContFract α = { g : GenContFract α // g.IsSimpContFract }
Instances For
Constructs a simple continued fraction without fractional part.
Equations
Instances For
Equations
- SimpContFract.instInhabited = { default := SimpContFract.ofInteger 1 }
Lift a scf to a gcf using the inclusion map.
Equations
- SimpContFract.instCoeGenContFract = { coe := Subtype.val }
A simple continued fraction is a (regular) continued fraction ((r)cf) if all partial denominators
bᵢ
are positive, i.e. 0 < bᵢ
.
Instances For
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
- ContFract α = { s : SimpContFract α // s.IsContFract }
Instances For
Interlude: define some expected coercions.
Constructs a continued fraction without fractional part.
Equations
- ContFract.ofInteger a = ⟨SimpContFract.ofInteger a, ⋯⟩
Instances For
Equations
- ContFract.instInhabited = { default := ContFract.ofInteger 0 }
Lift a cf to a scf using the inclusion map.
Equations
- ContFract.instCoeSimpContFract = { coe := Subtype.val }
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ₙ₋₂
, andB₋₁ = 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ₙ
.
Returns the next numerator Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂
, where predA
is Aₙ₋₁
,
ppredA
is Aₙ₋₂
, a
is aₙ₋₁
, and b
is bₙ₋₁
.
Equations
- GenContFract.nextNum a b ppredA predA = b * predA + a * ppredA
Instances For
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
- GenContFract.nextDen aₙ bₙ ppredB predB = bₙ * predB + aₙ * ppredB
Instances For
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
- GenContFract.nextConts a b ppred pred = { a := GenContFract.nextNum a b ppred.a pred.a, b := GenContFract.nextDen a b ppred.b pred.b }
Instances For
Returns the continuants ⟨Aₙ₋₁, Bₙ₋₁⟩
of g
.
Equations
Instances For
Returns the continuants ⟨Aₙ, Bₙ⟩
of g
.
Equations
- g.conts = g.contsAux.tail
Instances For
Returns the numerators Aₙ
of g
.
Equations
- g.nums = Stream'.map GenContFract.Pair.a g.conts
Instances For
Returns the denominators Bₙ
of g
.
Equations
- g.dens = Stream'.map GenContFract.Pair.b g.conts
Instances For
Returns the convergents Aₙ / Bₙ
of g
, where Aₙ, Bₙ
are the nth continuants of g
.
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
- GenContFract.convs'Aux x 0 = 0
- GenContFract.convs'Aux x n.succ = match x.head with | none => 0 | some gp => gp.a / (gp.b + GenContFract.convs'Aux x.tail n)
Instances For
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
- g.convs' n = g.h + GenContFract.convs'Aux g.s n