proposition: Lemma integrable_summable (F : (set T)^nat) (g : T -> \bar R): trivIset setT F -> (forall k, measurable (F k)) -> mu.-integrable (\bigcup_k F k) g -> summable [set: nat] (fun i => \int[mu]_(x in F i) g x).
proof: Proof. move=> tF mF fi. rewrite /summable -(_ : [set _ | true] = setT); last exact/seteqP. rewrite -nneseries_esum//. case: (integrableP _ _ _ fi) => _. rewrite ge0_integral_bigcup//; last exact: integrable_abse. apply: le_lt_trans; apply: lee_lim. - exact: is_cvg_ereal_nneg_natsum_cond. - by apply: is_cvg_ereal_nneg_natsum_cond => n _ _; exact: integral_ge0. - apply: nearW => n; apply: lee_sum => m _; apply: le_abse_integral => //. apply: measurable_funS (measurable_int fi) => //; [exact: bigcup_measurable|]. exact: bigcup_sup. 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