mathlib documentation

algebra.continued_fractions.computation.approximations

Approximations for Continued Fraction Computations (gcf.of)

Summary

Let us write gcf for generalized_continued_fraction. This file contains useful approximations for the values involved in the continued fractions computation gcf.of.

Main Theorems

References

Shows that the fractional parts of the stream are in [0,1).

Shows that the fractional parts of the stream are nonnegative.

Shows that the fractional parts of the stream smaller than one.

Shows that the integer parts of the stream are at least one.

Shows that the n + 1th integer part bₙ₊₁ of the stream is smaller or equal than the inverse of the nth fractional part frₙ of the stream. This result is straight-forward as bₙ₊₁ is defined as the floor of 1 / frₙ

Shows that the integer parts of the continued fraction are at least one.

Shows that the partial numerators aᵢ of the continued fraction are equal to one and the partial denominators bᵢ correspond to integers.

Shows that the partial numerators aᵢ are equal to one.

Shows that the partial denominators bᵢ correspond to an integer.

Shows that the nth denominator is greater than or equal to the n + 1th fibonacci number, that is nat.fib (n + 1) ≤ Bₙ.

Shows that all denominators are nonnegative.

Shows that Bₙ₊₁ ≥ bₙ * Bₙ, where bₙ is the nth partial denominator and Bₙ₊₁ and Bₙ are the n + 1th and nth denominator of the continued fraction.

Shows that the sequence of denominators is monotonically increasing, that is Bₙ ≤ Bₙ₊₁.