feat(probability/probability_mass_function): construct a pmf from a…

… probability measure (#18270)

Given a measurable space `α` with a `measurable_singleton_class` instance, this PR defines a function `measure.to_pmf` that converts a probability measure `μ` to a `pmf`, by defining the mass of a point `x`
to be the measure of the singleton set `{x}` under `μ`.

src/measure_theory/measure/measure_space.lean

@@ -1852,6 +1852,16 @@ end
   sum (λ a, μ {a} • dirac a) = μ :=
 by simpa using (map_eq_sum μ id measurable_id).symm
 
+/-- Given that `α` is a countable, measurable space with all singleton sets measurable,
+write the measure of a set `s` as the sum of the measure of `{x}` for all `x ∈ s`. -/
+lemma tsum_indicator_apply_singleton [countable α] [measurable_singleton_class α]
+  (μ : measure α) (s : set α) (hs : measurable_set s) :
+  ∑' (x : α), s.indicator (λ x, μ {x}) x = μ s :=
+calc ∑' (x : α), s.indicator (λ x, μ {x}) x = measure.sum (λ a, μ {a} • measure.dirac a) s :
+    by simp only [measure.sum_apply _ hs, measure.smul_apply, smul_eq_mul, measure.dirac_apply,
+      set.indicator_apply, mul_ite, pi.one_apply, mul_one, mul_zero]
+  ... = μ s : by rw μ.sum_smul_dirac
+
 omit m0
 end sum
 

src/probability/probability_mass_function/basic.lean

@@ -20,14 +20,17 @@ by assigning each set the sum of the probabilities of each of its elements.
 Under this outer measure, every set is Carathéodory-measurable,
 so we can further extend this to a `measure` on `α`, see `pmf.to_measure`.
 `pmf.to_measure.is_probability_measure` shows this associated measure is a probability measure.
+Conversely, given a probability measure `μ` on a measurable space `α` with all singleton sets
+measurable, `μ.to_pmf` constructs a `pmf` on `α`, setting the probability mass of a point `x`
+to be the measure of the singleton set `{x}`.
 
 ## Tags
 
 probability mass function, discrete probability measure
 -/
 noncomputable theory
 variables {α β γ : Type*}
-open_locale classical big_operators nnreal ennreal
+open_locale classical big_operators nnreal ennreal measure_theory
 
 /-- A probability mass function, or discrete probability measures is a function `α → ℝ≥0∞` such
   that the values have (infinite) sum `1`. -/
@@ -103,6 +106,13 @@ variables (p : pmf α) (s t : set α)
 lemma to_outer_measure_apply : p.to_outer_measure s = ∑' x, s.indicator p x :=
 tsum_congr (λ x, smul_dirac_apply (p x) x s)
 
+@[simp] lemma to_outer_measure_caratheodory : p.to_outer_measure.caratheodory = ⊤ :=
+begin
+  refine (eq_top_iff.2 $ le_trans (le_Inf $ λ x hx, _) (le_sum_caratheodory _)),
+  exact let ⟨y, hy⟩ := hx in ((le_of_eq (dirac_caratheodory y).symm).trans
+    (le_smul_caratheodory _ _)).trans (le_of_eq hy),
+end
+
 @[simp]
 lemma to_outer_measure_apply_finset (s : finset α) : p.to_outer_measure s = ∑ x in s, p x :=
 begin
@@ -118,6 +128,13 @@ begin
   { exact ite_eq_left_iff.2 (λ ha', false.elim $ ha' rfl) }
 end
 
+lemma to_outer_measure_injective : (to_outer_measure : pmf α → outer_measure α).injective :=
+λ p q h, pmf.ext (λ x, (p.to_outer_measure_apply_singleton x).symm.trans
+  ((congr_fun (congr_arg _ h) _).trans $ q.to_outer_measure_apply_singleton x))
+
+@[simp] lemma to_outer_measure_inj {p q : pmf α} :
+  p.to_outer_measure = q.to_outer_measure ↔ p = q := to_outer_measure_injective.eq_iff
+
 lemma to_outer_measure_apply_eq_zero_iff : p.to_outer_measure s = 0 ↔ disjoint p.support s :=
 begin
   rw [to_outer_measure_apply, ennreal.tsum_eq_zero],
@@ -138,8 +155,7 @@ begin
     exact λ a ha, (p.apply_eq_zero_iff a).2 $ set.not_mem_subset h ha }
 end
 
-@[simp]
-lemma to_outer_measure_apply_inter_support :
+@[simp] lemma to_outer_measure_apply_inter_support :
   p.to_outer_measure (s ∩ p.support) = p.to_outer_measure s :=
 by simp only [to_outer_measure_apply, pmf.support, set.indicator_inter_support]
 
@@ -157,15 +173,6 @@ le_antisymm (p.to_outer_measure_mono (h.symm ▸ (set.inter_subset_left t p.supp
 lemma to_outer_measure_apply_fintype [fintype α] : p.to_outer_measure s = ∑ x, s.indicator p x :=
 (p.to_outer_measure_apply s).trans (tsum_eq_sum (λ x h, absurd (finset.mem_univ x) h))
 
-@[simp]
-lemma to_outer_measure_caratheodory (p : pmf α) : (to_outer_measure p).caratheodory = ⊤ :=
-begin
-  refine (eq_top_iff.2 $ le_trans (le_Inf $ λ x hx, _) (le_sum_caratheodory _)),
-  obtain ⟨y, hy⟩ := hx,
-  exact ((le_of_eq (dirac_caratheodory y).symm).trans
-    (le_smul_caratheodory _ _)).trans (le_of_eq hy),
-end
-
 end outer_measure
 
 section measure
@@ -191,8 +198,7 @@ lemma to_measure_apply (hs : measurable_set s) : p.to_measure s = ∑' x, s.indi
 
 lemma to_measure_apply_singleton (a : α) (h : measurable_set ({a} : set α)) :
   p.to_measure {a} = p a :=
-by simp [to_measure_apply_eq_to_outer_measure_apply p {a} h,
-  to_outer_measure_apply_singleton]
+by simp [to_measure_apply_eq_to_outer_measure_apply _ _ h, to_outer_measure_apply_singleton]
 
 lemma to_measure_apply_eq_zero_iff (hs : measurable_set s) :
   p.to_measure s = 0 ↔ disjoint p.support s :=
@@ -223,6 +229,14 @@ section measurable_singleton_class
 
 variables [measurable_singleton_class α]
 
+lemma to_measure_injective : (to_measure : pmf α → measure α).injective :=
+λ p q h, pmf.ext (λ x, (p.to_measure_apply_singleton x $ measurable_set_singleton x).symm.trans
+  ((congr_fun (congr_arg _ h) _).trans $ q.to_measure_apply_singleton x $
+    measurable_set_singleton x))
+
+@[simp] lemma to_measure_inj {p q : pmf α} : p.to_measure = q.to_measure ↔ p = q :=
+to_measure_injective.eq_iff
+
 @[simp]
 lemma to_measure_apply_finset (s : finset α) : p.to_measure s = ∑ x in s, p x :=
 (p.to_measure_apply_eq_to_outer_measure_apply s s.measurable_set).trans
@@ -239,11 +253,61 @@ lemma to_measure_apply_fintype [fintype α] : p.to_measure s = ∑ x, s.indicato
 
 end measurable_singleton_class
 
+end measure
+
+end pmf
+
+namespace measure_theory
+
+open pmf
+
+namespace measure
+
+/-- Given that `α` is a countable, measurable space with all singleton sets measurable,
+we can convert any probability measure into a `pmf`, where the mass of a point
+is the measure of the singleton set under the original measure. -/
+def to_pmf [countable α] [measurable_space α] [measurable_singleton_class α]
+  (μ : measure α) [h : is_probability_measure μ] : pmf α :=
+⟨λ x, μ ({x} : set α), ennreal.summable.has_sum_iff.2 (trans (symm $
+(tsum_indicator_apply_singleton μ set.univ measurable_set.univ).symm.trans
+  (tsum_congr (λ x, congr_fun (set.indicator_univ _) x))) (h.measure_univ))⟩
+
+variables [countable α] [measurable_space α] [measurable_singleton_class α]
+  (μ : measure α) [is_probability_measure μ]
+
+lemma to_pmf_apply (x : α) : μ.to_pmf x = μ {x} := rfl
+
+@[simp] lemma to_pmf_to_measure : μ.to_pmf.to_measure = μ :=
+measure.ext (λ s hs, by simpa only [μ.to_pmf.to_measure_apply s hs,
+  ← μ.tsum_indicator_apply_singleton s hs])
+
+end measure
+
+end measure_theory
+
+namespace pmf
+
+open measure_theory
+
 /-- The measure associated to a `pmf` by `to_measure` is a probability measure -/
-instance to_measure.is_probability_measure (p : pmf α) : is_probability_measure (p.to_measure) :=
+instance to_measure.is_probability_measure [measurable_space α] (p : pmf α) :
+  is_probability_measure (p.to_measure) :=
 ⟨by simpa only [measurable_set.univ, to_measure_apply_eq_to_outer_measure_apply,
   set.indicator_univ, to_outer_measure_apply, ennreal.coe_eq_one] using tsum_coe p⟩
 
-end measure
+variables [countable α] [measurable_space α] [measurable_singleton_class α]
+  (p : pmf α) (μ : measure α) [is_probability_measure μ]
+
+@[simp] lemma to_measure_to_pmf : p.to_measure.to_pmf = p :=
+pmf.ext (λ x, by rw [← p.to_measure_apply_singleton x (measurable_set_singleton x),
+  p.to_measure.to_pmf_apply])
+
+lemma to_measure_eq_iff_eq_to_pmf (μ : measure α) [is_probability_measure μ] :
+  p.to_measure = μ ↔ p = μ.to_pmf :=
+by rw [← to_measure_inj, measure.to_pmf_to_measure]
+
+lemma to_pmf_eq_iff_to_measure_eq (μ : measure α) [is_probability_measure μ] :
+  μ.to_pmf = p ↔ μ = p.to_measure :=
+by rw [← to_measure_inj, measure.to_pmf_to_measure]
 
 end pmf

src/probability/probability_mass_function/monad.lean

@@ -21,6 +21,7 @@ so that the second argument only needs to be defined on the support of the first
 noncomputable theory
 variables {α β γ : Type*}
 open_locale classical big_operators nnreal ennreal
+open measure_theory
 
 namespace pmf
 
@@ -54,11 +55,20 @@ begin
     exact ite_eq_right_iff.2 (λ hb, ite_eq_right_iff.2 (λ h, (ha $ h ▸ hb).elim)) }
 end
 
+variable [measurable_space α]
+
 /-- The measure of a set under `pure a` is `1` for sets containing `a` and `0` otherwise -/
-@[simp] lemma to_measure_pure_apply [measurable_space α] (hs : measurable_set s) :
+@[simp] lemma to_measure_pure_apply (hs : measurable_set s) :
   (pure a).to_measure s = if a ∈ s then 1 else 0 :=
 (to_measure_apply_eq_to_outer_measure_apply (pure a) s hs).trans (to_outer_measure_pure_apply a s)
 
+lemma to_measure_pure : (pure a).to_measure = measure.dirac a :=
+measure.ext (λ s hs, by simpa only [to_measure_pure_apply a s hs, measure.dirac_apply' a hs])
+
+@[simp] lemma to_pmf_dirac [countable α] [h : measurable_singleton_class α] :
+  (measure.dirac a).to_pmf = pure a :=
+by rw [to_pmf_eq_iff_to_measure_eq, to_measure_pure]
+
 end measure
 
 end pure