proposition: Lemma ge0_integral_measure_sum (D : set T) (mD : measurable D) (f : T -> \bar R) : (forall x, D x -> 0 <= f x) -> measurable_fun D f -> forall N, \int[msum m_ N]_(x in D) f x = \sum_(n < N) \int[m_ n]_(x in D) f x.
proof: Proof. move=> f0 mf. have [f_ [f_nd f_f]] := approximation mD mf f0. elim => [|N ih]; first by rewrite big_ord0 msum_mzero integral_measure_zero. rewrite big_ord_recr/= -ih. rewrite (_ : _ m_ N.+1 = measure_add [the measure _ _ of msum m_ N] (m_ N)); last first. by apply/funext => A; rewrite measure_addE /msum/= big_ord_recr. have mf_ n : measurable_fun D (fun x => (f_ n x)%:E). exact/measurable_funTS/EFin_measurable_fun. have f_ge0 n x : D x -> 0 <= (f_ n x)%:E by move=> Dx; rewrite lee_fin. have cvg_f_ (m : {measure set T -> \bar R}) : cvgn (fun x => \int[m]_(x0 in D) (f_ x x0)%:E). apply: ereal_nondecreasing_is_cvgn => a b ab. apply: ge0_le_integral => //; [exact: f_ge0|exact: f_ge0|]. by move=> t Dt; rewrite lee_fin; apply/lefP/f_nd. transitivity (limn (fun n => \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//; last first. by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd. by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: f_f. transitivity (limn (fun n => \int[msum m_ N]_(x in D) (f_ n x)%:E + \int[m_ N]_(x in D) (f_ n x)%:E)). by congr (limn _); apply/funext => n; by rewrite integral_measure_add_nnsfun. rewrite limeD//; do?[exact: cvg_f_]; last first. by apply: ge0_adde_def; rewrite inE; apply: lime_ge => //; do?[exact: cvg_f_]; apply: nearW => n; apply: integral_ge0 => //; exact: f_ge0. by congr (_ + _); (rewrite -monotone_convergence//; [ apply: eq_integral => t /[!inE] Dt; apply/cvg_lim => //; exact: f_f | move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd]). 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