# Documentation

Mathlib.Algebra.ContinuedFractions.Computation.Approximations

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

## Summary #

This file contains useful approximations for the values involved in the continued fractions computation GeneralizedContinuedFraction.of. In particular, we derive the so-called determinant formula for GeneralizedContinuedFraction.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 - (GeneralizedContinuedFraction.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 (GeneralizedContinuedFraction.of v).convergents converges to v in Algebra.ContinuedFractions.Computation.ApproximationCorollaries.

## Main Theorems #

• GeneralizedContinuedFraction.of_part_num_eq_one: shows that all partial numerators aᵢ are equal to one.
• GeneralizedContinuedFraction.exists_int_eq_of_part_denom: shows that all partial denominators bᵢ correspond to an integer.
• GeneralizedContinuedFraction.of_one_le_get?_part_denom: shows that 1 ≤ bᵢ.
• GeneralizedContinuedFraction.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).
• GeneralizedContinuedFraction.le_of_succ_get?_denom: shows that bₙ * Bₙ ≤ Bₙ₊₁, where bₙ is the nth partial denominator of the continued fraction.
• GeneralizedContinuedFraction.abs_sub_convergents_le: shows that |v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁), where Aₙ is the nth partial numerator.
• [Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph][hardy2008introduction]
• https://en.wikipedia.org/wiki/Generalized_continued_fraction#The_determinant_formula