proposition: Lemma dRV_expectation (X : {dRV P >-> R}) : P.-integrable [set: T] (EFin \o X) -> 'E_P[X] = \sum_(n <oo) enum_prob X n * (dRV_enum X n)%:E.
proof: Proof. move=> ix; rewrite unlock. rewrite -[in LHS](_ : \bigcup_k (if k \in dRV_dom X then X @^-1` [set dRV_enum X k] else set0) = setT); last first. apply/seteqP; split => // t _. exists ((dRV_enum X)^-1%function (X t)) => //. case: ifPn=> [_|]. by rewrite invK// inE. by rewrite notin_set/=; apply; apply: funS. have tA : trivIset (dRV_dom X) (fun k => [set dRV_enum X k]). by move=> i j iX jX [r [/= ->{r}]] /inj; rewrite !inE; exact. have {tA}/trivIset_mkcond tXA : trivIset (dRV_dom X) (fun k => X @^-1` [set dRV_enum X k]). apply/trivIsetP => /= i j iX jX ij. move/trivIsetP : tA => /(_ i j iX jX) Aij. by rewrite -preimage_setI Aij ?preimage_set0. rewrite integral_bigcup //; last 2 first. - by move=> k; case: ifPn. - apply: (integrableS measurableT) => //. by rewrite -bigcup_mkcond; exact: bigcup_measurable. transitivity (\sum_(i <oo) \int[P]_(x in (if i \in dRV_dom X then X @^-1` [set dRV_enum X i] else set0)) (dRV_enum X i)%:E). apply: eq_eseriesr => i _; case: ifPn => iX. by apply: eq_integral => t; rewrite in_setE/= => ->. by rewrite !integral_set0. transitivity (\sum_(i <oo) (dRV_enum X i)%:E * \int[P]_(x in (if i \in dRV_dom X then X @^-1` [set dRV_enum X i] else set0)) 1). apply: eq_eseriesr => i _; rewrite -integralZl//; last 2 first. - by case: ifPn. - apply/integrableP; split => //. rewrite (eq_integral (cst 1%E)); last by move=> x _; rewrite abse1. rewrite integral_cst//; last by case: ifPn. rewrite mul1e (@le_lt_trans _ _ 1%E) ?ltey//. by case: ifPn => // _; exact: probability_le1. by apply: eq_integral => y _; rewrite mule1. apply: eq_eseriesr => k _; case: ifPn => kX. rewrite /= integral_cst//= mul1e probability_distribution muleC. by rewrite distribution_dRV_enum. by rewrite integral_set0 mule0 /enum_prob patchE (negbTE kX) mul0e. 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