From 89a20e475efbb245d7ec5b727589507dd046a425 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 27 Jun 2024 11:31:54 +0900 Subject: [PATCH] fixes #122 --- ecc_modern/ldpc_algo.v | 2 +- information_theory/channel_code.v | 2 +- information_theory/channel_coding_direct.v | 4 +-- information_theory/entropy.v | 14 ++++---- information_theory/joint_typ_seq.v | 10 +++--- information_theory/jtypes.v | 16 ++++----- .../source_coding_vl_converse.v | 4 +-- information_theory/typ_seq.v | 2 +- information_theory/types.v | 5 +-- probability/bayes.v | 28 +++++++-------- probability/jfdist_cond.v | 8 +++-- probability/proba.v | 36 ++++++++++--------- 12 files changed, 68 insertions(+), 63 deletions(-) diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v index 6b452592..65a37c29 100644 --- a/ecc_modern/ldpc_algo.v +++ b/ecc_modern/ldpc_algo.v @@ -203,7 +203,7 @@ Extract Constant Rmult => "( *.)". Extract Constant Rplus => "(+.)". Extract Constant Rinv => "fun x -> 1. /. x". Extract Constant Ropp => "(~-.)". -(*Extraction "extraction/sumprod.ml" sumprod estimation.*) +Extraction "extraction/sumprod.ml" sumprod estimation. Section ToGraph. diff --git a/information_theory/channel_code.v b/information_theory/channel_code.v index 965404a3..fc2ed823 100644 --- a/information_theory/channel_code.v +++ b/information_theory/channel_code.v @@ -73,7 +73,7 @@ Proof. rewrite /CodeErrRate div1R. apply/RleP/ (@leR_pmul2l (INR #|M|)); first exact/ltR0n. rewrite mulRA mulRV ?INR_eq0' -?lt0n // mul1R -iter_addR -big_const. -by apply: leR_sumR => m _; exact: Pr_1. +by apply: leR_sumR => m _; exact: Pr_le1. Qed. Definition scha (W : `Ch(A, B)) (c : code) := (1 - echa(W , c))%R. diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v index 2a567bfd..3198c51f 100644 --- a/information_theory/channel_coding_direct.v +++ b/information_theory/channel_coding_direct.v @@ -734,7 +734,7 @@ apply (@leR_ltR_trans move: (preimC_Cal_E epsilon0 i tb); by rewrite inE. apply (@leR_trans (Pr (W ``(| i ord0)) (~: Cal_E i ord0) + Pr (W ``(| i ord0)) (\bigcup_(i0 | i0 != ord0) (Cal_E i i0)))%R). - exact: Pr_union. + exact: le_Pr_setU. exact/leR_add2l/Pr_bigcup. rewrite first_summand //. set lhs := (\sum_(_ < _ | _) _)%R. @@ -756,7 +756,7 @@ rewrite card_ord /=. apply (@leR_ltR_trans (epsilon0 + k%:R * Pr P `^ n `x (`O(P , W)) `^ n [set x | prod_rV x \in `JTS P W n epsilon0])%R). apply leR_add2r. - rewrite Pr_of_cplt leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //. + rewrite Pr_setC leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //. by case: Hepsilon0. by case: Hn => _ [_ []]. apply (@leR_ltR_trans (epsilon0 + diff --git a/information_theory/entropy.v b/information_theory/entropy.v index 6f4a9aba..f55bde35 100644 --- a/information_theory/entropy.v +++ b/information_theory/entropy.v @@ -490,8 +490,8 @@ rewrite fdistXE fdist_proj13E big_distrl /= -big_split; apply eq_bigr => b _ /=. rewrite !(fdistXE,fdistAE,fdistC12E) /= -mulRDr. have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R. rewrite -logM; last 2 first. - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0. - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1 fdistAE /= fdistC12E. + by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0. + by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1 fdistAE /= fdistC12E. congr (_ * log _). by rewrite -setX1 product_ruleC !setX1 mulRC. Qed. @@ -570,7 +570,7 @@ transitivity (- (\sum_(a in A) \sum_(b in B) PQ (a, b) * log (P a)) + rewrite addRC -mulRN -mulRDr addR_opp. have [->|H0] := eqVneq (PQ (a, b)) 0; first by rewrite !mul0R. congr (_ * _); rewrite logDiv //. - - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1. + - by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1. - by apply/RltP; rewrite -fdist_gt0; exact: dom_by_fdist_fstN H0. rewrite -subR_opp; congr (_ - _). - rewrite /entropy; congr (- _); apply/eq_bigr => a _. @@ -759,12 +759,12 @@ rewrite fdistXE fdistAE /= -mulRN -mulRDr. have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R. congr (_ * _). rewrite addRC addR_opp -logDiv; last 2 first. - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdistA_dominN H0. - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0. + by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdistA_dominN H0. + by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0. congr (log _). rewrite divRM; last 2 first. - by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0. - by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj23_dominN H0. + by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0. + by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj23_dominN H0. rewrite {2}/Rdiv -mulRA mulRCA {1}/Rdiv [in LHS]mulRC; congr (_ * _). rewrite -[in X in _ = X * _]setX1 jproduct_rule_cond setX1 -mulRA mulRV ?mulR1 //. rewrite /jcPr divR_neq0' // ?setX1 !Pr_set1. diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v index 024b1ae8..eb0aa812 100644 --- a/information_theory/joint_typ_seq.v +++ b/information_theory/joint_typ_seq.v @@ -130,7 +130,7 @@ have : (JTS_1_bound <= n)%nat -> have : 1 <= 3 by lra. move/(set_typ_seq_incl P m (ltRW He)) => Hincl. rewrite (Pr_DMC_fst P W (fun x => x \notin `TS P m epsilon)). - apply/Pr_incl/subsetP => i /=; rewrite !inE. + apply/subset_Pr/subsetP => i /=; rewrite !inE. apply contra. by move/subsetP : Hincl => /(_ i); rewrite !inE. have {H1}HnP : forall n, ('| up (aep_bound P (epsilon / 3)) | <= n)%nat -> @@ -159,7 +159,7 @@ have : (JTS_1_bound <= n)%nat -> have : 1 <= 3 by lra. move/(set_typ_seq_incl (`O(P , W)) m (ltRW He)) => Hincl. rewrite Pr_DMC_out. - apply/Pr_incl/subsetP => i /=; rewrite !inE. + apply/subset_Pr/subsetP => i /=; rewrite !inE. apply contra. move/subsetP : Hincl => /(_ i). by rewrite !inE. @@ -187,7 +187,7 @@ have : (JTS_1_bound <= n)%nat -> Pr (((P `X W) ) `^ m) (~: `TS ((P `X W)) m (epsilon / 3)). have : 1 <= 3 by lra. move/(set_typ_seq_incl ((P `X W)) m (ltRW He)) => Hincl. - apply/Pr_incl/subsetP => /= v; rewrite !inE. + apply/subset_Pr/subsetP => /= v; rewrite !inE. apply contra. by move/subsetP : Hincl => /(_ v); by rewrite !inE. have {H1}HnP_W m : ('| up (aep_bound ((P `X W)) (epsilon / 3)) | <= m)%nat -> @@ -229,8 +229,8 @@ apply (@leR_trans ( Pr ((P `X W) `^ n) [set x | (rV_prod x).1 \notin `TS P n epsilon] + Pr ((P `X W) `^ n) ([set x | ((rV_prod x).2 \notin `TS (`O( P , W)) n epsilon)] :|: (~: `TS ((P `X W)) n epsilon)))). - exact: Pr_union. -rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (Pr_union _ _ _). + exact: le_Pr_setU. +rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (le_Pr_setU _ _ _). by apply/Req_le; congr Pr; apply/setP => t; rewrite !inE rV_prodK. Qed. diff --git a/information_theory/jtypes.v b/information_theory/jtypes.v index 1ed16f3d..2207417f 100644 --- a/information_theory/jtypes.v +++ b/information_theory/jtypes.v @@ -252,13 +252,13 @@ by move=> a b; rewrite ffunE. Defined. Definition jtype_enum A B n := pmap (@jtype_enum_f A B n) - (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat}]). + (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat})). Lemma jtype_enumP A B n : Finite.axiom (@jtype_enum A B n). Proof. case=> d f Hf H /=. -have : Finite.axiom (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} | - (\sum_(a in A) \sum_(b in B) f a b == n)%nat }]). +have : Finite.axiom (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}} | + (\sum_(a in A) \sum_(b in B) f a b == n)%nat })). rewrite enumT; by apply enumP. move/(_ (@exist _ _ f Hf)) => <-. rewrite /jtype_enum /=. @@ -291,8 +291,8 @@ eq_ind_r else (sval f a b)%:R / (\sum_(b0 in B) (sval f a) b0)%:R)*) |} - ) (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} | - (\sum_(a in A) \sum_(b in B) f a b)%nat == n}]). + ) (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}} | + (\sum_(a in A) \sum_(b in B) f a b)%nat == n})). apply: eq_pmap => V. destruct Sumbool.sumbool_of_bool; last by rewrite Anot0 in e. destruct Sumbool.sumbool_of_bool; last by rewrite Bnot0 in e0. @@ -357,13 +357,13 @@ move=> Anot0 Bnot0. move: (Anot0); case/card_gt0P => a _. move: (Bnot0); case/card_gt0P => b _. apply/card_gt0P. -have [tmp Htmp] : [finType of {f : {ffun A -> {ffun B -> 'I_n.+1}} | - \sum_(a1 in A) \sum_(b1 in B) f a1 b1 == n}]. +have [tmp Htmp] : {f : {ffun A -> {ffun B -> 'I_n.+1}} | + \sum_(a1 in A) \sum_(b1 in B) f a1 b1 == n}. exists [ffun a1 => [ffun b1 => if (a1, b1) == (a, b) then Ordinal (ltnSn n) else Ordinal (ltn0Sn n)]]. rewrite pair_big /=. rewrite (bigD1 (a, b)) //= big1 ; first by rewrite 2!ffunE eqxx addn0. - move=> p /negbTE Hp ; by rewrite 2!ffunE -surjective_pairing Hp. + by move=> p /negbTE Hp ; rewrite 2!ffunE -surjective_pairing Hp. have Htmp' : (forall a b, (chan_of_jtype Anot0 Bnot0 tmp) a b = (let ln := \sum_(b0 in B) (tmp a) b0 in diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v index 371d8754..3d82477f 100644 --- a/information_theory/source_coding_vl_converse.v +++ b/information_theory/source_coding_vl_converse.v @@ -689,9 +689,9 @@ Proof. pose m' := m.-1. have mpos : m = m'.+1. rewrite prednK // -ltR_nat ltR_neqAle; split => //; exact/leR0n. -have: (@extension [finType of 'rV[A]_n] _ f) \o +have: (@extension 'rV[A]_n _ f) \o (flatten \o map (fun x => @tval m _ (tuple_of_row x))) =1 - @extension [finType of {: 'rV[ 'rV[A]_n ]_m} ] _ fm. + @extension {: 'rV[ 'rV[A]_n ]_m} _ fm. by elim => //= ta sta; rewrite /extension /= map_cat flatten_cat => <-. apply: eq_inj. apply: inj_comp => //. diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v index 384cf5e5..549618c8 100644 --- a/information_theory/typ_seq.v +++ b/information_theory/typ_seq.v @@ -237,7 +237,7 @@ Lemma TS_inf : aep_bound P epsilon <= n.+1%:R -> Proof. move=> k0_k. have H1 : (1 - epsilon <= Pr (P `^ n.+1) (`TS P n.+1 epsilon) <= 1)%mcR. - by apply/andP; split; apply/RleP; [exact: Pr_TS_1 | exact: Pr_1]. + by apply/andP; split; apply/RleP; [exact: Pr_TS_1 | exact: Pr_le1]. have H2 : (forall x, x \in `TS P n.+1 epsilon -> exp2 (- n.+1%:R * (`H P + epsilon)) <= P `^ n.+1 x <= exp2 (- n.+1%:R * (`H P - epsilon)))%mcR. diff --git a/information_theory/types.v b/information_theory/types.v index 861e1f0f..cc459edb 100644 --- a/information_theory/types.v +++ b/information_theory/types.v @@ -473,10 +473,11 @@ case/boolP : [exists x, x \in T_{P}] => x_T_P. rewrite -(row_of_tupleK ta) in Hta. rewrite -(tuple_dist_type_entropy Hta). rewrite [X in X <= _](_ : _ = Pr (type.d P) `^ n (@row_of_tuple A n @: T_{P})). - by apply Pr_1. + exact: Pr_le1. symmetry. rewrite /Pr. - transitivity (\sum_(a| (a \in [finType of 'rV[A]_n]) && [pred x in (@row_of_tuple A n @: T_{P})] a) + transitivity (\sum_(a | (a \in [finType of 'rV[A]_n]) && + [pred x in (@row_of_tuple A n @: T_{P})] a) exp2 (- INR n * `H P)). apply eq_big => // ta'/= Hta'. rewrite -(@tuple_dist_type_entropy ta') //. diff --git a/probability/bayes.v b/probability/bayes.v index 4d79586e..ab45adc1 100644 --- a/probability/bayes.v +++ b/probability/bayes.v @@ -421,10 +421,10 @@ split. case ac: (a == c). rewrite -(eqP ac); exact. move=> _ _ _. - rewrite (proj2 (cPr_eq0 _ _ _)); last first. + rewrite (proj2 (cPr_eq0P _ _ _)); last first. apply/Pr_set0P => u. by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ac. - rewrite (proj2 (cPr_eq0 _ _ _)); last first. + rewrite (proj2 (cPr_eq0P _ _ _)); last first. apply/Pr_set0P => u. by rewrite !inE => /andP [] /= /eqP ->; rewrite ac. by rewrite mul0R. @@ -441,7 +441,7 @@ split. set x := (X in X = X * X). move/Rxx2 => [] Hx. rewrite -/x Hx. - rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //. + rewrite (proj2 (cPr_eq0P _ _ _)) ?mul0R //. apply/Pr_set0P => u. by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ab. rewrite /cPr. @@ -459,17 +459,17 @@ split. move/eqP in Hden. rewrite /cPr /Rdiv -mulRA mulVR // mulR1 mul1R. move/(f_equal (Rminus den)). - rewrite subRR setIC -Pr_diff => /Pr_set0P/(_ u). - rewrite !inE (eqP Hi) Hk eq_sym ab; exact. + rewrite subRR setIC -Pr_setD => /Pr_set0P/(_ u). + by rewrite !inE (eqP Hi) Hk eq_sym ab; exact. case: (ord_eq_dec k j). move=> <- {j} ik b. case bc: (b == c). rewrite (eqP bc); exact. move=> _ _ _. - rewrite (proj2 (cPr_eq0 _ _ _)); last first. + rewrite (proj2 (cPr_eq0P _ _ _)); last first. apply/Pr_set0P => u. by rewrite !inE => /andP [] /andP [] _ /= /eqP ->; rewrite bc. - rewrite mulRC (proj2 (cPr_eq0 _ _ _)) ?mul0R //. + rewrite mulRC (proj2 (cPr_eq0P _ _ _)) ?mul0R //. by apply/Pr_set0P => u; rewrite !inE => /andP [] /= /eqP ->; rewrite bc. move=> nkj nij b HG Hvals; apply: HG => //. by rewrite Hvals set_val_tl // set_val_tl // set_val_hd. @@ -631,10 +631,10 @@ case /boolP: [forall i in (e :&: g), _]. rewrite negb_forall => /existsP [i]. rewrite inE negb_imply => /andP [] /andP [Hie Hig] /eqP Hvi. right; rewrite /cinde_events. -rewrite (proj2 (cPr_eq0 _ _ _)); last first. +rewrite (proj2 (cPr_eq0P _ _ _)); last first. apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi. case/andP: Hprod => /andP[] /eqP <- _ /eqP <-; exact: prod_vars_inter. -rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //. +rewrite (proj2 (cPr_eq0P _ _ _)) ?mul0R //. apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi. case/andP: Hprod => /eqP <- /eqP <-; exact: prod_vars_inter. Qed. @@ -664,7 +664,7 @@ rewrite (proj2 (Pr_set0P _ _)); last first. suff : `Pr_P[finset (prod_vars f @^-1 B) | finset (prod_vars g @^-1 C)] = 0. by rewrite /cPr => ->; rewrite mulR0 div0R. (* prove incompatibility between B and C *) -apply/cPr_eq0/Pr_set0P => u. +apply/cPr_eq0P/Pr_set0P => u. rewrite !inE => /andP [] /eqP HB /eqP HC. move: Hnum; rewrite /den. have -> : g = (e :&: f :|: g) :\: ((e :&: f) :\: g). @@ -745,7 +745,7 @@ split. rewrite negb_imply /vals => /andP [Hif]. case /boolP: (i \in g) => Hig. (* B and C are incompatible *) - move: (Hfg i); by rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->. + by move: (Hfg i); rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->. case /boolP: (i \in e) => Hie; last by rewrite set_vals_tl // set_vals_tl // eqxx. (* A and B are incompatible *) @@ -756,7 +756,7 @@ split. rewrite {1}/cinde_events -!preim_vars_inter setUid /=. case/Rxx2. (* cPr = 0 *) - move/cPr_eq0/Pr_set0P => Hx. + move/cPr_eq0P/Pr_set0P => Hx. have HAC : Pr P (finset (prod_vars e @^-1 A) :&: finset (prod_vars g @^-1 C)) = 0. apply Pr_set0P => u Hu; apply Hx. @@ -767,8 +767,8 @@ split. by rewrite set_vals_prod_vars. case/boolP: (j \in e) => // je. by rewrite set_vals_tl // set_vals_prod_vars. - rewrite /cinde_events (proj2 (cPr_eq0 _ _ _)). - by rewrite (proj2 (cPr_eq0 _ _ _)) // mul0R. + rewrite /cinde_events (proj2 (cPr_eq0P _ _ _)). + by rewrite (proj2 (cPr_eq0P _ _ _)) // mul0R. apply/Pr_set0P => u Hu. apply(proj1 (Pr_set0P _ _) HAC). move: Hu; by rewrite !inE => /andP[] /andP[] -> _ ->. diff --git a/probability/jfdist_cond.v b/probability/jfdist_cond.v index c41cb4e4..b3a4eee7 100644 --- a/probability/jfdist_cond.v +++ b/probability/jfdist_cond.v @@ -20,7 +20,7 @@ Require Import fdist proba. (* jfdist_cond PQ a == The conditional distribution derived from PQ *) (* given a; same as fdist_cond0 when *) (* fdist_fst PQ a != 0. *) -(* PQ `(| a |) == notation jfdist_cond PQ a *) +(* PQ `(| a ) == notation jfdist_cond PQ a *) (* *) (******************************************************************************) @@ -59,10 +59,10 @@ Lemma jcPr_ge0 E F : 0 <= \Pr_[E | F]. Proof. by rewrite jcPrE. Qed. Lemma jcPr_le1 E F : \Pr_[E | F] <= 1. -Proof. by rewrite jcPrE; exact: cPr_max. Qed. +Proof. by rewrite jcPrE; exact: cPr_le1. Qed. Lemma jcPr_gt0 E F : 0 < \Pr_[E | F] <-> \Pr_[E | F] != 0. -Proof. by rewrite !jcPrE; apply cPr_gt0. Qed. +Proof. by rewrite !jcPrE; apply cPr_gt0P. Qed. Lemma Pr_jcPr_gt0 E F : 0 < Pr P (E `* F) <-> 0 < \Pr_[E | F]. Proof. @@ -73,11 +73,13 @@ 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]. 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]. Proof. rewrite jcPrE DsetT cPr_diff jcPrE; congr (_ - _). diff --git a/probability/proba.v b/probability/proba.v index 0e17c035..8d89a9a3 100644 --- a/probability/proba.v +++ b/probability/proba.v @@ -1328,7 +1328,7 @@ Lemma cPr_ge0 E F : 0 <= `Pr_[E | F]. Proof. rewrite /cPr; have [PF0|PF0] := eqVneq (Pr d F) 0. by rewrite setIC (Pr_domin_setI _ PF0) div0R. -by apply divR_ge0 => //; rewrite Pr_gt0. +by apply divR_ge0 => //; rewrite Pr_gt0P. Qed. Local Hint Resolve cPr_ge0 : core. @@ -1344,7 +1344,7 @@ Proof. rewrite /cPr. have [PF0|PF0] := eqVneq (Pr d F) 0. by rewrite setIC (Pr_domin_setI E PF0) div0R. -apply leR_pdivr_mulr; first by rewrite Pr_gt0. +apply leR_pdivr_mulr; first by rewrite Pr_gt0P. rewrite mul1R /Pr; apply leR_sumRl => //. by move=> a _; apply/RleP; rewrite lexx. by move=> a; rewrite inE => /andP[]. @@ -1364,16 +1364,18 @@ Qed. Lemma Pr_cPr_gt0 E F : 0 < Pr d (E :&: F) <-> 0 < `Pr_[E | F]. Proof. -rewrite Pr_gt0; split => H; last first. +rewrite Pr_gt0P; split => H; last first. by move/cPr_gt0P : H; apply: contra => /eqP; rewrite /cPr => ->; rewrite div0R. -rewrite /cPr; apply/divR_gt0; rewrite Pr_gt0 //. +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 : `Pr_[F1 :\: F2 | E] = `Pr_[F1 | E] - `Pr_[F1 :&: F2 | E]. -Proof. by rewrite /cPr -divRBl setIDAC Pr_diff setIAC. Qed. +Proof. by rewrite /cPr -divRBl setIDAC Pr_setD setIAC. Qed. +(* TODO: rename *) Lemma cPr_union_eq 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. @@ -1556,7 +1558,7 @@ Definition cPr_eq (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) := locked (`Pr_P[ finset (X @^-1 a) | finset (Y @^-1 b)]). Local Notation "`Pr[ X = a | Y = b ]" := (cPr_eq X a Y b). -Lemma cPr_eqE' (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) : +Lemma cPr_eq_def (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) : `Pr[ X = a | Y = b ] = `Pr_P [ finset (X @^-1 a) | finset (Y @^-1 b) ]. Proof. by rewrite /cPr_eq; unlock. Qed. @@ -1565,19 +1567,19 @@ Notation "`Pr[ X = a | Y = b ]" := (cPr_eq X a Y b) : proba_scope. #[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_eq`")] Notation cpr_eq0 := cPr_eq (only parsing). -#[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_eqE`")] -Notation cpr_eqE' := cPr_eqE' (only parsing). +#[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_eq_def`")] +Notation cpr_eqE' := cPr_eq_def (only parsing). 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. +Proof. by rewrite cPr_eq_def cPrET pr_eqE. Qed. Lemma cpr_eqE (U : finType) (P : {fdist U}) (TA TB : eqType) (X : {RV P -> TA}) (Y : {RV P -> TB}) a b : `Pr[ X = a | Y = b ] = `Pr[ [% X, Y] = (a, b) ] / `Pr[Y = b]. Proof. -rewrite cpr_eqE' /cPr /dist_of_RV 2!pr_eqE; congr (Pr _ _ / _). +rewrite cPr_eq_def /cPr /dist_of_RV 2!pr_eqE; congr (Pr _ _ / _). by apply/setP => u; rewrite !inE xpair_eqE. Qed. @@ -1596,7 +1598,7 @@ Proof. by rewrite /cpr_eq_set; unlock. Qed. 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. +by rewrite cpr_eq_setE cPr_eq_def; congr cPr; apply/setP => u; rewrite !inE. Qed. End crandom_variable_finType. @@ -1659,7 +1661,7 @@ Lemma cpr_eq_pairA a b c d : `Pr[ [% TX, [% TY, TZ]] = (a, (b, c)) | TW = d ] = `Pr[ [% TX, TY, TZ] = (a, b, c) | TW = d]. Proof. -rewrite 2!cpr_eqE'; congr (Pr _ _ / _). +rewrite 2!cPr_eq_def; congr (Pr _ _ / _). by apply/setP => u; rewrite !inE /= !xpair_eqE andbA. Qed. @@ -1756,13 +1758,13 @@ Lemma cpr_eq_product_rule (U : finType) (P : {fdist U}) (A B C : eqType) `Pr[ [% X, Y] = (a, b) | Z = c ] = `Pr[ X = a | [% Y, Z] = (b, c) ] * `Pr[ Y = b | Z = c ]. Proof. -rewrite cpr_eqE'. +rewrite cPr_eq_def. 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 _ _ _ * _). +rewrite product_rule_cond cPr_eq_def; congr (cPr _ _ _ * _). - by apply/setP=> u; rewrite !inE xpair_eqE. -- by rewrite cpr_eqE'. +- by rewrite cPr_eq_def. Qed. Lemma reasoning_by_cases (U : finType) (P : {fdist U}) @@ -1807,9 +1809,9 @@ Lemma cinde_rv_events : cinde_rv <-> (forall x y z, cinde_events P (finset (X @^-1 x)) (finset (Y @^-1 y)) (finset (Z @^-1 z))). Proof. split=> [H /= x y z|/= H x y z]. -- rewrite /cinde_events -2!cpr_eqE' -H cpr_eqE'; congr cPr. +- rewrite /cinde_events -2!cPr_eq_def -H cPr_eq_def; congr cPr. by apply/setP => /= ab; rewrite !inE. -- rewrite (cpr_eqE' _ x) (cpr_eqE' _ y) -H cpr_eqE'; congr cPr. +- rewrite (cPr_eq_def _ x) (cPr_eq_def _ y) -H cPr_eq_def; congr cPr. by apply/setP => /= ab; rewrite !inE. Qed.