-
Notifications
You must be signed in to change notification settings - Fork 273
Tiny improvements on the proof of the beta function lemma#159
Open
iblech wants to merge 2 commits intoOpenLogicProject:master from
Open
Tiny improvements on the proof of the beta function lemma #159iblech wants to merge 2 commits intoOpenLogicProject:master from
iblech wants to merge 2 commits intoOpenLogicProject:master from
Conversation
Member
rzach
commented
Nov 10, 2017
Thanks! I'm travelling right now and hope to review this in two weeks or so.
Contributor
Author
iblech
commented
Dec 2, 2018
Just for the record, no hurry, I'm still on a page with my past self on this pull request :-), that is, I'm still in favor of these changes and could give additional justifications, if needed.
Contributor
I think this should be ok to close, as these improvements are now included.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The first commit very slightly sharpens the construction by making
ja tiny bit smaller. (With the current definition ofj, even the numbersx_0, ..., x_{n+1}will be relatively prime; a fact we don't need.)The second commit adds an explicit witness to the relative primality of the
x_i, obtained from the argument given in the text by proof mining. Personally, I'm interested in such things, but if you feel that the new footnote is a distraction, then please feel free to not merge the second commit.I stumbled on the Open Logic Project only a couple of days ago. I'm amazed by its scope and quality. Thank you for your hard work in maintaining this project!