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): various additions #5389

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(measure_theory): various additions #5389

wants to merge 8 commits into from

Conversation

fpvandoorn
Copy link
Member

@fpvandoorn fpvandoorn commented Dec 16, 2020 •
edited

Some computations of measures on non-measurable sets
Some more measurability lemmas for pi-types
Cleanup in measure_space

@fpvandoorn
feat(measure_theory): various additions
358e301 
Some computations of measures on non-measurable sets
Some more measurability lemmas for pi-types
@fpvandoorn
fix
4d4f3c2
@fpvandoorn fpvandoorn added the awaiting-review The author would like community review of the PR label Dec 16, 2020
@fpvandoorn fpvandoorn removed the request for review from urkud December 17, 2020 04:48
@fpvandoorn fpvandoorn added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Dec 17, 2020
@fpvandoorn
Copy link
Member Author

I think I'm still going to make some changes here.

@fpvandoorn fpvandoorn added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 18, 2020
@fpvandoorn
Copy link
Member Author

For the review of measure_space.lean it might be useful to split it up in

@fpvandoorn fpvandoorn mentioned this pull request Dec 18, 2020
Closed
2 tasks
sgouezel
sgouezel reviewed Dec 20, 2020
View reviewed changes
src/measure_theory/measurable_space.lean Outdated
Comment on lines 127 to 128
have := encodable.trunc_encodable_of_fintype β,
induction this using trunc.rec_on_subsingleton,
Copy link
Collaborator

Choose a reason for hiding this comment

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

This looks like a nasty trick, although this is exactly how it is supposed to be used if I understand correctly. Is it possible to have in the encodable file a nonconstructive def giving encodable out of [fintype], and use it here with a local attribute [instance] (so that the proof would just be is_measurable.Union h). Like

noncomputable def fintype.encodable [fintype β] : encodable β :=
(encodable.trunc_encodable_of_fintype β).out

and

local attribute [instance] fintype.encodable

lemma is_measurable.Union_fintype [fintype β] {f : β → set α} (h : ∀ b, is_measurable (f b)) :
  is_measurable (⋃ b, f b) :=
is_measurable.Union h

(Then the proof below simplifies similarly).

Copy link
Member Author

Choose a reason for hiding this comment

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

What you suggest is more user-friendly indeed.

sgouezel
sgouezel reviewed Dec 20, 2020
View reviewed changes
src/measure_theory/prod.lean Outdated
by_cases hti : ν t = ⊤,
{ convert le_top, simp_rw [hti, ennreal.mul_top, hs0, if_false] },
rw [measure_eq_infi' μ],
simp_rw [ennreal.infi_mul hti], refine le_infi _, rintro ⟨s', h1s', h2s'⟩,
Copy link
Collaborator

Choose a reason for hiding this comment

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

I thought that in general we had only one command per line, unless this is a trivial one-liner closing a goal. Same thing below line 356.

Copy link
Member Author

Choose a reason for hiding this comment

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

I am not aware of this style convention (I don't think it is in the style guide), but I'm happy to add some newlines.

@PatrickMassot PatrickMassot 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 Dec 21, 2020
@fpvandoorn fpvandoorn 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 Dec 28, 2020
@sgouezel
Copy link
Collaborator

bors r+
Thanks!

@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 Dec 30, 2020
@sgouezel sgouezel mentioned this pull request Dec 30, 2020
Closed
bors bot pushed a commit that referenced this pull request Dec 30, 2020
@fpvandoorn
feat(measure_theory): various additions (#5389)
9988193 
Some computations of measures on non-measurable sets
Some more measurability lemmas for pi-types
Cleanup in `measure_space`
@bors
Copy link

bors bot commented Dec 30, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory): various additions [Merged by Bors] - feat(measure_theory): various additions Dec 30, 2020
@bors bors bot closed this Dec 30, 2020
@bors bors bot deleted the measure_stuff branch December 30, 2020 23:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
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
3 participants
@fpvandoorn @sgouezel @PatrickMassot