-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(continued_fractions) add equivalence of convergents computations #2459
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just some typos and style nitpicks.
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Thanks! Sorry for the typos D: I should get a spellchecker. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The Lean looks great (as you can see, I only have minor formatting comments).
What would be extremely helpful, I think, would be to have a sketch of the proof at the beginning of the file, in informal math talk and without details or computations (but pointers to the relevant lemmas in the file), and maybe also recall what the two definitions of convergents
and convergents'
are, to help the reader understand where the file is going.
From a math point of view, I would probably have done things using a formalism based on matrix products and homographies instead of the more elementary point of view that you develop, but in the end it is also nice like this.
Also, you should change the header text of the PR to reflect the changes you have made (for instance, you have removed |
Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Also fixed this. Thanks for the kind and detailled review :) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Otherwise LGTM!
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bors r+ |
…#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. Co-authored-by: Kevin Kappelmann <kappelmann@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…leanprover-community#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. Co-authored-by: Kevin Kappelmann <kappelmann@users.noreply.github.com>
…leanprover-community#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. Co-authored-by: Kevin Kappelmann <kappelmann@users.noreply.github.com>
…leanprover-community#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. Co-authored-by: Kevin Kappelmann <kappelmann@users.noreply.github.com>
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.
TO CONTRIBUTORS:
Please include a summary of the changes made in this PR above "TO CONTRIBUTORS:", as that text will become the commit message. You are also encouraged to append the following co-authorship template if you'd like to acknowledge suggestions / commits made by other users:
Co-authored-by: name name@example.com
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list
If you're confused by comments on your PR like
bors r+
orbors d+
, please see our notes on bors for information on our merging workflow.