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/probability_mass_function): Add definitions for filtering pmfs on a predicate #6033

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(measure_theory/probability_mass_function): Add definitions for filtering pmfs on a predicate #6033

wants to merge 8 commits into from

Conversation

dtumad
Copy link
Collaborator

@dtumad dtumad commented Feb 4, 2021

No description provided.

@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Feb 4, 2021
@dtumad
Copy link
Collaborator Author

dtumad commented Feb 4, 2021

I would like to be able to loosen the fintype restriction on these definitions, but I'm not sure how to best approaching that. Is there some way to normalize a sum over a non-fintype Type?

@sgouezel
Copy link
Collaborator

sgouezel commented Feb 4, 2021

Indeed you can remove completely the fintype assumption. Your lemma of_fintype' will not hold like that, you should additionally assume that f is summable. Once it is summable, you can follow your proofs. Instead of using the finite set sums as you do, you should replace them with infinite sums (notation ∑' in mathlib).

@sgouezel sgouezel 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 Feb 4, 2021
@dtumad dtumad 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 Feb 4, 2021
@dtumad
Copy link
Collaborator Author

dtumad commented Feb 4, 2021

I ended up using tsum f ≠ 0 as the hypothesis instead of summable f, since the sum needs to be non-zero anyways to do the normalizing, and summable f can be derived from tsum f ≠ 0. This only works since tsum is definitionally 0 for non-summable functions, which I assume is just a convention of the implementation of tsum, so I'm not sure whether it is a good idea or not, but it does simplify a lot of the assumptions and proofs.

sgouezel
sgouezel reviewed Feb 5, 2021
View reviewed changes
src/measure_theory/probability_mass_function.lean Outdated Show resolved Hide resolved
src/measure_theory/probability_mass_function.lean Outdated Show resolved Hide resolved
src/measure_theory/probability_mass_function.lean Outdated Show resolved Hide resolved
src/topology/instances/ennreal.lean Outdated Show resolved Hide resolved
src/algebra/big_operators/order.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel 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 Feb 5, 2021
@dtumad dtumad 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 Feb 5, 2021
sgouezel
sgouezel reviewed Feb 5, 2021
View reviewed changes
src/measure_theory/probability_mass_function.lean Outdated
def filter (p : pmf α) (s : set α) (h : ∃ a ∈ s, p a ≠ 0) : pmf α :=
pmf.normalize (s.indicator p) $ nnreal.tsum_indicator_ne_zero p.2.summable h

lemma filter_apply (p : pmf α) {s : set α} {h : ∃ a ∈ s, p a ≠ 0} {a : α} :
Copy link
Collaborator

Choose a reason for hiding this comment

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

The h and a parameters should be explicit here, as they can not be inferred from anything. If you want to rewrite, this is not a problem (rw filter_apply will work just fine), but if you want to do something else being able to specify the parameters may help. Same thing in all the other lemmas: a parameter should be implicit only when it can be inferred from subsequent parameters.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I had assumed it was also fine if the parameter could be inferred from the return type, but I see how that could cause issues if multiple patterns in the target match the return type. I've changed these all to be explicit now.

@sgouezel sgouezel 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 Feb 5, 2021
@dtumad dtumad 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 Feb 5, 2021
sgouezel
sgouezel reviewed Feb 7, 2021
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

Almost there! I have left a final minor comment. Once you're done with it, you can merge yourself.
bors d+

src/measure_theory/probability_mass_function.lean Outdated
end

lemma filter_apply_ne_zero_iff (p : pmf α) {s : set α} (h : ∃ a ∈ s, p a ≠ 0) (a : α) :
(p.filter s h) a ≠ 0 ↔ a ∈ p.support ∧ a ∈ s :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

can you write the right hand side as being a member of the intersection? Also, this lemma and the previous one would be good simp lemmas.

@bors
Copy link

bors bot commented Feb 7, 2021

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

@sgouezel sgouezel 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 Feb 8, 2021
@sgouezel sgouezel added the delegated The PR author may merge after reviewing final suggestions. label Feb 8, 2021
@dtumad
Copy link
Collaborator Author

dtumad commented Feb 8, 2021

bors r+

bors bot pushed a commit that referenced this pull request Feb 8, 2021
@dtumad
feat(measure_theory/probability_mass_function): Add definitions for f…
4e9fbb9 
…iltering pmfs on a predicate (#6033)
@bors
Copy link

bors bot commented Feb 8, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/probability_mass_function): Add definitions for filtering pmfs on a predicate [Merged by Bors] - feat(measure_theory/probability_mass_function): Add definitions for filtering pmfs on a predicate Feb 8, 2021
@bors bors bot closed this Feb 8, 2021
@bors bors bot deleted the pmf_filter branch February 8, 2021 21:41
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
@dtumad @b-mehta
feat(measure_theory/probability_mass_function): Add definitions for f…
0e0be96 
…iltering pmfs on a predicate (#6033)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bryangingechen bryangingechen bryangingechen left review comments

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@dtumad @sgouezel @bryangingechen