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

Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
354e613
feat(measure_theory/probability_mass_function): Add definitions for f…
dtumad Feb 3, 2021
5f7d630
Add alternative definition of filter in terms of indicator function
dtumad Feb 4, 2021
a892c2e
Generalize filter over non finite types
dtumad Feb 4, 2021
4c9de4d
Fix linting error from simp tags
dtumad Feb 5, 2021
73c9212
Changes from PR review
dtumad Feb 5, 2021
c1cd2f8
Change some parameters back to explicit
dtumad Feb 5, 2021
cc339db
Make some parameters implicit again
dtumad Feb 5, 2021
85c2c98
State lemmas in terms of set intersections
dtumad Feb 8, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/measure_theory/probability_mass_function.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ lemma summable_coe (p : pmf α) : summable p := (p.has_sum_coe_one).summable
/-- The support of a `pmf` is the set where it is nonzero. -/
def support (p : pmf α) : set α := {a | p.1 a ≠ 0}

@[simp] lemma mem_support_iff {p : pmf α} {a : α} :
@[simp] lemma mem_support_iff (p : pmf α) (a : α) :
a ∈ p.support ↔ p a ≠ 0 := iff.rfl

/-- The pure `pmf` is the `pmf` where all the mass lies in one point.
Expand Down Expand Up @@ -157,22 +157,22 @@ def normalize (f : α → ℝ≥0) (hf0 : tsum f ≠ 0) : pmf α :=
(mul_inv_cancel hf0) ▸ has_sum.mul_right (∑' x, f x)⁻¹
(not_not.mp (mt tsum_eq_zero_of_not_summable hf0 : ¬¬summable f)).has_sum⟩

lemma normalize_apply (f : α → ℝ≥0) {hf0 : tsum f ≠ 0} {a : α} :
lemma normalize_apply (f : α → ℝ≥0) (hf0 : tsum f ≠ 0) (a : α) :
(normalize f hf0) a = f a * (∑' x, f x)⁻¹ := rfl

/-- Create new `pmf` by filtering on a set with non-zero measure and normalizing -/
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 : α} :
lemma filter_apply (p : pmf α) (s : set α) (h : ∃ a ∈ s, p a ≠ 0) {a : α} :
dtumad marked this conversation as resolved.
Show resolved Hide resolved
(p.filter s h) a = (s.indicator p a) * (∑' x, (s.indicator p) x)⁻¹ :=
by rw [filter, normalize_apply]

lemma filter_apply_eq_zero_of_not_mem (p : pmf α) {s : set α} {h : ∃ a ∈ s, p a ≠ 0}
lemma filter_apply_eq_zero_of_not_mem (p : pmf α) (s : set α) (h : ∃ a ∈ s, p a ≠ 0)
{a : α} (ha : a ∉ s) : (p.filter s h) a = 0 :=
by rw [filter_apply, set.indicator_apply_eq_zero.mpr (λ ha', absurd ha' ha), zero_mul]

lemma filter_apply_eq_zero_iff (p : pmf α) {s : set α} {h : ∃ a ∈ s, p a ≠ 0} {a : α} :
lemma filter_apply_eq_zero_iff (p : pmf α) (s : set α) (h : ∃ a ∈ s, p a ≠ 0) (a : α) :
(p.filter s h) a = 0 ↔ p a = 0 ∨ a ∉ s :=
begin
split; intro ha,
Expand All @@ -183,7 +183,7 @@ begin
{ rw [filter_apply, set.indicator_apply_eq_zero.2 (λ h, ha.by_cases id (absurd h)), zero_mul] }
end

lemma filter_apply_ne_zero_iff (p : pmf α) {s : set α} {h : ∃ a ∈ s, p a ≠ 0} {a : α} :
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.

by rw [← not_iff, filter_apply_eq_zero_iff, not_iff, not_or_distrib, not_not, mem_support_iff]

Expand Down