Library discprob.prob.indep
Require Export Reals Psatz Omega.
From discprob.prob Require Export prob countable stochastic_order markov double.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.
Definition independent {A} {B: eqType} {Ω: distrib A} (l: list (rvar Ω B)) :=
∀ lb, length lb = length l →
pr Ω (λ a, fold_right andb true (map (λ Xb, (rvar_fun _ _ (fst Xb)) a == (snd Xb))
(seq.zip l lb)))
= fold_right Rmult 1 (map (λ Xb, pr_eq (fst Xb) (snd Xb)) (seq.zip l lb)).
Definition indep2 {A} {B1 B2: eqType} {Ω: distrib A} (X: rvar Ω B1) (Y: rvar Ω B2) :=
∀ b1 b2, pr Ω (λ a, (X a == b1) && (Y a == b2)) =
pr_eq X b1 × pr_eq Y b2.
Lemma indep2_pair_var {A} {B1 B2: eqType} {Ω: distrib A} (X: rvar Ω B1) (Y: rvar Ω B2) :
indep2 X Y →
(∀ b1 b2, pr_eq (mkRvar Ω (λ a, (X a, Y a))) (b1, b2) =
pr_eq X b1 × pr_eq Y b2).
Lemma zip_nil {S T: Type} (s: seq.seq T) : seq.zip (@nil S) s = nil.
Lemma independent_tl {A} {B: eqType} {Ω: distrib A} (X: rvar Ω B) (lX: list (rvar Ω B)):
independent (X :: lX) → independent lX.
Lemma indep2_indendent {A} {B: eqType} {Ω: distrib A} (X Y: rvar Ω B) :
indep2 X Y ↔ independent (X :: Y :: nil).
Section joint_pr.
Variable (A: countType).
Variable (B1 B2: eqType).
Variable (Ω: distrib A).
Variable (X1 : rvar Ω B1).
Variable (X2 : rvar Ω B2).
Variable P: pred (B1).
Variable Q: pred (B2).
Variable (INDEP: indep2 X1 X2).
Lemma imgT_pr1 ab:
ab \in img (λ x : A, (X1 x, X2 x)) → (fst ab) \in img X1.
Lemma imgT_pr2 ab:
ab \in img (λ x : A, (X1 x, X2 x)) → (snd ab) \in img X2.
Definition σprod : nat → nat × nat.
Definition aprod :=
λ mn, match mn with
| (S m, S n) ⇒
match (@pickle_inv [countType of (imgT X1)] m),
(@pickle_inv [countType of (imgT X2)] n) with
| Some a, Some b ⇒
if P (sval a) && Q (sval b) then
pr_eq X1 (sval a) × pr_eq X2 (sval b)
else
0
| _, _ ⇒ 0
end
| _ ⇒ 0
end.
Lemma aprod_double_summable: double_summable aprod.
Lemma σprod_inj: ∀ n n', aprod (σprod n) ≠ 0 → σprod n = σprod n' → n = n'.
Lemma σprod_cov: ∀ n, aprod n ≠ 0 → ∃ m, σprod m = n.
Lemma is_series_prod_row:
is_series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
if P (fst (sval ab)) && Q (snd (sval ab)) then
pr_eq X1 (fst (sval ab)) × pr_eq X2 (snd (sval ab))
else
0))
(Series (λ j, Series (λ k, aprod (S j, S k)))).
Lemma Series_prod_row:
Series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
if P (fst (sval ab)) && Q (snd (sval ab)) then
pr_eq X1 (fst (sval ab)) × pr_eq X2 (snd (sval ab))
else
0)) =
(Series (λ j, Series (λ k, aprod (S j, S k)))).
Lemma indep2_pred:
pr Ω (λ a, P (X1 a) && Q (X2 a)) =
pr Ω (λ a, P (X1 a)) × pr Ω (λ a, Q (X2 a)).
End joint_pr.
Section exp.
Variable (A: countType).
Variable (B1 B2: eqType).
Variable (Ω: distrib A).
Variable (X1 X2 : rrvar Ω).
Variable (INDEP: indep2 X1 X2).
Variable (EX1: ex_Ex X1).
Variable (EX2: ex_Ex X2).
Definition σprod_exp : nat → nat × nat.
Definition aprod_exp :=
λ mn, match mn with
| (S m, S n) ⇒
match (@pickle_inv [countType of (imgT X1)] m),
(@pickle_inv [countType of (imgT X2)] n) with
| Some a, Some b ⇒
(sval a × pr_eq X1 (sval a)) × (sval b × pr_eq X2 (sval b))
| _, _ ⇒ 0
end
| _ ⇒ 0
end.
Lemma aprod_exp_double_summable: double_summable aprod_exp.
Lemma σprod_exp_inj: ∀ n n', aprod_exp (σprod_exp n) ≠ 0 → σprod_exp n = σprod_exp n' → n = n'.
Lemma σprod_exp_cov: ∀ n, aprod_exp n ≠ 0 → ∃ m, σprod_exp m = n.
Lemma is_series_prod_exp_row:
is_series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
(pr_eq (mkRvar Ω (λ a, (X1 a, X2 a))) (sval ab)
× (fst (sval ab) × snd (sval ab)))))
(Series (λ j, Series (λ k, aprod_exp (S j, S k)))).
Lemma is_series_prod_exp_row_abs:
is_series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
(pr_eq (mkRvar Ω (λ a, (X1 a, X2 a))) (sval ab)
× Rabs (fst (sval ab) × snd (sval ab)))))
(Series (λ j, Series (λ k, Rabs (aprod_exp (S j, S k))))).
Lemma Series_prod_exp_row:
Series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
(pr_eq (mkRvar Ω (λ a, (X1 a, X2 a))) (sval ab)
× (fst (sval ab) × snd (sval ab))))) =
(Series (λ j, Series (λ k, aprod_exp (S j, S k)))).
Lemma indep2_ex_Ex_prod :
ex_Ex (mkRvar Ω (λ a, X1 a × X2 a)).
Lemma indep2_Ex_prod :
Ex (mkRvar Ω (λ a, X1 a × X2 a)) = Ex X1 × Ex X2.
End exp.
Lemma indep2_fn {A} {B1 B2 C1 C2: eqType} {Ω: distrib A} (X: rvar Ω B1) (Y: rvar Ω B2)
(f1: B1 → C1) (f2: B2 → C2):
indep2 X Y → indep2 (rvar_comp X f1) (rvar_comp Y f2).
Lemma rvar_list_eq_foldr {A} {B: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) bl i:
length bl = length lX →
((rvar_list lX) i == bl
↔ fold_right andb true (List.map (λ Xb : rvar Ω B × B, Xb.1 i == Xb.2) (zip lX bl))).
Lemma rvar_list_eq_short {A} {B: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) bl:
length bl ≠ length lX →
∀ i, ((rvar_list lX) i == bl) = false.
Lemma independent_rvar_list {A} {B: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) :
independent lX →
∀ bl, length bl = length lX →
pr_eq (rvar_list lX) bl =
fold_right Rmult 1 (map (λ Xb, pr_eq (fst Xb) (snd Xb)) (seq.zip lX bl)).
Lemma independent_indep2_tl {A} {B: eqType} {Ω: distrib A} (X: rvar Ω B) (lX: list (rvar Ω B)) :
independent (X :: lX) →
indep2 X (rvar_list lX).
Lemma independent_nil {A} {B} {Ω: distrib A} :
@independent A B Ω [::].
Lemma independent_singleton {A} {B} {Ω: distrib A} X:
@independent A B Ω [::X].
Lemma indep2_independent_cons {A} {B: eqType} {Ω: distrib A} (X: rvar Ω B) (lX: list (rvar Ω B)) :
indep2 X (rvar_list lX) →
independent lX →
independent (X :: lX).
Lemma rvar_list_comp_ext {A} {B C: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) (f: B → C) :
(rvar_comp (rvar_list lX) (map f)) =1 (rvar_list (map (rvar_comp^~f) lX)).
Lemma indep2_ext {A} {B C: eqType} {Ω: distrib A} (X X': rvar Ω B) (Y Y': rvar Ω C):
X =1 X' →
Y =1 Y' →
indep2 X Y →
indep2 X' Y'.
Lemma indep_fn {A} {B C: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) (f: B → C):
independent lX → independent (map (rvar_comp^~ f) lX).
Lemma ex_Ex_indep_prod_list {A} {Ω: distrib A} (l: list (rrvar Ω)) :
independent l →
(∀ X, In X l → ex_Ex X) →
ex_Ex (prod_list_rrvar l).
Lemma Ex_indep_prod_list {A} {Ω: distrib A} (l: list (rrvar Ω)) :
independent l →
(∀ X, In X l → ex_Ex X) →
Ex (prod_list_rrvar l) = fold_right Rmult 1 (map Ex l).
From discprob.prob Require Export prob countable stochastic_order markov double.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.
Definition independent {A} {B: eqType} {Ω: distrib A} (l: list (rvar Ω B)) :=
∀ lb, length lb = length l →
pr Ω (λ a, fold_right andb true (map (λ Xb, (rvar_fun _ _ (fst Xb)) a == (snd Xb))
(seq.zip l lb)))
= fold_right Rmult 1 (map (λ Xb, pr_eq (fst Xb) (snd Xb)) (seq.zip l lb)).
Definition indep2 {A} {B1 B2: eqType} {Ω: distrib A} (X: rvar Ω B1) (Y: rvar Ω B2) :=
∀ b1 b2, pr Ω (λ a, (X a == b1) && (Y a == b2)) =
pr_eq X b1 × pr_eq Y b2.
Lemma indep2_pair_var {A} {B1 B2: eqType} {Ω: distrib A} (X: rvar Ω B1) (Y: rvar Ω B2) :
indep2 X Y →
(∀ b1 b2, pr_eq (mkRvar Ω (λ a, (X a, Y a))) (b1, b2) =
pr_eq X b1 × pr_eq Y b2).
Lemma zip_nil {S T: Type} (s: seq.seq T) : seq.zip (@nil S) s = nil.
Lemma independent_tl {A} {B: eqType} {Ω: distrib A} (X: rvar Ω B) (lX: list (rvar Ω B)):
independent (X :: lX) → independent lX.
Lemma indep2_indendent {A} {B: eqType} {Ω: distrib A} (X Y: rvar Ω B) :
indep2 X Y ↔ independent (X :: Y :: nil).
Section joint_pr.
Variable (A: countType).
Variable (B1 B2: eqType).
Variable (Ω: distrib A).
Variable (X1 : rvar Ω B1).
Variable (X2 : rvar Ω B2).
Variable P: pred (B1).
Variable Q: pred (B2).
Variable (INDEP: indep2 X1 X2).
Lemma imgT_pr1 ab:
ab \in img (λ x : A, (X1 x, X2 x)) → (fst ab) \in img X1.
Lemma imgT_pr2 ab:
ab \in img (λ x : A, (X1 x, X2 x)) → (snd ab) \in img X2.
Definition σprod : nat → nat × nat.
Definition aprod :=
λ mn, match mn with
| (S m, S n) ⇒
match (@pickle_inv [countType of (imgT X1)] m),
(@pickle_inv [countType of (imgT X2)] n) with
| Some a, Some b ⇒
if P (sval a) && Q (sval b) then
pr_eq X1 (sval a) × pr_eq X2 (sval b)
else
0
| _, _ ⇒ 0
end
| _ ⇒ 0
end.
Lemma aprod_double_summable: double_summable aprod.
Lemma σprod_inj: ∀ n n', aprod (σprod n) ≠ 0 → σprod n = σprod n' → n = n'.
Lemma σprod_cov: ∀ n, aprod n ≠ 0 → ∃ m, σprod m = n.
Lemma is_series_prod_row:
is_series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
if P (fst (sval ab)) && Q (snd (sval ab)) then
pr_eq X1 (fst (sval ab)) × pr_eq X2 (snd (sval ab))
else
0))
(Series (λ j, Series (λ k, aprod (S j, S k)))).
Lemma Series_prod_row:
Series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
if P (fst (sval ab)) && Q (snd (sval ab)) then
pr_eq X1 (fst (sval ab)) × pr_eq X2 (snd (sval ab))
else
0)) =
(Series (λ j, Series (λ k, aprod (S j, S k)))).
Lemma indep2_pred:
pr Ω (λ a, P (X1 a) && Q (X2 a)) =
pr Ω (λ a, P (X1 a)) × pr Ω (λ a, Q (X2 a)).
End joint_pr.
Section exp.
Variable (A: countType).
Variable (B1 B2: eqType).
Variable (Ω: distrib A).
Variable (X1 X2 : rrvar Ω).
Variable (INDEP: indep2 X1 X2).
Variable (EX1: ex_Ex X1).
Variable (EX2: ex_Ex X2).
Definition σprod_exp : nat → nat × nat.
Definition aprod_exp :=
λ mn, match mn with
| (S m, S n) ⇒
match (@pickle_inv [countType of (imgT X1)] m),
(@pickle_inv [countType of (imgT X2)] n) with
| Some a, Some b ⇒
(sval a × pr_eq X1 (sval a)) × (sval b × pr_eq X2 (sval b))
| _, _ ⇒ 0
end
| _ ⇒ 0
end.
Lemma aprod_exp_double_summable: double_summable aprod_exp.
Lemma σprod_exp_inj: ∀ n n', aprod_exp (σprod_exp n) ≠ 0 → σprod_exp n = σprod_exp n' → n = n'.
Lemma σprod_exp_cov: ∀ n, aprod_exp n ≠ 0 → ∃ m, σprod_exp m = n.
Lemma is_series_prod_exp_row:
is_series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
(pr_eq (mkRvar Ω (λ a, (X1 a, X2 a))) (sval ab)
× (fst (sval ab) × snd (sval ab)))))
(Series (λ j, Series (λ k, aprod_exp (S j, S k)))).
Lemma is_series_prod_exp_row_abs:
is_series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
(pr_eq (mkRvar Ω (λ a, (X1 a, X2 a))) (sval ab)
× Rabs (fst (sval ab) × snd (sval ab)))))
(Series (λ j, Series (λ k, Rabs (aprod_exp (S j, S k))))).
Lemma Series_prod_exp_row:
Series (countable_sum (λ ab : imgT (λ x, (X1 x, X2 x)),
(pr_eq (mkRvar Ω (λ a, (X1 a, X2 a))) (sval ab)
× (fst (sval ab) × snd (sval ab))))) =
(Series (λ j, Series (λ k, aprod_exp (S j, S k)))).
Lemma indep2_ex_Ex_prod :
ex_Ex (mkRvar Ω (λ a, X1 a × X2 a)).
Lemma indep2_Ex_prod :
Ex (mkRvar Ω (λ a, X1 a × X2 a)) = Ex X1 × Ex X2.
End exp.
Lemma indep2_fn {A} {B1 B2 C1 C2: eqType} {Ω: distrib A} (X: rvar Ω B1) (Y: rvar Ω B2)
(f1: B1 → C1) (f2: B2 → C2):
indep2 X Y → indep2 (rvar_comp X f1) (rvar_comp Y f2).
Lemma rvar_list_eq_foldr {A} {B: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) bl i:
length bl = length lX →
((rvar_list lX) i == bl
↔ fold_right andb true (List.map (λ Xb : rvar Ω B × B, Xb.1 i == Xb.2) (zip lX bl))).
Lemma rvar_list_eq_short {A} {B: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) bl:
length bl ≠ length lX →
∀ i, ((rvar_list lX) i == bl) = false.
Lemma independent_rvar_list {A} {B: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) :
independent lX →
∀ bl, length bl = length lX →
pr_eq (rvar_list lX) bl =
fold_right Rmult 1 (map (λ Xb, pr_eq (fst Xb) (snd Xb)) (seq.zip lX bl)).
Lemma independent_indep2_tl {A} {B: eqType} {Ω: distrib A} (X: rvar Ω B) (lX: list (rvar Ω B)) :
independent (X :: lX) →
indep2 X (rvar_list lX).
Lemma independent_nil {A} {B} {Ω: distrib A} :
@independent A B Ω [::].
Lemma independent_singleton {A} {B} {Ω: distrib A} X:
@independent A B Ω [::X].
Lemma indep2_independent_cons {A} {B: eqType} {Ω: distrib A} (X: rvar Ω B) (lX: list (rvar Ω B)) :
indep2 X (rvar_list lX) →
independent lX →
independent (X :: lX).
Lemma rvar_list_comp_ext {A} {B C: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) (f: B → C) :
(rvar_comp (rvar_list lX) (map f)) =1 (rvar_list (map (rvar_comp^~f) lX)).
Lemma indep2_ext {A} {B C: eqType} {Ω: distrib A} (X X': rvar Ω B) (Y Y': rvar Ω C):
X =1 X' →
Y =1 Y' →
indep2 X Y →
indep2 X' Y'.
Lemma indep_fn {A} {B C: eqType} {Ω: distrib A} (lX: list (rvar Ω B)) (f: B → C):
independent lX → independent (map (rvar_comp^~ f) lX).
Lemma ex_Ex_indep_prod_list {A} {Ω: distrib A} (l: list (rrvar Ω)) :
independent l →
(∀ X, In X l → ex_Ex X) →
ex_Ex (prod_list_rrvar l).
Lemma Ex_indep_prod_list {A} {Ω: distrib A} (l: list (rrvar Ω)) :
independent l →
(∀ X, In X l → ex_Ex X) →
Ex (prod_list_rrvar l) = fold_right Rmult 1 (map Ex l).