proposition: Lemma emeasurable_fun_sum D I s (h : I -> (T -> \bar R)) : (forall n, measurable_fun D (h n)) -> measurable_fun D (fun x => \sum_(i <- s) h i x).
proof: Proof. elim: s => [|s t ih] mf. by under eq_fun do rewrite big_nil; exact: measurable_cst. under eq_fun do rewrite big_cons //=; apply: emeasurable_funD => //. exact: ih. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun