Add lemma pmf_measurable

CHANGELOG_UNRELEASED.md

@@ -5,6 +5,8 @@
 ### Added
 - in order_topology.v
   + lemma `itv_closed_ends_closed`
+- in classical_sets.v
+  + lemma `in_set1_eq`
 
 - in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
@@ -15,6 +17,9 @@
 
 - in `Rstruct_topology.v`:
   + lemma `RlnE`
+- in probability.v
+  + lemma `pmf_ge0`
+  + lemmas `pmf_gt0_countable`, `pmf_measurable`
 
 ### Changed
 - in set_interval.v

classical/classical_sets.v

@@ -422,6 +422,11 @@ Lemma nat_nonempty : [set: nat] !=set0. Proof. by exists 1%N. Qed.
 
 #[global] Hint Resolve nat_nonempty : core.
 
+Lemma in_set1_eq {T : eqType} (a : T) (x : T) : x \in [set a] = (x == a).
+Proof.
+by apply/(sameP _ idP)/(equivP idP); rewrite inE eq_opE.
+Qed.
+
 Lemma itv_sub_in2 d (T : porderType d) (P : T -> T -> Prop) (i j : interval T) :
   [set` j] `<=` [set` i] ->
   {in i &, forall x y, P x y} -> {in j &, forall x y, P x y}.

theories/probability.v

@@ -1072,6 +1072,71 @@ Qed.
 
 End distribution_dRV.
 
+Section pmf_definition.
+Context {d} {T : measurableType d} {R : realType}.
+Variables (P : probability T R).
+
+Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])).
+
+Lemma pmf_ge0 (X : {RV P >-> R}) (r : R) : 0 <= pmf X r.
+Proof. by rewrite fine_ge0. Qed.
+
+End pmf_definition.
+
+Section pmf_measurable.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType)
+  (P : probability T R) (X : {RV P >-> R}).
+
+Lemma pmf_gt0_countable : countable [set r | 0 < pmf X r]%R.
+Proof.
+rewrite [X in countable X](_ : _ =
+    \bigcup_n [set r | n.+1%:R^-1 < pmf X r]%R); last first.
+  by apply/seteqP; split=> [r/= /ltr_add_invr[k /[!add0r] kXr]|r/= [k _]];
+    [exists k|exact: lt_trans].
+apply: bigcup_countable => // n _; apply: finite_set_countable.
+apply: contrapT => /infiniteP/pcard_leP/injfunPex[/= q q_fun q_inj].
+have /(probability_le1 P) : measurable (\bigcup_k X @^-1` [set q k]).
+  by apply: bigcup_measurable => k _; exact: measurable_funPTI.
+rewrite leNgt => /negP; apply.
+rewrite [ltRHS](_ : _ = \sum_(0 <= k <oo) P (X @^-1` [set q k])); last first.
+  rewrite measure_bigcup//; first by apply: eq_eseriesl =>// i; rewrite in_setT.
+  rewrite (trivIset_comp (fun r => X@^-1` [set r]))//.
+  exact: trivIset_preimage1.
+apply: (lt_le_trans _ (nneseries_lim_ge n.+1 _)) => //.
+rewrite -EFin_sum_fine//; last by move=> ? _; rewrite fin_num_measure.
+under eq_bigr do rewrite -/(pmf X (q _)).
+rewrite lte_fin (_ : 1%R = (\sum_(0 <= k < n.+1) n.+1%:R^-1:R)%R); last first.
+  by rewrite sumr_const_nat subn0 -[RHS]mulr_natr mulVf.
+by apply: ltr_sum => // k _; exact: q_fun.
+Qed.
+
+Lemma pmf_measurable : measurable_fun [set: R] (pmf X).
+Proof.
+have /countable_bijP[S] := pmf_gt0_countable.
+rewrite card_eq_sym => /pcard_eqP/bijPex[/= h h_bij].
+have pmf1_ge0 k s : 0 <= (pmf X (h k) * \1_[set h k] s)%:E.
+  by rewrite EFinM mule_ge0// lee_fin pmf_ge0.
+pose sfun r := \sum_(0 <= k <oo | k \in S) (pmf X (h k) * \1_[set h k] r)%:E.
+apply/measurable_EFinP; apply: (eq_measurable_fun sfun) => [r _|]; last first.
+  by apply: ge0_emeasurable_sum => // *; exact/measurable_EFinP/measurable_funM.
+have [rS|nrS] := boolP (r \in [set h k | k in S]).
+- pose kr := pinv S h r.
+  have neqh k : k \in S /\ k != kr -> r != h k.
+    move=> [Sk]; apply: contra_neq.
+    by rewrite /kr => ->; rewrite pinvKV//; exact: (set_bij_inj h_bij).
+  rewrite /sfun (@nneseriesD1 _ _ kr)//; last by rewrite inE; exact/invS/set_mem.
+  by rewrite eseries0 => [| k k_ge0 /andP/neqh]; rewrite indicE in_set1_eq;
+    [rewrite pinvK// eqxx mulr1 addr0|move/negPf => ->; rewrite mulr0].
+- rewrite /sfun eseries0 => [|k k_ge0 Sk]/=.
+    apply: le_anti; rewrite !lee_fin pmf_ge0/= leNgt; apply: contraNN nrS.
+    by rewrite (surj_image_eq _ (set_bij_surj h_bij)) ?inE//; exact:set_bij_sub.
+  rewrite indicE in_set1_eq (_ : (r == h k) = false) ?mulr0//.
+  by apply: contraNF nrS => /eqP ->; exact/image_f.
+Qed.
+
+End pmf_measurable.
+
 Section discrete_distribution.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType) (P : probability T R).
@@ -1122,11 +1187,10 @@ apply: eq_eseriesr => k _; case: ifPn => kX.
 by rewrite integral_set0 mule0 /enum_prob patchE (negbTE kX) mul0e.
 Qed.
 
-Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])).
-
 Lemma expectation_pmf (X : {dRV P >-> R}) :
-    P.-integrable [set: T] (EFin \o X) -> 'E_P[X] =
-  \sum_(n <oo | n \in dRV_dom X) (pmf X (dRV_enum X n))%:E * (dRV_enum X n)%:E.
+  P.-integrable [set: T] (EFin \o X) ->
+  'E_P[X] = \sum_(n <oo | n \in dRV_dom X)
+              (@pmf _ _ _ P X (dRV_enum X n))%:E * (dRV_enum X n)%:E.
 Proof.
 move=> iX; rewrite dRV_expectation// [in RHS]eseries_mkcond.
 apply: eq_eseriesr => k _.