proposition: Lemma ge0_integral_bigcup (F : (set _)^nat) (f : T -> \bar R) : (forall k, measurable (F k)) -> let D := \bigcup_k F k in mu.-integrable D f -> (forall x, D x -> 0 <= f x) -> trivIset setT F -> \int[mu]_(x in D) f x = \sum_(i <oo) \int[mu]_(x in F i) f x.
proof: Proof. move=> mF D /integrableP fi f0 tF. pose f_ N := f \_ (\big[setU/set0]_(0 <= i < N) F i). have lim_f_ t : f_ ^~ t @ \oo --> (f \_ D) t. rewrite [X in _ --> X](_ : _ = ereal_sup (range (f_ ^~ t))); last first. apply/eqP; rewrite eq_le; apply/andP; split. rewrite /restrict; case: ifPn => [|_]. rewrite in_setE => -[n _ Fnt]; apply: ereal_sup_ub; exists n.+1 => //. by rewrite /f_ big_mkord patchT// in_setE big_ord_recr/=; right. rewrite (@le_trans _ _ (f_ O t))// ?ereal_sup_ub//. by rewrite /f_ patchN// big_mkord big_ord0 inE/= in_set0. apply: ub_ereal_sup => x [n _ <-]. by rewrite /f_ restrict_lee// big_mkord; exact: bigsetU_bigcup. apply: ereal_nondecreasing_cvgn => a b ab. rewrite /f_ !big_mkord restrict_lee //; last exact: subset_bigsetU. by move=> x Dx; apply: f0 => //; exact: bigsetU_bigcup Dx. transitivity (\int[mu]_x limn (f_ ^~ x)). rewrite integral_mkcond; apply: eq_integral => x _. by apply/esym/cvg_lim => //; exact: lim_f_. rewrite monotone_convergence//; last 3 first. - move=> n; apply/(measurable_restrict f) => //. by apply: bigsetU_measurable => k _; exact: mF. case: fi => + _; apply/measurable_funS =>//; first exact: bigcup_measurable. by rewrite big_mkord; exact: bigsetU_bigcup. - move=> n x _; apply: erestrict_ge0 => y; rewrite big_mkord => Dy; apply: f0. exact: bigsetU_bigcup Dy. - move=> x _ a b ab; apply: restrict_lee. by move=> y; rewrite big_mkord => Dy; apply: f0; exact: bigsetU_bigcup Dy. by rewrite 2!big_mkord; apply: subset_bigsetU. transitivity (limn (fun N => \int[mu]_(x in \big[setU/set0]_(i < N) F i) f x)). by apply/congr_lim/funext => n; rewrite /f_ [in RHS]integral_mkcond big_mkord. apply/congr_lim/funext => /= n. rewrite -(big_mkord xpredT) ge0_integral_bigsetU ?big_mkord//. - exact: iota_uniq. - exact: sub_trivIset tF. - case: fi => + _; apply: measurable_funS => //; first exact: bigcup_measurable. exact: bigsetU_bigcup. - by move=> y Dy; apply: f0; exact: bigsetU_bigcup Dy. 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