proposition: 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.
proof: Proof. move=> iX; rewrite dRV_expectation// [in RHS]eseries_mkcond. apply: eq_eseriesr => k _. rewrite /enum_prob patchE; case: ifPn => kX; last by rewrite mul0e. by rewrite /pmf fineK// fin_num_measure. 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