From 034959646450d139964babadf3cda9e7453a122f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 27 May 2024 16:12:18 +0900
Subject: [PATCH] copy-pasting the previous Bernoulli PR by Alessandro

---
 theories/probability.v | 1132 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 1125 insertions(+), 7 deletions(-)

diff --git a/theories/probability.v b/theories/probability.v
index 1d69b232c..1b7e500e7 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -1369,10 +1369,1128 @@ Qed.
 
 End uniform_probability.
 
-(* TODO: formalize https://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf *)
-Theorem sampling p (X : {RV P >-> R}^nat) (n : nat) (theta delta : R) :
-  let X_sum x := \sum_(i < n) (X i x)%:E in
-  let X' x := X_sum x * (n%:R)^-1%:E in
-  (forall i, bernoulli p (X i)) ->
-  (n%:R > 3 / (theta ^+ 2) * ln (2 / delta))%R ->
-  P [set i | `| X' i - p%:E | < theta%:E] >= 1 - delta%:E.
+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//.
+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 _)).
+Qed.
+
+End probability.
+
+Notation "\prod_ ( i <- r | P ) F" :=
+  (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i <- r ) F" :=
+  (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n | P ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i | P ) F" :=
+  (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope.
+Notation "\prod_ i F" :=
+  (\big[*%E/1%:E]_i F%E) : ereal_scope.
+Notation "\prod_ ( i : t | P ) F" :=
+  (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i : t ) F" :=
+  (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i < n | P ) F" :=
+  (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i < n ) F" :=
+  (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A | P ) F" :=
+  (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A ) F" :=
+  (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope.
+
+(* independent class of events, klenke def 2.11, p.59 *)
+Section independent_class.
+Context {d : measure_display} {T : measurableType d} {R : realType}
+        {P : probability T R}.
+Variable (I : choiceType) (E : I -> set (set T)).
+Hypothesis mE : forall i, E i `<=` measurable.
+Local Open Scope ereal_scope.
+
+Definition independent_class :=
+  forall J : {fset I},
+    forall e : I -> set T, (forall i, (E i) (e i)) ->
+      P (\big[setI/setT]_(i <- J) e i) = (\prod_(i <- J) P (e i))%E.
+
+End independent_class.
+
+Section independent_events.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+Local Open Scope ereal_scope.
+
+Definition mutually_independent (I : choiceType) (A : set I) (E : I -> set T) :=
+  (forall i, A i -> measurable (E i)) /\
+  forall B : {fset I}, [set` B] `<=` A ->
+    P (\bigcap_(i in [set` B]) E i) = \prod_(i <- B) P (E i).
+
+Lemma sub_mutually_independent (I : choiceType) (A B : set I) (E : I -> set T) :
+  A `<=` B -> mutually_independent B E -> mutually_independent A E.
+Proof.
+by move=> AB [mE h]; split=> [i /AB/mE//|C CA]; apply: h; apply: subset_trans AB.
+Qed.
+
+Definition kwise_independent (I : choiceType) (A : set I) (E : I -> set T) k :=
+  (forall i, A i -> measurable (E i)) /\
+  forall B : {fset I}, [set` B] `<=` A -> (#|` B | <= k)%nat ->
+    P (\bigcap_(i in [set` B]) E i) = \prod_(i <- B) P (E i).
+
+Lemma sub_kwise_independent (I : choiceType) (A B : set I) (E : I -> set T) k :
+  A `<=` B -> kwise_independent B E k -> kwise_independent A E k.
+Proof.
+by move=> AB [mE h]; split=> [i /AB/mE//|C CA]; apply: h; apply: subset_trans AB.
+Qed.
+
+Lemma mutual_indep_is_kwise_indep (I : choiceType) (A : set I) (E : I -> set T) k :
+  mutually_independent A E -> kwise_independent A E k.
+Proof.
+rewrite/mutually_independent/kwise_independent.
+move=> [mE miE]; split=> // B BleA _.
+exact: miE.
+Qed.
+
+Lemma nwise_indep_is_mutual_indep (I : choiceType) (A : {fset I}) (E : I -> set T) n :
+  #|` A | = n -> kwise_independent [set` A] E n -> mutually_independent [set` A] E.
+Proof.
+rewrite/mutually_independent/kwise_independent.
+move=> nA [mE miE]; split=> // B BleA.
+apply: miE => //; rewrite -nA fsubset_leq_card//.
+by apply/fsubsetP => x xB; exact: (BleA x).
+Qed.
+
+Lemma mutually_independent_weak (I : choiceType) (E : I -> set T) (B : set I) :
+  (forall b, ~ B b -> E b = setT) ->
+  mutually_independent [set: I] E <->
+  mutually_independent B E.
+Proof.
+move=> BE; split; first exact: sub_mutually_independent.
+move=> [mE h]; split=> [i _|C _].
+  by have [Bi|Bi] := pselect (B i); [exact: mE|rewrite BE].
+have [CB|CB] := pselect ([set` C] `<=` B); first by rewrite h.
+rewrite -(setIT [set` C]) -(setUv B) setIUr bigcap_setU.
+rewrite (@bigcapT _ _ (_ `&` ~` _)) ?setIT//; last by move=> i [_ /BE].
+have [D CBD] : exists D : {fset I}, [set` C] `&` B = [set` D].
+  exists (fset_set ([set` C] `&` B)).
+  by rewrite fset_setK//; exact: finite_setIl.
+rewrite CBD h; last first.
+  rewrite -CBD; exact: subIsetr.
+rewrite [RHS]fsbig_seq//= [RHS](fsbigID B)//=.
+rewrite [X in _ * X](_ : _ = 1) ?mule1; last first.
+  by rewrite fsbig1// => m [_ /BE] ->; rewrite probability_setT.
+by rewrite CBD -fsbig_seq.
+Qed.
+
+Lemma kwise_independent_weak (I : choiceType) (E : I -> set T) (B : set I) k :
+  (forall b, ~ B b -> E b = setT) ->
+  kwise_independent [set: I] E k <->
+  kwise_independent B E k.
+Proof.
+move=> BE; split; first exact: sub_kwise_independent.
+move=> [mE h]; split=> [i _|C _ Ck].
+  by have [Bi|Bi] := pselect (B i); [exact: mE|rewrite BE].
+have [CB|CB] := pselect ([set` C] `<=` B); first by rewrite h.
+rewrite -(setIT [set` C]) -(setUv B) setIUr bigcap_setU.
+rewrite (@bigcapT _ _ (_ `&` ~` _)) ?setIT//; last by move=> i [_ /BE].
+have [D CBD] : exists D : {fset I}, [set` C] `&` B = [set` D].
+  exists (fset_set ([set` C] `&` B)).
+  by rewrite fset_setK//; exact: finite_setIl.
+rewrite CBD h; last 2 first.
+  - rewrite -CBD; exact: subIsetr.
+  - rewrite (leq_trans _ Ck)// fsubset_leq_card// -(set_fsetK D) -(set_fsetK C).
+    by rewrite -fset_set_sub// -CBD; exact: subIsetl.
+rewrite [RHS]fsbig_seq//= [RHS](fsbigID B)//=.
+rewrite [X in _ * X](_ : _ = 1) ?mule1; last first.
+  by rewrite fsbig1// => m [_ /BE] ->; rewrite probability_setT.
+by rewrite CBD -fsbig_seq.
+Qed.
+
+Lemma kwise_independent_weak01 E1 E2 :
+  kwise_independent [set: nat] (bigcap2 E1 E2) 2%N <->
+  kwise_independent [set 0%N; 1%N] (bigcap2 E1 E2) 2%N.
+Proof.
+apply: kwise_independent_weak.
+by move=> n /= /not_orP[/eqP /negbTE -> /eqP /negbTE ->].
+Qed.
+
+Lemma mutually_independent_weak' (I : choiceType) (E : I -> set T) (B : set I) :
+  (forall b, ~ B b -> E b = setT) ->
+  mutually_independent [set: I] E <->
+  mutually_independent B E.
+Proof.
+move=> BE; split; first exact: sub_mutually_independent.
+move=> [mE h]; split=> [i _|C CI].
+  by have [Bi|Bi] := pselect (B i); [exact: mE|rewrite BE].
+have [CB|CB] := pselect ([set` C] `<=` B); first by rewrite h.
+rewrite -(setIT [set` C]) -(setUv B) setIUr bigcap_setU.
+rewrite (@bigcapT _ _ (_ `&` ~` _)) ?setIT//; last by move=> i [_ /BE].
+have [D CBD] : exists D : {fset I}, [set` C] `&` B = [set` D].
+  exists (fset_set ([set` C] `&` B)).
+  by rewrite fset_setK//; exact: finite_setIl.
+rewrite CBD h; last first.
+  - rewrite -CBD; exact: subIsetr.
+rewrite [RHS]fsbig_seq//= [RHS](fsbigID B)//=.
+rewrite [X in _ * X](_ : _ = 1) ?mule1; last first.
+  by rewrite fsbig1// => m [_ /BE] ->; rewrite probability_setT.
+by rewrite CBD -fsbig_seq.
+Qed.
+
+Definition pairwise_independent E1 E2 :=
+  kwise_independent [set 0; 1]%N (bigcap2 E1 E2) 2.
+
+Lemma pairwise_independentM_old (E1 E2 : set T) :
+  pairwise_independent E1 E2 <->
+  [/\ d.-measurable E1, d.-measurable E2 & P (E1 `&` E2) = P E1 * P E2].
+Proof.
+split.
+- move=> [mE1E2 /(_ [fset 0%N; 1%N]%fset)].
+  rewrite bigcap_fset !big_fsetU1 ?inE//= !big_seq_fset1/= => ->; last 2 first.
+  + by rewrite set_fsetU !set_fset1; exact: subset_refl.
+  + rewrite cardfs2//.
+  split => //.
+  + by apply: (mE1E2 0%N) => /=; left.
+  + by apply: (mE1E2 1%N) => /=; right.
+- move=> [mE1 mE2 E1E2M].
+  split => //=.
+  + by move=> [| [| [|]]]//=.
+  + move=> B _; have [B0|B0] := boolP (0%N \in B); last first.
+      have [B1|B1] := boolP (1%N \in B); last first.
+        rewrite big1_fset; last first.
+          move=> k kB _; rewrite /bigcap2.
+          move: kB B0; case: ifPn => [/eqP -> ->//|k0 kB B0].
+          move: kB B1; case: ifPn => [/eqP -> ->//|_ _ _].
+          by rewrite probability_setT.
+        rewrite bigcapT ?probability_setT// => k/= kB.
+        move: kB B0 B1; case: ifPn => [/eqP -> ->//|k0].
+        by case: ifPn => [/eqP -> ->|].
+      rewrite (bigcap_setD1 1%N _ [set` B])//=.
+      rewrite bigcapT ?setIT; last first.
+        move=> k [/= kB /eqP /negbTE ->].
+        by move: kB B0; case: ifPn => [/eqP -> ->|].
+      rewrite (big_fsetD1 1%N)//= big1_fset ?mule1// => k.
+      rewrite !inE => /andP[/negbTE -> kB] _.
+      move: kB B0; case: ifPn => [/eqP -> ->//|k0 kB B0].
+      by rewrite probability_setT.
+    rewrite (bigcap_setD1 0%N _ [set` B])//.
+    have [B1|B1] := boolP (1%N \in B); last first.
+      rewrite bigcapT ?setIT; last first.
+        move=> k [/= kB /eqP /negbTE ->].
+        by move: kB B1; case: ifPn => [/eqP -> ->|].
+      rewrite (big_fsetD1 0%N)//= big1_fset ?mule1// => k.
+      rewrite !inE => /andP[/negbTE -> kB] _.
+      move: kB B1; case: ifPn => [/eqP -> ->//|k1 kB B1].
+      by rewrite probability_setT.
+    rewrite (bigcap_setD1 1%N _ ([set` B] `\ 0%N))// bigcapT ?setIT; last first.
+      by move=> n/= [[nB]/eqP/negbTE -> /eqP/negbTE ->].
+    rewrite E1E2M (big_fsetD1 0%N)//= (big_fsetD1 1%N)/=; last by rewrite !inE B1.
+    rewrite big1_fset ?mule1//= => k.
+    rewrite !inE => -/and3P[/negbTE -> /negbTE -> kB] _;
+    by rewrite probability_setT.
+Qed.
+
+Lemma pairwise_independentM (E1 E2 : set T) :
+  pairwise_independent E1 E2 <->
+  [/\ d.-measurable E1, d.-measurable E2 & P (E1 `&` E2) = P E1 * P E2].
+Proof.
+split.
+- move=> [mE1E2 /(_ [fset 0%N; 1%N]%fset)].
+  rewrite bigcap_fset !big_fsetU1 ?inE//= !big_seq_fset1/= => ->; last 2 first.
+  + by rewrite set_fsetU !set_fset1; exact: subset_refl.
+  + by rewrite cardfs2.
+  split => //.
+  + by apply: (mE1E2 0%N) => /=; left.
+  + by apply: (mE1E2 1%N) => /=; right.
+- move=> [mE1 mE2 E1E2M].
+  rewrite /pairwise_independent.
+  split.
+  + by move=> [| [| [|]]]//=.
+  + move=> B B01 B2.
+    have [B_set0|B_set0|B_set1|B_set01] := subset_set2 B01.
+    * rewrite B_set0.
+      move: B_set0 => /eqP; rewrite set_fset_eq0 => /eqP ->.
+      by rewrite big_nil bigcap_set0 probability_setT.
+    * rewrite B_set0 bigcap_set1 /=.
+      by rewrite fsbig_seq//= B_set0 fsbig_set1/=.
+    * rewrite B_set1 bigcap_set1 /=.
+      by rewrite fsbig_seq//= B_set1 fsbig_set1/=.
+    * rewrite B_set01 bigcap_setU1 bigcap_set1/=.
+      rewrite fsbig_seq//= B_set01.
+      rewrite fsbigU//=; last first.
+        by move=> n [/= ->].
+      by rewrite !fsbig_set1//=.
+Qed.
+
+Lemma pairwise_independent_setC (E1 E2 : set T) :
+  pairwise_independent E1 E2 -> pairwise_independent E1 (~` E2).
+Proof.
+rewrite/pairwise_independent.
+move/pairwise_independentM=> [mE1 mE2 h].
+apply/pairwise_independentM; split=> //.
+- exact: measurableC.
+- rewrite -setDE measureD//; last first.
+    exact: (le_lt_trans (probability_le1 P mE1) (ltry _)).
+  rewrite probability_setC// muleBr// ?mule1 -?h//.
+  exact: probability_fin_num.
+Qed.
+
+Lemma pairwise_independentC (E1 E2 : set T) :
+  pairwise_independent E1 E2 -> pairwise_independent E2 E1.
+Proof.
+rewrite/pairwise_independent/kwise_independent; move=> [mE1E2 /(_ [fset 0%N; 1%N]%fset)].
+rewrite bigcap_fset !big_fsetU1 ?inE//= !big_seq_fset1/= => h.
+split.
+- case=> [_|[_|]]//=.
+  + by apply: (mE1E2 1%N) => /=; right.
+  + by apply: (mE1E2 0%N) => /=; left.
+- move=> B B01 B2.
+  have [B_set0|B_set0|B_set1|B_set01] := subset_set2 B01.
+  + rewrite B_set0.
+    move: B_set0 => /eqP; rewrite set_fset_eq0 => /eqP ->.
+    by rewrite big_nil bigcap_set0 probability_setT.
+  + rewrite B_set0 bigcap_set1 /=.
+    by rewrite fsbig_seq//= B_set0 fsbig_set1/=.
+  + rewrite B_set1 bigcap_set1 /=.
+    by rewrite fsbig_seq//= B_set1 fsbig_set1/=.
+  + rewrite B_set01 bigcap_setU1 bigcap_set1/=.
+    rewrite fsbig_seq//= B_set01.
+    rewrite fsbigU//=; last first.
+    by move=> n [/= ->].
+    rewrite !fsbig_set1//= muleC setIC.
+    apply: h.
+    * by rewrite set_fsetU !set_fset1; exact: subset_refl.
+    * by rewrite cardfs2.
+Qed.
+(* ale: maybe interesting is thm 8.3 and exercise 8.6 from shoup/ntb at this point *)
+
+End independent_events.
+
+Section conditional_probability.
+Context d (T : measurableType d) (R : realType).
+Local Open Scope ereal_scope.
+
+Definition conditional_probability (P : probability T R) E1 E2 := (fine (P (E1 `&` E2)) / fine (P E2))%:E.
+Local Notation "' P [ E1 | E2 ]" := (conditional_probability P E1 E2).
+
+Lemma conditional_independence (P : probability T R) E1 E2 :
+  P E2 != 0 -> pairwise_independent P E1 E2 -> 'P [ E1 | E2 ] = P E1.
+Proof.
+move=> PE2ne0 iE12.
+have /= mE1 := (iE12.1 0%N).
+have /= mE2 := (iE12.1 1%N).
+rewrite/conditional_probability.
+have [_ _ ->] := (pairwise_independentM _ _ _).1 iE12.
+rewrite fineM ?probability_fin_num//; [|apply: mE1; left=>//|apply: mE2; right=>//].
+rewrite -mulrA mulfV ?mulr1 ?fineK// ?probability_fin_num//; first by apply: mE1; left.
+by rewrite fine_eq0// probability_fin_num//; apply: mE2; right.
+Qed.
+
+(* TODO (klenke thm 8.4): if P B > 0 then 'P[.|B] is a probability measure *)
+
+Lemma conditional_independent_is_pairwise_independent (P : probability T R) E1 E2 :
+  d.-measurable E1 -> d.-measurable E2 ->
+  P E2 != 0 ->
+    'P[E1 | E2] = P E1 -> pairwise_independent P E1 E2.
+Proof.
+rewrite /conditional_probability/pairwise_independent=> mE1 mE2 pE20 pE1E2.
+split.
+- by case=> [|[|]]//=.
+- move=> B B01 B2; have [B_set0|B_set0|B_set1|B_set01] := subset_set2 B01.
+  + rewrite B_set0.
+    move: B_set0 => /eqP; rewrite set_fset_eq0 => /eqP ->.
+    by rewrite big_nil bigcap_set0 probability_setT.
+  + rewrite B_set0 bigcap_set1 /=.
+    by rewrite fsbig_seq//= B_set0 fsbig_set1/=.
+  + rewrite B_set1 bigcap_set1 /=.
+    by rewrite fsbig_seq//= B_set1 fsbig_set1/=.
+  + rewrite B_set01 bigcap_setU1 bigcap_set1/=.
+    rewrite fsbig_seq//= B_set01.
+    rewrite fsbigU//=; last first.
+    by move=> n [/= ->].
+    rewrite !fsbig_set1//= -pE1E2 -{2}(@fineK _ (P E2)).
+    rewrite -EFinM -mulrA mulVf ?mulr1 ?fine_eq0// ?fineK//.
+    all: by apply: probability_fin_num => //; apply: measurableI.
+Qed.
+
+Lemma conditional_independentC (P : probability T R) E1 E2 :
+  d.-measurable E1 -> d.-measurable E2 ->
+  P E1 != 0 -> P E2 != 0 ->
+    reflect ('P[E1 | E2] == P E1) ('P[E2 | E1] == P E2).
+Proof.
+move=> mE1 mE2 pE10 pE20.
+apply/(iffP idP)=>/eqP.
++ move/(@conditional_independent_is_pairwise_independent _ _ _ mE2 mE1 pE10).
+  move/pairwise_independentC.
+  by move/(conditional_independence pE20)/eqP.
++ move/(@conditional_independent_is_pairwise_independent _ _ _ mE1 mE2 pE20).
+  move/pairwise_independentC.
+  by move/(conditional_independence pE10)/eqP.
+Qed.
+
+(* Lemma summation (I : choiceType) (A : {fset I}) E F (P : probability T R) : *)
+(*   (* the sets are disjoint *) *)
+(*   P (\bigcap_(i in [set` A]) F i) = 1 -> P E = \prod_(i <- A) ('P [E | F i] * P (F i)). *)
+(* Proof. *)
+(* move=> pF1. *)
+
+Lemma bayes (P : probability T R) E F :
+  d.-measurable E -> d.-measurable F ->
+  'P[ E | F ] = ((fine ('P[F | E] * P E)) / (fine (P F)))%:E.
+Proof.
+rewrite /conditional_probability => mE mF.
+have [PE0|PE0] := eqVneq (P E) 0.
+  have -> : P (E `&` F) = 0.
+    by apply/eqP; rewrite eq_le -{1}PE0 (@measureIl _ _ _ P E F mE mF)/= measure_ge0.
+  by rewrite PE0 fine0 invr0 mulr0 mule0 mul0r.
+by rewrite -{2}(@fineK _ (P E)) -?EFinM -?(mulrA (fine _)) ?mulVf ?fine_eq0 ?probability_fin_num// mul1r setIC//.
+Qed.
+
+End conditional_probability.
+Notation "' P [ E1 | E2 ]" := (conditional_probability P E1 E2).
+
+Require Import real_interval.
+
+Section independent_RVs.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+Local Open Scope ereal_scope.
+
+Definition pairwise_independent_RV (X Y : {RV P >-> R}) :=
+  forall s t, pairwise_independent P (X @^-1` s) (Y @^-1` t).
+
+Lemma conditional_independent_RV (X Y : {RV P >-> R}) :
+  pairwise_independent_RV X Y ->
+  forall s t, P (Y @^-1` t) != 0 -> 'P [X @^-1` s | Y @^-1` t] = P (X @^-1` s).
+Proof.
+move=> iRVXY s t PYtne0.
+exact: conditional_independence.
+Qed.
+
+Definition mutually_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) :=
+  forall x_ : I -> R, mutually_independent P A (fun i => X i @^-1` `[(x_ i), +oo[%classic).
+
+Definition kwise_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) k :=
+  forall x_ : I -> R, kwise_independent P A (fun i => X i @^-1` `[(x_ i), +oo[%classic) k.
+
+Lemma nwise_indep_is_mutual_indep_RV (I : choiceType) (A : {fset I}) (X : I -> {RV P >-> R}) n :
+  #|` A | = n -> kwise_independent_RV [set` A] X n -> mutually_independent_RV [set` A] X.
+Proof.
+rewrite/mutually_independent_RV/kwise_independent_RV=> nA kwX s.
+by apply: nwise_indep_is_mutual_indep; rewrite ?nA.
+Qed.
+
+(* alternative formalization
+Definition inde_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) :=
+  forall (s : I -> set R), mutually_independent P A (fun i => X i @^-1` s i).
+Definition kwise_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) k :=
+  forall (s : I -> set R), kwise_independent P A (fun i => X i @^-1` s i) k.
+this should be equivalent according to wikipedia https://en.wikipedia.org/wiki/Independence_(probability_theory)#For_real_valued_random_variables
+*)
+
+(* Remark 2.15 (i) *)
+Lemma prob_inde_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) :
+  mutually_independent_RV A X ->
+    forall J : {fset I}, [set` J] `<=` A ->
+      forall x_ : I -> R,
+        P (\bigcap_(i in [set` J]) X i @^-1` `[(x_ i), +oo[%classic) =
+          \prod_(i <- J) P (X i @^-1` `[(x_ i), +oo[%classic).
+Proof.
+move=> iRVX J JleA x_.
+apply: (iRVX _).2 => //.
+Qed.
+
+Lemma inde_expectation (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) :
+  mutually_independent_RV A X ->
+    forall B : {fset I}, [set` B] `<=` A ->
+    'E_P[\prod_(i <- B) X i] = \prod_(i <- B) 'E_P[X i].
+Proof.
+move=> AX B BA.
+rewrite [in LHS]unlock.
+rewrite /mutually_independent_RV in AX.
+rewrite /mutually_independent in AX.
+Admitted.
+
+End independent_RVs.
+
+Local Open Scope ereal_scope.
+
+Section integrable_comp.
+Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType).
+Variable phi : X -> Y.
+Hypothesis mphi : measurable_fun [set: X] phi.
+Variable mu : {measure set X -> \bar R}.
+Variable f : Y -> \bar R.
+Hypothesis mf : measurable_fun [set: Y] f.
+Hypothesis intf : mu.-integrable [set: X] (f \o phi).
+Local Open Scope ereal_scope.
+
+Lemma integrable_comp_funeneg : (pushforward mu mphi).-integrable [set: Y] f^\-.
+Proof.
+apply/integrableP; split.
+  exact: measurable_funeneg.
+move/integrableP : (intf) => [_].
+apply: le_lt_trans.
+rewrite integral_pushforward//=; last first.
+  apply: measurableT_comp => //=.
+  exact: measurable_funeneg.
+apply: ge0_le_integral => //=.
+apply: measurableT_comp => //=.
+apply: measurableT_comp => //=.
+exact: measurable_funeneg.
+apply: measurableT_comp => //=.
+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//.
+Qed.
+
+Lemma integrable_comp_funepos : (pushforward mu mphi).-integrable [set: Y] f^\+.
+Proof.
+apply/integrableP; split.
+  exact: measurable_funepos.
+move/integrableP : (intf) => [_].
+apply: le_lt_trans.
+rewrite integral_pushforward//=; last first.
+  apply: measurableT_comp => //=.
+  exact: measurable_funepos.
+apply: ge0_le_integral => //=.
+apply: measurableT_comp => //=.
+apply: measurableT_comp => //=.
+exact: measurable_funepos.
+apply: measurableT_comp => //=.
+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//.
+Qed.
+
+End integrable_comp.
+
+Section transfer.
+Local Open Scope ereal_scope.
+Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType).
+Variables (phi : X -> Y) (mphi : measurable_fun setT phi).
+Variables (mu : {measure set X -> \bar R}).
+
+Lemma integral_pushforward_new (f : Y -> \bar R) :
+  measurable_fun setT f ->
+  mu.-integrable setT (f \o phi) ->
+  \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x.
+Proof.
+move=> mf intf.
+transitivity (\int[mu]_y ((f^\+ \o phi) \- (f^\- \o phi)) y); last first.
+  by apply: eq_integral => x _; rewrite [in RHS](funeposneg (f \o phi)).
+rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg].
+rewrite -[X in _ = X - _]integral_pushforward//; last first.
+  exact: measurable_funepos.
+rewrite -[X in _ = _ - X]integral_pushforward//; last first.
+  exact: measurable_funeneg.
+rewrite -integralB//=; last first.
+- apply: integrable_comp_funepos => //.
+    exact: measurableT_comp.
+  exact: integrableN.
+- exact: integrable_comp_funepos.
+- apply/eq_integral => x _.
+  by rewrite /= [in LHS](funeposneg f).
+Qed.
+
+End transfer.
+
+Section transfer_probability.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType) (P : probability T R).
+
+Lemma integral_distribution_new (X : {RV P >-> R}) (f : R -> \bar R) :
+    measurable_fun setT f ->
+    P.-integrable [set: T] (f \o X) ->
+  \int[distribution P X]_y f y = \int[P]_x (f \o X) x.
+Proof. by move=> mf intf; rewrite integral_pushforward_new. Qed.
+
+End transfer_probability.
+
+Section integral_measure_add_new.
+Context d (T : measurableType d) (R : realType)
+  (m1 m2 : {measure set T -> \bar R}) (D : set T).
+Hypothesis mD : measurable D.
+Variable f : T -> \bar R.
+Hypothesis intf1 : m1.-integrable D f.
+Hypothesis intf2 : m2.-integrable D f.
+Hypothesis mf : measurable_fun D f.
+
+Lemma integral_measure_add_new :
+  \int[measure_add m1 m2]_(x in D) f x = \int[m1]_(x in D) f x + \int[m2]_(x in D) f x.
+transitivity (\int[m1]_(x in D) (f^\+ \- f^\-) x +
+              \int[m2]_(x in D) (f^\+ \- f^\-) x); last first.
+  by congr +%E; apply: eq_integral => x _; rewrite [in RHS](funeposneg f).
+rewrite integralB//; last 2 first.
+  exact: integrable_funepos.
+  exact: integrable_funeneg.
+rewrite integralB//; last 2 first.
+  exact: integrable_funepos.
+  exact: integrable_funeneg.
+rewrite addeACA.
+rewrite -integral_measure_add//; last first.
+  apply: measurable_funepos.
+  exact: measurable_int intf1.
+rewrite -oppeD; last first.
+  by rewrite ge0_adde_def// inE integral_ge0.
+rewrite -integral_measure_add//; last first.
+  apply: measurable_funeneg.
+  exact: measurable_int intf1.
+by rewrite integralE.
+Qed.
+
+End integral_measure_add_new.
+
+Section bernoulli.
+
+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 real_of_bool := fun b : bool => b%:R : R.
+
+Lemma measurable_fun_real_of_bool : measurable_fun setT real_of_bool.
+Proof. by []. Qed.
+
+Lemma real_of_bool1 : real_of_bool @^-1` [set 1%R] = [set true].
+Proof.
+by apply/seteqP; split => [x|x ->] //=; case: x => //= /esym/eqP; rewrite oner_eq0.
+Qed.
+
+Lemma real_of_bool0 : real_of_bool @^-1` [set 0%R] = [set false].
+Proof.
+by apply/seteqP; split => [x|x ->] //=; case: x => //= /eqP/=; rewrite oner_eq0.
+Qed.
+
+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.
+
+Lemma bernoulli_RV1 (X : {RV P >-> R}) : bernoulli_RV X ->
+  P [set i | X i == 1%R] == p%:num%:E.
+Proof.
+move=> [/(congr1 (fun f => f [set 1%:R]))].
+rewrite /bernoulli/= /pushforward ifT; last exact/andP.
+rewrite real_of_bool1 fsbig_set1/= /distribution /= => <- _.
+apply/eqP; congr (P _).
+by apply/seteqP; split => [x /eqP H//|x /eqP].
+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]))]].
+rewrite /bernoulli/= /pushforward ifT; last exact/andP.
+rewrite real_of_bool0 fsbig_set1/= /distribution /= => <- _.
+apply/eqP; congr (P _).
+by apply/seteqP; split => [x /eqP H//|x /eqP].
+Qed.
+
+Lemma bernoulli_ge0 (X : {RV P >-> R}) : bernoulli_RV X ->
+  forall t, (X t >= 0)%R.
+Proof.
+move=> bX t.
+suff: (range X) (X t) by rewrite bX.2 => -[] ->.
+by exists t.
+Qed.
+
+Lemma bernoulli_expectation (X : {RV P >-> R}) :
+  bernoulli_RV X -> 'E_P[X] = p%:num%:E.
+Proof.
+move=> bX.
+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 //=.
+  exact: measurableT_comp.
+rewrite bX.1.
+rewrite integral_pushforward/=; last 2 first.
+  exact: measurableT_comp.
+  by move=> /= r; rewrite lee_fin.
+rewrite integral_bernoulli//; last exact/andP.
+by rewrite /real_of_bool normr1 normr0 !mule0 adde0 mule1.
+Qed.
+
+Lemma bernoulli_sqr (X : {RV P >-> R}) :
+  bernoulli_RV X -> bernoulli_RV (X ^+ 2 : {RV P >-> R})%R.
+Proof.
+rewrite /bernoulli_RV => -[Xp1 X01]; split.
+  rewrite -Xp1; apply/funext => A.
+  rewrite /distribution /pushforward/=; congr (P _).
+  by apply/seteqP; split => [t|t];
+    (have : (range X) (X t) by exists t);
+    rewrite X01/= /GRing.mul/= => -[] ->; rewrite ?(mul0r,mul1r).
+rewrite -X01; apply/seteqP; split => [x|x].
+- move=> [t _] /=; rewrite /GRing.mul/= -expr2 => <-;
+  (have : (range X) (X t) by exists t);
+  by rewrite X01/= /GRing.mul/= => -[] Xt;
+    exists t => //; rewrite Xt ?(expr0n,expr1n).
+- move=> [t _] /=; rewrite /GRing.mul/= => <-;
+  (have : (range X) (X t) by exists t);
+  by rewrite X01/= => -[] Xt;
+    exists t => //=; rewrite Xt/= ?(mulr0,mulr1).
+Qed.
+
+Lemma integrable_bernoulli (X : {RV P >-> R}) :
+  bernoulli_RV X -> P.-integrable [set: T] (EFin \o X).
+Proof.
+move=> bX.
+apply/integrableP; split; first by apply: measurableT_comp.
+have -> : \int[P]_x `|(EFin \o X) x| = 'E_P[X].
+  rewrite unlock /expectation.
+  apply: eq_integral => x _.
+  rewrite gee0_abs //= lee_fin.
+  by rewrite bernoulli_ge0//.
+by rewrite bernoulli_expectation// ltry.
+Qed.
+
+Lemma bernoulli_variance (X : {RV P >-> R}) :
+(* NB(rei): no need for that?
+   P.-integrable setT (EFin \o X) ->
+   P.-integrable [set: T] (EFin \o (X ^+ 2)%R) ->*)
+bernoulli_RV X -> 'V_P[X] = (p%:num * (`1-(p%:num)))%:E.
+move=> b.
+rewrite varianceE; last 2 first.
+  exact: integrable_bernoulli.
+  exact: integrable_bernoulli (bernoulli_sqr b).
+rewrite (bernoulli_expectation b).
+have b2 := bernoulli_sqr b.
+rewrite (bernoulli_expectation b2) /=.
+by rewrite -EFinD mulrDr mulr1 mulrN.
+Qed.
+
+Definition independent (X Y : {RV P >-> R}) := 'E_P[X * Y] = 'E_P[X] * 'E_P[Y].
+
+Definition independent_RVs (X : seq {RV P >-> R}) :=
+  forall Xi, Xi \in X -> forall Xj, Xj \in X -> independent Xi Xj.
+
+Lemma independent_RVs_expectation (X : seq {RV P >-> R}) :
+  independent_RVs X -> 'E_P[\prod_(Xi <- X) Xi] = \prod_(Xi <- X) 'E_P[Xi].
+Proof.
+elim: X => [_|X0 X IH hRVs].
+  by rewrite !big_nil expectation_cst.
+rewrite !big_cons.
+rewrite -IH.
+Admitted.
+
+(*
+Definition independent_RVs (X : seq {RV P >-> R}) := forall t,
+    (fine ('E_P[expR \o t \o* \sum_(Xi <- X) Xi]) = \prod_(Xi <- X) fine ('E_P[expR \o t \o* Xi]))%R.
+*)
+
+Definition is_bernoulli_trial (X : seq {RV P >-> R}) n :=
+  (forall Xi, Xi \in X -> bernoulli_RV Xi) /\
+    independent_RVs X /\
+    size X = n(*NB: used n.-tuple instead of seq*).
+
+Definition bernoulli_trial (X : seq {RV P >-> R}) :=
+  (\sum_(Xi <- X) Xi)%R.
+
+Lemma expectation_bernoulli_trial (X : seq {RV P >-> R}) n :
+  is_bernoulli_trial X n -> 'E_P[@bernoulli_trial X] = (n%:R * p%:num)%:E.
+Proof.
+move=> [bRV [_ Xn]]; rewrite expectation_sum; last first.
+  by move=> Xi XiX; exact: (integrable_bernoulli (bRV _ XiX)).
+under eq_big_seq => Xi XiX.
+  by rewrite (bernoulli_expectation (bRV Xi _))//; over.
+rewrite /= -Xn -sum1_size natr_sum big_distrl/= sumEFin; congr EFin.
+by under [RHS]eq_bigr do rewrite mul1r.
+Qed.
+
+Lemma bernoulli_trial_ge0 (X : seq {RV P >-> R}) n : is_bernoulli_trial X n ->
+  (forall t, 0 <= bernoulli_trial X t)%R.
+Proof.
+move=> [bRV Xn] t.
+rewrite /bernoulli_trial [leRHS](_ : _ = \sum_(Xi <- X) Xi t)%R; last first.
+  by rewrite {bRV Xn}; elim/big_ind2 : _ => //= _ f _ g <- <-.
+  (* NB: this maybe need to be a lemma*)
+by rewrite big_seq; apply: sumr_ge0 => i iX; exact/bernoulli_ge0/bRV.
+Qed.
+
+(* this seems to be provable like in https://www.cs.purdue.edu/homes/spa/courses/pg17/mu-book.pdf page 65 *)
+Axiom taylor_ln_le : forall (delta : R), ((1 + delta) * ln (1 + delta) >= delta + delta^+2 / 3)%R.
+
+Lemma expR_prod (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.
+
+Lemma bernoulli_mmt_gen_fun (X : {RV P >-> R}) (t : R) :
+  bernoulli_RV X -> 'E_P[expR \o t \o* X] = (p%:num * expR t + (1-p%:num))%:E.
+Admitted.
+
+Lemma binomial_mmt_gen_fun (X_ : seq {RV P >-> R}) n (t : R) :
+  is_bernoulli_trial X_ n ->
+  let X := bernoulli_trial X_ : {RV P >-> R} in
+  mmt_gen_fun X t = ((p%:num * expR t + (1-p%:num))`^(n%:R))%:E.
+Proof.
+rewrite /is_bernoulli_trial /independent_RVs /bernoulli_trial.
+move=> [bX1 [bX2 bX3]] /=.
+rewrite -[LHS]fineK; last first.
+  rewrite /mmt_gen_fun unlock /expectation.
+  apply: integral_fune_fin_num => //.
+  admit.
+(*rewrite bX2 big_seq.
+apply: congr1.
+under eq_bigr => Xi XiX do rewrite (bernoulli_mmt_gen_fun _ (bX1 _ _))//=.*)
+Admitted.
+
+Lemma lm23 (X_ : seq {RV P >-> R}) (t : R) n :
+  (0 <= t)%R ->
+  is_bernoulli_trial X_ n ->
+  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.
+Proof.
+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 rewrite (binomial_mmt_gen_fun _ bX)//.
+  apply: congr1; (*apply: bX.2.1 => //*) admit.
+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.
+    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 _)).
+  move=> Xi _.
+  rewrite addr_ge0 ?mulr_ge0 ?subr_ge0 ?andTb//; last first.
+    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.
+  by rewrite subr_gt0 -expR0 ltr_expR.
+rewrite /mu big_seq expectation_sum; last first.
+  move=> Xi XiX; apply: integrable_bernoulli; 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.
+Admitted.
+
+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_ : seq {RV P >-> R}) n (t delta : R) :
+  is_bernoulli_trial X_ n ->
+  (0 < delta)%R ->
+  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 *
+    (expR (- t * (1 + delta)) `^ fine mu)%:E <=
+    ((expR delta / (1 + delta) `^ (1 + delta)) `^ fine mu)%:E.
+Proof.
+move=> bX d0 /=.
+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//.
+  by rewrite -powRN mulNr -mulrN expR_powR lnK// posrE addr_gt0.
+Qed.
+
+(* theorem 2.4 Rajani / thm 4.4.(2) mu-book *)
+Theorem thm24 (X_ : seq {RV P >-> R}) n (delta : R) :
+  is_bernoulli_trial X_ n ->
+  (0 < delta)%R ->
+  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.
+Proof.
+rewrite /= => bX delta0.
+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.
+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.
+exact: (end_thm24 _ bX).
+Qed.
+
+(* theorem 2.5 *)
+Theorem poisson_ineq (X : seq {RV P >-> R}) (delta : R) n :
+  is_bernoulli_trial X n ->
+  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.
+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) => //.
+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).
+  rewrite ler_sub//.
+  exact: taylor_ln_le.
+rewrite le_eqVlt; apply/orP; left; apply/eqP; congr (expR _)%:E.
+by rewrite opprD addrA subrr add0r mulrC mulrN mulNr mulrA.
+Qed.
+
+(* TODO: move *)
+Lemma ln_div : {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 : normr \o expR = (expR : R -> R).
+Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.
+
+Require Import derive.
+
+Lemma le01_expR_ge1Dx (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.
+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 ler_oppr oppr0 ltW.
+Admitted.
+
+(* Rajani thm 2.6 / mu-book thm 4.5.(2) *)
+Theorem thm26 (X : seq {RV P >-> R}) (delta : R) n :
+  is_bernoulli_trial X n -> (0 < delta < 1)%R ->
+  let X' := @bernoulli_trial X : {RV P >-> R} 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.
+Proof.
+move=> bX /andP[delta0 delta1] /=.
+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)).
+  (* 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].
+    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.
+  set t := ln (1 - delta).
+  have ln1delta : (t < 0)%R.
+    (* TODO: lacking a lemma here *)
+    rewrite -oppr0 ltr_oppr -lnV ?posrE ?subr_gt0// ln_gt0//.
+    by rewrite invf_gt1// ?subr_gt0// ltr_subl_addr ltr_addl.
+  have {H1}-> := H1 _ ln1delta.
+  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: expR_gt0.
+    - admit. (* oops *)
+    - 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).
+    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 [].
+    rewrite (binomial_mmt_gen_fun _ bX)/=.
+    rewrite /mu /X' (expectation_bernoulli_trial bX)/=.
+    rewrite !lnK ?posrE ?subr_gt0//.
+    rewrite expR_powR 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 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 !lnK ?posrE ?subr_gt0//.
+  rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expR_powR 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.
+rewrite lee_fin.
+rewrite -mulrN -mulrA [in leRHS]mulrC expR_powR 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.
+- rewrite -ler_ln ?posrE ?divr_gt0 ?expR_gt0 ?powR_gt0 ?subr_gt0//.
+  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.
+Admitted.
+
+Lemma measurable_fun_le D (f g : T -> R) : d.-measurable D -> measurable_fun D f ->
+  measurable_fun D g -> measurable (D `&` [set x | f x <= g x]%R).
+Proof.
+move=> mD mf mg.
+under eq_set => x do rewrite -lee_fin.
+apply: emeasurable_fun_le => //; apply: measurableT_comp => //.
+Qed.
+
+(* Rajani -> corollary 2.7 / mu-book -> corollary 4.7 *)
+Corollary cor27 (X : seq {RV P >-> R}) (delta : R) n :
+  is_bernoulli_trial X n -> (0 < delta < 1)%R ->
+  (0 < n)%nat ->
+  (0 < p%:num)%R ->
+  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.
+Proof.
+move=> bX /andP[d0 d1] n0 p0 /=.
+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 -{2}(mul1r (fine mu)) -mulrBl.
+  rewrite -!lee_fin.
+  over.
+rewrite /=.
+rewrite set_orb.
+rewrite measureU; last 3 first.
+- rewrite -(@setIidr _ setT [set _ | _]) ?subsetT//.
+  apply: emeasurable_fun_le => //.
+  apply: measurableT_comp => //.
+- rewrite -(@setIidr _ setT [set _ | _]) ?subsetT//.
+  apply: emeasurable_fun_le => //.
+  apply: measurableT_comp => //.
+- rewrite disjoints_subset => x /=.
+  rewrite /mem /in_mem/= => X0; apply/negP.
+  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//=.
+- 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 ler_opp2.
+  rewrite ler_pmul//; last by rewrite lef_pinv ?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).
+Qed.
+
+(* Rajani thm 3.1 / mu-book thm 4.7 *)
+Theorem sampling (X : seq {RV P >-> R}) (theta delta : R) :
+  let n := size X in
+  let X_sum := bernoulli_trial X in
+  let X' x := (X_sum x) / n%:R in
+  (0 < p%:num)%R ->
+  is_bernoulli_trial X n ->
+  (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.
+Proof.
+move=> n X_sum X' p0 bX /andP[delta0 delta1] /andP[theta0 thetap] n0 tdn.
+have E_X_sum: 'E_P[X_sum] = (p%:num * n%:R)%:E.
+  rewrite expectation_sum/=; last first.
+    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.
+  rewrite /= sumEFin big_const_seq iter_addr_0/= mulr_natr; congr ((_ *+ _)%:E).
+  by rewrite /n -count_predT; apply: eq_in_count => x ->.
+set epsilon := theta / p%:num.
+have epsilon01 : (0 < epsilon < 1)%R.
+  by rewrite /epsilon ?ltr_pdivr_mulr ?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 <=
+    ((expR (- (p%:num * n%:R * (epsilon ^+ 2)) / 3)) *+ 2)%:E.
+  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.
+      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).
+    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.
+    by rewrite -mulrA divff ?mulr1// gt_eqF// ltr0n.
+  rewrite -mulrA.
+  have -> : (p%:num * n%:R)%R = fine (p%:num * n%:R)%:E by [].
+  rewrite -E_X_sum.
+  by apply: (@cor27 X epsilon _ bX).
+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 -2![in leRHS]mulrA [in leRHS]mulrCA -[in leLHS]mulrA ler_wpmul2l//.
+  rewrite (mulrC epsilon) exprMn -mulrA ler_wpmul2r//.
+    by rewrite divr_ge0// sqr_ge0.
+  by rewrite expr2 ler_pimull.*) admit.
+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]/=.
+      by rewrite leNgt => /negP.
+    by rewrite ltNge => /negP/negPn.
+  have ? : measurable [set i | (`|X' i - p%:num| < theta)%R].
+    under eq_set => x do rewrite -lte_fin.
+    rewrite -(@setIidr _ setT [set _ | _]) ?subsetT /X'//.
+    by apply: emeasurable_fun_lt => //; apply: measurableT_comp => //;
+      apply: measurableT_comp => //; apply: measurable_funD => //;
+      apply: measurable_funM.
+  rewrite probability_setC// lee_subel_addr//.
+  rewrite -lee_subel_addl//; last by rewrite fin_num_measure.
+  move=> /le_trans; apply.
+  rewrite le_measure ?inE//.
+    under eq_set => x do rewrite -lee_fin.
+    rewrite -(@setIidr _ setT [set _ | _]) ?subsetT /X'//.
+    by apply: emeasurable_fun_le => //; apply: measurableT_comp => //;
+      apply: measurableT_comp => //; apply: measurable_funD => //;
+      apply: measurable_funM.
+  by move=> t/= /ltW.
+(* NB: last step in the pdf *)
+apply: (le_trans step2).
+rewrite lee_fin -(mulr_natr _ 2) -ler_pdivl_mulr//.
+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_pdivr_mulr; last by rewrite exprn_gt0.
+by rewrite mulrAC.
+Admitted.
+
+End bernoulli.