Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(measure_theory/measure/content): regular contents #16289

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(measure_theory/measure/content): regular contents #16289

wants to merge 6 commits into from

Conversation

ReimannJ
Copy link
Collaborator

@ReimannJ ReimannJ commented Aug 29, 2022 •
edited
Loading

Define regular contents and prove that regular contents agree with their induced measures on compact sets.

Open in Gitpod

@ReimannJ ReimannJ added the awaiting-review The author would like community review of the PR label Aug 29, 2022
mcdoll
mcdoll reviewed Aug 29, 2022
View reviewed changes
Copy link
Member

@mcdoll mcdoll left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please format your PR title according to the commit conventions. Note that you need a newline before the three dashes in the PR message.

src/measure_theory/measure/content.lean Outdated Show resolved Hide resolved
src/measure_theory/measure/content.lean Outdated Show resolved Hide resolved
ReimannJ and others added 2 commits August 29, 2022 17:13
@ReimannJ @mcdoll
Update src/measure_theory/measure/content.lean
469cf03 
Co-authored-by: mcdoll <moritz.doll@googlemail.com>
@ReimannJ @mcdoll
Update src/measure_theory/measure/content.lean
ea92552 
Co-authored-by: mcdoll <moritz.doll@googlemail.com>
@ReimannJ ReimannJ changed the title initial commit feat(measure_theory/measure/content): regular contents Aug 29, 2022
fpvandoorn
fpvandoorn reviewed Sep 14, 2022
View reviewed changes
Copy link
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

The mathematical content looks good, but I have some style comments.

src/measure_theory/measure/content.lean Show resolved Hide resolved
src/measure_theory/measure/content.lean Show resolved Hide resolved
src/measure_theory/measure/content.lean Show resolved Hide resolved
src/measure_theory/measure/content.lean Show resolved Hide resolved
@fpvandoorn fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes t-analysis Analysis (normed *, calculus) and removed awaiting-review The author would like community review of the PR labels Sep 14, 2022
@ReimannJ ReimannJ added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 8, 2022
@ADedecker ADedecker requested a review from a team October 22, 2022 14:45
@fpvandoorn
Copy link
Member

Oops, I forgot about this until the ping.

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 24, 2022
bors bot pushed a commit that referenced this pull request Oct 24, 2022
@ReimannJ
feat(measure_theory/measure/content): regular contents (#16289)
9ca9708 
Define regular contents and prove that regular contents agree with their induced measures on compact sets. 



Co-authored-by: ReimannJ <105789986+ReimannJ@users.noreply.github.com>
@bors
Copy link

bors bot commented Oct 24, 2022

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Oct 24, 2022
@ReimannJ
feat(measure_theory/measure/content): regular contents (#16289)
5b54590 
Define regular contents and prove that regular contents agree with their induced measures on compact sets. 



Co-authored-by: ReimannJ <105789986+ReimannJ@users.noreply.github.com>
@bors
Copy link

bors bot commented Oct 24, 2022

Build failed (retrying...):

@ocfnash
Copy link
Collaborator

ocfnash commented Oct 24, 2022

It looks like this PR caused a failure on bors.

Please merge master and merge once it passes CI.

bors r-

bors d+

@bors
Copy link

bors bot commented Oct 24, 2022

✌️ ReimannJ can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@bors
Copy link

bors bot commented Oct 24, 2022

Canceled.

@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Oct 24, 2022
@fpvandoorn
Copy link
Member

I merged master for you

@fpvandoorn fpvandoorn added the awaiting-CI The author would like to see what CI has to say before doing more work. label Oct 25, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Oct 25, 2022
@ReimannJ
Copy link
Collaborator Author

I merged master for you

@fpvandoorn Thank you! I'm curious, why did both K.compact and K.is_compact cause issues? I don't really understand what happened there.

@fpvandoorn
Copy link
Member

fpvandoorn commented Oct 25, 2022 •
edited
Loading

I made a recent change (in #16949) that renamed the projections.
When bors tries to compile the files, it will do so at the latest commit of mathlib (where the projection is called is_compact).
This PR is still on an old version of mathlib (where the projection was called compact), so we had to merge this branch with the master branch (using git merge origin/master) so that it is also on the newest version of mathlib.

In any case. It now compiles, so let's put it on the queue again.

bors merge

bors bot pushed a commit that referenced this pull request Oct 25, 2022
@ReimannJ @fpvandoorn
feat(measure_theory/measure/content): regular contents (#16289)
90cde5e 
Define regular contents and prove that regular contents agree with their induced measures on compact sets. 



Co-authored-by: ReimannJ <105789986+ReimannJ@users.noreply.github.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link

bors bot commented Oct 25, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/measure/content): regular contents [Merged by Bors] - feat(measure_theory/measure/content): regular contents Oct 25, 2022
@bors bors bot closed this Oct 25, 2022
@bors bors bot deleted the regular_contents branch October 25, 2022 14:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fpvandoorn fpvandoorn fpvandoorn left review comments

@mcdoll mcdoll mcdoll left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@ReimannJ @fpvandoorn @ocfnash @mcdoll