# mathlibdocumentation

algebra.continued_fractions.computation.approximations

# Approximations for Continued Fraction Computations (generalized_continued_fraction.of) #

## Summary #

This file contains useful approximations for the values involved in the continued fractions computation generalized_continued_fraction.of. In particular, we derive the so-called determinant formula for generalized_continued_fraction.of: Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1).

Moreover, we derive some upper bounds for the error term when computing a continued fraction up a given position, i.e. bounds for the term |v - (generalized_continued_fraction.of v).convergents n|. The derived bounds will show us that the error term indeed gets smaller. As a corollary, we will be able to show that (generalized_continued_fraction.of v).convergents converges to v in algebra.continued_fractions.computation.approximation_corollaries.

## Main Theorems #

• generalized_continued_fraction.of_part_num_eq_one: shows that all partial numerators aᵢ are equal to one.
• generalized_continued_fraction.exists_int_eq_of_part_denom: shows that all partial denominators bᵢ correspond to an integer.
• generalized_continued_fraction.one_le_of_nth_part_denom: shows that 1 ≤ bᵢ.
• generalized_continued_fraction.succ_nth_fib_le_of_nth_denom: shows that the nth denominator Bₙ is greater than or equal to the n + 1th fibonacci number nat.fib (n + 1).
• generalized_continued_fraction.le_of_succ_nth_denom: shows that bₙ * Bₙ ≤ Bₙ₊₁, where bₙ is the nth partial denominator of the continued fraction.
• generalized_continued_fraction.abs_sub_convergents_le: shows that |v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁), where Aₙ is the nth partial numerator.