Correctness of Terminating 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 #
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_valuecan be used to compute the exact value approximated by the continued fractiongeneralized_continued_fraction.of vby adding a residual term as described in the summary.
Main Theorems #
generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_someshows thatgeneralized_continued_fraction.comp_exact_valueindeed returns the valuevwhen given the convergent and fractional part as described in the summary.generalized_continued_fraction.of_correctness_of_terminated_atshows the equalityv = (generalized_continued_fraction.of v).convergents nifgeneralized_continued_fraction.of vterminated at positionn.
Given two continuants pconts and conts and a value fr, this function returns
conts.a / conts.biffr = 0exact_conts.a / exact_conts.bwhereexact_conts = next_continuants 1 fr⁻¹ pconts contsotherwise.
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)
Just a computational lemma we need for the next main proof.
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⟩, andgeneralized_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 position2is0.5. We hence havev = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4. This computation corresponds exactly to the one using the recurrence equation incomp_exact_value.
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.
If generalized_continued_fraction.of v terminated at step n, then the nth convergent is
exactly v.
If generalized_continued_fraction.of v terminates, then there is n : ℕ such that the nth
convergent is exactly v.
If generalized_continued_fraction.of v terminates, then its convergents will eventually always
be v.