Documentation

Mathlib.Algebra.ContinuedFractions.Computation.Approximations

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 #

References #

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

Creates the simple continued fraction of a value.

Equations
Instances For
    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] :

    Creates the continued fraction of a value.

    Equations
    Instances For

      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.