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

Summary #

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

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

Main Definitions #

Main Theorems #

Tags #

convergence, fractions

Creates the simple continued fraction of a value.

Instances For

    Creates the continued fraction of a value.

    Instances For

      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 (GeneralizedContinuedFraction.of v).convergents v converges to v.