Commit 2020-04-25 18:43 632c4baa
View on Github →feat(continued_fractions) add equivalence of convergents computations (#2459)
What
Add lemmas showing that the two methods for computing the convergents of a continued fraction (recurrence relation vs direct evaluation) coincide. A high-level overview on how the proof works is given in the header of the file.
Why
One wants to be able to relate both computations. The recurrence relation can be faster to compute, the direct evaluation is more intuitive and might be easier for some proofs.
How
The proof of the equivalence is by induction. To make the induction work, one needs to "squash" a sequence into a shorter one while maintaining the value of the convergents computations. Most lemmas in this commit deal with this squashing operation.