proposition: Lemma le_abse_integral d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R) (mD : measurable D) : measurable_fun D f -> (`| \int[mu]_(x in D) (f x) | <= \int[mu]_(x in D) `|f x|)%E.
proof: Proof. move=> mf. rewrite integralE (le_trans (lee_abs_sub _ _))// gee0_abs; last first. exact: integral_ge0. rewrite gee0_abs; last exact: integral_ge0. by rewrite -ge0_integralD // -?fune_abse//; [exact: measurable_funepos | 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