# Documentation

Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

# 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 #

• ContinuedFraction.of returns the (regular) continued fraction of a value.

## Main Theorems #

• GeneralizedContinuedFraction.of_convergents_eq_convergents' shows that the convergents computations for GeneralizedContinuedFraction.of are equivalent.
• GeneralizedContinuedFraction.of_convergence shows that (GeneralizedContinuedFraction.of v).convergents converges to v.

## Tags #

convergence, fractions

def SimpleContinuedFraction.of {K : Type u_1} (v : K) [] :

Creates the simple continued fraction of a value.

Instances For
def ContinuedFraction.of {K : Type u_1} (v : K) [] :

Creates the continued fraction of a value.

Instances For
theorem GeneralizedContinuedFraction.convergents_succ {K : Type u_1} (v : K) [] (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 (GeneralizedContinuedFraction.of v).convergents v converges to v.

theorem GeneralizedContinuedFraction.of_convergence_epsilon {K : Type u_1} (v : K) [] [] (ε : K) :
ε > 0N, ∀ (n : ), n N
theorem GeneralizedContinuedFraction.of_convergence {K : Type u_1} (v : K) [] [] [] :
Filter.Tendsto () Filter.atTop (nhds v)