Theorems · Theorem · number theory

GenContFract.compExactValue_correctness_of_stream_eq_some

∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] {v : K} {n : ℕ} [inst_2 : FloorRing K]
  {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n →
    v = GenContFract.compExactValue ((GenContFract.of v).contsAux n) ((GenContFract.of v).contsAux (n + 1)) ifp_n.fr

Shows the correctness of compExactValue in case the continued fraction GenContFract.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 IntFractPair.stream n to compExactValue. The correctness might be seen more readily if one uses convs' to evaluate the continued fraction. Here is an example to illustrate the idea: Let (v : ℚ) := 3.4. We have - GenContFract.IntFractPair.stream v 0 = some ⟨3, 0.4⟩, and - GenContFract.IntFractPair.stream v 1 = some ⟨2, 0.5⟩. Now (GenContFract.of v).convs' 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 compExactValue.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Cited by

2 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderFloorRing