Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes