# mathlib3documentation

algebra.continued_fractions.computation.approximation_corollaries

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## 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, _⟩
theorem generalized_continued_fraction.convergents_succ {K : Type u_1} (v : K) [floor_ring 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 (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