proposition: Lemma integral_ae_eq (D : set T) (mD : measurable D) (g f : T -> \bar R) : mu.-integrable D f -> measurable_fun D g -> (forall E, E `<=` D -> measurable E -> \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> ae_eq mu D f g.
proof: Proof. move=> fi mg fg; have mf := measurable_int fi; have gi : mu.-integrable D g. apply/integrableP; split => //; apply/abse_integralP => //; rewrite -fg//. by apply/abse_integralP => //; case/integrableP : fi. have mugf : mu (D `&` [set x | g x < f x]) = 0 by apply: integral_measure_lt. have mufg : mu (D `&` [set x | f x < g x]) = 0. by apply: integral_measure_lt => // E ED mE; rewrite fg. have h : ~` [set x | D x -> f x = g x] = D `&` [set x | f x != g x]. apply/seteqP; split => [x/= /not_implyP[? /eqP]//|x/= [Dx fgx]]. by apply/not_implyP; split => //; exact/eqP. apply/negligibleP. by rewrite h; apply: emeasurable_fun_neq. rewrite h set_neq_lt setIUr measureU//. - by rewrite [X in X + _]mufg add0e [LHS]mugf. - exact: emeasurable_fun_lt. - exact: emeasurable_fun_lt. - apply/seteqP; split => [x [[Dx/= + [_]]]|//]. by move=> /lt_trans => /[apply]; rewrite ltxx. 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