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
gcf.of_part_num_eq_one: shows that all partial numeratorsaᵢare equal to one.gcf.exists_int_eq_of_part_denom: shows that all partial denominatorsbᵢcorrespond to an integer.gcf.one_le_of_nth_part_denom: shows that1 ≤ bᵢ.gcf.succ_nth_fib_le_of_nth_denom: shows that thenth denominatorBₙis greater than or equal to then + 1th fibonacci numbernat.fib (n + 1).gcf.le_of_succ_nth_denom: shows thatBₙ₊₁ ≥ bₙ * Bₙ, wherebₙis thenth partial denominator of the continued fraction.
References
- [Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph][hardy2008introduction]
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ₙ₊₁.