proposition: Lemma ge0_integral_bigsetU (I : eqType) (F : I -> set T) (f : T -> \bar R) (s : seq I) : (forall n, measurable (F n)) -> uniq s -> trivIset [set` s] F -> let D := \big[setU/set0]_(i <- s) F i in measurable_fun D f -> (forall x, D x -> 0 <= f x) -> \int[mu]_(x in D) f x = \sum_(i <- s) \int[mu]_(x in F i) f x.
proof: Proof. move=> mF; elim: s => [|h t ih] us tF D mf f0. by rewrite /D 2!big_nil integral_set0. rewrite /D big_cons integral_setU//. - rewrite big_cons ih//. + by move: us => /= /andP[]. + by apply: sub_trivIset tF => /= i /= it; rewrite inE it orbT. + apply: measurable_funS mf => //; first exact: bigsetU_measurable. by rewrite /D big_cons; exact: subsetUr. + by move=> x UFx; apply: f0; rewrite /D big_cons; right. - exact: bigsetU_measurable. - by move: mf; rewrite /D big_cons. - by move: f0; rewrite /D big_cons. - apply/eqP; rewrite big_distrr/= big_seq big1// => i it. move/trivIsetP : tF; apply => //=; rewrite ?mem_head//. + by rewrite inE it orbT. + by apply/eqP => hi; move: us => /=; rewrite hi it. 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