generalize le_er_map

theories/ereal.v

@@ -149,13 +149,12 @@ Section ERealArithTh_realDomainType.
 Context {R : realDomainType}.
 Implicit Types (x y z u a b : \bar R) (r : R).
 
-Lemma le_er_map (f : R -> R) :
-  {in `[0, +oo[%classic%R &, {homo f : x y / (x <= y)%O}} ->
-  {in `[0, +oo[%classic%E &, {homo er_map f : x y / (x <= y)%E}}.
+Lemma le_er_map (A : set R) (f : R -> R) :
+  {in A &, {homo f : x y / (x <= y)%O}} ->
+  {in (EFin @` A)%classic &, {homo er_map f : x y / (x <= y)%E}}.
 Proof.
-move=> f_nd x y; rewrite !inE/= !in_itv/= !andbT.
-move: x y => [x| |] [y| |] x0 y0 xy//=; last by rewrite leey.
-by rewrite lee_fin f_nd// inE /= in_itv/= andbT -lee_fin.
+move=> h x y; rewrite !inE/= => -[r Ar <-{x}] [s As <-{y}].
+by rewrite !lee_fin/= => /h; apply; rewrite inE.
 Qed.
 
 Lemma fsume_gt0 (I : choiceType) (P : set I) (F : I -> \bar R) :

theories/probability.v

@@ -248,7 +248,7 @@ Context d (T : measurableType d) (R : realType) (P : probability T R).
 
 Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) :
     (0 < eps)%R ->
-    measurable_fun [set: R] f -> (forall r : R, 0 <= f r)%R ->
+    measurable_fun [set: R] f -> (forall r, 0 <= f r)%R ->
     {in `[0, +oo[%classic &, {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].
@@ -258,7 +258,7 @@ apply: (le_trans (@le_integral_comp_abse d T R P setT measurableT (EFin \o X)
   eps (er_map f) _ _ _ _ e0)) => //=.
 - exact: measurable_fun_er_map.
 - by case => //= r _; exact: f0.
-- exact: le_er_map.
+- by move=> [x| |] [y| |] xP yP xy//=; rewrite ?leey ?leNye// lee_fin f_nd.
 - exact/EFin_measurable_fun.
 Qed.