# mathlibdocumentation

algebra.continued_fractions.computation.approximation_corollaries

# Corollaries From Approximation Lemmas (algebra.continued_fractions.computation.approximations) #

## Summary #

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

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

## Main Definitions #

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

## Main Theorems #

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

## Tags #

convergence, fractions

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

Creates the simple continued fraction of a value.

Equations
def continued_fraction.of {K : Type u_1} (v : K) [floor_ring K] :

Creates the continued fraction of a value.

Equations
• = _inst_2, _⟩

### Convergence #

We next show that (generalized_continued_fraction.of v).convergents v converges to v.

theorem generalized_continued_fraction.of_convergence_epsilon {K : Type u_1} (v : K) [floor_ring K] [archimedean K] (ε : K) (H : ε > 0) :
∃ (N : ), ∀ (n : ), n N
theorem generalized_continued_fraction.of_convergence {K : Type u_1} (v : K) [floor_ring K] [archimedean K]  :