proposition: Lemma integral_nneseries : \int[mu]_(x in D) (\sum_(n <oo) f n x) = \sum_(n <oo) (\int[mu]_(x in D) (f n x)).
proof: Proof. rewrite monotone_convergence //. - by rewrite -lim_mkord; under eq_fun do rewrite ge0_integral_sum// big_mkord. - by move=> n; exact: emeasurable_fun_sum. - by move=> n x Dx; apply: sume_ge0 => m _; exact: f0. - by move=> x Dx m n mn; apply: lee_sum_nneg_natr => // k _ _; exact: f0. 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