proposition: Lemma ae_measurable_fun : ae_eq mu D f g -> measurable_fun D f -> measurable_fun D g.
proof: Proof. move=> [N [mN N0 subN]] mf B mB mD. apply: (measurability (ErealGenOInfty.measurableE R)) => // _ [_ [x ->] <-]. rewrite [X in measurable X](_ : _ = D `&` ~` N `&` (f @^-1` `]x%:E, +oo[) `|` (D `&` N `&` g @^-1` `]x%:E, +oo[)); last first. apply/seteqP; split=> [y /= [Dy gyxoo]|y /= [[[Dy Ny] fyxoo]|]]. - have [->|fgy] := eqVneq (f y) (g y). have [yN|yN] := boolP (y \in N). by right; split => //; rewrite inE in yN. by left; split => //; rewrite notin_set in yN. by right; split => //; split => //; apply: subN => /= /(_ Dy); exact/eqP. - split => //; have [<-//|fgy] := eqVneq (f y) (g y). by exfalso; apply/Ny/subN => /= /(_ Dy); exact/eqP. - by move=> [[]]. apply: measurableU. - rewrite setIAC; apply: measurableI; last exact/measurableC. exact/mf/emeasurable_itv. - by apply: cmu; exists N; split => //; rewrite setIAC; apply: subIset; right. 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