diff --git a/theories/sampling.v b/theories/sampling.v
index b4f2def48..6df9380b8 100644
--- a/theories/sampling.v
+++ b/theories/sampling.v
@@ -11,6 +11,11 @@ Require Import probability.
 
 (**md**************************************************************************)
 (* # Sampling experiment (wip)                                                *)
+(*                                                                            *)
+(* ref:                                                                       *)
+(* - Rajani https://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf       *)
+(* - Mitzenmacher Upfal Probability and Computing                             *)
+(*   https://www.cs.purdue.edu/homes/spa/courses/pg17/mu-book.pdf             *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -23,28 +28,25 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+(* TODO: move *)
 Section probability.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType) (P : probability T R).
 
 Lemma probability_setC A : d.-measurable A -> P (~` A) = 1 - P A.
 Proof.
-move=> mA; rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI A) -measureD ?setTD ?setCK//.
+move=> mA.
+rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI A).
+rewrite -measureD ?setTD ?setCK//.
 by rewrite [ltLHS](@probability_setT _ _ _ P) ltry.
 Qed.
 
 Lemma probability_setC' A : d.-measurable A -> P A = 1 - P (~` A).
 Proof.
-move=> mA. rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)) -measureD ?setTD ?setCK//; first exact: measurableC.
-by rewrite [ltLHS](@probability_setT _ _ _ P) ltry.
-Qed.
-
-Lemma probability_fin_num A : d.-measurable A -> P A \is a fin_num.
-Proof.
 move=> mA.
-rewrite fin_numElt.
-rewrite (le_lt_trans (probability_le1 P mA) (ltry _)).
-by rewrite (lt_le_trans ltNy0 (measure_ge0 P _)).
+rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)).
+rewrite -measureD ?setTD ?setCK//; first exact: measurableC.
+by rewrite [ltLHS](@probability_setT _ _ _ P) ltry.
 Qed.
 
 End probability.
@@ -74,122 +76,6 @@ Notation "\prod_ ( i 'in' A | P ) F" :=
 Notation "\prod_ ( i 'in' A ) F" :=
   (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope.
 
-Section independent_events.
-Context {R : realType} d {T : measurableType d}.
-Variable P : probability T R.
-Local Open Scope ereal_scope.
-
-(* def 2.3, independence of events *)
-(* TODO: rename to mutually_independent_events *)
-Definition mutually_independent (I : choiceType) (A : I -> set T) :=
-(*  (forall i, J i -> measurable (A i)) /\*)
-  forall J : {fset I},
-    P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i).
-
-End independent_events.
-
-(* independent class of events, klenke def 2.11, p.59 *)
-Section independent_class.
-Context {R : realType} d {T : measurableType d}.
-Variable P : probability T R.
-Local Open Scope ereal_scope.
-
-Definition independent_class (I : choiceType) (C : I -> set (set T)) :=
-  (forall i, C i `<=` @measurable _ T) /\
-  forall J : {fset I},
-    forall E : I -> set T,
-      (forall i : I, i \in J -> E i \in C i) ->
-        P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j).
-
-End independent_class.
-
-Section independent_RV.
-Context {R : realType} d (T : measurableType d).
-Variable P : probability T R.
-
-Definition generated_salgebra (X : {RV P >-> R}) : set (set T) :=
-  preimage_class setT X (@measurable _ R).
-
-Definition independent_RV (I : choiceType) (X : I -> {RV P >-> R}) :=
-  independent_class P (fun i : I => generated_salgebra (X i)).
-
-Definition independent_RV_tuple n (X : n.-tuple {RV P >-> R}) :=
-  independent_class P (fun i => generated_salgebra (X `_ i)).
-
-Lemma independent_RV_tuple_thead_prod_behead n (X : n.+1.-tuple {RV P >-> R}) :
-  independent_RV_tuple X ->
-  independent_RV_tuple [tuple thead X; (\prod_(j <- behead X) j)%R].
-Proof.
-move: X; elim: n => [X [h1 h2]|].
-  have -> : behead X = nil. admit.
-  rewrite big_nil.
-  rewrite /independent_RV_tuple/independent_class/=.
-  split.
-    case => //=.
-      by move: (h1 0); rewrite {1}(tuple_eta X).
-    case => //=.
-      rewrite /generated_salgebra /preimage_class.
-      admit.
-    case => /= [|_].
-      admit.
-    admit.
-  admit.
-(*rewrite /independent_RV_tuple/independent_class/= => [[h1 h2]].
-split.
-  admit.
-move=> J E h3.
-rewrite h2// => i iJ.
-have := h3 i iJ.
-move: iJ.
-case: i => [//|i _].*)
-Admitted.
-
-Lemma independent_RV_tuple_behead n (X : n.-tuple {RV P >-> R}) :
-  independent_RV_tuple X -> independent_RV_tuple [tuple of behead X].
-Proof.
-move: X; case: n => [X|n X].
-  by rewrite tuple0.
-rewrite /independent_RV_tuple/independent_class/=.
-move=> [iXm iX].
-split; first by move=> i; rewrite nth_behead; exact: iXm.
-move=> J E h.
-pose E' n := match n with
-               0 => setT
-             | S m => E m
-             end.
-have := (@iX (0 |` [fset i.+1 | i in J])%fset E').
-have ? : 0 \notin [fset i.+1 | i in J]%fset.
-  apply/negP.
-  move/imfsetP.
-  by case.
-rewrite big_fsetU1//=.
-rewrite setTI big_fsetU1//=.
-rewrite probability_setT mul1e.
-rewrite big_imfset/=; last first.
-  move=> x y _ _; exact: succn_inj.
-move=> ->; last first.
-  elim.
-    move=> _.
-    rewrite/generated_salgebra/preimage_class.
-    (* TODO: make lemma *)
-    rewrite inE/=.
-    exists setT => //.
-    by rewrite setTI preimage_setT.
-  rewrite /E' => l _ h1.
-  have := (h l).
-  rewrite /generated_salgebra.
-  rewrite nth_behead => -> //.
-  move: h1.
-  move/fset1UP => []//.
-  move/imfsetP.
-  case => k/= kJ.
-  by case => ->.
-rewrite big_imfset//=.
-move=> x y _ _; exact: succn_inj.
-Qed.
-
-End independent_RV.
-
 Lemma indic_setI {R : ringType} T (A B : set T) :
   \1_A \* \1_B = \1_(A `&` B) :> (T -> R).
 Proof.
@@ -255,8 +141,7 @@ apply: measurableT_comp => //=.
 move=> x _.
 rewrite -/((abse \o (f \o phi)) x).
 rewrite (fune_abse (f \o phi)) /=.
-rewrite gee0_abs//.
-by rewrite lee_addr//.
+by rewrite gee0_abs// leeDr.
 Qed.
 
 Lemma integrable_comp_funepos : (pushforward mu mphi).-integrable [set: Y] f^\+.
@@ -277,8 +162,7 @@ apply: measurableT_comp => //=.
 move=> x _.
 rewrite -/((abse \o (f \o phi)) x).
 rewrite (fune_abse (f \o phi)) /=.
-rewrite gee0_abs//.
-by rewrite lee_addl//.
+by rewrite gee0_abs// leeDl.
 Qed.
 
 End integrable_comp.
@@ -362,6 +246,216 @@ Qed.
 
 End integral_measure_add.
 
+Lemma expR_prod d (T : measurableType d) (R : realType) (P : probability T R)
+  (X : seq {RV P >-> R}) (f : {RV P >-> R} -> R) :
+  (\prod_(x <- X) expR (f x) = expR (\sum_(x <- X) f x))%R.
+Proof.
+elim: X => [|h t ih]; first by rewrite !big_nil expR0.
+by rewrite !big_cons ih expRD.
+Qed.
+
+(* TODO: move *)
+Lemma ln_div {R : realType} :
+  {in Num.pos &, {morph ln (R:=R) : x y / (x / y)%R >-> (x - y)%R}}.
+Proof.
+move=> x y; rewrite !posrE => x0 y0.
+by rewrite lnM ?posrE ?invr_gt0// lnV ?posrE.
+Qed.
+
+Lemma norm_expR {R : realType} : normr \o expR = (expR : R -> R).
+Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.
+
+Lemma le01_expR_ge1Dx {R : realType} (x : R) :
+  (-1 <= x <= 0 -> 1 + x <= expR x)%R.
+Proof.
+move=> /andP [N1x x0].
+pose f : R^o -> R := (expR \- (cst 1 \+ id))%R.
+rewrite -subr_ge0 (_ : 0%R = f 0%R); last first.
+  by rewrite /f !fctE/= expR0 addr0 subrr.
+pose f' : R^o -> R := (expR \- (cst 0 \+ cst 1))%R.
+move: N1x; rewrite le_eqVlt => /predU1P[<-|N1x].
+  by rewrite /f !fctE /= expR0 addr0 subrr subr0 expR_ge0.
+move: x0; rewrite le_eqVlt => /predU1P[<-//|x0].
+have [c cx] : exists2 c, c \in `]x, 0%R[ & (f 0 - f x)%R = (f' c * (0 - x))%R.
+  apply: MVT => //.
+  apply: continuous_subspaceT => /= z.
+  apply: cvgB; first exact: continuous_expR.
+  by apply: cvgD => //; exact: cvg_cst.
+rewrite -[leRHS]/(f x) -subr_le0 sub0r /f' => ->; apply: mulr_le0_ge0.
+  rewrite /=subr_le0 add0r -expR0 ler_expR.
+  by move: cx; rewrite in_itv => /andP[_ /ltW].
+by rewrite lerNr oppr0 ltW.
+Qed.
+
+(* mu-book p. 66 *)
+Lemma analytical_argument_thm22 {R : realType} (delta : R) :
+  0 <= delta <= 1 ->
+  (- delta - (1 - delta) * ln (1 - delta) <= - delta ^+ 2 / 2)%R.
+Proof.
+move=> d01.
+pose f (x : R) := - x - (1 - x) * ln (1 - x) + x ^+2 / 2.
+pose f' (x : R) := ln (1 - x) + x.
+pose f'' (x : R) := - (1 - x)^-1 + 1.
+have f''01 (x : R) : 0 <= x <= 1 -> f'' x < 0.
+  admit.
+have f'0 : f' 0 = 0 by rewrite /f' subr0 ln1 addr0.
+have f'01 (x : R) : 0 <= x <= 1 -> f' x <= 0.
+  admit.
+have f0 : f 0 = 0 :> R.
+  by rewrite /f subr0 ln1 mulr0 expr0n mul0r subr0 addrC subrr.
+have f01 (x : R) : 0 <= x <= 1 -> f x <= 0.
+  admit.
+rewrite -subr_le0.
+rewrite mulNr opprK.
+exact: f01.
+Admitted.
+
+(* mu-book p. 65 *)
+Lemma analytical_argument_thm26 {R : realType} (delta : R) :
+  0 <= delta <= 1 ->
+  ((1 + delta) * ln (1 + delta) >= delta + delta^+2 / 3)%R.
+Proof.
+move=> d01.
+pose f x : R := x - (1 + x) * ln (1 + x) + x^+2 / 3.
+pose f' x : R := 1 - (1 + x) / (1 - x) - ln (1 + x) + (2 / 3) * x.
+have f'E x : f' x = - ln (1 + x) + (2 / 3) * x.
+   admit.
+pose f'' x : R := - (1 + x)^-1 + 2 / 3.
+have f''P1 (x : R) : 0 <= x < 1/2 -> f'' x < 0.
+  admit.
+have f''P2 x : x > 1/2 -> f'' x > 0.
+  admit.
+have f'0 : f' 0 = 0.
+  by rewrite /f' subr0 divr1 mulr0 addr0 ln1 subr0 subrr addr0.
+have f'1 : f' 1 < 0.
+  admit.
+have f'01 (x : R) : 0 <= x <= 1 -> f' x <= 0.
+  admit.
+have f0 : f 0 = 0.
+  by rewrite /f addr0 expr0n/= mul0r ln1 mulr0 subrr addr0.
+have f01 (x : R) : 0 <= x <= 1 -> f x <= 0.
+  admit.
+have := f01 _ d01.
+by rewrite /f addrAC subr_le0.
+Admitted.
+
+(* WIP *)
+Section independent_events.
+Context {R : realType} d {T : measurableType d}.
+Variable P : probability T R.
+Local Open Scope ereal_scope.
+
+(* def 2.3, independence of events *)
+(* TODO: rename to mutually_independent_events *)
+Definition mutually_independent (I : choiceType) (A : I -> set T) :=
+(*  (forall i, J i -> measurable (A i)) /\*)
+  forall J : {fset I},
+    P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i).
+
+End independent_events.
+
+(* independent class of events, klenke def 2.11, p.59 *)
+Section independent_class.
+Context {R : realType} d {T : measurableType d}.
+Variable P : probability T R.
+Local Open Scope ereal_scope.
+
+Definition independent_class (I : choiceType) (C : I -> set (set T)) :=
+  (forall i, C i `<=` @measurable _ T) /\
+  forall J : {fset I},
+    forall E : I -> set T,
+      (forall i : I, i \in J -> E i \in C i) ->
+        P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j).
+
+End independent_class.
+
+Section independent_RV.
+Context {R : realType} d (T : measurableType d).
+Variable P : probability T R.
+
+Definition generated_salgebra (X : {RV P >-> R}) : set (set T) :=
+  preimage_class setT X (@measurable _ R).
+
+Definition independent_RV (I : choiceType) (X : I -> {RV P >-> R}) :=
+  independent_class P (fun i : I => generated_salgebra (X i)).
+
+Definition independent_RV_tuple n (X : n.-tuple {RV P >-> R}) :=
+  independent_class P (fun i => generated_salgebra (X `_ i)).
+
+Lemma independent_RV_tuple_thead_prod_behead n (X : n.+1.-tuple {RV P >-> R}) :
+  independent_RV_tuple X ->
+  independent_RV_tuple [tuple thead X; (\prod_(j <- behead X) j)%R].
+Proof.
+move: X; elim: n => [X [h1 h2]|].
+  have -> : behead X = nil. admit.
+  rewrite big_nil.
+  rewrite /independent_RV_tuple/independent_class/=.
+  split.
+    case => //=.
+      by move: (h1 0); rewrite {1}(tuple_eta X).
+    case => //=.
+      rewrite /generated_salgebra /preimage_class.
+      admit.
+    case => /= [|_].
+      admit.
+    admit.
+  admit.
+(*rewrite /independent_RV_tuple/independent_class/= => [[h1 h2]].
+split.
+  admit.
+move=> J E h3.
+rewrite h2// => i iJ.
+have := h3 i iJ.
+move: iJ.
+case: i => [//|i _].*)
+Admitted.
+
+Lemma independent_RV_tuple_behead n (X : n.-tuple {RV P >-> R}) :
+  independent_RV_tuple X -> independent_RV_tuple [tuple of behead X].
+Proof.
+move: X; case: n => [X|n X].
+  by rewrite tuple0.
+rewrite /independent_RV_tuple/independent_class/=.
+move=> [iXm iX].
+split; first by move=> i; rewrite nth_behead; exact: iXm.
+move=> J E h.
+pose E' n := match n with
+               0 => setT
+             | S m => E m
+             end.
+have := (@iX (0 |` [fset i.+1 | i in J])%fset E').
+have ? : 0 \notin [fset i.+1 | i in J]%fset.
+  apply/negP.
+  move/imfsetP.
+  by case.
+rewrite big_fsetU1//=.
+rewrite setTI big_fsetU1//=.
+rewrite probability_setT mul1e.
+rewrite big_imfset/=; last first.
+  move=> x y _ _; exact: succn_inj.
+move=> ->; last first.
+  elim.
+    move=> _.
+    rewrite/generated_salgebra/preimage_class.
+    (* TODO: make lemma *)
+    rewrite inE/=.
+    exists setT => //.
+    by rewrite setTI preimage_setT.
+  rewrite /E' => l _ h1.
+  have := (h l).
+  rewrite /generated_salgebra.
+  rewrite nth_behead => -> //.
+  move: h1.
+  move/fset1UP => []//.
+  move/imfsetP.
+  case => k/= kJ.
+  by case => ->.
+rewrite big_imfset//=.
+move=> x y _ _; exact: succn_inj.
+Qed.
+
+End independent_RV.
+
 Section independent_product.
 Context {R : realType} d {T : measurableType d}.
 Variable P : probability T R.
@@ -566,52 +660,8 @@ Definition kwise_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >->
 this should be equivalent according to wikipedia https://en.wikipedia.org/wiki/Independence_(probability_theory)#For_real_valued_random_variables
 *)
 
-
-(* this seems to be provable like in https://www.cs.purdue.edu/homes/spa/courses/pg17/mu-book.pdf page 65 *)
-Lemma taylor_ln_le {R : realType} :
-  forall (delta : R), ((1 + delta) * ln (1 + delta) >= delta + delta^+2 / 3)%R.
-Admitted.
-
-Lemma expR_prod d (T : measurableType d) (R : realType) (P : probability T R)
-  (X : seq {RV P >-> R}) (f : {RV P >-> R} -> R) :
-  (\prod_(x <- X) expR (f x) = expR (\sum_(x <- X) f x))%R.
-Proof.
-elim: X => [|h t ih]; first by rewrite !big_nil expR0.
-by rewrite !big_cons ih expRD.
-Qed.
-
-(* TODO: move *)
-Lemma ln_div {R : realType} : {in Num.pos &, {morph ln (R:=R) : x y / (x / y)%R >-> (x - y)%R}}.
-Proof.
-by move=> x y; rewrite !posrE => x0 y0; rewrite lnM ?posrE ?invr_gt0// lnV ?posrE.
-Qed.
-
-Lemma norm_expR {R : realType} : normr \o expR = (expR : R -> R).
-Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.
-
-Lemma le01_expR_ge1Dx {R : realType} (x : R) : (-1 <= x <= 0 -> 1 + x <= expR x)%R.
-Proof.
-move=> /andP [N1x x0].
-pose f : R^o -> R := (expR \- (cst 1 \+ id))%R.
-rewrite -subr_ge0 (_ : 0%R = f 0%R); last by rewrite /f !fctE/= expR0 addr0 subrr.
-pose f' : R^o -> R := (expR \- (cst 0 \+ cst 1))%R.
-move: N1x; rewrite le_eqVlt => /predU1P[<-|N1x].
-  by rewrite /f !fctE /= expR0 addr0 subrr subr0 expR_ge0.
-move: x0; rewrite le_eqVlt => /predU1P[<-//|x0].
-have [c cx] : exists2 c, c \in `]x, 0%R[ & (f 0 - f x)%R = (f' c * (0 - x))%R.
-  apply: MVT => //.
-  admit. (* TODO(rei) *)
-rewrite -[leRHS]/(f x) -subr_le0 sub0r /f' => ->; apply: mulr_le0_ge0.
-  by rewrite /=subr_le0 add0r -expR0 ler_expR; move: cx; rewrite in_itv => /andP[_ /ltW].
-by rewrite lerNr oppr0 ltW.
-Admitted.
-
-Section bernoulli_trial.
-
-Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType) (P : probability T R).
-Variable p : {nonneg R}.
-Hypothesis p1 : (p%:num <= 1)%R.
+Section real_of_bool.
+Context {R : realType}.
 
 Definition real_of_bool (b : bool) : R := b%:R.
 
@@ -628,6 +678,14 @@ Proof.
 by apply/seteqP; split => [x|x ->]; case: x => //= /eqP/=; rewrite oner_eq0.
 Qed.
 
+End real_of_bool.
+
+Section bernoulli_trial.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+Variable p : {nonneg R}.
+Hypothesis p1 : (p%:num <= 1)%R.
+
 Definition bernoulli_RV (X : {RV P >-> R}) :=
   distribution P X = pushforward (bernoulli p%:num) measurable_fun_real_of_bool
   /\ range X = [set 0; 1]%R.
@@ -645,7 +703,7 @@ Qed.
 Lemma bernoulli_RV2 (X : {RV P >-> R}) : bernoulli_RV X ->
   P [set i | X i == 0%R] == (`1-(p%:num))%:E.
 Proof.
-move=> [[/(congr1 (fun f => f [set 0%:R]))]].
+move=> [/(congr1 (fun f => f [set 0%:R]))].
 rewrite /bernoulli/= /pushforward ifT; last exact/andP.
 rewrite real_of_bool0 fsbig_set1/= /distribution /= => <- _.
 apply/eqP; congr (P _).
@@ -668,11 +726,10 @@ rewrite unlock.
 transitivity (\int[P]_w `|X w|%:E).
   apply: eq_integral => t _.
   by rewrite ger0_norm// bernoulli_ge0.
-rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last first.
-  by move=> y //=.
+rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last 2 first.
   exact: measurableT_comp.
-rewrite bX.1.
-rewrite ge0_integral_pushforward/=; last 2 first.
+  by move=> y //=.
+rewrite bX.1 ge0_integral_pushforward/=; last 2 first.
   exact: measurableT_comp.
   by move=> /= r; rewrite lee_fin.
 rewrite integral_bernoulli//; last exact/andP.
@@ -746,7 +803,8 @@ rewrite -sum1_size natr_sum big_distrl/= sumEFin; congr EFin.
 by under [RHS]eq_bigr do rewrite mul1r.
 Qed.
 
-Lemma bernoulli_trial_ge0 n (X : n.-tuple {RV P >-> R}) : is_bernoulli_trial X ->
+Lemma bernoulli_trial_ge0 n (X : n.-tuple {RV P >-> R}) :
+  is_bernoulli_trial X ->
   (forall t, 0 <= bernoulli_trial X t)%R.
 Proof.
 move=> [bRV Xn] t.
@@ -777,9 +835,18 @@ apply: congr1.
 under eq_bigr => Xi XiX do rewrite (bernoulli_mmt_gen_fun _ (bX1 _ _))//=.*)
 Admitted.
 
+End bernoulli_trial.
+
+Section rajani.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+Variable p : {nonneg R}.
+Hypothesis p1 : (p%:num <= 1)%R.
+
+(* Rajani lem 2.3 *)
 Lemma lm23 n (X_ : n.-tuple {RV P >-> R}) (t : R) :
   (0 <= t)%R ->
-  is_bernoulli_trial X_ ->
+  is_bernoulli_trial p X_ ->
   let X := bernoulli_trial X_ : {RV P >-> R} in
   let mu := 'E_P[X] in
   mmt_gen_fun X t <= (expR (fine mu * (expR t - 1)))%:E.
@@ -788,7 +855,7 @@ rewrite /= => t0 bX.
 set X := bernoulli_trial X_.
 set mu := 'E_P[X].
 have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%:E.
-  rewrite -[LHS]fineK; last by rewrite (binomial_mmt_gen_fun _ bX).
+  rewrite -[LHS]fineK; last by rewrite (binomial_mmt_gen_fun p1 _ bX).
   congr EFin.
   rewrite /mmt_gen_fun.
   transitivity (fine 'E_P[expR \o t \o* (\sum_(i < n) tnth X_ i)%R]).
@@ -796,6 +863,7 @@ have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%
     apply/funext => x/=.
     congr expR.
     rewrite /X /bernoulli_trial /=.
+    rewrite big_tnth//.
     admit.
   transitivity (fine 'E_P[\prod_(i < n ) (expR \o t \o* (tnth X_ i))]).
     congr (fine 'E_P[ _ ]).
@@ -806,32 +874,34 @@ have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%
 under eq_big_seq => Xi XiX.
   have -> : @mmt_gen_fun _ _ _ P Xi t = (1 + p%:num * (expR t - 1))%:E.
     rewrite /mmt_gen_fun.
-    rewrite bernoulli_mmt_gen_fun//; last exact: bX.1.
+    rewrite (bernoulli_mmt_gen_fun p1)//; last exact: bX.1.
     apply: congr1.
     by rewrite mulrBr mulr1 addrCA.
   over.
 rewrite lee_fin /=.
-apply: (le_trans (@ler_prod _ _ _ _ _ (fun x => expR (p%:num * (expR t - 1)))%R _)).
+apply: (le_trans (@ler_prod _ _ _ _ _
+    (fun x => expR (p%:num * (expR t - 1)))%R _)).
   move=> Xi _.
   rewrite addr_ge0 ?mulr_ge0 ?subr_ge0 ?andTb//; last first.
-    rewrite -expR0 ler_expR//.
+    by rewrite -expR0 ler_expR.
   by rewrite expR_ge1Dx ?mulr_ge0// subr_ge0 -expR0 ler_expR.
 rewrite expR_prod -mulr_suml.
 move: t0; rewrite le_eqVlt => /predU1P[<-|t0].
   by rewrite expR0 subrr !mulr0.
-rewrite ler_expR ler_pmul2r; last first.
+rewrite ler_expR ler_pM2r; last first.
   by rewrite subr_gt0 -expR0 ltr_expR.
 rewrite /mu big_seq expectation_sum; last first.
-  move=> Xi XiX; apply: integrable_bernoulli; exact: bX.1.
+  move=> Xi XiX; apply: (integrable_bernoulli p1); exact: bX.1.
 rewrite big_seq -sum_fine.
-  by apply: ler_sum => Xi XiX; rewrite bernoulli_expectation //=; exact: bX.1.
-move=> Xi XiX. rewrite bernoulli_expectation //=; exact: bX.1.
+  apply: ler_sum => Xi XiX; rewrite (bernoulli_expectation p1) //=.
+   exact: bX.1.
+by move=> Xi XiX; rewrite (bernoulli_expectation p1) //=; exact: bX.1.
 Admitted.
 
 Lemma end_thm24 n (X_ : n.-tuple {RV P >-> R}) (t delta : R) :
-  is_bernoulli_trial X_ ->
+  is_bernoulli_trial p X_ ->
   (0 < delta)%R ->
-  let X := @bernoulli_trial X_ in
+  let X := bernoulli_trial X_ in
   let mu := 'E_P[X] in
   let t := ln (1 + delta) in
   (expR (expR t - 1) `^ fine mu)%:E *
@@ -843,24 +913,24 @@ rewrite -EFinM lee_fin -powRM ?expR_ge0// ge0_ler_powR ?nnegrE//.
 - by rewrite fine_ge0// expectation_ge0// => x; exact: (bernoulli_trial_ge0 bX).
 - 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//.
+- rewrite lnK ?posrE ?addr_gt0// addrAC subrr add0r ler_wpM2l ?expR_ge0//.
   by rewrite -powRN mulNr -mulrN expRM lnK// posrE addr_gt0.
 Qed.
 
-(* theorem 2.4 Rajani / thm 4.4.(2) mu-book *)
+(* Rajani thm 2.4 Rajani / mu-book thm 4.4.(2) *)
 Theorem thm24 n (X_ : n.-tuple {RV P >-> R}) (delta : R) :
-  is_bernoulli_trial X_ ->
+  is_bernoulli_trial p X_ ->
   (0 < delta)%R ->
-  let X := @bernoulli_trial X_ in
+  let X := bernoulli_trial X_ in
   let mu := 'E_P[X] in
   P [set i | X i >= (1 + delta) * fine mu]%R <=
-  ((expR delta / ((1 + delta) `^ (1 + delta))) `^ (fine mu))%:E.
+    ((expR delta / ((1 + delta) `^ (1 + delta))) `^ (fine mu))%:E.
 Proof.
 rewrite /= => bX delta0.
-set X := @bernoulli_trial X_.
+set X := bernoulli_trial X_.
 set mu := 'E_P[X].
 set t := ln (1 + delta).
-have t0 : (0 < t)%R by rewrite ln_gt0// ltr_addl.
+have t0 : (0 < t)%R by rewrite ln_gt0// ltrDl.
 apply: (le_trans (chernoff _ _ t0)).
 apply: (@le_trans _ _ ((expR (fine mu * (expR t - 1)))%:E *
                        (expR (- (t * ((1 + delta) * fine mu))))%:E)).
@@ -870,64 +940,73 @@ rewrite mulrC expRM -mulNr mulrA expRM.
 exact: (end_thm24 _ bX).
 Qed.
 
-(* theorem 2.5 *)
+(* Rajani thm 2.5 *)
 Theorem poisson_ineq n (X : n.-tuple {RV P >-> R}) (delta : R) :
-  is_bernoulli_trial X ->
-  let X' := @bernoulli_trial X in
+  is_bernoulli_trial p X ->
+  let X' := bernoulli_trial X in
   let mu := 'E_P[X'] in
   (0 < n)%nat ->
   (0 < delta < 1)%R ->
   P [set i | X' i >= (1 + delta) * fine mu]%R <=
-  (expR (- (fine mu * delta ^+ 2) / 3))%:E.
+    (expR (- (fine mu * delta ^+ 2) / 3))%:E.
 Proof.
-move=> bX X' mu n0 /andP[delta0 _].
-apply: (@le_trans _ _ (expR ((delta - (1 + delta) * ln (1 + delta)) * fine mu))%:E).
-  rewrite expRM expRB (mulrC _ (ln _)) expRM lnK; last rewrite posrE addr_gt0//.
-  apply: (thm24 bX) => //.
+move=> bX X' mu n0 /andP[delta0 delta1].
+apply: (@le_trans _ _
+    (expR ((delta - (1 + delta) * ln (1 + delta)) * fine mu))%:E).
+  rewrite expRM expRB (mulrC _ (ln _)) expRM lnK; last by rewrite posrE addr_gt0.
+  exact: (thm24 bX).
 apply: (@le_trans _ _ (expR ((delta - (delta + delta ^+ 2 / 3)) * fine mu))%:E).
   rewrite lee_fin ler_expR ler_wpM2r//.
-    by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX).
-  rewrite ler_sub//.
-  exact: taylor_ln_le.
+    rewrite fine_ge0//; apply: expectation_ge0 => t.
+    exact: (bernoulli_trial_ge0 bX).
+  by rewrite lerB// analytical_argument_thm26// (ltW delta0) (ltW delta1).
 rewrite le_eqVlt; apply/orP; left; apply/eqP; congr (expR _)%:E.
 by rewrite opprD addrA subrr add0r mulrC mulrN mulNr mulrA.
 Qed.
 
 (* Rajani thm 2.6 / mu-book thm 4.5.(2) *)
 Theorem thm26 n (X : n.-tuple {RV P >-> R}) (delta : R) :
-  is_bernoulli_trial X -> (0 < delta < 1)%R ->
-  let X' := @bernoulli_trial X : {RV P >-> R} in
+  is_bernoulli_trial p X -> (0 < delta < 1)%R ->
+  let X' : {RV P >-> R} := bernoulli_trial X  in
   let mu := 'E_P[X'] in
-  P [set i | X' i <= (1 - delta) * fine mu]%R <= (expR (-(fine mu * delta ^+ 2) / 2)%R)%:E.
+  P [set i | X' i <= (1 - delta) * fine mu]%R <=
+    (expR (-(fine mu * delta ^+ 2) / 2)%R)%:E.
 Proof.
 move=> bX /andP[delta0 delta1] /=.
-set X' := @bernoulli_trial X : {RV P >-> R}.
+set X' := bernoulli_trial X : {RV P >-> R}.
 set mu := 'E_P[X'].
-apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine mu))%:E)).
+apply: (@le_trans _ _
+    (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine mu))%:E)).
   (* using Markov's inequality somewhere, see mu's book page 66 *)
   have H1 t : (t < 0)%R ->
-    P [set i | (X' i <= (1 - delta) * fine mu)%R] = P [set i | `|(expR \o t \o* X') i|%:E >= (expR (t * (1 - delta) * fine mu))%:E].
+      P [set i | (X' i <= (1 - delta) * fine mu)%R] =
+      P [set i | `|(expR \o t \o* X') i|%:E >=
+                 (expR (t * (1 - delta) * fine mu))%:E].
     move=> t0; apply: congr1; apply: eq_set => x /=.
     rewrite lee_fin ger0_norm ?expR_ge0// ler_expR (mulrC _ t) -mulrA.
-    by rewrite -[in RHS]ler_ndivr_mull// mulrA mulVf ?lt_eqF// mul1r.
+    by rewrite -[in RHS]ler_ndivrMl// mulrA mulVf ?lt_eqF// mul1r.
   set t := ln (1 - delta).
   have ln1delta : (t < 0)%R.
     (* TODO: lacking a lemma here *)
     rewrite -oppr0 ltrNr -lnV ?posrE ?subr_gt0// ln_gt0//.
-    by rewrite invf_gt1// ?subr_gt0// ltr_subl_addr ltr_addl.
+    by rewrite invf_gt1// ?subr_gt0// ltrBlDr ltrDl.
   have {H1}-> := H1 _ ln1delta.
-  apply: (@le_trans _ _ (((fine 'E_P[normr \o expR \o t \o* X']) / (expR (t * (1 - delta) * fine mu))))%:E).
+  apply: (@le_trans _ _
+      ((fine 'E_P[normr \o expR \o t \o* X']) /
+       (expR (t * (1 - delta) * fine mu)))%:E).
     rewrite EFinM lee_pdivl_mulr ?expR_gt0// muleC fineK.
-    apply: (@markov _ _ _ P (expR \o t \o* X' : {RV P >-> R}) id (expR (t * (1 - delta) * fine mu))%R _ _ _ _) => //.
+    apply: (@markov _ _ _ P (expR \o t \o* X' : {RV P >-> R}) id
+       (expR (t * (1 - delta) * fine mu))%R _ _ _ _) => //.
     - exact: expR_gt0.
     - rewrite norm_expR.
       have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun 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).
+      by rewrite (binomial_mmt_gen_fun p1 _ bX).
+  apply: (@le_trans _ _ ((expR ((expR t - 1) * fine mu)) /
+                         (expR (t * (1 - delta) * fine mu)))%:E).
     rewrite norm_expR lee_fin ler_wpM2r ?invr_ge0 ?expR_ge0//.
     have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by [].
-    rewrite (binomial_mmt_gen_fun _ bX)/=.
-    rewrite /mu /X' (expectation_bernoulli_trial bX)/=.
+    rewrite (binomial_mmt_gen_fun p1 _ bX)/=.
+    rewrite /mu /X' (expectation_bernoulli_trial p1 bX)/=.
     rewrite !lnK ?posrE ?subr_gt0//.
     rewrite expRM powRrM powRAC.
     rewrite ge0_ler_powR ?ler0n// ?nnegrE ?powR_ge0//.
@@ -935,8 +1014,8 @@ apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine
     rewrite addrAC subrr sub0r -expRM.
     rewrite addrCA -{2}(mulr1 (p%:num)) -mulrBr addrAC subrr sub0r mulrC mulNr.
     apply: le01_expR_ge1Dx.
-    rewrite ler_oppl opprK mulr_ile1//=; [|exact: ltW..].
-    by rewrite ler_oppl oppr0 mulr_ge0// ltW.
+    rewrite lerNl opprK mulr_ile1//=; [|exact: ltW..].
+    by rewrite lerNl oppr0 mulr_ge0// ltW.
   rewrite !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//.
@@ -950,27 +1029,27 @@ rewrite -mulrN -mulrA [in leRHS]mulrC expRM ge0_ler_powR// ?nnegrE.
   rewrite expRK// ln_div ?posrE ?expR_gt0 ?powR_gt0 ?subr_gt0//.
   rewrite expRK//.
   rewrite /powR (*TODO: lemma ln of powR*) gt_eqF ?subr_gt0// expRK.
-  (* requires analytical argument: see p.66 of mu's book *)
-  admit. (* TODO(rei) *)
-Admitted.
+  apply: analytical_argument_thm22.
+  by rewrite (ltW delta0) (ltW delta1).
+Qed.
 
-(* Rajani -> corollary 2.7 / mu-book -> corollary 4.7 *)
+(* Rajani corollary 2.7 / mu-book -> corollary 4.6 *)
 Corollary cor27 n (X : n.-tuple {RV P >-> R}) (delta : R) :
-  is_bernoulli_trial X -> (0 < delta < 1)%R ->
+  is_bernoulli_trial p X -> (0 < delta < 1)%R ->
   (0 < n)%nat ->
   (0 < p%:num)%R ->
-  let X' := @bernoulli_trial X in
+  let X' := bernoulli_trial X in
   let mu := 'E_P[X'] in
   P [set i | `|X' i - fine mu | >=  delta * fine mu]%R <=
-  (expR (- (fine mu * delta ^+ 2) / 3)%R *+ 2)%:E.
+    (expR (- (fine mu * delta ^+ 2) / 3)%R *+ 2)%:E.
 Proof.
 move=> bX /andP[d0 d1] n0 p0 /=.
-set X' := @bernoulli_trial X.
+set X' := bernoulli_trial X.
 set mu := 'E_P[X'].
 under eq_set => x.
   rewrite ler_normr.
-  rewrite ler_subr_addl opprD opprK -{1}(mul1r (fine mu)) -mulrDl.
-  rewrite -ler_sub_addr -(ler_opp2 (- _)%R) opprK opprB.
+  rewrite lerBrDl opprD opprK -{1}(mul1r (fine mu)) -mulrDl.
+  rewrite -lerBDr -(lerN2 (- _)%R) opprK opprB.
   rewrite -{2}(mul1r (fine mu)) -mulrBl.
   rewrite -!lee_fin.
   over.
@@ -988,13 +1067,14 @@ rewrite measureU; last 3 first.
   rewrite -ltNge.
   apply: (@lt_le_trans _ _ _ _ _ _ X0).
   rewrite !EFinM.
-  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//=.
+  rewrite lte_pmul2r//; first by rewrite lte_fin ltrD2l gt0_cp.
+  rewrite fineK /mu/X' (expectation_bernoulli_trial p1 bX)// lte_fin.
+  by rewrite mulr_gt0 ?ltr0n.
+rewrite mulr2n EFinD leeD//=.
 - by apply: (poisson_ineq bX); rewrite //d0 d1.
 - apply: (le_trans (@thm26 _ _ delta bX _)); first by rewrite d0 d1.
   rewrite lee_fin ler_expR !mulNr lerN2.
-  rewrite ler_pM//; last by rewrite lef_pinv ?posrE ?ler_nat.
+  rewrite ler_pM//; last by rewrite lef_pV2 ?posrE ?ler_nat.
   rewrite mulr_ge0 ?fine_ge0 ?sqr_ge0//.
   rewrite /mu unlock /expectation integral_ge0// => x _.
   by rewrite /X' lee_fin; apply: (bernoulli_trial_ge0 bX).
@@ -1005,7 +1085,7 @@ Theorem sampling n (X : n.-tuple {RV P >-> R}) (theta delta : R) :
   let X_sum := bernoulli_trial X in
   let X' x := (X_sum x) / n%:R in
   (0 < p%:num)%R ->
-  is_bernoulli_trial X ->
+  is_bernoulli_trial p X ->
   (0 < delta <= 1)%R -> (0 < theta < p%:num)%R -> (0 < n)%nat ->
   (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R ->
   P [set i | `| X' i - p%:num | <= theta]%R >= 1 - delta%:E.
@@ -1016,12 +1096,12 @@ have E_X_sum: 'E_P[X_sum] = (p%:num * n%:R)%:E.
     by move=> Xi XiX; exact: integrable_bernoulli (bX.1 Xi XiX).
   rewrite big_seq.
   under eq_bigr.
-    move=> Xi XiX; rewrite (bernoulli_expectation (bX.1 _ XiX)); over.
+    move=> Xi XiX; rewrite (bernoulli_expectation p1 (bX.1 _ XiX)); over.
   rewrite /= -[in RHS](size_tuple X).
   by rewrite -sum1_size natr_sum big_distrr/= sumEFin mulr1 -big_seq.
 set epsilon := theta / p%:num.
 have epsilon01 : (0 < epsilon < 1)%R.
-  by rewrite /epsilon ?ltr_pdivr_mulr ?divr_gt0 ?mul1r.
+  by rewrite /epsilon ?ltr_pdivrMr ?divr_gt0 ?mul1r.
 have thetaE : theta = (epsilon * p%:num)%R.
   by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF.
 have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <=
@@ -1029,10 +1109,10 @@ have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <=
   rewrite [X in P X <= _](_ : _ =
       [set i | `| X_sum i - p%:num * n%:R | >= epsilon * p%:num * n%:R]%R); last first.
     apply/seteqP; split => [t|t]/=.
-      move/(@ler_wpmul2r _ n%:R (ler0n _ _)) => /le_trans; apply.
+      move/(@ler_wpM2r _ n%:R (ler0n _ _)) => /le_trans; apply.
       rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R)// -normrM mulrBl.
       by rewrite -mulrA mulVf ?mulr1// gt_eqF ?ltr0n.
-    move/(@ler_wpmul2r _ n%:R^-1); rewrite invr_ge0// ler0n => /(_ erefl).
+    move/(@ler_wpM2r _ n%:R^-1); rewrite invr_ge0// ler0n => /(_ erefl).
     rewrite -(mulrA _ _ n%:R^-1) divff ?mulr1 ?gt_eqF ?ltr0n//.
     move=> /le_trans; apply.
     rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R^-1)// -normrM mulrBl.
@@ -1044,14 +1124,14 @@ have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <=
 have step2 : P [set i | `| X' i - p%:num | >= theta]%R <=
     ((expR (- (n%:R * theta ^+ 2) / 3)) *+ 2)%:E.
   rewrite thetaE; move/le_trans : step1; apply.
-  rewrite lee_fin ler_wmuln2r// ler_expR mulNr ler_oppl mulNr opprK.
+  rewrite lee_fin ler_wMn2r// ler_expR mulNr lerNl mulNr opprK.
   rewrite -2![leRHS]mulrA.
   rewrite [leRHS]mulrCA.
   rewrite -[leLHS]mulrA.
   rewrite ler_wpM2l//.
-  rewrite (mulrC epsilon) exprMn -mulrA ler_wpmul2r//.
+  rewrite (mulrC epsilon) exprMn -mulrA ler_wpM2r//.
     by rewrite divr_ge0// sqr_ge0.
-  by rewrite expr2 ler_pimull.
+  by rewrite expr2 ler_piMl.
 suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) theta)%R].
   rewrite [X in P X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p%:num| < theta)%R]); last first.
     apply/seteqP; split => [t|t]/=.
@@ -1075,12 +1155,12 @@ suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) th
   by move=> t/= /ltW.
 (* NB: last step in the pdf *)
 apply: (le_trans step2).
-rewrite lee_fin -(mulr_natr _ 2) -ler_pdivl_mulr//.
+rewrite lee_fin -(mulr_natr _ 2) -ler_pdivlMr//.
 rewrite -(@lnK _ (delta / 2)); last by rewrite posrE divr_gt0.
-rewrite ler_expR mulNr ler_oppl -lnV; last by rewrite posrE divr_gt0.
-rewrite invf_div ler_pdivl_mulr// mulrC.
+rewrite ler_expR mulNr lerNl -lnV; last by rewrite posrE divr_gt0.
+rewrite invf_div ler_pdivlMr// mulrC.
 rewrite -ler_pdivrMr; last by rewrite exprn_gt0.
 by rewrite mulrAC.
 Qed.
 
-End bernoulli_trial.
+End rajani.