Computable Continued Fractions

Summary

We formalise the standard computation of (regular) continued fractions for linear ordered floor fields. The algorithm is rather simple. Here is an outline of the procedure adapted from Wikipedia:

Take a value v. We call ⌊v⌋ the integer part of v and v - ⌊v⌋ the fractional part of v. A continued fraction representation of v can then be given by [⌊v⌋; b₀, b₁, b₂,...], where [b₀; b₁, b₂,...] recursively is the continued fraction representation of 1 / (v - ⌊v⌋). This process stops when the fractional part hits 0.

In other words: to calculate a continued fraction representation of a number v, write down the integer part (i.e. the floor) of v. Subtract this integer part from v. If the difference is 0, stop; otherwise find the reciprocal of the difference and repeat. The procedure will terminate if and only if v is rational.

For an example, refer to IntFractPair.stream.

Main definitions

• GenContFract.IntFractPair.stream: computes the stream of integer and fractional parts of a given value as described in the summary.
• GenContFract.of: computes the generalised continued fraction of a value v. In fact, it computes a regular continued fraction that terminates if and only if v is rational.

Implementation Notes

There is an intermediate definition GenContFract.IntFractPair.seq1 between GenContFract.IntFractPair.stream and GenContFract.of to wire up things. Users should not (need to) directly interact with it.

The computation of the integer and fractional pairs of a value can elegantly be captured by a recursive computation of a stream of option pairs. This is done in IntFractPair.stream. However, the type then does not guarantee the first pair to always be some value, as expected by a continued fraction.

To separate concerns, we first compute a single head term that always exists in GenContFract.IntFractPair.seq1 followed by the remaining stream of option pairs. This sequence with a head term (seq1) is then transformed to a generalized continued fraction in GenContFract.of by extracting the wanted integer parts of the head term and the stream.

References

• https://en.wikipedia.org/wiki/Continued_fraction

Tags

numerics, number theory, approximations, fractions

structure GenContFract.IntFractPair (K : Type u_1) : Type u_1

We collect an integer part b = ⌊v⌋ and fractional part fr = v - ⌊v⌋ of a value v in a pair ⟨b, fr⟩.

• b : ℤ
• fr : K

Interlude: define some expected coercions and instances.

instance GenContFract.IntFractPair.instRepr {K : Type u_1} [Repr K] : Repr (GenContFract.IntFractPair K)

Make an IntFractPair printable.

Equations

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

instance GenContFract.IntFractPair.inhabited {K : Type u_1} [Inhabited K] : Inhabited (GenContFract.IntFractPair K)

Equations

• GenContFract.IntFractPair.inhabited = { default := { b := 0, fr := default } }

def GenContFract.IntFractPair.mapFr {K : Type u_1} {β : Type u_2} (f : K → β) (gp : GenContFract.IntFractPair K) : GenContFract.IntFractPair β

Maps a function f on the fractional components of a given pair.

Equations

• GenContFract.IntFractPair.mapFr f gp = { b := gp.b, fr := f gp.fr }

Interlude: define some expected coercions.

def GenContFract.IntFractPair.coeFn {K : Type u_1} {β : Type u_2} [Coe K β] : GenContFract.IntFractPair K → GenContFract.IntFractPair β

The coercion between integer-fraction pairs happens componentwise.

Equations

• GenContFract.IntFractPair.coeFn = GenContFract.IntFractPair.mapFr Coe.coe

instance GenContFract.IntFractPair.coe {K : Type u_1} {β : Type u_2} [Coe K β] : Coe (GenContFract.IntFractPair K) (GenContFract.IntFractPair β)

Coerce a pair by coercing the fractional component.

Equations

• GenContFract.IntFractPair.coe = { coe := GenContFract.IntFractPair.coeFn }

@[simp]

theorem GenContFract.IntFractPair.coe_to_intFractPair {K : Type u_1} {β : Type u_2} [Coe K β] {b : ℤ} {fr : K} : ↑{ b := b, fr := fr } = { b := b, fr := Coe.coe fr }

def GenContFract.IntFractPair.of {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : GenContFract.IntFractPair K

Creates the integer and fractional part of a value v, i.e. ⟨⌊v⌋, v - ⌊v⌋⟩.

Equations

• GenContFract.IntFractPair.of v = { b := ⌊v⌋, fr := Int.fract v }

def GenContFract.IntFractPair.stream {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : Stream' (Option (GenContFract.IntFractPair K))

Creates the stream of integer and fractional parts of a value v needed to obtain the continued fraction representation of v in GenContFract.of. More precisely, given a value v : K, it recursively computes a stream of option ℤ × K pairs as follows:

• stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩
• stream v (n + 1) = some ⟨⌊frₙ⁻¹⌋, frₙ⁻¹ - ⌊frₙ⁻¹⌋⟩, if stream v n = some ⟨_, frₙ⟩ and frₙ ≠ 0
• stream v (n + 1) = none, otherwise

For example, let (v : ℚ) := 3.4. The process goes as follows:

• stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩ = some ⟨3, 0.4⟩
• stream v 1 = some ⟨⌊0.4⁻¹⌋, 0.4⁻¹ - ⌊0.4⁻¹⌋⟩ = some ⟨⌊2.5⌋, 2.5 - ⌊2.5⌋⟩ = some ⟨2, 0.5⟩
• stream v 2 = some ⟨⌊0.5⁻¹⌋, 0.5⁻¹ - ⌊0.5⁻¹⌋⟩ = some ⟨⌊2⌋, 2 - ⌊2⌋⟩ = some ⟨2, 0⟩
• stream v n = none, for n ≥ 3

Equations

• One or more equations did not get rendered due to their size.
• GenContFract.IntFractPair.stream v 0 = some (GenContFract.IntFractPair.of v)

theorem GenContFract.IntFractPair.stream_isSeq {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : (GenContFract.IntFractPair.stream v).IsSeq

Shows that IntFractPair.stream has the sequence property, that is once we return none at position n, we also return none at n + 1.

def GenContFract.IntFractPair.seq1 {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : Stream'.Seq1 (GenContFract.IntFractPair K)

Uses IntFractPair.stream to create a sequence with head (i.e. seq1) of integer and fractional parts of a value v. The first value of IntFractPair.stream is never none, so we can safely extract it and put the tail of the stream in the sequence part.

This is just an intermediate representation and users should not (need to) directly interact with it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in Algebra.ContinuedFractions.Computation.Translations.

Equations

• GenContFract.IntFractPair.seq1 v = (GenContFract.IntFractPair.of v, Stream'.Seq.tail ⟨GenContFract.IntFractPair.stream v, ⋯⟩)

def GenContFract.of {K : Type u_1} [LinearOrderedField K] [FloorRing K] (v : K) : GenContFract K

Returns the GenContFract of a value. In fact, the returned gcf is also a ContFract that terminates if and only if v is rational (see Algebra.ContinuedFractions.Computation.TerminatesIffRat).

The continued fraction representation of v is given by [⌊v⌋; b₀, b₁, b₂,...], where [b₀; b₁, b₂,...] recursively is the continued fraction representation of 1 / (v - ⌊v⌋). This process stops when the fractional part v - ⌊v⌋ hits 0 at some step.

The implementation uses IntFractPair.stream to obtain the partial denominators of the continued fraction. Refer to said function for more details about the computation process.

Equations

• GenContFract.of v = match GenContFract.IntFractPair.seq1 v with | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun (p : GenContFract.IntFractPair K) => { a := 1, b := ↑p.b }) s }