proposition: Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) : (forall k x, 0 <= h k x) -> (forall k, measurable_fun D (h k)) -> measurable_fun D (fun x => \sum_(i <oo) h i x).
proof: Proof. move=> h0 mh; rewrite [X in measurable_fun _ X](_ : _ = (fun x => limn_esup (fun n => \sum_(0 <= i < n) h i x))); last first. apply/funext=> x; rewrite is_cvg_limn_esupE//. exact: is_cvg_ereal_nneg_natsum. by apply: measurable_fun_limn_esup => k; exact: emeasurable_fun_sum. 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