Approximations for Continued Fraction Computations (GenContFract.of)

Summary

This file contains useful approximations for the values involved in the continued fractions computation GenContFract.of. In particular, we show that the generalized continued fraction given by GenContFract.of in fact is a (regular) continued fraction.

Moreover, we derive some upper bounds for the error term when computing a continued fraction up a given position, i.e. bounds for the term |v - (GenContFract.of v).convs n|. The derived bounds will show us that the error term indeed gets smaller. As a corollary, we will be able to show that (GenContFract.of v).convs converges to v in Algebra.ContinuedFractions.Computation.ApproximationCorollaries.

Main Theorems

• GenContFract.of_partNum_eq_one: shows that all partial numerators aᵢ are equal to one.
• GenContFract.exists_int_eq_of_partDen: shows that all partial denominators bᵢ correspond to an integer.
• GenContFract.of_one_le_get?_partDen: shows that 1 ≤ bᵢ.
• ContFract.of returns the regular continued fraction of a value.
• GenContFract.succ_nth_fib_le_of_nthDen: shows that the nth denominator Bₙ is greater than or equal to the n + 1th fibonacci number Nat.fib (n + 1).
• GenContFract.le_of_succ_get?_den: shows that bₙ * Bₙ ≤ Bₙ₊₁, where bₙ is the nth partial denominator of the continued fraction.
• GenContFract.abs_sub_convs_le: shows that |v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁), where Aₙ is the nth partial numerator.

References

• [Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph][hardy2008introduction]

We begin with some lemmas about the stream of IntFractPairs, which presumably are not of great interest for the end user.

theorem GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {ifp_n : GenContFract.IntFractPair K} (nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n) : 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Shows that the fractional parts of the stream are in [0,1).

theorem GenContFract.IntFractPair.nth_stream_fr_nonneg {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {ifp_n : GenContFract.IntFractPair K} (nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n) : 0 ≤ ifp_n.fr

Shows that the fractional parts of the stream are nonnegative.

theorem GenContFract.IntFractPair.nth_stream_fr_lt_one {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {ifp_n : GenContFract.IntFractPair K} (nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n) : ifp_n.fr < 1

Shows that the fractional parts of the stream are smaller than one.

theorem GenContFract.IntFractPair.one_le_succ_nth_stream_b {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {ifp_succ_n : GenContFract.IntFractPair K} (succ_nth_stream_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n) : 1 ≤ ifp_succ_n.b

Shows that the integer parts of the stream are at least one.

theorem GenContFract.IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {ifp_n : GenContFract.IntFractPair K} {ifp_succ_n : GenContFract.IntFractPair K} (nth_stream_eq : GenContFract.IntFractPair.stream v n = some ifp_n) (succ_nth_stream_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n) : ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹

Shows that the n + 1th integer part bₙ₊₁ of the stream is smaller or equal than the inverse of the nth fractional part frₙ of the stream. This result is straight-forward as bₙ₊₁ is defined as the floor of 1 / frₙ.

Next we translate above results about the stream of IntFractPairs to the computed continued fraction GenContFract.of.

theorem GenContFract.of_one_le_get?_partDen {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {b : K} (nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b) : 1 ≤ b

Shows that the integer parts of the continued fraction are at least one.

theorem GenContFract.of_partNum_eq_one_and_exists_int_partDen_eq {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {gp : GenContFract.Pair K} (nth_s_eq : (GenContFract.of v).s.get? n = some gp) : gp.a = 1 ∧ ∃ (z : ℤ), gp.b = ↑z

Shows that the partial numerators aᵢ of the continued fraction are equal to one and the partial denominators bᵢ correspond to integers.

theorem GenContFract.of_partNum_eq_one {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {a : K} (nth_partNum_eq : (GenContFract.of v).partNums.get? n = some a) : a = 1

Shows that the partial numerators aᵢ are equal to one.

theorem GenContFract.exists_int_eq_of_partDen {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {b : K} (nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b) : ∃ (z : ℤ), b = ↑z

Shows that the partial denominators bᵢ correspond to an integer.

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

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

Creates the simple continued fraction of a value.

Equations

• SimpContFract.of v = ⟨GenContFract.of v, ⋯⟩

theorem SimpContFract.of_isContFract {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] : (SimpContFract.of v).IsContFract

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

Creates the continued fraction of a value.

Equations

• ContFract.of v = ⟨SimpContFract.of v, ⋯⟩

One of our next goals is to show that bₙ * Bₙ ≤ Bₙ₊₁. For this, we first show that the partial denominators Bₙ are bounded from below by the fibonacci sequence Nat.fib. This then implies that 0 ≤ Bₙ and hence Bₙ₊₂ = bₙ₊₁ * Bₙ₊₁ + Bₙ ≥ bₙ₊₁ * Bₙ₊₁ + 0 = bₙ₊₁ * Bₙ₊₁.

theorem GenContFract.fib_le_of_contsAux_b {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] : n ≤ 1 ∨ ¬(GenContFract.of v).TerminatedAt (n - 2) → ↑(Nat.fib n) ≤ ((GenContFract.of v).contsAux n).b

theorem GenContFract.succ_nth_fib_le_of_nth_den {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] (hyp : n = 0 ∨ ¬(GenContFract.of v).TerminatedAt (n - 1)) : ↑(Nat.fib (n + 1)) ≤ (GenContFract.of v).dens n

Shows that the nth denominator is greater than or equal to the n + 1th fibonacci number, that is Nat.fib (n + 1) ≤ Bₙ.

As a simple consequence, we can now derive that all denominators are nonnegative.

theorem GenContFract.zero_le_of_contsAux_b {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] : 0 ≤ ((GenContFract.of v).contsAux n).b

theorem GenContFract.zero_le_of_den {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] : 0 ≤ (GenContFract.of v).dens n

Shows that all denominators are nonnegative.

theorem GenContFract.le_of_succ_succ_get?_contsAux_b {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {b : K} (nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b) : b * ((GenContFract.of v).contsAux (n + 1)).b ≤ ((GenContFract.of v).contsAux (n + 2)).b

theorem GenContFract.le_of_succ_get?_den {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {b : K} (nth_partDenom_eq : (GenContFract.of v).partDens.get? n = some b) : b * (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1)

Shows that bₙ * Bₙ ≤ Bₙ₊₁, where bₙ is the nth partial denominator and Bₙ₊₁ and Bₙ are the n + 1th and nth denominator of the continued fraction.

theorem GenContFract.of_den_mono {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] : (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1)

Shows that the sequence of denominators is monotone, that is Bₙ ≤ Bₙ₊₁.

Approximation of Error Term

Next we derive some approximations for the error term when computing a continued fraction up a given position, i.e. bounds for the term |v - (GenContFract.of v).convs n|.

theorem GenContFract.sub_convs_eq {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {ifp : GenContFract.IntFractPair K} (stream_nth_eq : GenContFract.IntFractPair.stream v n = some ifp) : let g := GenContFract.of v; let B := (g.contsAux (n + 1)).b; let pB := (g.contsAux n).b; v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

This lemma follows from the finite correctness proof, the determinant equality, and by simplifying the difference.

theorem GenContFract.abs_sub_convs_le {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] (not_terminatedAt_n : ¬(GenContFract.of v).TerminatedAt n) : |v - (GenContFract.of v).convs n| ≤ 1 / ((GenContFract.of v).dens n * (GenContFract.of v).dens (n + 1))

Shows that |v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁).

theorem GenContFract.abs_sub_convergents_le' {K : Type u_1} {v : K} {n : ℕ} [LinearOrderedField K] [FloorRing K] {b : K} (nth_partDen_eq : (GenContFract.of v).partDens.get? n = some b) : |v - (GenContFract.of v).convs n| ≤ 1 / (b * (GenContFract.of v).dens n * (GenContFract.of v).dens n)

Shows that |v - Aₙ / Bₙ| ≤ 1 / (bₙ * Bₙ * Bₙ). This bound is worse than the one shown in GenContFract.abs_sub_convs_le, but sometimes it is easier to apply and sufficient for one's use case.