minor cleaning around random variables

changelog.txt

@@ -7,16 +7,24 @@ from 0.3.3 to 0.3.4
   + lemmas ltZ_addl, ltZ_addr, pmulZ_rgt0
   + lemmas intRD, leZ0n
 - in ssrR.v:
-  + lemma expRn_gt0
+  + lemmas expRn_gt0, ltR0n_neq0, lt0Rn_neq0', eqR_divl_mulr
+- in proba.v
+  + lemmas scalel_RVA, scaler_RVA, sq_RV_pow2, sq_RV_ge0, E_trans_min_RV
 * renamed:
 - in necset.v:
   + lemma nesetU_bigsetU -> nesetU_bigcup
 * removed:
 - in convex.v:
   + definition choice_of_Object
+- in aep.v
+  + lemma E_mlog (since it is equivalent to entropy.entropy_Ex)
 * changed:
 - in ssr_ext.v:
   + remove eq_tcast in favor of eq_tcast2 (renamed to eq_tcast)
+- in aep.v
+  + a cleaner expression for aep_sigma2
+- in proba.v
+  + stopped importing the unused Nsatz
 
 -------------------
 from 0.3.2 to 0.3.3

information_theory/aep.v

@@ -10,9 +10,9 @@ Require Import entropy.
 (******************************************************************************)
 (*              Asymptotic Equipartition Property (AEP)                       *)
 (*                                                                            *)
-(* Lemmas E_mlog, V_mlog == properties of the ``- log P'' random variable     *)
-(* Definition aep_bound  == constant used in the statement of AEP             *)
-(* Lemma aep             == AEP                                               *)
+(*         Lemma V_mlog == Var(-log P) = E((-log P)^2) - H(P)                 *)
+(* Definition aep_bound == constant used in the statement of AEP              *)
+(*            Lemma aep == AEP                                                *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -27,21 +27,23 @@ Local Open Scope ring_scope.
 Local Open Scope vec_ext_scope.
 
 Section mlog_prop.
-
 Variables (A : finType) (P : fdist A).
+Local Open Scope R_scope.
 
-Lemma E_mlog : `E (--log P) = `H P.
+Definition aep_sigma2 := `E ((--log P) `^2) - (`H P)^2.
+
+Lemma aep_sigma2E : aep_sigma2 = \sum_(a in A) P a * (log (P a))^2 - (`H P)^2.
 Proof.
-rewrite /entropy big_morph_oppR; apply eq_bigr=> a _; by rewrite /= mulNR mulRC.
+rewrite /aep_sigma2 /Ex [in LHS]/mlog_RV /sq_RV /comp_RV.
+by under eq_bigr do rewrite mulRC /ambient_dist -mulRR Rmult_opp_opp mulRR.
 Qed.
 
-Definition aep_sigma2 := (\sum_(a in A) P a * (log (P a))^2 - (`H P)^2)%R.
-
 Lemma V_mlog : `V (--log P) = aep_sigma2.
 Proof.
-rewrite /Var E_trans_RV_id_rem E_mlog /aep_sigma2.
+rewrite aep_sigma2E /Var E_trans_RV_id_rem -entropy_Ex.
 transitivity
-  (\sum_(a in A) ((- log (P a))^2 * P a - 2 * `H P * - log (P a) * P a + `H P ^ 2 * P a))%R.
+    (\sum_(a in A) ((- log (P a))^2 * P a - 2 * `H P * - log (P a) * P a +
+                    `H P ^ 2 * P a))%R.
   apply eq_bigr => a _.
   rewrite /scalel_RV /mlog_RV /trans_add_RV /sq_RV /comp_RV /= /sub_RV.
   by rewrite /ambient_dist; field.
@@ -54,7 +56,7 @@ rewrite (_ : \sum_(a in A) - _ = - (2 * `H P ^ 2))%R; last first.
   rewrite -big_distrr [in LHS]/= -{1}big_morph_oppR.
   by rewrite -/(entropy P) -mulRA /= mulR1.
 set s := ((\sum_(a in A ) _)%R in LHS).
-rewrite [in RHS](_ : \sum_(a in A) _ = s)%R; last by apply eq_bigr => a _; field.
+rewrite (_ : \sum_(a in A) _ = s)%R; last by apply eq_bigr => a _; field.
 field.
 Qed.
 
@@ -127,7 +129,7 @@ apply (@leR_trans (aep_sigma2 P / (n.+1%:R * epsilon ^ 2))); last first.
   by split; [by rewrite INR_eq0 | exact/eqP/gtR_eqF].
 have Hsum := sum_mlog_prod_sum_map_mlog P n.
 have H1 : forall k i, `E ((\row_(i < k.+1) --log P) ``_ i) = `H P.
-  by move=> k i; rewrite mxE E_mlog.
+  by move=> k i; rewrite mxE entropy_Ex.
 have H2 : forall k i, `V ((\row_(i < k.+1) --log P) ``_ i) = aep_sigma2 P.
   by move=> k i; rewrite mxE V_mlog.
 have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon).

information_theory/entropy.v

@@ -12,9 +12,15 @@ Require Import fdist proba jfdist binary_entropy_function divergence.
 (* `H P == the entropy of the (finite) probability distribution P             *)
 (*                                                                            *)
 (* Lemmas:                                                                    *)
-(*   entropy_ge0 == the entropy is non-negative                               *)
-(*   entropy_max == the entropy is bounded by log |A| where A is the support  *)
-(*                  of the distribution                                       *)
+(*       entropy_ge0 == the entropy is non-negative                           *)
+(*       entropy_max == the entropy is bounded by log |A| where A is the      *)
+(*                      support of the distribution                           *)
+(*       entropy_Ex  == the entropy is the expectation of the negative        *)
+(*                      logarithm                                             *)
+(*      xlnx_entropy == the entropy is the natural entropy scaled by ln(2)    *)
+(*   entropy_uniform == the entropy of a uniform distribution is just log     *)
+(*       entropy_H2  == the binary entropy H2 is the entropy over {x, y}      *)
+(*       entropy_max == the entropy is bound by log                           *)
 (******************************************************************************)
 
 Reserved Notation "'`H'" (at level 5).

lib/ssrR.v

@@ -562,6 +562,12 @@ Proof. by split => [/INR_lt/ltP|/ltP/lt_INR]. Qed.
 Lemma ltR_nat' m n : (m%:R <b n%:R) = (m < n)%nat.
 Proof. by apply/idP/idP => [/ltRP/ltR_nat|/ltR_nat/ltRP]. Qed.
 
+Lemma ltR0n_neq0 n : (0 < n)%nat <-> n%:R != 0.
+Proof. by rewrite lt0n; split => /eqP /INR_eq0 /eqP. Qed.
+
+Lemma ltR0n_neq0' n : (0 < n)%nat = (n%:R != 0).
+Proof. by apply/(sameP idP)/(iffP idP) => /ltR0n_neq0. Qed.
+
 (*************)
 (* invR/divR *)
 (*************)
@@ -679,6 +685,9 @@ move=> z0; split => [<-|->]; first by rewrite -mulRA mulVR // mulR1.
 by rewrite /Rdiv -mulRA mulRV // mulR1.
 Qed.
 
+Lemma eqR_divl_mulr z x y : z != 0 -> (x = y / z) <-> (x * z = y).
+Proof. by move=> z0; split; move/esym/eqR_divr_mulr => /(_ z0) ->. Qed.
+
 Lemma leR_pdivr_mulr z x y : 0 < z -> (y / z <= x) <-> (y <= x * z).
 Proof.
 move=> z0; split => [/(leR_wpmul2r (ltRW z0))|H].

probability/proba.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup perm finalg matrix.
 From mathcomp Require boolp.
 From mathcomp Require Import Rstruct.
-Require Import Reals Lra Nsatz.
+Require Import Reals Lra.
 Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop.
 Require Import fdist.
 
@@ -545,6 +545,24 @@ Notation "X '`-cst' m" := (trans_min_RV X m) : proba_scope.
 Notation "X '`^2' " := (sq_RV X) : proba_scope.
 Notation "'--log' P" := (mlog_RV P) : proba_scope.
 
+Section RV_lemmas.
+Variables (U : finType) (P : fdist U).
+Implicit Types X : {RV P -> R}.
+
+Lemma scalel_RVA k l X : scalel_RV (k * l) X = scalel_RV k (scalel_RV l X).
+Proof. by rewrite /scalel_RV boolp.funeqE => u; rewrite mulRA. Qed.
+
+Lemma scaler_RVA X k l : scaler_RV X (k * l) = scaler_RV (scaler_RV X k) l.
+Proof. by rewrite /scaler_RV boolp.funeqE => u; rewrite mulRA. Qed.
+
+Lemma sq_RV_pow2 X x : sq_RV X x = (X x) ^ 2.
+Proof. reflexivity. Qed.
+
+Lemma sq_RV_ge0 X x : 0 <= sq_RV X x.
+Proof. by rewrite sq_RV_pow2; exact: pow2_ge_0. Qed.
+
+End RV_lemmas.
+
 Section pair_of_RVs.
 Variables (U : finType) (P : fdist U).
 Variables (A : eqType) (X : {RV P -> A}) (B : eqType) (Y : {RV P -> B}).
@@ -553,18 +571,21 @@ End pair_of_RVs.
 
 Notation "'[%' x , y , .. , z ']'" := (RV2 .. (RV2 x y) .. z).
 
-Lemma fst_RV2 (U : finType) (P : fdist U) (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}) : Bivar.fst `d_[% X, Y] = `d_X.
+Lemma fst_RV2 (U : finType) (P : fdist U) (A B : finType)
+  (X : {RV P -> A}) (Y : {RV P -> B}) : Bivar.fst `d_[% X, Y] = `d_X.
 Proof. by rewrite /Bivar.fst /dist_of_RV FDistMap.comp. Qed.
 
-Lemma snd_RV2 (U : finType) (P : fdist U) (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}) : Bivar.snd `d_[% X, Y] = `d_Y.
+Lemma snd_RV2 (U : finType) (P : fdist U) (A B : finType)
+  (X : {RV P -> A}) (Y : {RV P -> B}) : Bivar.snd `d_[% X, Y] = `d_Y.
 Proof. by rewrite /Bivar.snd /dist_of_RV FDistMap.comp. Qed.
 
 Lemma pr_eq_unit (U : finType) (P : fdist U) : `Pr[ (unit_RV P) = tt ] = 1.
 Proof. by rewrite pr_eqE'; apply/eqP/FDist1.P; case. Qed.
 
 Lemma Pr_FDistMap_RV2 (U : finType) (P : fdist U) (A B : finType)
   (E : {set A}) (F : {set B}) (X : {RV P -> A}) (Z : {RV P -> B}) :
-  Pr (FDistMap.d [% X, Z] P) (E `* F) = Pr P ([set x | preim X (mem E) x] :&: [set x | preim Z (mem F) x]).
+  Pr (FDistMap.d [% X, Z] P) (E `* F) =
+  Pr P ([set x | preim X (mem E) x] :&: [set x | preim Z (mem F) x]).
 Proof.
 rewrite /Pr.
 transitivity (\sum_(a in ([% X, Z] @^-1: (E `* F))) P a); last first.
@@ -584,31 +605,40 @@ Lemma pr_in_pairC E F : `Pr[ [% Y, X] \in F `* E ] = `Pr[ [% X, Y] \in E `* F].
 Proof. by rewrite 2!pr_eq_setE; apply eq_bigl => u; rewrite !inE /= andbC. Qed.
 
 Lemma pr_eq_pairC a b : `Pr[ [% TY, TX] = (b, a) ] = `Pr[ [% TX, TY] = (a, b)].
-Proof. by rewrite !pr_eqE; congr Pr; apply/setP => u; rewrite !inE /= !xpair_eqE andbC. Qed.
+Proof.
+by rewrite !pr_eqE; congr Pr; apply/setP => u; rewrite !inE /= !xpair_eqE andbC.
+Qed.
 
 Lemma pr_in_pairA E F G :
-  `Pr[ [% X, [% Y, Z]] \in E `* (F `* G) ] = `Pr[ [% [% X, Y], Z] \in (E `* F) `* G].
+  `Pr[ [% X, [% Y, Z]] \in E `* (F `* G) ] =
+  `Pr[ [% [% X, Y], Z] \in (E `* F) `* G].
 Proof. by rewrite !pr_eq_setE; apply eq_bigl => u; rewrite !inE /= andbA. Qed.
 
 Lemma pr_eq_pairA a b c :
   `Pr[ [% TX, [% TY, TZ]] = (a, (b, c))] = `Pr[ [% TX, TY, TZ] = (a, b, c) ].
-Proof. by rewrite !pr_eqE; apply eq_bigl => u; rewrite !inE /= !xpair_eqE andbA. Qed.
+Proof.
+by rewrite !pr_eqE; apply eq_bigl => u; rewrite !inE /= !xpair_eqE andbA.
+Qed.
 
 Lemma pr_in_pairAC E F G :
 `Pr[ [% X, Y, Z] \in (E `* F) `* G] = `Pr[ [% X, Z, Y] \in (E `* G) `* F].
 Proof. by rewrite !pr_eq_setE; apply eq_bigl => u; rewrite !inE /= andbAC. Qed.
 
 Lemma pr_eq_pairAC a b c :
 `Pr[ [% TX, TY, TZ] = (a, b, c) ] = `Pr[ [% TX, TZ, TY] = (a, c, b)].
-Proof. by rewrite !pr_eqE; apply eq_bigl => u; rewrite !inE /= !xpair_eqE andbAC. Qed.
+Proof.
+by rewrite !pr_eqE; apply eq_bigl => u; rewrite !inE /= !xpair_eqE andbAC.
+Qed.
 
 Lemma pr_in_pairCA E F G :
 `Pr[ [% X, [%Y, Z]] \in E `* (F `* G) ] = `Pr[ [% Y, [%X, Z]] \in F `* (E `* G)].
 Proof. by rewrite !pr_eq_setE; apply eq_bigl => u; rewrite !inE /= andbCA. Qed.
 
 Lemma pr_eq_pairCA  a b c :
 `Pr[ [% TX, [%TY, TZ]] = (a, (b, c)) ] = `Pr[ [% TY, [% TX, TZ]] = (b, (a, c))].
-Proof. by rewrite !pr_eqE; apply eq_bigl => u; rewrite !inE /= !xpair_eqE andbCA. Qed.
+Proof.
+by rewrite !pr_eqE; apply eq_bigl => u; rewrite !inE /= !xpair_eqE andbCA.
+Qed.
 
 Lemma pr_in_comp (f : A -> B) E : injective f ->
   `Pr[ X \in E ] = `Pr[ (f `o X) \in f @: E ].
@@ -648,7 +678,8 @@ Qed.
 Lemma pr_eq_domin_RV2 a b : `Pr[ TX = a ] = 0 -> `Pr[ [% TX, TY] = (a, b) ] = 0.
 Proof.
 move=> H.
-by rewrite -pr_eq_set1 -setX1 pr_inE' Pr_domin_setX // fst_RV2 -pr_inE' pr_eq_set1.
+rewrite -pr_eq_set1 -setX1 pr_inE' Pr_domin_setX // fst_RV2 -pr_inE'.
+by rewrite pr_eq_set1.
 Qed.
 
 End RV_domin.
@@ -659,8 +690,8 @@ Definition cast_RV_tupledist1 U (P : fdist U) (T : eqType) (X : {RV P -> T})
    : {RV (P `^ 1) -> T} :=
   fun x => X (x ``_ ord0).
 
-Definition cast_rV1_RV_tupledist1 U (P : fdist U) (T : eqType) (Xs : 'rV[{RV P -> T}]_1)
-  : {RV (P `^ 1) -> T} :=
+Definition cast_rV1_RV_tupledist1 U (P : fdist U) (T : eqType)
+    (Xs : 'rV[{RV P -> T}]_1) : {RV (P `^ 1) -> T} :=
   cast_RV_tupledist1 (Xs ``_ ord0).
 
 Definition cast_fun_rV1 U (T : eqType) (X : U -> T) : 'rV[U]_1 -> T :=
@@ -744,6 +775,14 @@ transitivity (\sum_(u in U) (X u * `p_X u + m * `p_X u)).
 by rewrite big_split /= -big_distrr /= FDist.f1 mulR1.
 Qed.
 
+Lemma E_trans_min_RV m : `E (X `-cst m) = `E X - m.
+Proof.
+rewrite /trans_min_RV /=.
+transitivity (\sum_(u in U) (X u * `p_X u + - m * `p_X u)).
+  by apply eq_bigr => u _ /=; rewrite mulRDl.
+by rewrite big_split /= -big_distrr /= FDist.f1 mulR1.
+Qed.
+
 Lemma E_trans_RV_id_rem m :
   `E ((X `-cst m) `^2) = `E ((X `^2 `- (2 * m `cst* X)) `+cst m ^ 2).
 Proof.
@@ -772,7 +811,8 @@ Section conditional_expectation_def.
 
 Variable (U : finType) (P : fdist U) (X : {RV P -> R}) (F : {set U}).
 
-Definition cEx := \sum_(r <- fin_img X) r * Pr P (finset (X @^-1 r) :&: F) / Pr P F.
+Definition cEx :=
+  \sum_(r <- fin_img X) r * Pr P (finset (X @^-1 r) :&: F) / Pr P F.
 
 End conditional_expectation_def.
 Notation "`E_[ X | F ]" := (cEx X F).
@@ -1121,7 +1161,7 @@ rewrite mulRC /Var.
 apply (@leR_trans (\sum_(a in U | `| X a - `E X | >b= epsilon)
     (((X `-cst `E X) `^2) a  * `p_X a))); last first.
   apply leR_sumRl_support with (Q := xpredT) => // a .
-  by apply mulR_ge0 => //; exact: pow_even_ge0.
+  by apply mulR_ge0 => //; exact: sq_RV_ge0.
 rewrite /Pr big_distrr.
 rewrite  [_ ^2]lock /= -!lock.
 apply leR_sumRl => u; rewrite ?inE => Hu //=.
@@ -1130,7 +1170,7 @@ apply leR_sumRl => u; rewrite ?inE => Hu //=.
   apply (@leR_trans ((X u - `E X) ^ 2)); last exact/leRR.
   rewrite -(sqR_norm (X u - `E X)).
   by apply/pow_incr; split => //; [exact/ltRW | exact/leRP].
-- by apply mulR_ge0 => //; exact: pow_even_ge0.
+- by apply mulR_ge0 => //; exact: sq_RV_ge0.
 Qed.
 
 End chebyshev.
@@ -1147,7 +1187,8 @@ Proof.
 rewrite /inde_events => EF; have : Pr d E = Pr d (E :&: F) + Pr d (E :&: ~:F).
   rewrite (total_prob d E (fun b => if b then F else ~:F)) /=; last 2 first.
     move=> i j ij; rewrite -setI_eq0.
-    by case: ifPn ij => Hi; case: ifPn => //= Hj _; rewrite ?setICr // setIC setICr.
+    by case: ifPn ij => Hi; case: ifPn => //= Hj _;
+      rewrite ?setICr // setIC setICr.
     by rewrite cover_imset big_bool /= setUC setUCr.
   by rewrite big_bool addRC.
 by rewrite addRC -subR_eq EF -{1}(mulR1 (Pr d E)) -mulRBr -Pr_of_cplt.
@@ -1178,7 +1219,8 @@ split => [pi i j ij|].
   red in pi.
   have /pi : (#|[set i; j]| <= 2)%nat by rewrite cards2 ij.
   rewrite bigcap_setU !big_set1 => H.
-  by rewrite /inde_events H (big_setD1 i) ?inE ?eqxx ?orTb //= setU1K ?inE // big_set1.
+  rewrite /inde_events H (big_setD1 i) ?inE ?eqxx ?orTb //= setU1K ?inE//.
+  by rewrite big_set1.
 move=> H s.
 move sn : (#| s |) => n.
 case: n sn => [|[|[|//]]].
@@ -1273,7 +1315,8 @@ rewrite /cPr; apply/divR_gt0; rewrite Pr_gt0 //.
 by apply: contra H; rewrite setIC => /eqP F0; apply/eqP/Pr_domin_setI.
 Qed.
 
-Lemma cPr_diff F1 F2 E : `Pr_[F1 :\: F2 | E] = `Pr_[F1 | E] - `Pr_[F1 :&: F2 | E].
+Lemma cPr_diff F1 F2 E :
+  `Pr_[F1 :\: F2 | E] = `Pr_[F1 | E] - `Pr_[F1 :&: F2 | E].
 Proof. by rewrite /cPr -divRBl setIDAC Pr_diff setIAC. Qed.
 
 Lemma cPr_union_eq F1 F2 E :
@@ -1295,7 +1338,8 @@ have [/eqP PF0|PF0] := boolP (Pr d F == 0).
 by rewrite -mulRA mulVR ?mulR1.
 Qed.
 
-Lemma product_rule_cond E F G : `Pr_[E :&: F | G] = `Pr_[E | F :&: G] * `Pr_[F | G].
+Lemma product_rule_cond E F G :
+  `Pr_[E :&: F | G] = `Pr_[E | F :&: G] * `Pr_[F | G].
 Proof. by rewrite /cPr mulRA -setIA {1}product_rule. Qed.
 
 Lemma cPr_cplt E F : Pr d E != 0 -> `Pr_[ ~: F | E] = 1 - `Pr_[F | E].
@@ -1418,7 +1462,8 @@ Proof. by rewrite /cpr_eq; unlock. Qed.
 End crandom_variable_eqType.
 Notation "`Pr[ X = a | Y = b ]" := (cpr_eq X a Y b) : proba_scope.
 
-Lemma cpr_eq_unit_RV (U : finType) (A : eqType) (P : {fdist U}) (X : {RV P -> A}) (a : A) :
+Lemma cpr_eq_unit_RV (U : finType) (A : eqType) (P : {fdist U})
+    (X : {RV P -> A}) (a : A) :
   `Pr[ X = a | (unit_RV P) = tt ] = `Pr[ X = a ].
 Proof. by rewrite cpr_eqE' cPrET pr_eqE. Qed.
 
@@ -1432,25 +1477,31 @@ Qed.
 
 Section crandom_variable_finType.
 Variables (U A B : finType) (P : {fdist U}).
+Implicit Types X : {RV P -> A}.
 
-Definition cpr_eq_set (X : {RV P -> A}) (E : {set A}) (Y : {RV P -> B}) (F : {set B}) :=
+Definition cpr_eq_set X (E : {set A}) (Y : {RV P -> B}) (F : {set B}) :=
   locked (`Pr_P [ X @^-1: E | Y @^-1: F ]).
 Local Notation "`Pr[ X \in E | Y \in F ]" := (cpr_eq_set X E Y F).
 
-Lemma cpr_eq_setE (X : {RV P -> A}) (E : {set A}) (Y : {RV P -> B}) (F : {set B}) :
+Lemma cpr_eq_setE X (E : {set A}) (Y : {RV P -> B}) (F : {set B}) :
   `Pr[ X \in E | Y \in F ] = `Pr_P [ X @^-1: E | Y @^-1: F ].
 Proof. by rewrite /cpr_eq_set; unlock. Qed.
 
-Lemma cpr_eq_set1 (X : {RV P -> A}) x (Y : {RV P -> B}) y :
+Lemma cpr_eq_set1 X x (Y : {RV P -> B}) y :
   `Pr[ X \in [set x] | Y \in [set y] ] = `Pr[ X = x | Y = y ].
-Proof. by rewrite cpr_eq_setE cpr_eqE'; congr cPr; apply/setP => u; rewrite !inE. Qed.
+Proof.
+by rewrite cpr_eq_setE cpr_eqE'; congr cPr; apply/setP => u; rewrite !inE.
+Qed.
 
 End crandom_variable_finType.
 Notation "`Pr[ X '\in' E | Y '\in' F ]" := (cpr_eq_set X E Y F) : proba_scope.
-Notation "`Pr[ X '\in' E | Y = b ]" := (`Pr[ X \in E | Y \in [set b]]) : proba_scope.
-Notation "`Pr[ X = a | Y '\in' F ]" := (`Pr[ X \in [set a] | Y \in F]) : proba_scope.
+Notation "`Pr[ X '\in' E | Y = b ]" :=
+  (`Pr[ X \in E | Y \in [set b]]) : proba_scope.
+Notation "`Pr[ X = a | Y '\in' F ]" :=
+  (`Pr[ X \in [set a] | Y \in F]) : proba_scope.
 
-Lemma cpr_in_unit_RV (U A : finType) (P : {fdist U}) (X : {RV P -> A}) (E : {set A}) :
+Lemma cpr_in_unit_RV (U A : finType) (P : {fdist U}) (X : {RV P -> A})
+    (E : {set A}) :
   `Pr[ X \in E | (unit_RV P) = tt ] = `Pr[ X \in E ].
 Proof.
 rewrite cpr_eq_setE (_ : _ @^-1: [set tt] = setT); last first.
@@ -1599,7 +1650,8 @@ Lemma cpr_eq_product_rule (U : finType) (P : fdist U) (A B C : eqType)
   `Pr[ X = a | [% Y, Z] = (b, c) ] * `Pr[ Y = b | Z = c ].
 Proof.
 rewrite cpr_eqE'.
-rewrite (_ : [set x | preim [% X, Y] (pred1 (a, b)) x] = finset (X @^-1 a) :&: finset (Y @^-1 b)); last first.
+rewrite (_ : [set x | preim [% X, Y] (pred1 (a, b)) x] =
+             finset (X @^-1 a) :&: finset (Y @^-1 b)); last first.
   by apply/setP => u; rewrite !inE xpair_eqE.
 rewrite product_rule_cond cpr_eqE'; congr (cPr _ _ _ * _).
 - by apply/setP=> u; rewrite !inE xpair_eqE.