Library probsa.probability.independence
From prosa Require Import classic.util.list.
From probsa.util Require Export zip bigop r_mult tr_eq.
From probsa.probability Require Export conditional.
Lemma pr_cond_indep2 :
∀ {Ω : countType} {μ : measure Ω} (A B : pred Ω) ρ,
indep2 (mkRvar μ A) (mkRvar μ B) →
ℙ<μ,ρ>{[ A | B ]} = ℙ<μ>{[ A ]}.
Section Indep2.
Section IndepExt.
Context {Ω : countType} {μ : measure Ω} (B1 B2 C1 C2 : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ C1) (Y1 : rvar μ B2) (Y2 : rvar μ C2).
Variables (f1 : B1 → C1) (f2 : B2 → C2).
Lemma indep2_fn_ext :
(∀ ω, μ ω > 0 → rvar_comp X1 f1 ω = X2 ω) →
(∀ ω, μ ω > 0 → rvar_comp Y1 f2 ω = Y2 ω) →
indep2 X1 Y1 →
indep2 X2 Y2.
End IndepExt.
Section IndepExtL.
Context {Ω : countType} {μ: measure Ω} (B1 B2 C : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ B2) (Y : rvar μ C).
Variable f : B1 → B2.
Lemma indep2_fn_extl :
(∀ ω, μ ω > 0 → rvar_comp X1 f ω = X2 ω) →
indep2 X1 Y →
indep2 X2 Y.
End IndepExtL.
End Indep2.
Section IndependentCat.
Context {Ω} {μ : measure Ω} {T : eqType}.
Lemma indep_catC :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent (ys ++ xs).
Lemma indep_cat_split :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent xs ∧ independent ys.
Lemma indep_cat_indep2_list :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_list xs) (rvar_list ys).
Fact indep_cat_indep2_list_comp :
∀ (f : seq T → nat) (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_comp (rvar_list xs) f) (rvar_comp (rvar_list ys) f).
End IndependentCat.
Section IndependentMap.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → rvar μ B.
Lemma indep_perm_eq :
∀ (xs ys : seq A),
perm_eq xs ys →
independent [seq F i | i <- xs] →
independent [seq F i | i <- ys].
Lemma indep_filter :
∀ (P : pred A) (xs : seq A),
independent [seq F i | i <- xs] →
independent [seq F i | i <- xs & P i].
Lemma indep_subset :
∀ (xs ys : seq A),
(∀ x, x \in xs → x \in ys) →
uniq xs →
uniq ys →
independent [seq F y | y <- ys] →
independent [seq F x | x <- xs].
Lemma indep_comp :
∀ {C : eqType} (f : B → C) (xs : seq A),
independent [seq F x | x <- xs] →
independent [seq rvar_comp (F x) f | x <- xs].
Lemma indep_irr :
∀ (G : A → rvar μ B) (xs : seq A),
(∀ x ω, x \in xs → μ ω > 0 → F x ω = G x ω) →
independent [seq F x | x <- xs] →
independent [seq G x | x <- xs].
End IndependentMap.
Section IndependentPair.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Lemma indep_pair_swap :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Ω → Z),
independent [seq (mkRvar μ (fun ω ⇒ (B x ω, A x ω))) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x ω))) | x <- xs].
Lemma indep_pair_const_r :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Z),
independent [seq (mkRvar μ (A x)) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x))) | x <- xs].
End IndependentPair.
Section IndependentFlatten.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Variable f : X → Ω → Y → Z.
Variables (xs : seq X) (ys : X → seq Y).
Lemma independent_flatten :
independent [seq mkRvar μ (fun ω ⇒ f x ω y) | x <- xs, y <- ys x] →
independent [seq mkRvar μ (fun ω ⇒ [ seq f x ω y | y <- ys x]) | x <- xs].
End IndependentFlatten.
Section IndependentExtend.
Context {Ω} {μ : measure Ω} {X Y : eqType}.
Variable F : X → rvar μ Y.
Lemma indep_consts :
∀ (xs : seq X),
(∀ x, x \in xs → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs].
Lemma indep_extend_consts :
∀ (xs1 xs2 : seq X),
(∀ x, x \in xs2 → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs1] →
independent [seq F x | x <- xs1 ++ xs2].
End IndependentExtend.
Section IndependentSum.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → nrvar μ.
Lemma indep2_sum :
∀ (P : pred A) (xs ys : seq A),
independent [seq F i | i <- xs ++ ys] →
indep2 (∑[rv]_{x <- xs | P x} F x) (∑[rv]_{y <- ys | P y} F y).
Lemma indep2_sum_cons :
∀ (x : A) (xs : seq A),
independent [seq F i | i <- x::xs] →
indep2 (F x) (∑[rv]_{x <- xs} F x).
End IndependentSum.
From probsa.util Require Export zip bigop r_mult tr_eq.
From probsa.probability Require Export conditional.
Lemma pr_cond_indep2 :
∀ {Ω : countType} {μ : measure Ω} (A B : pred Ω) ρ,
indep2 (mkRvar μ A) (mkRvar μ B) →
ℙ<μ,ρ>{[ A | B ]} = ℙ<μ>{[ A ]}.
Section Indep2.
Section IndepExt.
Context {Ω : countType} {μ : measure Ω} (B1 B2 C1 C2 : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ C1) (Y1 : rvar μ B2) (Y2 : rvar μ C2).
Variables (f1 : B1 → C1) (f2 : B2 → C2).
Lemma indep2_fn_ext :
(∀ ω, μ ω > 0 → rvar_comp X1 f1 ω = X2 ω) →
(∀ ω, μ ω > 0 → rvar_comp Y1 f2 ω = Y2 ω) →
indep2 X1 Y1 →
indep2 X2 Y2.
End IndepExt.
Section IndepExtL.
Context {Ω : countType} {μ: measure Ω} (B1 B2 C : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ B2) (Y : rvar μ C).
Variable f : B1 → B2.
Lemma indep2_fn_extl :
(∀ ω, μ ω > 0 → rvar_comp X1 f ω = X2 ω) →
indep2 X1 Y →
indep2 X2 Y.
End IndepExtL.
End Indep2.
Section IndependentCat.
Context {Ω} {μ : measure Ω} {T : eqType}.
Lemma indep_catC :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent (ys ++ xs).
Lemma indep_cat_split :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent xs ∧ independent ys.
Lemma indep_cat_indep2_list :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_list xs) (rvar_list ys).
Fact indep_cat_indep2_list_comp :
∀ (f : seq T → nat) (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_comp (rvar_list xs) f) (rvar_comp (rvar_list ys) f).
End IndependentCat.
Section IndependentMap.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → rvar μ B.
Lemma indep_perm_eq :
∀ (xs ys : seq A),
perm_eq xs ys →
independent [seq F i | i <- xs] →
independent [seq F i | i <- ys].
Lemma indep_filter :
∀ (P : pred A) (xs : seq A),
independent [seq F i | i <- xs] →
independent [seq F i | i <- xs & P i].
Lemma indep_subset :
∀ (xs ys : seq A),
(∀ x, x \in xs → x \in ys) →
uniq xs →
uniq ys →
independent [seq F y | y <- ys] →
independent [seq F x | x <- xs].
Lemma indep_comp :
∀ {C : eqType} (f : B → C) (xs : seq A),
independent [seq F x | x <- xs] →
independent [seq rvar_comp (F x) f | x <- xs].
Lemma indep_irr :
∀ (G : A → rvar μ B) (xs : seq A),
(∀ x ω, x \in xs → μ ω > 0 → F x ω = G x ω) →
independent [seq F x | x <- xs] →
independent [seq G x | x <- xs].
End IndependentMap.
Section IndependentPair.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Lemma indep_pair_swap :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Ω → Z),
independent [seq (mkRvar μ (fun ω ⇒ (B x ω, A x ω))) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x ω))) | x <- xs].
Lemma indep_pair_const_r :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Z),
independent [seq (mkRvar μ (A x)) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x))) | x <- xs].
End IndependentPair.
Section IndependentFlatten.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Variable f : X → Ω → Y → Z.
Variables (xs : seq X) (ys : X → seq Y).
Lemma independent_flatten :
independent [seq mkRvar μ (fun ω ⇒ f x ω y) | x <- xs, y <- ys x] →
independent [seq mkRvar μ (fun ω ⇒ [ seq f x ω y | y <- ys x]) | x <- xs].
End IndependentFlatten.
Section IndependentExtend.
Context {Ω} {μ : measure Ω} {X Y : eqType}.
Variable F : X → rvar μ Y.
Lemma indep_consts :
∀ (xs : seq X),
(∀ x, x \in xs → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs].
Lemma indep_extend_consts :
∀ (xs1 xs2 : seq X),
(∀ x, x \in xs2 → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs1] →
independent [seq F x | x <- xs1 ++ xs2].
End IndependentExtend.
Section IndependentSum.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → nrvar μ.
Lemma indep2_sum :
∀ (P : pred A) (xs ys : seq A),
independent [seq F i | i <- xs ++ ys] →
indep2 (∑[rv]_{x <- xs | P x} F x) (∑[rv]_{y <- ys | P y} F y).
Lemma indep2_sum_cons :
∀ (x : A) (xs : seq A),
independent [seq F i | i <- x::xs] →
indep2 (F x) (∑[rv]_{x <- xs} F x).
End IndependentSum.