# mathlibdocumentation

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

• gcf.of_part_num_eq_one: shows that all partial numerators aᵢ are equal to one.
• gcf.exists_int_eq_of_part_denom: shows that all partial denominators bᵢ correspond to an integer.
• gcf.one_le_of_nth_part_denom: shows that 1 ≤ bᵢ.
• gcf.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).
• gcf.le_of_succ_nth_denom: shows that Bₙ₊₁ ≥ bₙ * Bₙ, where bₙ is the nth partial denominator of the continued fraction.

## References

• [Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph][hardy2008introduction]
theorem generalized_continued_fraction.int_fract_pair.nth_stream_fr_nonneg_lt_one {K : Type u_1} {v : K} {n : } [floor_ring K] (nth_stream_eq : = some ifp_n) :
0 ifp_n.fr ifp_n.fr < 1

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

theorem generalized_continued_fraction.int_fract_pair.nth_stream_fr_nonneg {K : Type u_1} {v : K} {n : } [floor_ring K] (nth_stream_eq : = some ifp_n) :
0 ifp_n.fr

Shows that the fractional parts of the stream are nonnegative.

theorem generalized_continued_fraction.int_fract_pair.nth_stream_fr_lt_one {K : Type u_1} {v : K} {n : } [floor_ring K] (nth_stream_eq : = some ifp_n) :
ifp_n.fr < 1

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

theorem generalized_continued_fraction.int_fract_pair.one_le_succ_nth_stream_b {K : Type u_1} {v : K} {n : } [floor_ring K] {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (succ_nth_stream_eq : = some ifp_succ_n) :
1 ifp_succ_n.b

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

theorem generalized_continued_fraction.int_fract_pair.succ_nth_stream_b_le_nth_stream_fr_inv {K : Type u_1} {v : K} {n : } [floor_ring K] {ifp_n ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (nth_stream_eq : = some ifp_n) (succ_nth_stream_eq : = some ifp_succ_n) :
(ifp_succ_n.b) (ifp_n.fr)⁻¹

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ₙ

theorem generalized_continued_fraction.of_one_le_nth_part_denom {K : Type u_1} {v : K} {n : } [floor_ring K] {b : K} (nth_part_denom_eq : = some b) :
1 b

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

theorem generalized_continued_fraction.of_part_num_eq_one_and_exists_int_part_denom_eq {K : Type u_1} {v : K} {n : } [floor_ring K] (nth_s_eq : = some gp) :
gp.a = 1 ∃ (z : ), gp.b = z

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

theorem generalized_continued_fraction.of_part_num_eq_one {K : Type u_1} {v : K} {n : } [floor_ring K] {a : K} (nth_part_num_eq : = some a) :
a = 1

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

theorem generalized_continued_fraction.exists_int_eq_of_part_denom {K : Type u_1} {v : K} {n : } [floor_ring K] {b : K} (nth_part_denom_eq : = some b) :
∃ (z : ), b = z

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

theorem generalized_continued_fraction.fib_le_of_continuants_aux_b {K : Type u_1} {v : K} {n : } [floor_ring K] :
n 1 ¬

theorem generalized_continued_fraction.succ_nth_fib_le_of_nth_denom {K : Type u_1} {v : K} {n : } [floor_ring K] (hyp : n = 0 ¬) :
(nat.fib (n + 1))

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

theorem generalized_continued_fraction.zero_le_of_denom {K : Type u_1} {v : K} {n : } [floor_ring K] :

Shows that all denominators are nonnegative.

theorem generalized_continued_fraction.le_of_succ_succ_nth_continuants_aux_b {K : Type u_1} {v : K} {n : } [floor_ring K] {b : K} (nth_part_denom_eq : = some b) :
b * (n + 1)).b (n + 2)).b

theorem generalized_continued_fraction.le_of_succ_nth_denom {K : Type u_1} {v : K} {n : } [floor_ring K] {b : K} (nth_part_denom_eq : = some b) :

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.

theorem generalized_continued_fraction.of_denom_mono {K : Type u_1} {v : K} {n : } [floor_ring K] :

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