proposition: Lemma expectation_sum (X : seq {RV P >-> R}) : (forall Xi, Xi \in X -> P.-integrable [set: T] (EFin \o Xi)) -> 'E_P[\sum_(Xi <- X) Xi] = \sum_(Xi <- X) 'E_P[Xi].
proof: Proof. elim: X => [|X0 X IHX] intX; first by rewrite !big_nil expectation_cst. have intX0 : P.-integrable [set: T] (EFin \o X0). by apply: intX; rewrite in_cons eqxx. have {}intX Xi : Xi \in X -> P.-integrable [set: T] (EFin \o Xi). by move=> XiX; apply: intX; rewrite in_cons XiX orbT. rewrite !big_cons expectationD ?IHX// (_ : _ \o _ = fun x => \sum_(f <- map (fun x : {RV P >-> R} => EFin \o x) X) f x). by apply: integrable_sum => // _ /mapP[h hX ->]; exact: intX. by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. 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