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

Summary #

We show the correctness of the algorithm computing continued fractions (GeneralizedContinuedFraction.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 (GeneralizedContinuedFraction.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 v n.

For an example, refer to GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some and for more information about the computation process, refer to Algebra.ContinuedFractions.Computation.Basic.

Main definitions #

Main Theorems #

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 = nextContinuants 1 fr⁻¹ pconts conts otherwise.

This function can be used to compute the exact value approximated by a continued fraction GeneralizedContinuedFraction.of v as described in lemma compExactValue_correctness_of_stream_eq_some.

  • One or more equations did not get rendered due to their size.
Instances For
    theorem GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some_aux_comp {K : Type u_1} [LinearOrderedField K] [FloorRing K] {a : K} (b : K) (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.

    Shows the correctness of compExactValue in case the continued fraction GeneralizedContinuedFraction.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 n to compExactValue.

    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

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

    theorem GeneralizedContinuedFraction.of_correctness_of_terminatedAt {K : Type u_1} [LinearOrderedField K] {v : K} {n : } [FloorRing K] (terminated_at_n : (GeneralizedContinuedFraction.of v).TerminatedAt n) :

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

    theorem GeneralizedContinuedFraction.of_correctness_of_terminates {K : Type u_1} [LinearOrderedField K] {v : K} [FloorRing K] (terminates : (GeneralizedContinuedFraction.of v).Terminates) :
    ∃ (n : ), v = (GeneralizedContinuedFraction.of v).convergents n

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

    theorem GeneralizedContinuedFraction.of_correctness_atTop_of_terminates {K : Type u_1} [LinearOrderedField K] {v : K} [FloorRing K] (terminates : (GeneralizedContinuedFraction.of v).Terminates) :
    ∀ᶠ (n : ) in Filter.atTop, v = (GeneralizedContinuedFraction.of v).convergents n

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