proposition: Lemma integral_measure_zero (D : set T) (f : T -> \bar R) : \int[mzero]_(x in D) f x = 0.
proof: Proof. have h g : (forall x, 0 <= g x) -> [set sintegral mzero h | h in [set h : {nnsfun T >-> R} | forall x, (h x)%:E <= g x]] = [set 0]. move=> g0; apply/seteqP; split => [_ [h/= Dt <-]|x -> /=]. by rewrite sintegral_measure_zero. by exists (cst_nnsfun _ (@NngNum _ 0 (lexx _))). rewrite integralE !ge0_integralE//= h ?ereal_sup1; last first. by move=> r; rewrite erestrict_ge0. by rewrite h ?ereal_sup1 ?subee// => r; rewrite erestrict_ge0. 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