wip

theories/probability.v

@@ -565,7 +565,6 @@ have [-> _|-> _|-> _ |-> _] := subset_set2 YT.
 Qed.
 Arguments emeasurable_fun_bool {D f} b.
 
-(* NB: do not rm, we should prove it this way *)
 Lemma markov (X : {RV P >-> R}) (f : {mfun R >-> R}) (eps : R) :
   0 < eps -> (forall r : R, 0 <= f r) -> {in `[0, +oo[%classic &, {homo f : x y / x <= y}} ->
  ((f eps)%:E * P [set x | eps%:E <= `| (X x)%:E | ]%E <=
@@ -656,6 +655,17 @@ Section cvg_random_variable.
 Variables (d : _) (T : measurableType d) (R : realType) (P : probability T R).
 
 Definition probabilistic_cvg (X : {RV P >-> R}^nat) (Y : {RV P >-> R})
-  := forall a : {posnum R}, [sequence P [set x | a%:num <= `| X n x - Y x | ] ]_n --> 0%E.
+  := forall a : {posnum R}, [sequence (fine \o P) [set x | a%:num <= `| X n x - Y x | ] ]_n --> (0%R:R).
+
+Lemma prop_23_1 (X : {RV P >-> R}^nat) (Y : {RV P >-> R})
+  : (*(@mabs R `o (X n `- Y) ) @[n --> \oo]--> cst_mfun 0*)
+    (forall x, `| X n x - Y x | @[n --> \oo]--> (0%R:R)) -> probabilistic_cvg X Y.
+Proof.
+move => h a /=.
+apply/(@cvg_distP _ [pseudoMetricNormedZmodType R of R^o]).
+move => eps heps.
+rewrite near_map /=.
+near=> n.
+
 
 End cvg_random_variable.