proposition: Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) : (0 < eps)%R -> measurable_fun [set: R] f -> (forall r, 0 <= f r)%R -> {in Num.nneg &, {homo f : x y / x <= y}}%R -> (f eps)%:E * P [set x | eps%:E <= `| (X x)%:E | ] <= 'E_P[f \o (fun x => `| x |%R) \o X].
proof: Proof. move=> e0 mf f0 f_nd; rewrite -(setTI [set _ | _]). apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X) eps (er_map f) _ _ _ _ e0)) => //=. - exact: measurable_er_map. - by case => //= r _; exact: f0. - move=> [x| |] [y| |]; rewrite !inE/= !in_itv/= ?andbT ?lee_fin ?leey//. by move=> ? ? ?; rewrite f_nd. - exact/EFin_measurable_fun. - by rewrite unlock. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) HB(structures) exp numfun lebesgue_measure lebesgue_integral reals ereal signed topology normedtype sequences esum measure exp numfun lebesgue_measure lebesgue_integral