renaming (#124)

changelog.txt

@@ -1,3 +1,7 @@
+
+
+- lemma `conv_pt_cset_is_convex` changed into a `Let`
+
 -------------------
 from 0.7.1 to 0.7.2
 -------------------

information_theory/aep.v

@@ -136,7 +136,7 @@ have H2 k i : `V ((\row_(i < k.+1) `-- (`log P)) ``_ i) = aep_sigma2 P.
   by rewrite mxE V_mlog.
 have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon).
 move/(leR_trans _); apply.
-apply/Pr_incl/subsetP => ta; rewrite 2!inE => /andP[H1].
+apply/subset_Pr/subsetP => ta; rewrite 2!inE => /andP[H1].
 rewrite /sum_mlog_prod [`-- (`log _)]lock /= -lock /= /scalel_RV /log_RV /neg_RV.
 rewrite fdist_rVE.
 rewrite log_prodR_sumR_mlog //.

information_theory/binary_symmetric_channel.v

@@ -274,7 +274,7 @@ Section dH_BSC.
 Variable p : {prob R}.
 Let card_F2 : #| 'F_2 | = 2%nat. by rewrite card_Fp. Qed.
 Let W := BSC.c card_F2 p.
-Variables (M : finType) (n : nat) (f : encT [finType of 'F_2] M n).
+Variables (M : finType) (n : nat) (f : encT 'F_2 M n).
 
 Local Open Scope vec_ext_scope.
 

information_theory/erasure_channel.v

@@ -61,7 +61,7 @@ apply/eqP; rewrite psumr_eq0/=; last first.
   by rewrite eqxx implybT.
 Qed.
 
-Definition c : `Ch(A, [finType of option A]) :=
+Definition c : `Ch(A, option A) :=
   fun a => FDist.make (f0 a) (f1 a).
 
 End EC_sect.

information_theory/typ_seq.v

@@ -196,11 +196,11 @@ have -> : Pr P `^ n.+1 (~: p) =
       by rewrite ler_norml; apply/andP; split;
         apply/RleP; rewrite -RminusE -RoppE;
         rewrite -RdivE ?gt_eqF// ?ltr0n// -INRE//.
-  rewrite Pr_union_disj // disjoints_subset; apply/subsetP => /= i.
+  rewrite disjoint_Pr_setU // disjoints_subset; apply/subsetP => /= i.
   by rewrite !inE /= => /eqP Hi; rewrite negb_and Hi ltxx.
 rewrite {1}/Pr (eq_bigr (fun=> 0)); last by move=> /= v; rewrite inE => /eqP.
 rewrite big_const iter_addR mulR0 add0R.
-apply/(leR_trans _ (aep He k0_k))/Pr_incl/subsetP => /= t.
+apply/(leR_trans _ (aep He k0_k))/subset_Pr/subsetP => /= t.
 rewrite !inE /= => /andP[-> H3].
 rewrite /log_RV /= /scalel_RV /= mulRN -mulNR.
 apply/ltW.

information_theory/types.v

@@ -69,7 +69,8 @@ Proof.
 case: P => /= d f d_f; by rewrite d_f mulRCA mulRV ?INR_eq0' // mulR1.
 Qed.
 
-Lemma INR_type_fun A n (P : P_ n ( A )) a : ((type.f P) a)%:R / n%:R = type.d(*TODO: fix coercion *)P a.
+Lemma INR_type_fun A n (P : P_ n ( A )) a :
+  ((type.f P) a)%:R / n%:R = type.d(*TODO: fix coercion *)P a.
 Proof. destruct P as [d f d_f] => /=. by rewrite d_f. Qed.
 
 Lemma no_0_type (A : finType) (d : {fdist A}) (t : {ffun A -> 'I_1}) :
@@ -476,7 +477,7 @@ case/boolP : [exists x, x \in T_{P}] => x_T_P.
     exact: Pr_le1.
   symmetry.
   rewrite /Pr.
-  transitivity (\sum_(a | (a \in [finType of 'rV[A]_n]) &&
+  transitivity (\sum_(a | (a \in 'rV[A]_n) &&
                           [pred x in (@row_of_tuple A n @: T_{P})] a)
       exp2 (- INR n * `H P)).
     apply eq_big => // ta'/= Hta'.

probability/bayes.v

@@ -107,7 +107,8 @@ Section univ_types.
 (* heterogeneous types *)
 Variable n : nat.
 Variable types : 'I_n -> eqType.
-Definition univ_types : eqType := [eqType of {dffun forall i, types i}].
+Definition univ_types : eqType :=
+  [eqType of {dffun forall i, types i}].
 
 Section prod_types.
 (* sets of indices *)

probability/fdist.v

@@ -660,11 +660,7 @@ Proof. by move=> Xa0; rewrite fdistD1E Xa0 mul0r; case: ifP. Qed.
 
 End fdistD1_prop.
 
-(* TODO: move? *)
-(* about_distributions_of_ordinals.*)
-
-Lemma fdistI0_False (R: realType) (d : R.-fdist 'I_O)
-  : False.
+Lemma fdistI0_False (R : realType) (d : R.-fdist 'I_O) : False.
 Proof. move: (fdist_card_neq0 d); by rewrite card_ord. Qed.
 
 Section fdistI2.

probability/fsdist.v

@@ -1070,7 +1070,8 @@ rewrite /ball_ => xball.
 rewrite /nbhs /= /nbhs /=.
 rewrite /eventually /=.
 rewrite /filter_from /=.
-suff: exists N, forall k, (N <= k)%nat -> P (\bigcup_n F n) = P (\bigcup_(i < k) F i).
+suff: exists N, forall k, (N <= k)%nat ->
+    P (\bigcup_n F n) = P (\bigcup_(i < k) F i).
   case=> N HN.
   exists N => //.
   move=> j /= ij.

probability/jfdist_cond.v

@@ -73,22 +73,21 @@ split.
   by apply/Pr_cPr_gt0; move: H; rewrite jcPrE -setTE -EsetT.
 Qed.
 
-(* TODO: rename *)
-Lemma jcPr_cplt E F : Pr (P`2) F != 0 -> \Pr_[ ~: E | F] = 1 - \Pr_[E | F].
+Lemma jcPr_setC E F : Pr (P`2) F != 0 -> \Pr_[ ~: E | F] = 1 - \Pr_[E | F].
 Proof.
 by move=> PF0; rewrite 2!jcPrE EsetT setCX cPr_cplt ?EsetT // setTE Pr_setTX.
 Qed.
 
-(* TODO: rename *)
-Lemma jcPr_diff E1 E2 F : \Pr_[E1 :\: E2 | F] = \Pr_[E1 | F] - \Pr_[E1 :&: E2 | F].
+Lemma jcPr_setD E1 E2 F :
+  \Pr_[E1 :\: E2 | F] = \Pr_[E1 | F] - \Pr_[E1 :&: E2 | F].
 Proof.
-rewrite jcPrE DsetT cPr_diff jcPrE; congr (_ - _).
+rewrite jcPrE DsetT cPr_setD jcPrE; congr (_ - _).
 by rewrite 2!EsetT setIX setTI -EsetT jcPrE.
 Qed.
 
-Lemma jcPr_union_eq E1 E2 F :
+Lemma jcPr_setU E1 E2 F :
   \Pr_[E1 :|: E2 | F] = \Pr_[E1 | F] + \Pr_[E2 | F] - \Pr_[E1 :&: E2 | F].
-Proof. by rewrite jcPrE UsetT cPr_union_eq !jcPrE IsetT. Qed.
+Proof. by rewrite jcPrE UsetT cPr_setU !jcPrE IsetT. Qed.
 
 Section total_probability.
 Variables (I : finType) (E : {set A}) (F : I -> {set B}).
@@ -118,6 +117,13 @@ End total_probability.
 End conditional_probability.
 Notation "\Pr_ P [ E | F ]" := (jcPr P E F) : proba_scope.
 
+#[deprecated(since="infotheo 0.7.3", note="renamed to `jcPr_setD`")]
+Notation jcPr_diff := jcPr_setD (only parsing).
+#[deprecated(since="infotheo 0.7.3", note="renamed to `jcPr_setC`")]
+Notation jcPr_cplt := jcPr_setC (only parsing).
+#[deprecated(since="infotheo 0.7.3", note="renamed to `jcPr_setU`")]
+Notation jcPr_union_eq := jcPr_setU (only parsing).
+
 Section jPr_Pr.
 Variables (U : finType) (P : {fdist U}) (A B : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (E : {set A}) (F : {set B}).

probability/necset.v

@@ -348,8 +348,7 @@ HB.instance Definition _ (X Y : neset A) :=
 HB.instance Definition _ (X : neset A) (n : nat) :=
   isNESet.Build _ _ (iter_conv_set_neq0 X n).
 
-(* TODO: Let insteaad of Lemma *)
-Lemma conv_pt_cset_is_convex (p : {prob R}) (x : A) (Y : {convex_set A}) :
+Let conv_pt_cset_is_convex (p : {prob R}) (x : A) (Y : {convex_set A}) :
   is_convex_set (conv_pt_set p x Y).
 Proof.
 apply/asboolP=> u v q.

probability/proba.v

@@ -1370,13 +1370,11 @@ rewrite /cPr; apply/divR_gt0; rewrite Pr_gt0P //.
 by apply: contra H; rewrite setIC => /eqP F0; apply/eqP/Pr_domin_setI.
 Qed.
 
-(* TODO: rename *)
-Lemma cPr_diff F1 F2 E :
+Lemma cPr_setD F1 F2 E :
   `Pr_[F1 :\: F2 | E] = `Pr_[F1 | E] - `Pr_[F1 :&: F2 | E].
 Proof. by rewrite /cPr -divRBl setIDAC Pr_setD setIAC. Qed.
 
-(* TODO: rename *)
-Lemma cPr_union_eq F1 F2 E :
+Lemma cPr_setU F1 F2 E :
   `Pr_[F1 :|: F2 | E] = `Pr_[F1 | E] + `Pr_[F2 | E] - `Pr_[F1 :&: F2 | E].
 Proof. by rewrite /cPr -divRDl -divRBl setIUl Pr_setU setIACA setIid. Qed.
 
@@ -1445,6 +1443,10 @@ Notation cPr_eq0 := cPr_eq0P (only parsing).
 Notation cPr_max := cPr_le1 (only parsing).
 #[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_gt0P`")]
 Notation cPr_gt0 := cPr_gt0P (only parsing).
+#[deprecated(since="infotheo 0.7.3", note="renamed to `cPr_setD`")]
+Notation cPr_diff := cPr_setD (only parsing).
+#[deprecated(since="infotheo 0.7.3", note="renamed to `cPr_setU`")]
+Notation cPr_union_eq := cPr_setU (only parsing).
 
 Section fdist_cond.
 Variables (A : finType) (P : R.-fdist A) (E : {set A}).

robust/robustmean.v

@@ -276,7 +276,7 @@ Lemma cEx_sub (X : {RV P -> R}) (F G: {set U}) :
   `| `E_[ X | F ] - `E_[X | G] |
 = `| `E ((X `-cst `E_[X | G]) `* Ind F : {RV P -> R}) | / Pr P F.
 Proof.
-move=> /[dup] /Pr_gt0 PrPF_neq0 /invR_gt0 /ltRW PrPFV_ge0 FsubG.
+move=> /[dup] /Pr_gt0P PrPF_neq0 /invR_gt0 /ltRW PrPFV_ge0 FsubG.
 rewrite divRE -(geR0_norm (/Pr P F)) // -normRM.
 apply: congr1.
 by rewrite -[RHS]cEx_ExInd cEx_trans_min_RV.
@@ -306,9 +306,9 @@ Lemma cEx_cVar (X : {RV P -> R}) (F G: {set U}) : 0 < Pr P F  ->
   `| `E_[ X | F ] - mu | <= sqrt (var * Pr P G / Pr P F ).
 Proof.
 move=> /[dup] /invR_gt0 /ltRW PrPFV_nneg /[dup] /invR_gt0
-        PrPFV_pos /[dup] /Pr_gt0 PrPF_neq0 PrPF_pos
-        /[dup] /(Pr_incl P) /(ltR_leR_trans PrPF_pos)
-        /[dup] /Pr_gt0 PrPG_neq0 PrPG_pos FsubG mu var.
+        PrPFV_pos /[dup] /Pr_gt0P PrPF_neq0 PrPF_pos
+        /[dup] /(subset_Pr P) /(ltR_leR_trans PrPF_pos)
+        /[dup] /Pr_gt0P PrPG_neq0 PrPG_pos FsubG mu var.
 rewrite cEx_sub //.
 pose y := sqrt (Ex P (((X `-cst mu) `^2) `* Ind F) * Ex P (Ind F)) / Pr P F.
 apply leR_trans with (y := y).
@@ -360,7 +360,7 @@ Proof.
   repeat rewrite mulR1.
   rewrite in_setC.
   destruct (i \in F); simpl; lra.
-  all: apply Pr_gt0; try rewrite Pr_of_cplt; lra.
+  all: apply Pr_gt0P; try rewrite Pr_setC; lra.
 Qed.
 
 Lemma cEx_Inv_int (X: {RV P -> R}) F:
@@ -372,7 +372,7 @@ Proof.
   repeat rewrite cEx_ExInd.
   (repeat have ->: forall x y, x != 0 -> x * (y / x) = y
   by move => x y Hz; rewrite mulRC -mulRA mulVR; last by []; rewrite mulR1);
-  try apply Pr_gt0; try rewrite Pr_of_cplt; try lra.
+  try apply Pr_gt0P; try rewrite Pr_setC; try lra.
   apply Rplus_eq_reg_r with (r:= Pr P F * `E X).
   rewrite -addRA Rplus_opp_l addR0 -addRA addRC.
   apply Rplus_eq_reg_r with (r:=`E (X `* Ind (~: F):{RV P -> R})).
@@ -392,9 +392,9 @@ Lemma cEx_Inv' (X: {RV P -> R}) (F G : {set U}) :
   `| `E_[X | F] - `E_[X | G]| = (Pr P (G :\: F)) / (Pr P F) * `| `E_[X | (G :\: F)] - `E_[X | G]|.
 Proof.
 move=> PrPF_gt0 /[dup] /setIidPr GIFF FsubG /[dup] /(ltR_trans PrPF_gt0)
-       /[dup] /Pr_gt0 /invR_neq0' /eqP PrPG_neq0 PrPG_gt0 PrPF_PrPG.
-have : 0 < Pr P (G :\: F) by rewrite Pr_diff subR_gt0 GIFF.
-move => /[dup] /Pr_gt0 PrPGF_neq0 PrPGF_gt0.
+       /[dup] /Pr_gt0P /invR_neq0' /eqP PrPG_neq0 PrPG_gt0 PrPF_PrPG.
+have : 0 < Pr P (G :\: F) by rewrite Pr_setD subR_gt0 GIFF.
+move => /[dup] /Pr_gt0P PrPGF_neq0 PrPGF_gt0.
 rewrite !cEx_sub ?subsetDl // !divRE mulRCA.
 rewrite Ind_setD//.
 rewrite !coqRE mulrAC divff// mul1r -!coqRE.
@@ -412,9 +412,9 @@ Lemma cEx_Inv (X: {RV P -> R}) F :
   0 < Pr P F -> Pr P F < 1 ->
   `| `E_[X | F] - `E X| = (1 - Pr P F) / Pr P F * `| `E_[X | (~: F)] - `E X|.
 Proof.
-move=> *; rewrite Ex_cExT -Pr_of_cplt -setTD; apply cEx_Inv' => //.
-apply ltR_neqAle; split; last by apply/Pr_incl/subsetT.
-by apply/eqP; rewrite Pr_setT -Pr_lt1.
+move=> *; rewrite Ex_cExT -Pr_setC -setTD; apply cEx_Inv' => //.
+apply ltR_neqAle; split; last by apply/subset_Pr/subsetT.
+by apply/eqP; rewrite Pr_setT -Pr_lt1P.
 Qed.
 
 Lemma cvariance_ge0 (X : {RV P -> R}) F : 0 <= `V_[X | F].
@@ -585,7 +585,7 @@ have [Pr_FG_eq|/eqP Pr_FG_neq] := eqVneq (Pr P F) (Pr P G).
     by move=> i /GFP0 ->; rewrite mulR0.
   exact/sqrt_pos.
 have [?|/eqP PrF_neq0] := eqVneq (Pr P F) 0; first nra.
-have ? := Pr_incl P FG.
+have ? := subset_Pr P FG.
 have ? := Pr_ge0 P F.
 have [?|/eqP PrG_neq0] := eqVneq (Pr P G) 0; first by nra.
 have HPrFpos : 0 < Pr P F by have := Pr_ge0 P F; lra.
@@ -607,7 +607,7 @@ rewrite cEx_Inv'//; last lra.
 apply: leR_trans.
   apply leR_wpmul2l; first exact: divR_ge0.
   apply cEx_cVar => //; last exact: subsetDl.
-  by rewrite Pr_diff HGnF_F subR_gt0; lra.
+  by rewrite Pr_setD HGnF_F subR_gt0; lra.
 apply: (@leR_trans
     (sqrt (`V_[ X | G] * (Pr P G * (1 - delta)) / (Pr P G * delta * delta)))).
   rewrite -(Rabs_pos_eq (Pr P (G :\: F) / Pr P F)); last exact: divR_ge0.
@@ -616,7 +616,7 @@ apply: (@leR_trans
   rewrite !divRE !mulRA [in X in X <= _](mulRC _  (`V_[X | G])) -!mulRA.
   apply: leR_wpmul2l; first exact: cvariance_ge0.
   rewrite !mulRA mulRC !mulRA mulVR ?mul1R; last first.
-    by rewrite Pr_diff HGnF_F; apply/eqP; nra.
+    by rewrite Pr_setD HGnF_F; apply/eqP; nra.
   rewrite mulRC (mulRC (/Pr P F)) -mulRA -invRM; [|exact/gtR_eqF|exact/gtR_eqF].
   rewrite mulRA; apply/leR_pdivr_mulr; first by nra.
   rewrite mulRAC; apply/leR_pdivl_mulr; first by apply: Rmult_lt_0_compat; nra.
@@ -625,7 +625,7 @@ apply: (@leR_trans
   rewrite (mulRC (Pr P G)) -mulRA; apply: leR_pmul => //.
   - apply: mulR_ge0 => //; apply/mulR_ge0; last exact/ltRW.
     by apply/mulR_ge0 => //; exact/ltRW.
-  - by rewrite Pr_diff HGnF_F; nra.
+  - by rewrite Pr_setD HGnF_F; nra.
   - by rewrite mulRCA; apply: leR_pmul; nra.
 apply sqrt_le_1_alt.
 rewrite divRE invRM; [|exact/gtR_eqF/mulR_gt0|exact/gtR_eqF].
@@ -669,21 +669,21 @@ move=> bad mu_hat mu sigma Hmin_outliers Hmax_outliers Hbad_ratio Hdrop_ratio
 have H : Pr P good = 1 - eps by apply/esym/subR_eq; rewrite -Hbad_ratio Pr_cplt.
 (* On the other hand, we remove at most 4ε good points *)
 have max_good_drop : Pr P (good :&: drop) <= 4 * eps.
-  by rewrite -Hdrop_ratio; exact/Pr_incl/subsetIr.
+  by rewrite -Hdrop_ratio; exact/subset_Pr/subsetIr.
 pose eps' := Pr P (bad :\: drop) / Pr P (~: drop).
 have Hcompl : Pr P (good :\: drop) / Pr P (~: drop) = 1 - eps'.
-  apply/esym/subR_eq; rewrite /eps' -mulRDl -Pr_union_disj.
-    by rewrite -setDUl setUCr setTD mulRV// Pr_of_cplt; apply/eqP; lra.
+  apply/esym/subR_eq; rewrite /eps' -mulRDl -disjoint_Pr_setU.
+    by rewrite -setDUl setUCr setTD mulRV// Pr_setC; apply/eqP; lra.
   by rewrite -setI_eq0 -setDIl setICr set0D.
 have eps'_ge0 : 0 <= eps'.
-  by apply: mulR_ge0 => //; apply/ltRW/invR_gt0; rewrite Pr_of_cplt; lra.
+  by apply: mulR_ge0 => //; apply/ltRW/invR_gt0; rewrite Pr_setC; lra.
 have eps'_le1 : eps' <= 1.
-  rewrite /eps'; apply/leR_pdivr_mulr; first by rewrite Pr_of_cplt; lra.
-  by rewrite mul1R; exact/Pr_incl/subsetDr.
+  rewrite /eps'; apply/leR_pdivr_mulr; first by rewrite Pr_setC; lra.
+  by rewrite mul1R; exact/subset_Pr/subsetDr.
 (* Remaining good points: 1 - (4 * eps) / (1 - eps) *)
 pose delta := 1 - (4 * eps) / (1 - eps).
 have min_good_remain : delta <= Pr P (good :\: drop) / Pr P good.
-  rewrite /delta Pr_diff H.
+  rewrite /delta Pr_setD H.
   apply: (@leR_trans ((1 - eps - 4 * eps) / (1 - eps))).
     apply/leR_pdivl_mulr; first lra.
     by rewrite mulRDl -mulNR -(mulRA _ (/ _)) Rinv_l; lra.
@@ -702,10 +702,10 @@ have Exgood_bound : `| `E_[X | good :\: drop ] - `E_[X | good] | <=
   - suff : `E_[X | (good :\: drop)] = `E_[X | good].
       by move=> ->; rewrite subRR normR0; exact: sqrt_pos.
     apply: eq_bigr => i _; rewrite gdg; congr (_ * _ * _).
-    rewrite setIDA Pr_diff -setIA.
+    rewrite setIDA Pr_setD -setIA.
     (* NB: lemma? *)
     apply/subR_eq; rewrite addRC; apply/subR_eq; rewrite subRR; apply/esym.
-    move: gdg; rewrite Pr_diff => /subR_eq; rewrite addRC => /subR_eq.
+    move: gdg; rewrite Pr_setD => /subR_eq; rewrite addRC => /subR_eq.
     by rewrite subRR [in X in _ -> X]setIC => /esym; exact: Pr_domin_setI.
   - apply cresilience.
     + apply (@ltR_pmul2r (1 - eps)); first lra.
@@ -731,7 +731,7 @@ have Exbad_bound : 0 < Pr P (bad :\: drop) ->
   move: ibaddrop; rewrite inE => /andP[idrop ibad].
   by rewrite leRNgt => /Hquantile_drop_bad => /(_ ibad); apply/negP.
 have max_bad_remain : Pr P (bad :\: drop) <= eps / Pr P (~: drop).
-  rewrite Pr_of_cplt Hdrop_ratio Pr_diff Hbad_ratio.
+  rewrite Pr_setC Hdrop_ratio Pr_setD Hbad_ratio.
   apply: (@leR_trans eps); first exact/leR_subl_addr/leR_addl.
   by apply/leR_pdivl_mulr; [lra|nra].
 have Ex_not_drop : `E_[ X | ~: drop ] =
@@ -741,7 +741,7 @@ have Ex_not_drop : `E_[ X | ~: drop ] =
   have good_bad : Pr P (good :\: drop) + Pr P (bad :\: drop) = Pr P (~: drop).
     rewrite -(_ : good :\: drop :|: bad :\: drop = ~: drop); last first.
       by rewrite -setDUl setUCr setTD.
-    rewrite Pr_union_eq.
+    rewrite Pr_setU.
     apply/subR_eq; rewrite subR_opp addRC; apply/esym/subR_eq; rewrite subRR.
     suff : (good :\: drop) :&: (bad :\: drop) = set0.
       by move=> ->; rewrite Pr_set0.
@@ -750,7 +750,7 @@ have Ex_not_drop : `E_[ X | ~: drop ] =
   - rewrite bd0 addR0 in good_bad.
     rewrite bd0 mulR0 addR0 good_bad.
     rewrite /Rdiv -mulRA mulRV ?mulR1; last first.
-      by apply/Pr_gt0; rewrite -good_bad Pr_diff H; lra.
+      by apply/Pr_gt0P; rewrite -good_bad Pr_setD H; lra.
     rewrite 2!cEx_ExInd good_bad; congr (_ / _).
     apply/eq_bigr => u _.
     rewrite /ambient_dist -!mulRA; congr (_ * _).
@@ -759,9 +759,9 @@ have Ex_not_drop : `E_[ X | ~: drop ] =
     have bad_drop0 : u \in bad :\: drop -> P u = 0 by apply Pr_set0P.
     case: ifPn => idrop //=.
     by case: ifPn => // igood; rewrite bad_drop0 ?mulR0// !inE idrop.
-  - apply/eqR_divl_mulr; first by rewrite Pr_of_cplt; apply/eqP; nra.
+  - apply/eqR_divl_mulr; first by rewrite Pr_setC; apply/eqP; nra.
     rewrite !cEx_ExInd -!mulRA.
-    rewrite Rinv_l ?mulR1; last by rewrite Pr_of_cplt; nra.
+    rewrite Rinv_l ?mulR1; last by rewrite Pr_setC; nra.
     rewrite Rinv_l ?mulR1; last nra.
     rewrite Rinv_l // mulR1.
     rewrite [in RHS]/Ex -big_split; apply: eq_bigr => i _ /=.
@@ -790,12 +790,12 @@ apply: (@leR_trans (sqrt (`V_[ X | good] / eps) * eps' +
     by rewrite !(mulR0,add0R,subR0,mulR1).
   have [->|/eqP eps'1] := eqVneq eps' 1.
     rewrite !(subRR,mulR0,addR0,mulR1); apply: Exbad_bound.
-    apply Pr_gt0; apply: contra_notN eps'0 => /eqP.
+    apply Pr_gt0P; apply: contra_notN eps'0 => /eqP.
     by rewrite /eps' => ->; rewrite div0R.
   have [bd0|bd0] := eqVneq (Pr P (bad :\: drop)) 0.
     by exfalso; apply/eps'0; rewrite /eps' bd0 div0R.
   apply: leR_add; (apply/leR_pmul2r; first lra).
-  - exact/Exbad_bound/Pr_gt0.
+  - exact/Exbad_bound/Pr_gt0P.
   - exact: Exgood_bound.
 rewrite /sigma /Rdiv !sqrt_mult //; last 8 first.
   - exact: cvariance_ge0.

robust/weightedmean.v

@@ -769,7 +769,7 @@ apply (@le_trans _ _ ((1 - eps) * (`V_[X | S] + (`E_[X | S] - `E (WP.-RV X))^+2)
 apply (@le_trans _ _ ((1 - eps) * (`V_[X | S] + (Num.sqrt (`V_[X | S] * 2 * eps / (2 - eps)) +
                                             Num.sqrt (`V (WP.-RV X) * 2 * eps / (1 - eps)))^+2))).
   apply ler_wpM2l.
-    by rewrite subr_ge0; exact/RleP/Pr_1.
+    by rewrite subr_ge0; exact/RleP/Pr_le1.
   rewrite lerD2l -ler_abs_sqr.
   rewrite [x in _ <= x]ger0_norm; first exact: (bound_mean_emean C eps_max).
   exact/addr_ge0/sqrtr_ge0/sqrtr_ge0.
@@ -877,7 +877,7 @@ Lemma bound_empirical_variance_cplt_S :
   2/denom * `V (WP.-RV X) <= \sum_(i in cplt_S) C i * P i * tau i.
 Proof.
 have ? := pr_S_gt0 eps_max01 low_eps.
-have /RleP pr1_cplt_S := Pr_1 P cplt_S.
+have /RleP pr1_cplt_S := Pr_le1 P cplt_S.
 
 have -> : \sum_(i in cplt_S) C i * P i * tau i =
   `V (WP.-RV X) * (\sum_(i in U) C i * P i) - (\sum_(i in S) C i * P i * tau i).