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): ext lemmas for measures #3895

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(measure_theory): ext lemmas for measures #3895

wants to merge 5 commits into from

Conversation

fpvandoorn
Copy link
Member

@fpvandoorn fpvandoorn commented Aug 21, 2020 •
edited

Add class sigma_finite.
Also some cleanup.
Rename measurable_space.is_measurable -> measurable_space.is_measurable'. This is to avoid name clash with _root_.is_measurable, which should almost always be used instead.
define is_pi_system.

@fpvandoorn fpvandoorn added the awaiting-review The author would like community review of the PR label Aug 21, 2020
@fpvandoorn fpvandoorn requested a review from urkud August 21, 2020 03:29
@fpvandoorn fpvandoorn added WIP Work in progress and removed awaiting-review The author would like community review of the PR WIP Work in progress labels Aug 21, 2020
@robertylewis robertylewis added the awaiting-review The author would like community review of the PR label Aug 21, 2020
@urkud
Copy link
Member

urkud commented Aug 22, 2020

Could you please have a look at #3760, more precisely ext_of_generate_from_of_cover_same in measure_space? We need to merge my changes with yours somehow, and I'm already too sleepy to compare two versions.

@fpvandoorn fpvandoorn changed the title feat(measure_theory): ext lemmas for measures feat(measure_theory): ext lemmas for measures [waiting for 3760] Aug 22, 2020
@fpvandoorn fpvandoorn added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed awaiting-review The author would like community review of the PR labels Aug 22, 2020
@fpvandoorn fpvandoorn mentioned this pull request Aug 22, 2020
Closed
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 28, 2020
@fpvandoorn
feat(measure_theory): ext lemmas for measures
72a7347 
Add class `sigma_finite`.
Also some cleanup.
rename `measurable_space.is_measurable` -> `measurable_space.is_measurable'`.
This is to avoid name clash with `_root_.is_measurable`, which should almost always be preferred.
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 15, 2020
@fpvandoorn fpvandoorn removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 15, 2020
@fpvandoorn fpvandoorn changed the title feat(measure_theory): ext lemmas for measures [waiting for 3760] feat(measure_theory): ext lemmas for measures Sep 15, 2020
@fpvandoorn fpvandoorn added the WIP Work in progress label Sep 15, 2020
@fpvandoorn fpvandoorn added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Sep 18, 2020
@fpvandoorn
Copy link
Member Author

@urkud how do you feel about the renaming measurable_space.is_measurable -> measurable_space.is_measurable'. If you are going to rename is_measurable to measurable_set soon, what do we want to be the name of measurable_space.is_measurable after that change? I expect the least confusing thing is to name it something like measurable_space.measurable_set' (so that there is no name conflict, but the name is basically the same). If so, the fact that I already prime those occurrences should be also helpful for your renaming.

urkud
urkud reviewed Sep 21, 2020
View reviewed changes
src/measure_theory/measure_space.lean Outdated
/-- A set `s` is called σ-finite w.r.t. measure `μ` if there is a countable collection of sets
`{ A i | i ∈ ℕ }` such that `μ (A i) < ⊤` and `⋃ i, A i = s`.
A measure `μ` is called σ-finite if `univ` is σ-finite w.r.t. `μ`.
Note that this class is not a Proposition.
Copy link
Member

@urkud urkud Sep 21, 2020 •
edited

Choose a reason for hiding this comment

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

Why don't you want it to be a Prop? I'm afraid that this will create some problems with non-defeq instances later. Am I right that Prop-version is equivalent to ∃ t : ℕ → set α, (⋃ i, t i) = s ∧∀ i, μ (t i) < ⊤? BTW, what do you think about using sigma_finite (μ.restrict s) for s ≠ univ?

Otherwise LGTM. Could you please delete sigma_finite from this PR (nothing else depends on it), merge the rest into master, and open a new PR with sigma_finite?

bors d+

Copy link
Member Author

Choose a reason for hiding this comment

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

Those are great points! I will delete sigma_finite for now, and will make a new PR with the sigma_finite stuff.

@urkud
Copy link
Member

urkud commented Sep 21, 2020

Let me try again

bors d+

@bors
Copy link

bors bot commented Sep 21, 2020

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

@urkud urkud added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Sep 22, 2020
@fpvandoorn
Copy link
Member Author

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Sep 23, 2020
bors bot pushed a commit that referenced this pull request Sep 23, 2020
@fpvandoorn
feat(measure_theory): ext lemmas for measures (#3895)
72e5b9f 
Add class `sigma_finite`.
Also some cleanup.
Rename `measurable_space.is_measurable` -> `measurable_space.is_measurable'`. This is to avoid name clash with `_root_.is_measurable`, which should almost always be used instead.
define `is_pi_system`.
@bors
Copy link

bors bot commented Sep 23, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory): ext lemmas for measures [Merged by Bors] - feat(measure_theory): ext lemmas for measures Sep 23, 2020
@bors bors bot closed this Sep 23, 2020
@bors bors bot deleted the pi-lambda branch September 23, 2020 20:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud 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+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@fpvandoorn @urkud @robertylewis