Corollaries From Approximation Lemmas (Algebra.ContinuedFractions.Computation.Approximations) #

Summary #

We show that the generalized continued fraction given by GenContFract.of in fact is a (regular) continued fraction. Using the equivalence of the convergents computations (GenContFract.convs and GenContFract.convs') for continued fractions (see Algebra.ContinuedFractions.ConvergentsEquiv), it follows that the convergents computations for GenContFract.of are equivalent.

Moreover, we show the convergence of the continued fractions computations, that is (GenContFract.of v).convs indeed computes v in the limit.

Main Definitions #

Main Theorems #

Tags #

convergence, fractions

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.

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.

    Instances For
      theorem GenContFract.convs_succ {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] (n : ) :
      (GenContFract.of v).convs (n + 1) = v + 1 / (GenContFract.of (Int.fract v)⁻¹).convs n

      The recurrence relation for the convergents of the continued fraction expansion of an element v of K in terms of the convergents of the inverse of its fractional part.

      Convergence #

      We next show that (GenContFract.of v).convs v converges to v.

      theorem GenContFract.of_convergence_epsilon {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] [Archimedean K] (ε : K) :
      ε > 0∃ (N : ), nN, |v - (GenContFract.of v).convs n| < ε