proposition: Lemma negligible_integral (D N : set T) (f : T -> \bar R) : measurable N -> measurable D -> mu.-integrable D f -> mu N = 0 -> \int[mu]_(x in D) f x = \int[mu]_(x in D `\` N) f x.
proof: Proof. move=> mN mD mf muN0; rewrite [f]funeposneg ?integralB //; first last. - exact: integrable_funeneg. - exact: integrable_funepos. - apply: (integrableS mD) => //; first exact: measurableD. exact: integrable_funeneg. - apply: (integrableS mD) => //; first exact: measurableD. exact: integrable_funepos. - exact: measurableD. congr (_ - _); apply: ge0_negligible_integral => //; apply: measurable_int. exact: (integrable_funepos mD mf). exact: (integrable_funeneg mD mf). 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