proposition: Lemma le_integral_comp_abse d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D) (g : T -> \bar R) a (f : \bar R -> \bar R) (mf : measurable_fun setT f) (f0 : forall r, 0 <= r -> 0 <= f r) (f_nd : {in `[0, +oo[%classic &, {homo f : x y / x <= y}}) : measurable_fun D g -> (0 < a)%R -> (f a%:E) * mu (D `&` [set x | (`|g x| >= a%:E)%E]) <= \int[mu]_(x in D) f `|g x|.
proof: Proof. move=> mg a0; have ? : measurable (D `&` [set x | (a%:E <= `|g x|)%E]). by apply: emeasurable_fun_c_infty => //; exact: measurableT_comp. apply: (@le_trans _ _ (\int[mu]_(x in D `&` [set x | `|g x| >= a%:E]) f `|g x|)). rewrite -integral_cst//; apply: ge0_le_integral => //. - by move=> x _ /=; rewrite f0 // lee_fin ltW. - by move=> x _ /=; rewrite f0. - apply: measurableT_comp => //; apply: measurableT_comp => //. exact: measurable_funS mg. - by move=> x /= [Dx]; apply: f_nd; rewrite inE /= in_itv /= andbT// lee_fin ltW. apply: subset_integral => //; last by move=> x _ /=; rewrite f0. by apply: measurableT_comp => //; 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