proposition: Lemma eq_measure_integral m2 m1 (f : T -> \bar R) : (forall A, measurable A -> A `<=` D -> m1 A = m2 A) -> \int[m1]_(x in D) f x = \int[m2]_(x in D) f x.
proof: Proof. move=> m12; rewrite /integral funepos_restrict funeneg_restrict. by congr (ereal_sup _ - ereal_sup _)%E; rewrite eqEsubset; split; apply: eq_measure_integral0 => A /m12 // /[apply]. 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