proposition: Lemma integral_bigcup (F : (set _)^nat) (g : T -> \bar R) : trivIset setT F -> (forall k, measurable (F k)) -> mu.-integrable (\bigcup_k F k) g -> (\int[mu]_(x in \bigcup_i F i) g x = \sum_(i <oo) \int[mu]_(x in F i) g x)%E.
proof: Proof. move=> tF mF fi. have ? : \int[mu]_(x in \bigcup_i F i) g x \is a fin_num. rewrite fin_numElt -(lte_absl _ +oo). apply: le_lt_trans (integrableP _ _ _ fi).2; apply: le_abse_integral => //. exact: bigcupT_measurable. exact: measurable_int fi. transitivity (\int[mu]_(x in \bigcup_i F i) g^\+ x - \int[mu]_(x in \bigcup_i F i) g^\- x)%E. rewrite -integralB; last 3 first. - exact: bigcupT_measurable. - by apply: integrable_funepos => //; exact: bigcupT_measurable. - by apply: integrable_funeneg => //; exact: bigcupT_measurable. by apply: eq_integral => t Ft; rewrite [in LHS](funeposneg g). transitivity (\sum_(i <oo) (\int[mu]_(x in F i) g^\+ x - \int[mu]_(x in F i) g^\- x)); last first. by apply: eq_eseriesr => // i; rewrite [RHS]integralE. transitivity ((\sum_(i <oo) \int[mu]_(x in F i) g^\+ x) - (\sum_(i <oo) \int[mu]_(x in F i) g^\- x))%E. rewrite ge0_integral_bigcup//; last first. by apply: integrable_funepos => //; exact: bigcupT_measurable. by rewrite ge0_integral_bigcup//; apply: integrable_funepos => //; [exact: bigcupT_measurable|exact: integrableN]. rewrite [X in X - _]nneseries_esum; last by move=> n _; exact: integral_ge0. rewrite [X in _ - X]nneseries_esum; last by move=> n _; exact: integral_ge0. rewrite set_true -esumB//=; last 4 first. - apply: integrable_summable => //; apply: integrable_funepos => //. exact: bigcup_measurable. - apply: integrable_summable => //; apply: integrable_funepos => //. exact: bigcup_measurable. - exact: integrableN. - by move=> n _; exact: integral_ge0. - by move=> n _; exact: integral_ge0. rewrite summable_eseries; last first. under [X in summable _ X]eq_fun do rewrite -integralE. by rewrite fun_true; exact: integrable_summable. by congr (_ - _)%E; rewrite nneseries_esum// set_true. 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