proposition: Lemma sum_enum_prob : \sum_(n <oo) (enum_prob X) n = 1.
proof: Proof. have := distribution_dRV measurableT. rewrite probability_setT/= => /esym; apply: eq_trans. by rewrite [RHS]eseries_mkcond; apply: eq_eseriesr => k _; rewrite diracT mule1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) HB(structures) exp numfun lebesgue_measure lebesgue_integral reals ereal signed topology normedtype sequences esum measure exp numfun lebesgue_measure lebesgue_integral