proposition: Lemma le_integral_abse (D : set T) (mD : measurable D) (g : T -> \bar R) a : measurable_fun D g -> (0 < a)%R -> a%:E * mu (D `&` [set x | `|g x| >= a%:E]) <= \int[mu]_(x in D) `|g x|.
proof: Proof. move=> mg a0; have ? : measurable (D `&` [set x | a%:E <= `|g x|]). by apply: emeasurable_fun_c_infty => //; exact: measurableT_comp. apply: (@le_trans _ _ (\int[mu]_(x in D `&` [set x | `|g x| >= a%:E]) `|g x|)). rewrite -integral_cstr//; apply: ge0_le_integral => //. - by move=> x _ /=; exact/ltW. - by apply: measurableT_comp => //; exact: measurable_funS mg. - by move=> x /= []. by apply: subset_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