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/regular): more material on regular measures #7680

Closed
wants to merge 46 commits into from
Closed

[Merged by Bors] - feat(measure_theory/regular): more material on regular measures #7680

wants to merge 46 commits into from

Conversation

sgouezel
Copy link
Collaborator

This PR:

  • defines weakly regular measures
  • shows that for weakly regular measures any finite measure set can be approximated from inside by closed sets
  • shows that for regular measures any finite measure set can be approximated from inside by compact sets
  • shows that any finite measure on a metric space is weakly regular
  • shows that any locally finite measure on a sigma compact locally compact metric space is regular

sgouezel and others added 30 commits May 12, 2021 16:58
@sgouezel
staging
2ff5d28
@sgouezel
Merge remote-tracking branch 'upstream/master' into regular
5151085
@sgouezel
refactor content
15a2f6f
@sgouezel
refactor content and regular
1e86350
@sgouezel
lint
83d9f0d
@sgouezel
start on regularity of measures in metric spaces
77ae65e
@sgouezel
change name to haar_content, use sup
025ed62
@sgouezel
Merge branch 'regular' into regular2
53d0315
@sgouezel
further progress
fcf6cb5
@sgouezel
progress
492820e
@sgouezel
staging
a1ce339
@sgouezel
finish proof
ddaf0df
@sgouezel
staging
32e2985
@sgouezel
staging
02fee8d
@sgouezel
dot notation for is_open.inter and friends
69a1713
@sgouezel
fix 1
eebb023
@sgouezel
merge master
d4354c2
@sgouezel
long line
10450b6
@sgouezel
fix 2
d5ad92c
@sgouezel
Merge branch 'is_open_dot' into regular2
01a7f40
@sgouezel
fix 3
a77d260
@sgouezel
Merge branch 'is_open_dot' into regular2
7c0930c
@sgouezel
staging
f732bc0
@sgouezel
further changes
51c2cab
@sgouezel
staging
4a4fd32
@sgouezel
also for clopen
6164f7f
@sgouezel
some more
e81e0f8
@sgouezel
oops
000df13
@sgouezel @eric-wieser
Apply suggestions from code review
7c278c9 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@sgouezel
staging
2216147
@sgouezel sgouezel added the awaiting-review The author would like community review of the PR label May 20, 2021
@fpvandoorn fpvandoorn self-assigned this May 24, 2021
fpvandoorn
fpvandoorn reviewed May 25, 2021
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.

The regular and weakly_regular namespaces are not very important anymore since those are now classes. Maybe you can rename the most useful results to enable projection notation?

The results and documentation look very good!

src/measure_theory/regular.lean Show resolved Hide resolved
src/measure_theory/regular.lean Show resolved Hide resolved
@fpvandoorn fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 25, 2021
@sgouezel
Copy link
Collaborator Author

I have changed the names of a few statements to make them compatible with dot notation, and updated the documentation accordingly.

@sgouezel sgouezel 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 May 26, 2021
@fpvandoorn
Copy link
Member

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 May 26, 2021
bors bot pushed a commit that referenced this pull request May 26, 2021
@sgouezel
feat(measure_theory/regular): more material on regular measures (#7680)
0970fda 
This PR:
* defines weakly regular measures
* shows that for weakly regular measures any finite measure set can be approximated from inside by closed sets
* shows that for regular measures any finite measure set can be approximated from inside by compact sets
* shows that any finite measure on a metric space is weakly regular
* shows that any locally finite measure on a sigma compact locally compact metric space is regular
@bors
Copy link

bors bot commented May 27, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/regular): more material on regular measures [Merged by Bors] - feat(measure_theory/regular): more material on regular measures May 27, 2021
@bors bors bot closed this May 27, 2021
@bors bors bot deleted the regular2 branch May 27, 2021 00:46
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

Assignees

@fpvandoorn fpvandoorn

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@sgouezel @fpvandoorn