proposition: Lemma integral_setU (A B : set T) (mA : measurable A) (mB : measurable B) (f : T -> \bar R) : measurable_fun (A `|` B) f -> (forall x, (A `|` B) x -> 0 <= f x) -> [disjoint A & B] -> \int[mu]_(x in A `|` B) f x = \int[mu]_(x in A) f x + \int[mu]_(x in B) f x.
proof: Proof. move=> mf f0 AB. transitivity (\int[mu]_(x in A `|` B) ((f \_ A) x + (f \_ B) x)). apply: eq_integral => x; rewrite inE => -[xA|xB]. rewrite /patch mem_set// ifF ?adde0//; apply/negbTE/negP; rewrite inE => xB. by move: AB; rewrite disj_set2E => /eqP; apply/eqP/set0P; exists x. rewrite /patch addeC mem_set// ifF ?adde0//; apply/negbTE/negP; rewrite inE => xA. by move: AB; rewrite disj_set2E => /eqP; apply/eqP/set0P; exists x. rewrite ge0_integralD//; last 5 first. - exact: measurableU. - by move=> x _; apply: erestrict_ge0 => y Ay; apply: f0; left. - have : measurable_fun A f. by apply: measurable_funS mf; [exact: measurableU|exact: subsetUl]. by apply/(measurable_restrict _ _ _ _).1 => //; exact: measurableU. - by move=> x _; apply: erestrict_ge0 => y By; apply: f0; right. - have : measurable_fun B f. by apply: measurable_funS mf; [exact: measurableU|exact: subsetUr]. by apply/(measurable_restrict _ _ _ _).1 => //; exact: measurableU. by rewrite -integral_mkcondl setIC setUK -integral_mkcondl setKU. 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