# 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
`ContinuedFractions`

in the library. - 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 #

We collect a partial numerator `aᵢ`

and partial denominator `bᵢ`

in a pair `⟨aᵢ, bᵢ⟩`

.

- a : α
Partial numerator

- b : α
Partial denominator

## Instances For

## Equations

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

Interlude: define some expected coercions and instances.

Make a `GCF.Pair`

printable.

## Equations

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

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 }

## Instances For

The coercion between numerator-denominator pairs happens componentwise.

## Equations

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

## Instances For

Coerce a pair by elementwise coercion.

## Equations

- GeneralizedContinuedFraction.Pair.instCoePairPair = { coe := GeneralizedContinuedFraction.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
`GeneralizedContinuedFraction.Pair`

s `s`

.
For convenience, one often writes `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`

.

- h : α
Head term

Sequence of partial numerator and denominator pairs.

## Instances For

Constructs a generalized continued fraction without fractional part.

## Equations

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

## Instances For

## Equations

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

Returns the sequence of partial numerators `aᵢ`

of `g`

.

## Equations

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

## Instances For

Returns the sequence of partial denominators `bᵢ`

of `g`

.

## Equations

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

## Instances For

A gcf terminated at position `n`

if its sequence terminates at position `n`

.

## Equations

## Instances For

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

## Equations

- GeneralizedContinuedFraction.terminatedAtDecidable g n = id inferInstance

A gcf terminates if its sequence terminates.

## Equations

## Instances For

Interlude: define some expected coercions.

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 }

## Instances For

Coerce a gcf by elementwise coercion.

## Equations

- GeneralizedContinuedFraction.instCoeGeneralizedContinuedFractionGeneralizedContinuedFraction = { coe := GeneralizedContinuedFraction.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}}}}
$$

## Equations

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

## 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
`GeneralizedContinuedFraction.IsSimpleContinuedFraction`

.

## Equations

## Instances For

Constructs a simple continued fraction without fractional part.

## Equations

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

## Instances For

## Equations

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

Lift a scf to a gcf using the inclusion map.

## Equations

- SimpleContinuedFraction.instCoeSimpleContinuedFractionGeneralizedContinuedFraction = { 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ᵢ`

.

## Equations

- SimpleContinuedFraction.IsContinuedFraction s = ∀ (n : ℕ) (bₙ : α), Stream'.Seq.get? (GeneralizedContinuedFraction.partialDenominators ↑s) n = some bₙ → 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
`SimpleContinuedFraction.IsContinuedFraction`

.

## Equations

## Instances For

Interlude: define some expected coercions.

Constructs a continued fraction without fractional part.

## Equations

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

## Instances For

## Equations

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

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ₙ`

.

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

## 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

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

## Instances For

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.

## Instances For

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 }

## Instances For

Returns the continuants `⟨Aₙ, Bₙ⟩`

of `g`

.

## Equations

## Instances For

Returns the numerators `Aₙ`

of `g`

.

## Equations

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

## Instances For

Returns the denominators `Bₙ`

of `g`

.

## Equations

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

## Instances For

Returns the convergents `Aₙ / Bₙ`

of `g`

, where `Aₙ, Bₙ`

are the nth continuants of `g`

.

## Equations

## Instances For

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

## Instances For

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`