mathlib documentation


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 #

Main Theorems #

Tags #

convergence, fractions

Creates the simple continued fraction of a value.


Creates the continued fraction of a value.


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) [linear_ordered_field K] [floor_ring K] [archimedean K] (ε : K) (H : ε > 0) :
∃ (N : ), ∀ (n : ), n N|v - (generalized_continued_fraction.of v).convergents n| < ε