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

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

## Main Theorems #

• GenContFract.of_convs_eq_convs' shows that the convergents computations for GenContFract.of are equivalent.
• GenContFract.of_convergence shows that (GenContFract.of v).convs converges to v.

## Tags #

convergence, fractions

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

Creates the simple continued fraction of a value.

Equations
• = ⟨,
Instances For
theorem SimpContFract.of_isContFract {K : Type u_1} (v : K) [] :
().IsContFract
def ContFract.of {K : Type u_1} (v : K) [] :

Creates the continued fraction of a value.

Equations
• = ⟨,
Instances For
theorem GenContFract.of_convs_eq_convs' {K : Type u_1} (v : K) [] :
().convs = ().convs'
theorem GenContFract.convs_succ {K : Type u_1} (v : K) [] (n : ) :
().convs (n + 1) = v + 1 / ().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) [] [] (ε : K) :
ε > 0∃ (N : ), nN, |v - ().convs n| < ε
theorem GenContFract.of_convergence {K : Type u_1} (v : K) [] [] [] [] :
Filter.Tendsto ().convs Filter.atTop (nhds v)