proposition: Lemma integral_le_bound (D : set T) (f : T -> \bar R) (M : \bar R) : measurable D -> measurable_fun D f -> 0 <= M -> {ae mu, forall x, D x -> `|f x| <= M} -> \int[mu]_(x in D) `|f x| <= M * mu D.
proof: Proof. move=> mD mf M0 dfx; rewrite -integral_cst => //. by apply: ae_ge0_le_integral => //; exact: measurableT_comp. 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