proposition: Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) : measurable D -> measurable_fun D f -> measurable_fun D g -> (forall x, D x -> 0 <= f x) -> (forall x, D x -> 0 <= g x) -> ae_eq D f g -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x).
proof: Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. rewrite integralEindic// [RHS]integralEindic//. rewrite (ge0_negligible_integral mN)//; last 2 first. - by apply: emeasurable_funM => //; exact/EFin_measurable_fun. - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin]. rewrite [RHS](ge0_negligible_integral mN)//; last 2 first. - by apply: emeasurable_funM => //; exact/EFin_measurable_fun. - by move=> x Dx; apply: mule_ge0 => //; [exact: g0|rewrite lee_fin]. - apply: eq_integral => x;rewrite in_setD => /andP[_ xN]. apply: contrapT; rewrite indicE; have [|?] := boolP (x \in D). rewrite inE => Dx; rewrite !mule1. move: xN; rewrite notin_set; apply: contra_not => fxgx; apply: subN => /=. exact/not_implyP. by rewrite !mule0. 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