Skip to content

Commit

Permalink
graphoid
Browse files Browse the repository at this point in the history
  • Loading branch information
@t6s
t6s committed Jul 17, 2024
1 parent 16bf357 commit 11cf6db
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 19 deletions.
39 changes: 25 additions & 14 deletions probability/graphoid.v
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(* infotheo: information theory and error-correcting codes in Coq *)
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
From mathcomp Require Import Rstruct.
From mathcomp Require Import reals.
Require Import realType_ext logb ssr_ext ssralg_ext bigop_ext fdist.
Require Import proba jfdist_cond.

Expand All @@ -26,8 +26,9 @@ Import GRing.Theory.
(* TODO: rename *)
Module Proj124.
Section proj124.
Variables (A B D C : finType) (P : {fdist A * B * D * C}).
Definition d : {fdist A * B * C} := fdistX (fdistA (fdistX (fdistA P)))`2.
Context {R : realType}.
Variables (A B D C : finType) (P : R.-fdist (A * B * D * C)).
Definition d : R.-fdist (A * B * C) := fdistX (fdistA (fdistX (fdistA P)))`2.
Lemma dE abc : d abc = \sum_(x in D) P (abc.1.1, abc.1.2, x, abc.2).
Proof.
case: abc => [[a b] c] /=.
Expand All @@ -39,33 +40,37 @@ Proof. by rewrite /fdist_snd /d !fdistmap_comp. Qed.
End proj124.
End Proj124.

Definition Proj14d (A B C D : finType) (d : {fdist A * B * D * C}) : {fdist A * C} :=
Definition Proj14d {R : realType} (A B C D : finType) (d : R.-fdist (A * B * D * C)) :
R.-fdist (A * C) :=
fdist_proj13 (Proj124.d d).

(* TODO: rename *)
Module QuadA23.
Section def.
Variables (A B C D : finType) (P : {fdist A * B * D * C}).
Context {R : realType}.
Variables (A B C D : finType) (P : R.-fdist (A * B * D * C)).
Definition f (x : A * B * D * C) : A * (B * D) * C :=
(x.1.1.1, (x.1.1.2, x.1.2), x.2).
Lemma inj_f : injective f.
Proof. by rewrite /f => -[[[? ?] ?] ?] [[[? ?] ?] ?] /= [-> -> -> ->]. Qed.
Definition d : {fdist A * (B * D) * C} := fdistmap f P.
Definition d : R.-fdist (A * (B * D) * C) := fdistmap f P.
Lemma dE x : d x = P (x.1.1, x.1.2.1, x.1.2.2, x.2).
Proof.
case: x => -[a [b d] c]; rewrite /def.d fdistmapE /= -/(f (a, b, d, c)).
by rewrite (big_pred1_inj inj_f).
Qed.
End def.
Section prop.
Variables (A B C D : finType) (P : {fdist A * B * D * C}).
Context {R : realType}.
Variables (A B C D : finType) (P : R.-fdist (A * B * D * C)).
Lemma snd : (QuadA23.d P)`2 = P`2.
Proof. by rewrite /fdist_snd /d fdistmap_comp. Qed.
End prop.
End QuadA23.

Section cinde_rv_prop.
Variables (U : finType) (P : {fdist U}) (A B C D : finType).
Context {R : realType}.
Variables (U : finType) (P : R.-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 cinde_drv_2C : P |= X _|_ [% Y, W] | Z -> P |= X _|_ [% W, Y] | Z.
Expand All @@ -84,7 +89,8 @@ End cinde_rv_prop.

Section symmetry.

Variable (U : finType) (P : {fdist U}).
Context {R : realType}.
Variable (U : finType) (P : R.-fdist U).
Variables (A B C : finType) (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}).

Lemma symmetry : P |= X _|_ Y | Z -> P |= Y _|_ X | Z.
Expand All @@ -100,7 +106,8 @@ End symmetry.

Section decomposition.

Variables (U : finType) (P : {fdist U}) (A B C D : finType).
Context {R : realType}.
Variables (U : finType) (P : R.-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 decomposition : P |= X _|_ [% Y, W] | Z -> P |= X _|_ Y | Z.
Expand All @@ -122,7 +129,8 @@ End decomposition.

Section weak_union.

Variables (U : finType) (P : {fdist U}) (A B C D : finType).
Context {R : realType}.
Variables (U : finType) (P : R.-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 weak_union : P |= X _|_ [% Y, W] | Z -> P |= X _|_ Y | [% Z, W].
Expand All @@ -146,7 +154,8 @@ End weak_union.

Section contraction.

Variables (U : finType) (P : {fdist U}) (A B C D : finType).
Context {R : realType}.
Variables (U : finType) (P : R.-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 contraction : P |= X _|_ W | [% Z, Y] -> P |= X _|_ Y | Z -> P |= X _|_ [% Y, W] | Z.
Expand All @@ -170,7 +179,8 @@ End contraction.
(* Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference, Pearl, p.88 *)
Section derived_rules.

Variables (U : finType) (P : {fdist U}) (A B C D : finType).
Context {R : realType}.
Variables (U : finType) (P : R.-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 chaining_rule : P |= X _|_ Z | Y /\ P |= [% X, Y] _|_ W | Z -> P |= X _|_ W | Y.
Expand All @@ -192,7 +202,8 @@ End derived_rules.

Section intersection.

Variables (U : finType) (P : {fdist U}) (A B C D : finType).
Context {R : realType}.
Variables (U : finType) (P : R.-fdist U) (A B C D : finType).
Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).

Hypothesis P0 : forall b c d, `Pr[ [% Y, Z, W] = (b, c, d) ] != 0.
Expand Down
9 changes: 4 additions & 5 deletions probability/jensen.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
From mathcomp Require Import boolp Rstruct.
Require Import Reals.
Require Import ssrR Reals_ext ssr_ext realType_ext ssralg_ext logb.
Require Import ssrR realType_ext ssr_ext realType_ext ssralg_ext logb.
Require Import fdist proba convex.

(******************************************************************************)
Expand All @@ -14,7 +13,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Local Open Scope R_scope.
Local Open Scope ring_scope.
Local Open Scope reals_ext_scope.
Local Open Scope convex_scope.
Local Open Scope fdist_scope.
Expand Down Expand Up @@ -80,8 +79,8 @@ Lemma Jensen (P : {fdist A}) (X : {RV P -> R}) : (forall x, X x \in D) ->
f (`E X) <= `E (f `o X).
Proof.
move=> H.
rewrite {2}/Ex; erewrite eq_bigr; last by move=> a _; rewrite mulRC.
rewrite {1}/Ex; erewrite eq_bigr; last by move=> a _; rewrite mulRC.
rewrite {2}/Ex; erewrite eq_bigr; last by move=> a _; rewrite mulrC.
rewrite {1}/Ex; erewrite eq_bigr; last by move=> a _; rewrite mulrC.
exact: jensen_dist H.
Qed.

Expand Down

0 comments on commit 11cf6db

Please sign in to comment.