mathlib documentation

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 #

References #

We begin with some lemmas about the stream of int_fract_pairs, which presumably are not of great interest for the end user.

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 are 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ₙ

Next we translate above results about the stream of int_fract_pairs to the computed continued fraction generalized_continued_fraction.of.

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.

theorem generalized_continued_fraction.of_part_num_eq_one {K : Type u_1} {v : K} {n : } [linear_ordered_field K] [floor_ring K] {a : K} (nth_part_num_eq : (generalized_continued_fraction.of v).partial_numerators.nth n = 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 : } [linear_ordered_field K] [floor_ring K] {b : K} (nth_part_denom_eq : (generalized_continued_fraction.of v).partial_denominators.nth n = some b) :
∃ (z : ), b = z

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

One of our next goals is to show that bₙ * Bₙ ≤ Bₙ₊₁. For this, we first show that the partial denominators Bₙ are bounded from below by the fibonacci sequence nat.fib. This then implies that 0 ≤ Bₙ and hence Bₙ₊₂ = bₙ₊₁ * Bₙ₊₁ + Bₙ ≥ bₙ₊₁ * Bₙ₊₁ + 0 = bₙ₊₁ * Bₙ₊₁.

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

As a simple consequence, we can now derive that all denominators are nonnegative.

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 monotone, that is Bₙ ≤ Bₙ₊₁.

Determinant Formula #

Next we prove the so-called determinant formula for generalized_continued_fraction.of: Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1).

The determinant formula Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)

Approximation of Error Term #

Next we derive some approximations 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|.

This lemma follows from the finite correctness proof, the determinant equality, and by simplifying the difference.

Shows that |v - Aₙ / Bₙ| ≤ 1 / (bₙ * Bₙ * Bₙ). This bound is worse than the one shown in gcf.abs_sub_convergents_le, but sometimes it is easier to apply and sufficient for one's use case.