proposition: Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) : measurable D -> measurable_fun D f -> measurable_fun D g -> ae_eq D f g -> integral mu D f = integral mu D g.
proof: Proof. move=> mD mf mg /ae_eq_funeposneg[Dfgp Dfgn]. rewrite integralE// [in RHS]integralE//; congr (_ - _). by apply: ge0_ae_eq_integral => //; [exact: measurable_funepos| exact: measurable_funepos]. by apply: ge0_ae_eq_integral => //; [exact: measurable_funeneg| exact: measurable_funeneg]. 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