diff --git a/theories/probability.v b/theories/probability.v
index ac2bab340..4c16e01f7 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -258,7 +258,7 @@ by apply: (@subset_trans _ [set` Interval x z]);
   [exact: subset_itvr | exact: subset_itvl].
 Qed.
 
-Lemma gtr0_derive1_homo (R : realType) (f : R -> R) (a b : R) (sa sb : bool) :
+Lemma gtr0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) :
   (forall x : R, x \in `]a, b[ -> derivable f x 1) ->
   (forall x : R, x \in `]a, b[ -> 0 < 'D_1 f x) ->
   {within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
@@ -272,7 +272,7 @@ have zab z : z \in `]x, y[ -> z \in `]a, b[.
   apply: subset_itvW_bound.
     by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW.
   by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW.
-have HMVT0 z : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
+have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
   by move=> zxy; exact/derivableP/df/zab.
 rewrite -subr_gt0.
 have[z zxy ->]:= MVT xy HMVT0 HMVT1.
@@ -280,7 +280,7 @@ rewrite mulr_gt0// ?subr_gt0// dfgt0//.
 exact: zab.
 Qed.
 
-Lemma ger0_derive1_homo (R : realType) (f : R -> R) (a b : R) (sa sb : bool) :
+Lemma ger0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) :
   (forall x : R, x \in `]a, b[ -> derivable f x 1) ->
   (forall x : R, x \in `]a, b[ -> 0 <= 'D_1 f x) ->
   {within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
@@ -294,7 +294,7 @@ have zab z : z \in `]x, y[ -> z \in `]a, b[.
   apply: subset_itvW_bound.
     by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW.
   by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW.
-have HMVT0 z : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
+have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
   by move=> zxy; exact/derivableP/df/zab.
 rewrite -subr_ge0.
 move: (xy); rewrite le_eqVlt=> /orP [/eqP-> | xy']; first by rewrite subrr.
@@ -306,6 +306,7 @@ Qed.
 Lemma memB_itv (R : numDomainType) (b0 b1 : bool) (x y z : R) :
   (y - z \in Interval (BSide b0 x) (BSide b1 y)) =
   (x + z \in Interval (BSide (~~ b1) x) (BSide (~~ b0) y)).
+Proof.
 rewrite !in_itv /= /Order.lteif !if_neg.
 by rewrite gerBl gtrBl lerDl ltrDl lerBrDr ltrBrDr andbC.
 Qed.
@@ -979,7 +980,7 @@ move=> AX B BA.
 rewrite [in LHS]unlock.
 rewrite /mutually_independent_RV in AX.
 rewrite /mutually_independent in AX.
-Admitted.
+Abort.
 
 End independent_RVs.
 
@@ -1317,6 +1318,8 @@ HB.instance Definition _ (f : {mfun aT >-> rT}) :=
 
 End mfun_measurable_realType.
 
+Reserved Notation "'M_ X t" (format "''M_' X  t", at level 5, t, X at next level).
+
 Section markov_chebyshev_cantelli.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType) (P : probability T R).
@@ -1340,10 +1343,13 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X)
 Qed.
 
 Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X].
+
+Local Notation "'M_ X t" := (mmt_gen_fun X t).
+
 Definition nth_mmt (X : {RV P >-> R}) (n : nat) := 'E_P[X^+n].
 
 Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R ->
-  P [set x | X x >= a]%R <= mmt_gen_fun X r * (expR (- (r * a)))%:E.
+  P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E.
 Proof.
 move=> t0.
 rewrite /mmt_gen_fun; have -> : expR \o r \o* X =
@@ -1472,6 +1478,8 @@ Qed.
 
 End markov_chebyshev_cantelli.
 
+Notation "'M_ X t" := (mmt_gen_fun X t) : ereal_scope.
+
 HB.mixin Record MeasurableFun_isDiscrete d d' (T : measurableType d) (U : measurableType d')
     (X : T -> U) of @MeasurableFun d _ T U X := {
   countable_range : countable (range X)
@@ -1676,7 +1684,7 @@ move=> iX; rewrite dRV_expectation// [in RHS]eseries_mkcond.
 apply: eq_eseriesr => k _.
 rewrite /enum_prob patchE; case: ifPn => kX; last by rewrite mul0e.
 by rewrite /pmf fineK// fin_num_measure.
-Qed.
+Abort.
 
 End discrete_distribution.
 
@@ -3119,17 +3127,19 @@ Qed.
 Lemma independent_mmt_gen_fun (X : {dRV P >-> bool}^nat) n t :
   let mmtX (i : nat) : {RV P >-> R} := expR \o t \o* (btr P (X i)) in
   independent_RVs P `I_n X -> independent_RVs P `I_n mmtX.
+Proof.
 Admitted. (* from Reynald's PR, independent_RVs2_comp, "when applying a function, the sigma algebra only gets smaller" *)
 
 Lemma expectation_prod_independent_RVs (X : {RV P >-> R}^nat) n :
   independent_RVs P `I_n X ->
   'E_P[\prod_(i < n) (X i)] = \prod_(i < n) 'E_P[X i].
+Proof.
 Admitted.
 
 Lemma bernoulli_trial_mmt_gen_fun (X_ : {dRV P >-> bool}^nat) n (t : R) :
   is_bernoulli_trial n X_ ->
   let X := bernoulli_trial n X_ in
-  mmt_gen_fun X t = \prod_(i < n) mmt_gen_fun (btr P (X_ i)) t.
+  'M_X t = \prod_(i < n) 'M_(btr P (X_ i)) t.
 Proof.
 move=> []bRVX iRVX /=.
 rewrite /bernoulli_trial/mmt_gen_fun.
@@ -3148,7 +3158,7 @@ Arguments sub_countable [T U].
 Arguments card_le_finite [T U].
 
 Lemma bernoulli_mmt_gen_fun (X : {dRV P >-> bool}) (t : R) :
-  bernoulli_RV X -> mmt_gen_fun (btr P X : {RV P >-> R}) t = (p * expR t + (1-p))%:E.
+  bernoulli_RV X -> 'M_(btr P X : {RV P >-> R}) t = (p * expR t + (1-p))%:E.
 Proof.
 move=> bX. rewrite/mmt_gen_fun.
 pose mmtX : {RV P >-> R} := expR \o t \o* (btr P X).
@@ -3188,7 +3198,7 @@ Proof. by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed.
 Lemma binomial_mmt_gen_fun (X_ : {dRV P >-> bool}^nat) n (t : R) :
   is_bernoulli_trial n X_ ->
   let X := bernoulli_trial n X_ : {RV P >-> R} in
-  mmt_gen_fun X t = ((p * expR t + (1-p))`^(n%:R))%:E.
+  'M_X t = ((p * expR t + (1-p))`^(n%:R))%:E.
 Proof.
 move: p01 => /andP[p0 p1] bX/=.
 rewrite bernoulli_trial_mmt_gen_fun//.
@@ -3199,6 +3209,7 @@ rewrite big_const iter_mule mule1 cardT size_enum_ord -EFin_expe powR_mulrn//.
 by rewrite addr_ge0// ?subr_ge0// mulr_ge0// expR_ge0.
 Qed.
 
+(* TODO: add to the PR by reynald that adds the \prod notation to master *)
 Lemma prod_EFin U l Q (f : U -> R) : \prod_(i <- l | Q i) ((f i)%:E) = (\prod_(i <- l | Q i) f i)%:E.
 Proof.
 elim: l; first by rewrite !big_nil.
@@ -3208,11 +3219,11 @@ case: ifP => //= aQ.
 by rewrite EFinM ih.
 Qed.
 
-Lemma lm23 (X_ : {dRV P >-> bool}^nat) (t : R) n :
+Lemma mmt_gen_fun_expectation (X_ : {dRV P >-> bool}^nat) (t : R) n :
   (0 <= t)%R ->
   is_bernoulli_trial n X_ ->
   let X := bernoulli_trial n X_ : {RV P >-> R} in
-  mmt_gen_fun X t <= (expR (fine 'E_P[X] * (expR t - 1)))%:E.
+  'M_X t <= (expR (fine 'E_P[X] * (expR t - 1)))%:E.
 Proof.
 move=> t0 bX/=.
 have /andP[p0 p1] := p01.
@@ -3224,9 +3235,6 @@ rewrite -mulrA (mulrC (n%:R)) expRM ge0_ler_powR// ?nnegrE ?expR_ge0//.
 exact: expR_ge1Dx.
 Qed.
 
-Lemma expR_powR (x y : R) : (expR (x * y) = (expR x) `^ y)%R.
-Proof. by rewrite /powR gt_eqF ?expR_gt0// expRK mulrC. Qed.
-
 Lemma end_thm24 (X_ : {dRV P >-> bool}^nat) n (t delta : R) :
   is_bernoulli_trial n X_ ->
   (0 < delta)%R ->
@@ -3243,11 +3251,11 @@ rewrite -EFinM lee_fin -powRM ?expR_ge0// ge0_ler_powR ?nnegrE//.
 - by rewrite mulr_ge0// expR_ge0.
 - by rewrite divr_ge0 ?expR_ge0// powR_ge0.
 - rewrite lnK ?posrE ?addr_gt0// addrAC subrr add0r ler_wpmul2l ?expR_ge0//.
-  by rewrite -powRN mulNr -mulrN expR_powR lnK// posrE addr_gt0.
+  by rewrite -powRN mulNr -mulrN expRM lnK// posrE addr_gt0.
 Qed.
 
 (* theorem 2.4 Rajani / thm 4.4.(2) mu-book *)
-Theorem thm24 (X_ : {dRV P >-> bool}^nat) n (delta : R) :
+Theorem bernoulli_trial_inequality1 (X_ : {dRV P >-> bool}^nat) n (delta : R) :
   is_bernoulli_trial n X_ ->
   (0 < delta)%R ->
   let X := @bernoulli_trial n X_ in
@@ -3264,13 +3272,13 @@ apply: (le_trans (chernoff _ _ t0)).
 apply: (@le_trans _ _ ((expR (fine mu * (expR t - 1)))%:E *
                        (expR (- (t * ((1 + delta) * fine mu))))%:E)).
   rewrite lee_pmul2r ?lte_fin ?expR_gt0//.
-  by apply: (lm23 _ bX); rewrite le_eqVlt t0 orbT.
-rewrite mulrC expR_powR -mulNr mulrA expR_powR.
+  by apply: (mmt_gen_fun_expectation _ bX); rewrite le_eqVlt t0 orbT.
+rewrite mulrC expRM -mulNr mulrA expRM.
 exact: (end_thm24 _ bX).
 Qed.
 
 (* theorem 2.5 *)
-Theorem poisson_ineq (X : {dRV P >-> bool}^nat) (delta : R) n :
+Theorem bernoulli_trial_inequality2 (X : {dRV P >-> bool}^nat) (delta : R) n :
   is_bernoulli_trial n X ->
   let X' := @bernoulli_trial n X in
   let mu := 'E_P[X'] in
@@ -3281,8 +3289,8 @@ Theorem poisson_ineq (X : {dRV P >-> bool}^nat) (delta : R) n :
 Proof.
 move=> bX X' mu n0 /andP[delta0 _].
 apply: (@le_trans _ _ (expR ((delta - (1 + delta) * ln (1 + delta)) * fine mu))%:E).
-  rewrite expR_powR expRB (mulrC _ (ln _)) expR_powR lnK; last rewrite posrE addr_gt0//.
-  apply: (thm24 bX) => //.
+  rewrite expRM expRB (mulrC _ (ln _)) expRM lnK; last rewrite posrE addr_gt0//.
+  apply: (bernoulli_trial_inequality1 bX) => //.
 apply: (@le_trans _ _ (expR ((delta - (delta + delta ^+ 2 / 3)) * fine mu))%:E).
   rewrite lee_fin ler_expR ler_wpmul2r//.
     by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX).
@@ -3302,7 +3310,7 @@ Lemma norm_expR : normr \o expR = (expR : R -> R).
 Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.
 
 (* Rajani thm 2.6 / mu-book thm 4.5.(2) *)
-Theorem thm26 (X : {dRV P >-> bool}^nat) (delta : R) n :
+Theorem bernoulli_trial_inequality3 (X : {dRV P >-> bool}^nat) (delta : R) n :
   is_bernoulli_trial n X -> (0 < delta < 1)%R ->
   let X' := @bernoulli_trial n X : {RV P >-> R} in
   let mu := 'E_P[X'] in
@@ -3330,26 +3338,26 @@ apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine
     apply: (@markov _ _ _ P (expR \o t \o* X' : {RV P >-> R}) id (expR (t * (1 - delta) * fine mu))%R _ _ _ _) => //.
     - apply: expR_gt0.
     - rewrite norm_expR.
-      have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by [].
+      have -> : 'E_P[expR \o t \o* X'] = 'M_X' t by [].
       by rewrite (binomial_mmt_gen_fun _ bX).
   apply: (@le_trans _ _ (((expR ((expR t - 1) * fine mu)) / (expR (t * (1 - delta) * fine mu))))%:E).
     rewrite norm_expR lee_fin ler_wpmul2r ?invr_ge0 ?expR_ge0//.
-    have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by [].
+    have -> : 'E_P[expR \o t \o* X'] = 'M_X' t by [].
     rewrite (binomial_mmt_gen_fun _ bX)/=.
     rewrite /mu /X' (expectation_bernoulli_trial bX)/=.
     rewrite !lnK ?posrE ?subr_gt0//.
-    rewrite expR_powR powRrM powRAC.
+    rewrite expRM powRrM powRAC.
     rewrite ge0_ler_powR ?ler0n// ?nnegrE ?powR_ge0//.
       by rewrite addr_ge0 ?mulr_ge0// subr_ge0// ltW.
-    rewrite addrAC subrr sub0r -expR_powR.
+    rewrite addrAC subrr sub0r -expRM.
     rewrite addrCA -{2}(mulr1 p) -mulrBr addrAC subrr sub0r mulrC mulNr.
     by apply: expR_ge1Dx.
   rewrite !lnK ?posrE ?subr_gt0//.
-  rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expR_powR lnK ?posrE ?subr_gt0//.
+  rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expRM lnK ?posrE ?subr_gt0//.
   rewrite -[in leRHS]powR_inv1 ?powR_ge0// powRM// ?expR_ge0 ?invr_ge0 ?powR_ge0//.
-  by rewrite powRAC powR_inv1 ?powR_ge0// powRrM expR_powR.
+  by rewrite powRAC powR_inv1 ?powR_ge0// powRrM expRM.
 rewrite lee_fin.
-rewrite -mulrN -mulrA [in leRHS]mulrC expR_powR ge0_ler_powR// ?nnegrE.
+rewrite -mulrN -mulrA [in leRHS]mulrC expRM ge0_ler_powR// ?nnegrE.
 - by rewrite fine_ge0// expectation_ge0// => x; exact: (bernoulli_trial_ge0 bX).
 - by rewrite divr_ge0 ?expR_ge0// powR_ge0.
 - by rewrite expR_ge0.
@@ -3367,7 +3375,7 @@ rewrite -mulrN -mulrA [in leRHS]mulrC expR_powR ge0_ler_powR// ?nnegrE.
     by rewrite -(mulr_natr (- delta) 2) mulNr.
   rewrite addrAC subr_le0.
   set f := fun (x : R) => x ^+ 2 + - (x * ln x) * 2.
-  have @idf (x : R) : 0 < x -> {df | is_derive x 1 f df}.
+  have @idf (x : R^o) : 0 < x -> {df | is_derive x 1 (f : R^o -> R^o) df}.
     move=> x0; evar (df : (R : Type)); exists df.
     apply: is_deriveD; first by [].
     apply: is_deriveM; last by [].
@@ -3408,7 +3416,7 @@ apply: emeasurable_fun_le => //; apply: measurableT_comp => //.
 Qed.
 
 (* Rajani -> corollary 2.7 / mu-book -> corollary 4.7 *)
-Corollary cor27 (X : {dRV P >-> bool}^nat) (delta : R) n :
+Corollary bernoulli_trial_inequality4 (X : {dRV P >-> bool}^nat) (delta : R) n :
   is_bernoulli_trial n X -> (0 < delta < 1)%R ->
   (0 < n)%nat ->
   (0 < p)%R ->
@@ -3444,8 +3452,8 @@ rewrite measureU; last 3 first.
   rewrite lte_pmul2r//; first by rewrite lte_fin ltr_add2l gt0_cp.
   by rewrite fineK /mu/X' (expectation_bernoulli_trial bX)// lte_fin  mulr_gt0 ?ltr0n.
 rewrite mulr2n EFinD lee_add//=.
-- by apply: (poisson_ineq bX); rewrite //d0 d1.
-- apply: (le_trans (@thm26 _ delta _ bX _)); first by rewrite d0 d1.
+- by apply: (bernoulli_trial_inequality2 bX); rewrite //d0 d1.
+- apply: (le_trans (@bernoulli_trial_inequality3 _ delta _ bX _)); first by rewrite d0 d1.
   rewrite lee_fin ler_expR !mulNr ler_opp2.
   rewrite ler_pmul//; last by rewrite lef_pinv ?posrE ?ler_nat.
   rewrite mulr_ge0 ?fine_ge0 ?sqr_ge0//.
@@ -3488,7 +3496,7 @@ have step1 : P [set i | `| X' i - p | >= epsilon * p]%R <=
   rewrite -mulrA.
   have -> : (p * n%:R)%R = fine (p * n%:R)%:E by [].
   rewrite -E_X_sum.
-  by apply: (@cor27 X epsilon _ bX).
+  by apply: (@bernoulli_trial_inequality4 X epsilon _ bX).
 have step2 : P [set i | `| X' i - p | >= theta]%R <=
     ((expR (- (n%:R * theta ^+ 2) / 3)) *+ 2)%:E.
   rewrite thetaE; move/le_trans : step1; apply.