proposition: Lemma integral_measure_series (D : set T) (mD : measurable D) (f : T -> \bar R) : (forall n, integrable (m_ n) D f) -> measurable_fun D f -> \sum_(n <oo) `|\int[m_ n]_(x in D) f^\- x | < +oo%E -> \sum_(n <oo) `|\int[m_ n]_(x in D) f^\+ x | < +oo%E -> \int[m]_(x in D) f x = \sum_(n <oo) \int[m_ n]_(x in D) f x.
proof: Proof. move=> fi mf fmoo fpoo; rewrite integralE. rewrite ge0_integral_measure_series//; last exact/measurable_funepos. rewrite ge0_integral_measure_series//; last exact/measurable_funeneg. transitivity (\sum_(n <oo) (fine (\int[m_ n]_(x in D) f^\+ x))%:E - \sum_(n <oo) (fine (\int[m_ n]_(x in D) f^\- x))%:E). by congr (_ - _); apply: eq_eseriesr => n _; rewrite fineK//; [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num]. have fineKn : \sum_(n <oo) `|\int[m_ n]_(x in D) f^\- x| = \sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\- x))%:E|. apply: eq_eseriesr => n _; congr abse; rewrite fineK//. exact: integrable_neg_fin_num. have fineKp : \sum_(n <oo) `|\int[m_ n]_(x in D) f^\+ x| = \sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\+ x))%:E|. apply: eq_eseriesr => n _; congr abse; rewrite fineK//. exact: integrable_pos_fin_num. rewrite nneseries_esum; last by move=> n _; exact/fine_ge0/integral_ge0. rewrite nneseries_esum; last by move=> n _; exact/fine_ge0/integral_ge0. rewrite -esumB//; last 4 first. - by rewrite /= /summable -nneseries_esum// -fineKp. - by rewrite /summable /= -nneseries_esum// -fineKn; exact: fmoo. - by move=> n _; exact/fine_ge0/integral_ge0. - by move=> n _; exact/fine_ge0/integral_ge0. rewrite -summable_eseries_esum; last first. apply: (@le_lt_trans _ _ (\esum_(i in (fun=> true)) `|(fine (\int[m_ i]_(x in D) f x))%:E|)). by apply: le_esum => k _; rewrite -EFinB -fineB// -?integralE//; [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num]. rewrite -nneseries_esum; last by []. apply: (@le_lt_trans _ _ (\sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\+ x))%:E| + \sum_(n <oo) `|(fine (\int[m_ n]_(x in D) f^\- x))%:E|)). rewrite -nneseriesD//; apply: lee_nneseries => // n _. rewrite integralE fineB// ?EFinB. - exact: (le_trans (lee_abs_sub _ _)). - exact: integrable_pos_fin_num. - exact: integrable_neg_fin_num. apply: lte_add_pinfty; first by rewrite -fineKp. by rewrite -fineKn; exact: fmoo. by apply: eq_eseriesr => k _; rewrite !fineK// -?integralE//; [exact: integrable_neg_fin_num|exact: integrable_pos_fin_num]. 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