proposition: Lemma ge0_negligible_integral (D N : set T) (f : T -> \bar R) : measurable N -> measurable D -> measurable_fun D f -> (forall x, D x -> 0 <= f x) -> mu N = 0 -> \int[mu]_(x in D) f x = \int[mu]_(x in D `\` N) f x.
proof: Proof. move=> mN mD mf f0 muN0. rewrite {1}(funID mN f) ge0_integralD//; last 4 first. - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. - apply: emeasurable_funM=> //; apply/EFin_measurable_fun=> //. exact: measurable_funTS. - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. - apply: emeasurable_funM=> //; apply/EFin_measurable_fun=> //. exact: measurable_funTS. rewrite -integral_setI_indic//; last exact: measurableC. rewrite -integral_setI_indic// [X in _ + X = _](_ : _ = 0) ?adde0//. rewrite (eq_integral (abse \o f)); last first. move=> x; rewrite in_setI => /andP[xD xN]. by rewrite /= gee0_abs// f0//; rewrite inE in xD. rewrite (@integral_abs_eq0 D)//; first exact: measurableI. by apply: (subset_measure0 _ _ _ muN0) => //; exact: measurableI. 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