cleaning

- renamed cinde.v
- remove useless import of topology
- minor PRs to mathcomp-analysis

fixes #18

_CoqProject

@@ -29,7 +29,7 @@ probability/fsdist.v
 probability/convex_choice.v
 probability/convex_stone.v
 probability/jfdist.v
-probability/cinde.v
+probability/graphoid.v
 probability/jensen.v
 probability/ln_facts.v
 probability/divergence.v

changelog.txt

@@ -1,6 +1,8 @@
 -----------------
-from 0.1.2 to ???
+from 0.1.2 to 0.2
 -----------------
+warning: this changelog entry is not exhaustive
+
 - renamed:
   + in Rbigop.v:
     * rsumr_ge0 -> sumR_ge0, rsumr_gt0 -> sumR_gt0
@@ -63,6 +65,7 @@ from 0.1.2 to ???
   + cpr_in_Eset1, cpr_in_set1F
   + reasoning_by_cases, creasoning_by_cases
   + cpr_in_pair* lemmas in proba.v
+  + cinde.v -> graphoid.v
 - changed:
   + generalize pr_geq to any porderType
   + definition of notation @^-1 now uses preim instead of finset notations
@@ -78,7 +81,7 @@ from 0.1.2 to ???
   + Pr_domin_snd
   + RVarPr
   + most marginal_* lemmas and technical lemmas from cinde.v
-  + RV_Pr_lC, etc. from cinde.v
+  + RV_Pr_lC, etc., RV2_Pr*congr* lemmas, from cinde.v
 
 ---------------------
 from 0.1.1 to 0.1.2 :

information_theory/chap2.v

@@ -89,7 +89,6 @@ Qed.
 End rV.
 End JointEntropy.
 
-Require Import cinde.
 Section notation_with_random_variables.
 Section jointentropy_drv.
 Variables (U A B : finType) (P : {fdist U}) (X : {RV P -> A}) (Y : {RV P -> B}).

information_theory/convex_fdist.v

@@ -397,7 +397,7 @@ Variables (A B : finType) (P : fdist A).
 Local Open Scope divergence_scope.
 
 Lemma mutual_information_convex :
-  convex_function (fun Q : depfun_choiceType (fun _ : A => fdist_convType B) =>
+  convex_function (fun Q : dep_arrow_choiceType (fun _ : A => fdist_convType B) =>
     MutualInfo.mi (CJFDist.make_joint P Q)).
 Proof.
 move=> p1yx p2yx t.

lib/classical_sets_ext.v

@@ -54,12 +54,13 @@ apply eqEsubset=> a;
   by [case=> i Pi ->; apply imageP | case=> i Pi <-; exists i].
 Qed.
 
+(* TODO: PR in progress in mathcomp-analysis *)
 Lemma bigcup_set0 (X : U -> set T) : \bigcup_(i in set0) X i = set0.
 Proof. by apply eqEsubset => a // [] //. Qed.
 
-(* NB: less general lemma with the same name in mathcomp-analysis *)
 Lemma bigcup_set1 (i : U) (X : U -> set T) : \bigcup_(i in [set i]) X i = X i.
 Proof. apply eqEsubset => a; by [case=> j -> | exists i]. Qed.
+(* TODO: end PR *)
 
 Lemma bigcup_image V (P : set V) (f : V -> U) (X : U -> set T) :
   \bigcup_(x in f @` P) X x = \bigcup_(x in P) X (f x).

probability/convex_choice.v

@@ -115,6 +115,14 @@ Import Prenex Implicits.
 Local Open Scope reals_ext_scope.
 Local Open Scope proba_scope.
 
+(* TODO: PR to mathcomp-analysis in progress *)
+Section depfun.
+Variable (I : Type) (T : I -> choiceType).
+Definition depfun_choiceClass :=
+  Choice.Class (Equality.class (dep_arrow_eqType T)) gen_choiceMixin.
+Definition dep_arrow_choiceType := Choice.Pack depfun_choiceClass.
+End depfun.
+
 Section tmp.
 Variables (n m : nat) (d1 : {fdist 'I_n}) (d2 : {fdist 'I_m}) (p : prob).
 Lemma ConvnFDist_Add (A : finType) (g : 'I_n -> fdist A) (h : 'I_m -> fdist A) :
@@ -1939,19 +1947,9 @@ Definition funConvMixin := ConvexSpace.Mixin avg1 avgI avgC avgA.
 Canonical funConvType := ConvexSpace.Pack (ConvexSpace.Class funConvMixin).
 End fun_convex_space.
 
-From mathcomp Require Import topology.
-
-(* TODO: move to topology? *)
-Section depfun.
-Variable (I : Type) (T : I -> choiceType).
-Definition depfun_choiceClass :=
-  Choice.Class (Equality.class (dep_arrow_eqType T)) gen_choiceMixin.
-Definition depfun_choiceType := Choice.Pack depfun_choiceClass.
-End depfun.
-
 Section depfun_convex_space.
 Variables (A : choiceType) (B : A -> convType).
-Let T := depfun_choiceType B.
+Let T := dep_arrow_choiceType B.
 Implicit Types p q : prob.
 Let avg p (x y : T) := fun a : A => (x a <| p |> y a).
 Let avg1 (x y : T) : avg 1%:pr x y = x.

probability/cinde.v → probability/graphoid.v

@@ -5,46 +5,40 @@ Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop fdist.
 Require Import proba jfdist.
 
 (******************************************************************************)
-(*   Conditional independence over joint distributions and graphoid axioms    *)
+(*                              Graphoid axioms                               *)
 (*                                                                            *)
-(*         X _|_  Y | Z == X is conditionally independent of Y given Z in the *)
-(*                      distribution P for all values a, b, and c (belonging  *)
-(*                      resp. to the codomains of X, Y , and Z); equivalent   *)
-(*                      to P |= X _|_ Y | Z from proba.v                      *)
-(* \Pr[ X = a | Y = b ] == probability that the random variable X is a        *)
-(*                         knowing that the random variable Y is b            *)
-(*                                                                            *)
-(* Lemmas:                                                                    *)
-(*  Graphoid axioms: symmetry, decomposition, weak_union, contraction,        *)
-(*  intersection, derived rules                                               *)
+(* The main purpose of this file is to provide a formalization of the         *)
+(* graphoid axioms (symmetry, decomposition, weak_union, contraction, and     *)
+(* intersection) and derived rules.                                           *)
 (******************************************************************************)
 
 (*
 contents:
 - Various distributions (Proj124.d, Proj14d, QuadA23.d)
-- Section pair_of_RVs.
 - Section RV2_prop.
 - Section RV3_prop.
-- Section conditionnally_independent_discrete_random_variables.
 *)
 
-Reserved Notation "X _|_  Y | Z" (at level 50, Y, Z at next level).
-Reserved Notation "\Pr[ X '\in' E | Y '\in' F ]" (at level 6, X, Y, E, F at next level,
-  format "\Pr[  X  '\in'  E  |  Y  '\in'  F  ]").
-Reserved Notation "\Pr[ X '\in' E | Y = b ]" (at level 6, X, Y, E, b at next level,
-  format "\Pr[  X  '\in'  E  |  Y  =  b  ]").
-Reserved Notation "\Pr[ X = a | Y '\in' F ]" (at level 6, X, Y, a, F at next level,
-  format "\Pr[  X  =  a  |  Y  '\in'  F  ]").
-Reserved Notation "\Pr[ X = a | Y = b ]" (at level 6, X, Y, a, b at next level,
-  format "\Pr[  X  =  a  |  Y  =  b  ]").
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
 Local Open Scope R_scope.
 Local Open Scope proba_scope.
 
+(* TODO: move? *)
+Section setX_structural_lemmas.
+Variables (A B C : finType).
+Variables (E : {set A}) (F : {set B}).
+
+Lemma imset_fst b : b \in F -> [set x.1 | x in E `* F] = E.
+Proof.
+move=> bF; apply/setP => a; apply/imsetP/idP.
+- by rewrite ex2C; move=> -[[a' b']] /= ->; rewrite inE => /andP [] ->.
+- by move=> aE; exists (a, b); rewrite // inE; apply/andP; split.
+Qed.
+
+End setX_structural_lemmas.
 Module Proj124.
 Section proj124.
 Variables (A B D C : finType) (P : {fdist A * B * D * C}).
@@ -85,20 +79,11 @@ Proof. by rewrite /Bivar.snd /d FDistMap.comp. Qed.
 End prop.
 End QuadA23.
 
-Notation "\Pr[ X '\in' E | Y '\in' F ]" := (\Pr_(`d_[% X, Y])[ E | F ]).
-Notation "\Pr[ X '\in' E | Y = b ]" := (\Pr[ X \in E | Y \in [set b]]).
-Notation "\Pr[ X = a | Y '\in' F ]" := (\Pr[ X \in [set a] | Y \in F]).
-Notation "\Pr[ X = a | Y = b ]" := (\Pr[ X \in [set a] | Y \in [set b]]).
-
 Section RV2_prop.
 Variables (U : finType) (P : fdist U).
 Variables (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}).
 Implicit Types (E : {set A}) (F : {set B}).
 
-Goal forall a b, \Pr[ X = a | Y = b ] = \Pr_(FDistMap.d [% X, Y] P)[ [set a] | [set b] ].
-by [].
-Abort.
-
 Lemma RV20 : fst \o [% X, unit_RV P] =1 X.
 Proof. by []. Qed.
 
@@ -128,43 +113,11 @@ Proof. by rewrite /TripC12.d /dist_of_RV /TripA.d FDistMap.comp. Qed.
 
 End RV3_prop.
 
-(* TODO: move *)
-Section setX_structural_lemmas.
-Variables (A B C : finType).
-Variables (E : {set A}) (F : {set B}).
-
-Lemma imset_fst b : b \in F -> [set x.1 | x in E `* F] = E.
-Proof.
-move=> bF; apply/setP => a; apply/imsetP/idP.
-- by rewrite ex2C; move=> -[[a' b']] /= ->; rewrite inE => /andP [] ->.
-- by move=> aE; exists (a, b); rewrite // inE; apply/andP; split.
-Qed.
-
-End setX_structural_lemmas.
-
-Section conditionnally_independent_discrete_random_variables.
-
-Variables (U : finType) (P : fdist U) (A B C : finType).
-Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}).
-
-Definition jcinde_rv := forall a b c,
-  \Pr[ [% X, Y] = (a, b) | Z = c ] = \Pr[ X = a | Z = c ] * \Pr[ Y = b | Z = c].
-
-End conditionnally_independent_discrete_random_variables.
-
-Notation "X _|_  Y | Z" := (jcinde_rv X Y Z) : proba_scope.
-
 Section cinde_rv_prop.
 
 Variables (U : finType) (P : fdist U) (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 
-Lemma jcinde_cinde_rv : X _|_ Y | Z <-> P |= X _|_ Y | Z.
-Proof.
-split; rewrite /jcinde_rv /cinde_rv; by
-  move=> H a b c; have {H} := H a b c; rewrite 3!jcPrE -!cpr_inE' !cpr_eq_set1.
-Qed.
-
 Lemma cinde_drv_2C : P |= X _|_ [% Y, W] | Z -> P |= X _|_ [% W, Y] | Z.
 Proof.
 move=> H a -[d b] c.
@@ -366,38 +319,3 @@ by rewrite pr_eq_pairC => ->.
 Qed.
 
 End intersection.
-
-(* wip*)
-
-Section vector_of_RVs.
-Variables (U : finType) (P : fdist U).
-Variables (A : finType) (n : nat) (X : 'rV[{RV P -> A}]_n).
-Local Open Scope ring_scope.
-Local Open Scope vec_ext_scope.
-Definition RVn : {RV P -> 'rV[A]_n} := fun x => \row_(i < n) (X ``_ i) x.
-End vector_of_RVs.
-
-Section prob_chain_rule.
-Variables (U : finType) (P : {fdist U}).
-Variables (A : finType) .
-Local Open Scope vec_ext_scope.
-Lemma prob_chain_rule : forall (n : nat) (X : 'rV[{RV P -> A}]_n.+1) x,
-  `Pr[ (RVn X) = x ] =
-  \prod_(i < n.+1)
-    if i == ord0 then
-      `Pr[ (X ``_ ord0) = (x ``_ ord0)   ]
-    else
-      \Pr[ (X ``_ i) = (x ``_ i) |
-        (RVn (row_drop (inord (n - i.+1)) X)) = (row_drop (inord (n - i.+1)) x) ].
-Proof.
-elim => [X /= x|n ih X /= x].
-  rewrite big_ord_recl big_ord0 mulR1.
-  rewrite /pr_eq; unlock.
-  apply eq_bigl => u.
-  rewrite !inE /RVn.
-  apply/eqP/eqP => [<-|H]; first by rewrite mxE.
-  by apply/rowP => i; rewrite {}(ord1 i) !mxE.
-rewrite big_ord_recr /=.
-Abort.
-
-End prob_chain_rule.

probability/proba.v

@@ -34,8 +34,9 @@ Require Import fdist.
 (*  `Pr_P [ A | B ] == conditional probability for events                     *)
 (*  `Pr[ X = a | Y = b ], `Pr[ X \in E | Y \in F ] == conditional probability *)
 (*                     for random variables                                   *)
-(*  P |= X _|_ Y | Z == the random variable X is conditionally independent of *)
-(*                     the random variable Y given Z in a distribution P      *)
+(*  P |= X _|_ Y | Z, X _|_  Y | Z == the random variable X is conditionally  *)
+(*                     independent of the random variable Y given Z in a      *)
+(*                     distribution P                                          *)
 (*  P |= X _|_ Y    == unconditional independence                             *)
 (*  Z \= X @+ Y     == Z is the sum of two random variables                   *)
 (*  X \=sum Xs      == X is the sum of the n>=1 independent and identically   *)
@@ -110,6 +111,7 @@ Reserved Notation "`Pr[ X '\in' E | Y = F ]" (at level 6, X, Y, E, F at next lev
   format "`Pr[  X  '\in'  E  |  Y  =  F  ]").
 Reserved Notation "`Pr[ X = E | Y '\in' F ]" (at level 6, X, Y, E, F at next level,
   format "`Pr[  X  =  E  |  Y  '\in'  F  ]").
+Reserved Notation "X _|_  Y | Z" (at level 50, Y, Z at next level).
 Reserved Notation "P |= X _|_  Y | Z" (at level 50, X, Y, Z at next level).
 Reserved Notation "P |= X _|_ Y" (at level 50, X, Y at next level,
   format "P  |=  X  _|_  Y").
@@ -1645,6 +1647,7 @@ Qed.
 End conditionnally_independent_discrete_random_variables.
 
 Notation "P |= X _|_  Y | Z" := (@cinde_rv _ P _ _ _ X Y Z) : proba_scope.
+Notation "X _|_  Y | Z" := (cinde_rv X Y Z) : proba_scope.
 
 Section independent_rv.
 
@@ -2038,3 +2041,38 @@ by move/leR_trans: (chebyshev_inequality (X `/ n.+1) e0); apply; exact/leRR.
 Qed.
 
 End weak_law_of_large_numbers.
+
+(* wip*)
+
+Section vector_of_RVs.
+Variables (U : finType) (P : fdist U).
+Variables (A : finType) (n : nat) (X : 'rV[{RV P -> A}]_n).
+Local Open Scope ring_scope.
+Local Open Scope vec_ext_scope.
+Definition RVn : {RV P -> 'rV[A]_n} := fun x => \row_(i < n) (X ``_ i) x.
+End vector_of_RVs.
+
+Section prob_chain_rule.
+Variables (U : finType) (P : {fdist U}).
+Variables (A : finType) .
+Local Open Scope vec_ext_scope.
+Lemma prob_chain_rule : forall (n : nat) (X : 'rV[{RV P -> A}]_n.+1) x,
+  `Pr[ (RVn X) = x ] =
+  \prod_(i < n.+1)
+    if i == ord0 then
+      `Pr[ (X ``_ ord0) = (x ``_ ord0)   ]
+    else
+      `Pr[ (X ``_ i) = (x ``_ i) |
+        (RVn (row_drop (inord (n - i.+1)) X)) = (row_drop (inord (n - i.+1)) x) ].
+Proof.
+elim => [X /= x|n ih X /= x].
+  rewrite big_ord_recl big_ord0 mulR1.
+  rewrite /pr_eq; unlock.
+  apply eq_bigl => u.
+  rewrite !inE /RVn.
+  apply/eqP/eqP => [<-|H]; first by rewrite mxE.
+  by apply/rowP => i; rewrite {}(ord1 i) !mxE.
+rewrite big_ord_recr /=.
+Abort.
+
+End prob_chain_rule.