Correctness of Terminating Continued Fraction Computations (`generalized_continued_fraction.of`) #

Summary #

We show the correctness of the algorithm computing continued fractions (generalized_continued_fraction.of) in case of termination in the following sense:

At every step n : ℕ, we can obtain the value v by adding a specific residual term to the last denominator of the fraction described by (generalized_continued_fraction.of v).convergents' n. The residual term will be zero exactly when the continued fraction terminated; otherwise, the residual term will be given by the fractional part stored in generalized_continued_fraction.int_fract_pair.stream v n.

For an example, refer to generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_some and for more information about the computation process, refer to algebra.continued_fraction.computation.basic.

Main definitions #

generalized_continued_fraction.comp_exact_value can be used to compute the exact value approximated by the continued fraction generalized_continued_fraction.of v by adding a residual term as described in the summary.

Main Theorems #

generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_some shows that generalized_continued_fraction.comp_exact_value indeed returns the value v when given the convergent and fractional part as described in the summary.
generalized_continued_fraction.of_correctness_of_terminated_at shows the equality v = (generalized_continued_fraction.of v).convergents n if generalized_continued_fraction.of v terminated at position n.

source

@[protected]

def generalized_continued_fraction.comp_exact_value {K : Type u_1} [linear_ordered_field K] (pconts conts : generalized_continued_fraction.pair K) (fr : K) :

Given two continuants pconts and conts and a value fr, this function returns

conts.a / conts.b if fr = 0
exact_conts.a / exact_conts.b where exact_conts = next_continuants 1 fr⁻¹ pconts conts otherwise.

This function can be used to compute the exact value approxmated by a continued fraction generalized_continued_fraction.of v as described in lemma comp_exact_value_correctness_of_stream_eq_some.

Equations

generalized_continued_fraction.comp_exact_value pconts conts fr = ite (fr = 0) (conts.a / conts.b) (let exact_conts : generalized_continued_fraction.pair K := generalized_continued_fraction.next_continuants 1 fr⁻¹ pconts conts in exact_conts.a / exact_conts.b)

source

@[protected]

theorem generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_some_aux_comp {K : Type u_1} [linear_ordered_field K] [floor_ring K] {a : K} (b c : K) (fract_a_ne_zero : int.fract a ≠ 0) :

(↑⌊a⌋ * b + c) / int.fract a + b = (b * a + c) / int.fract a

Just a computational lemma we need for the next main proof.

source

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

generalized_continued_fraction.int_fract_pair.stream v n = option.some ifp_n → v = generalized_continued_fraction.comp_exact_value ((generalized_continued_fraction.of v).continuants_aux n) ((generalized_continued_fraction.of v).continuants_aux (n + 1)) ifp_n.fr

Shows the correctness of comp_exact_value in case the continued fraction generalized_continued_fraction.of v did not terminate at position n. That is, we obtain the value v if we pass the two successive (auxiliary) continuants at positions n and n + 1 as well as the fractional part at int_fract_pair.stream n to comp_exact_value.

The correctness might be seen more readily if one uses convergents' to evaluate the continued fraction. Here is an example to illustrate the idea:

Let (v : ℚ) := 3.4. We have

generalized_continued_fraction.int_fract_pair.stream v 0 = some ⟨3, 0.4⟩, and
generalized_continued_fraction.int_fract_pair.stream v 1 = some ⟨2, 0.5⟩. Now (generalized_continued_fraction.of v).convergents' 1 = 3 + 1/2, and our fractional term at position 2 is 0.5. We hence have v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4. This computation corresponds exactly to the one using the recurrence equation in comp_exact_value.

source

theorem generalized_continued_fraction.of_correctness_of_nth_stream_eq_none {K : Type u_1} [linear_ordered_field K] {v : K} {n : ℕ} [floor_ring K] (nth_stream_eq_none : generalized_continued_fraction.int_fract_pair.stream v n = option.none) :

v = (generalized_continued_fraction.of v).convergents (n - 1)

The convergent of generalized_continued_fraction.of v at step n - 1 is exactly v if the int_fract_pair.stream of the corresponding continued fraction terminated at step n.

source

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

v = (generalized_continued_fraction.of v).convergents n

If generalized_continued_fraction.of v terminated at step n, then the nth convergent is exactly v.

source

theorem generalized_continued_fraction.of_correctness_of_terminates {K : Type u_1} [linear_ordered_field K] {v : K} [floor_ring K] (terminates : (generalized_continued_fraction.of v).terminates) :

∃ (n : ℕ), v = (generalized_continued_fraction.of v).convergents n

If generalized_continued_fraction.of v terminates, then there is n : ℕ such that the nth convergent is exactly v.

source

theorem generalized_continued_fraction.of_correctness_at_top_of_terminates {K : Type u_1} [linear_ordered_field K] {v : K} [floor_ring K] (terminates : (generalized_continued_fraction.of v).terminates) :

∀ᶠ (n : ℕ) in filter.at_top, v = (generalized_continued_fraction.of v).convergents n

If generalized_continued_fraction.of v terminates, then its convergents will eventually always be v.

Correctness of Terminating Continued Fraction Computations (generalized_continued_fraction.of) #

Summary #

Main definitions #

Main Theorems #

Correctness of Terminating Continued Fraction Computations (`generalized_continued_fraction.of`) #