proposition: Lemma ge0_integral_measure_series (D : set T) (mD : measurable D) (f : T -> \bar R) : (forall t, D t -> 0 <= f t) -> measurable_fun D f -> \int[m]_(x in D) f x = \sum_(n <oo) \int[m_ n]_(x in D) f x.
proof: Proof. move=> f0 mf. apply/eqP; rewrite eq_le; apply/andP; split; last first. suff : forall n, \sum_(k < n) \int[m_ k]_(x in D) f x <= \int[m]_(x in D) f x. move=> n; apply: lime_le => //. by apply: is_cvg_ereal_nneg_natsum => k _; exact: integral_ge0. by apply: nearW => x; rewrite big_mkord. move=> n. rewrite [X in _ <= X](_ : _ = (\sum_(k < n) \int[m_ k]_(x in D) f x + \int[mseries m_ n]_(x in D) f x)); last first. transitivity (\int[measure_add [the measure _ _ of msum m_ n] [the measure _ _ of mseries m_ n]]_(x in D) f x). congr (\int[_]_(_ in D) _); apply/funext => A. by rewrite measure_addE; exact: nneseries_split. rewrite integral_measure_add//; congr (_ + _). by rewrite -ge0_integral_measure_sum. by apply: leeDl; exact: integral_ge0. rewrite ge0_integralE//=; apply: ub_ereal_sup => /= _ [g /= gf] <-. rewrite -integralT_nnsfun (integral_measure_series_nnsfun _ mD). apply: lee_nneseries => n _. by apply: integral_ge0 => // x _; rewrite lee_fin. rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //. - by move=> x _; rewrite lee_fin. - exact/EFin_measurable_fun. - by move=> x _; rewrite erestrict_ge0. - exact/(measurable_restrict _ mD). 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