mathlib3 documentation

algebra.continued_fractions.computation.approximations

Approximations for Continued Fraction Computations (`generalized_continued_fraction.of`) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

References #

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

theorem generalized_continued_fraction.int_fract_pair.nth_stream_fr_nonneg_lt_one {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] {ifp_n : generalized_continued_fraction.int_fract_pair K} (nth_stream_eq : generalized_continued_fraction.int_fract_pair.stream v n = option.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 : ℕ} [linear_ordered_field K] [floor_ring K] {ifp_n : generalized_continued_fraction.int_fract_pair K} (nth_stream_eq : generalized_continued_fraction.int_fract_pair.stream v n = option.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 : ℕ} [linear_ordered_field K] [floor_ring K] {ifp_n : generalized_continued_fraction.int_fract_pair K} (nth_stream_eq : generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp_n) :

ifp_n.fr < 1

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

theorem generalized_continued_fraction.int_fract_pair.one_le_succ_nth_stream_b {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] {ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (succ_nth_stream_eq : generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.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 : ℕ} [linear_ordered_field K] [floor_ring K] {ifp_n ifp_succ_n : generalized_continued_fraction.int_fract_pair K} (nth_stream_eq : generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp_n) (succ_nth_stream_eq : generalized_continued_fraction.int_fract_pair.stream v (n + 1) = option.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ₙ

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

theorem generalized_continued_fraction.of_one_le_nth_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 = option.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 : ℕ} [linear_ordered_field K] [floor_ring K] {gp : generalized_continued_fraction.pair K} (nth_s_eq : (generalized_continued_fraction.of v).s.nth n = option.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 : ℕ} [linear_ordered_field K] [floor_ring K] {a : K} (nth_part_num_eq : (generalized_continued_fraction.of v).partial_numerators.nth n = option.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 = option.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ₙ₊₁.

theorem generalized_continued_fraction.fib_le_of_continuants_aux_b {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] :

n ≤ 1 ∨ ¬(generalized_continued_fraction.of v).terminated_at (n - 2) → ↑(nat.fib n) ≤ ((generalized_continued_fraction.of v).continuants_aux n).b

theorem generalized_continued_fraction.succ_nth_fib_le_of_nth_denom {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] (hyp : n = 0 ∨ ¬(generalized_continued_fraction.of v).terminated_at (n - 1)) :

↑(nat.fib (n + 1)) ≤ (generalized_continued_fraction.of v).denominators n

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.

theorem generalized_continued_fraction.zero_le_of_continuants_aux_b {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] :

0 ≤ ((generalized_continued_fraction.of v).continuants_aux n).b

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

0 ≤ (generalized_continued_fraction.of v).denominators n

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 : ℕ} [linear_ordered_field K] [floor_ring K] {b : K} (nth_part_denom_eq : (generalized_continued_fraction.of v).partial_denominators.nth n = option.some b) :

b * ((generalized_continued_fraction.of v).continuants_aux (n + 1)).b ≤ ((generalized_continued_fraction.of v).continuants_aux (n + 2)).b

theorem generalized_continued_fraction.le_of_succ_nth_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 = option.some b) :

b * (generalized_continued_fraction.of v).denominators n ≤ (generalized_continued_fraction.of v).denominators (n + 1)

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 : ℕ} [linear_ordered_field K] [floor_ring K] :

(generalized_continued_fraction.of v).denominators n ≤ (generalized_continued_fraction.of v).denominators (n + 1)

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).

theorem generalized_continued_fraction.determinant_aux {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] (hyp : n = 0 ∨ ¬(generalized_continued_fraction.of v).terminated_at (n - 1)) :

((generalized_continued_fraction.of v).continuants_aux n).a * ((generalized_continued_fraction.of v).continuants_aux (n + 1)).b - ((generalized_continued_fraction.of v).continuants_aux n).b * ((generalized_continued_fraction.of v).continuants_aux (n + 1)).a = (-1) ^ n

theorem generalized_continued_fraction.determinant {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] (not_terminated_at_n : ¬(generalized_continued_fraction.of v).terminated_at n) :

(generalized_continued_fraction.of v).numerators n * (generalized_continued_fraction.of v).denominators (n + 1) - (generalized_continued_fraction.of v).denominators n * (generalized_continued_fraction.of v).numerators (n + 1) = (-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|.

theorem generalized_continued_fraction.sub_convergents_eq {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] {ifp : generalized_continued_fraction.int_fract_pair K} (stream_nth_eq : generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp) :

let g : generalized_continued_fraction K := generalized_continued_fraction.of v, B : K := (g.continuants_aux (n + 1)).b, pB : K := (g.continuants_aux n).b in v - g.convergents n = ite (ifp.fr = 0) 0 ((-1) ^ n / (B * ((ifp.fr)⁻¹ * B + pB)))

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

theorem generalized_continued_fraction.abs_sub_convergents_le {K : Type u_1} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K] (not_terminated_at_n : ¬(generalized_continued_fraction.of v).terminated_at n) :

|v - (generalized_continued_fraction.of v).convergents n| ≤ 1 / ((generalized_continued_fraction.of v).denominators n * (generalized_continued_fraction.of v).denominators (n + 1))

Shows that |v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁)

theorem generalized_continued_fraction.abs_sub_convergents_le' {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 = option.some b) :

|v - (generalized_continued_fraction.of v).convergents n| ≤ 1 / (b * (generalized_continued_fraction.of v).denominators n * (generalized_continued_fraction.of v).denominators n)

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.