Require Import Program.Basics.
Require Import Coq.Reals.Rbase.
Require Import Coq.Reals.Rfunctions.
Require Import Coq.Reals.RiemannInt.
Require Import Lra Lia.
Require Import List.
Require Import Morphisms EquivDec.
Require Import Classical ClassicalFacts.
Require Import ClassicalChoice.
Require Import ProofIrrelevance.
Require Ensembles.
Require Import hilbert.
Require Import utils.Utils DVector.
Import ListNotations.
Require Export Event.
Set Bullet Behavior "
Strict Subproofs".
Local Open Scope prob.
Definition sum_of_probs_equals {
T:
Type} {σ:
SigmaAlgebra T}
(
p :
event σ ->
R)
(
collection:
nat ->
event σ) (
result:
R) :=
infinite_sum' (
fun n:
nat =>
p (
collection n))
result.
Class ProbSpace {
T:
Type} (σ:
SigmaAlgebra T) :=
{
ps_P :
event σ ->
R;
ps_proper :>
Proper (
event_equiv ==>
eq)
ps_P ;
ps_countable_disjoint_union (
collection:
nat ->
event σ) :
collection_is_pairwise_disjoint collection ->
sum_of_probs_equals ps_P collection (
ps_P (
union_of_collection collection));
ps_one :
ps_P Ω =
R1;
ps_pos (
A:
event σ): (0 <=
ps_P A)%
R
}.
Lemma ps_all {
T:
Type} {
S:
SigmaAlgebra T} (
ps:
ProbSpace S) :
ps_P Ω =
R1.
Proof.
Lemma ps_none {
T:
Type} {
S:
SigmaAlgebra T} (
ps:
ProbSpace S) :
ps_P ∅ =
R0.
Proof.
generalize (
ps_countable_disjoint_union
(
fun n =>
match n with
| 0 => Ω
|
_ => ∅
end))
;
intros HH.
cut_to HH.
-
simpl in HH.
red in HH.
apply (
infinite_sum'
_split 1)
in HH.
simpl in HH.
apply (
infinite_sum'
_ext (
fun x :
nat =>
ps_P match (
x + 1)%
nat with
| 0%
nat => Ω
|
S _ => ∅
end)
(
fun x :
nat =>
ps_P ∅))
in HH.
+
rewrite (@
ps_proper _ _ _ (
union_of_collection
(
fun n :
nat =>
match n with
| 0%
nat => Ω
|
S _ => ∅
end)) (Ω))
in HH.
*
replace (
ps_P (
ProbSpace:=
ps) Ω)
with R1 in HH
by (
symmetry;
apply ps_one).
replace (
R1 - (0 +
R1))%
R with R0 in HH by lra.
eapply infinite_sum'
_const1;
eauto.
*
unfold event_equiv,
pre_event_equiv, Ω,
pre_Ω;
simpl;
intuition.
exists 0%
nat;
trivial.
+
destruct x;
simpl;
trivial.
-
unfold collection_is_pairwise_disjoint;
intros.
repeat match_destr;
repeat red;
tauto.
Qed.
Hint Rewrite @
ps_none @
ps_all :
prob.
Local Open Scope R.
Lemma ps_list_disjoint_union {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
l:
list (
event σ)) :
ForallOrdPairs event_disjoint l ->
ps_P (
list_union l) =
fold_right Rplus 0 (
map ps_P l).
Proof.
Lemma ps_disjoint_union {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
x1 x2:
event σ) :
event_disjoint x1 x2 ->
ps_P (
x1 ∪
x2) =
ps_P x1 +
ps_P x2.
Proof.
Lemma ps_sub {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A B:
event σ) :
A ≤
B ->
ps_P A <=
ps_P B.
Proof.
Lemma ps_le1 {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A:
event σ)
:
ps_P A <=
R1.
Proof.
Lemma ps_countable_total {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A:
event σ) (
coll:
nat ->
event σ) :
collection_is_pairwise_disjoint coll ->
union_of_collection coll === Ω ->
infinite_sum' (
fun i =>
ps_P (
A ∩ (
coll i))) (
ps_P A).
Proof.
Lemma ps_list_total {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A:
event σ) (
l:
list (
event σ)) :
ForallOrdPairs event_disjoint l ->
list_union l === Ω ->
ps_P A =
fold_right Rplus 0 (
map ps_P (
map (
event_inter A)
l)).
Proof.
Lemma ps_total {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A B C:
event σ) :
event_disjoint B C ->
B ∪
C === Ω ->
ps_P A =
ps_P (
A ∩
B) +
ps_P (
A ∩
C).
Proof.
intros.
intros.
rewrite (
ps_list_total ps A [
B;
C]);
trivial.
-
simpl;
lra.
-
repeat constructor;
trivial.
-
rewrite list_union2;
trivial.
Qed.
Lemma ps_complement {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A:
event σ) :
ps_P (¬
A) = 1 -
ps_P A.
Proof.
generalize (
ps_total ps Ω
A (¬
A));
intros HH.
cut_to HH;
eauto with prob.
rewrite ps_one in HH.
autorewrite with prob in HH.
lra.
Qed.
Lemma ps_union {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A B:
event σ) :
ps_P (
A ∪
B) =
ps_P A +
ps_P B -
ps_P (
A ∩
B).
Proof.
Lemma ps_union3 {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A B C:
event σ) :
ps_P (
A ∪
B ∪
C) =
ps_P A +
ps_P B +
ps_P C
-
ps_P (
A ∩
B) -
ps_P (
A ∩
C) -
ps_P (
B ∩
C)
+
ps_P (
A ∩
B ∩
C).
Proof.
Lemma ps_boole_inequality {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ)
(
l:
list (
event σ)) :
ps_P (
list_union l) <=
fold_right Rplus 0 (
map ps_P l).
Proof.
intros.
induction l;
simpl.
-
autorewrite with prob.
lra.
-
autorewrite with prob.
rewrite ps_union;
trivial.
generalize (
ps_pos (
a ∩
list_union l));
intros.
lra.
Qed.
Definition make_collection_disjoint {
T:
Type} {σ:
SigmaAlgebra T} (
coll:
nat->
event σ) :
nat ->
event σ
:=
fun x =>
coll x \ (
union_of_collection (
fun y =>
if lt_dec y x
then coll y
else ∅)).
Lemma make_collection_disjoint_sub {
T:
Type} {σ:
SigmaAlgebra T} (
En:
nat ->
event σ)
n :
event_sub (
make_collection_disjoint En n) (
En n).
Proof.
now intros x [??].
Qed.
Lemma make_collection_disjoint0 {
T:
Type} {σ:
SigmaAlgebra T} (
En:
nat ->
event σ) :
event_equiv (
make_collection_disjoint En 0) (
En 0%
nat).
Proof.
Hint Rewrite @
make_collection_disjoint0 :
prob.
Lemma make_collection_disjoint_in {
T:
Type} {σ:
SigmaAlgebra T} (
coll:
nat->
event σ) (
x:
nat) (
e:
T) :
proj1_sig (
make_collection_disjoint coll x)
e <->
(
proj1_sig (
coll x)
e /\
forall y, (
y <
x)%
nat -> ~
proj1_sig (
coll y)
e).
Proof.
Lemma make_collection_disjoint_disjoint {
T:
Type} {σ:
SigmaAlgebra T} (
coll:
nat->
event σ) :
collection_is_pairwise_disjoint (
make_collection_disjoint coll).
Proof.
Lemma union_of_make_collection_disjoint {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
coll:
nat->
event σ) :
sum_of_probs_equals ps_P (
make_collection_disjoint coll) (
ps_P (
union_of_collection (
make_collection_disjoint coll))).
Proof.
Lemma ps_diff_sub {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
A B :
event σ) :
event_sub B A ->
ps_P (
event_diff A B) =
ps_P A -
ps_P B.
Proof.
Require Import Classical ClassicalFacts.
Section classic.
Lemma make_collection_disjoint_union {
T:
Type} {σ:
SigmaAlgebra T} (
coll:
nat->
event σ) :
union_of_collection coll
===
union_of_collection (
make_collection_disjoint coll).
Proof.
Lemma ps_diff_le {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ)
x y :
ps_P (
x \
y) <=
ps_P x.
Proof.
intros.
apply ps_sub;
auto with prob.
Qed.
Lemma make_collection_disjoint_le {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ)
(
coll:
nat ->
event σ) :
forall n,
ps_P (
make_collection_disjoint coll n) <=
ps_P (
coll n).
Proof.
Theorem ps_countable_boole_inequality {
T:
Type} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ)
(
coll:
nat ->
event σ)
sum :
infinite_sum' (
fun n =>
ps_P (
coll n))
sum ->
ps_P (
union_of_collection coll) <=
sum.
Proof.
Lemma classic_event_none_or_has {
A} {σ:
SigmaAlgebra A} (
p:
event σ) : (
exists y,
proj1_sig p y) \/
event_equiv p event_none.
Proof.
destruct (
classic (
exists y,
proj1_sig p y)).
-
eauto.
-
right;
intros x.
destruct p;
simpl.
unfold pre_event_none.
split; [|
tauto].
intros px.
apply H.
eauto.
Qed.
End classic.
Section take.
Lemma sum_prob_fold_right {
T} {σ:
SigmaAlgebra T} (
ps:
ProbSpace σ) (
E :
nat ->
event σ)
n :
sum_n (
fun n0 :
nat =>
ps_P (
E n0))
n =
fold_right Rplus 0 (
map ps_P (
collection_take E (
S n))).
Proof.
End take.
Hint Rewrite @
collection_take_Sn @
collection_take1 :
prob.
Section ascending.
Context {
T:
Type} {σ:
SigmaAlgebra T}.
Definition ascending_collection (
En:
nat ->
event σ) := (
forall (
n:
nat),
event_sub (
En n) (
En (
S n))).
Lemma ascending_collection_le (
En:
nat ->
event σ) :
ascending_collection En ->
(
forall m n, (
m <=
n)%
nat ->
event_sub (
En m) (
En n)).
Proof.
intros asc.
induction n;
simpl.
-
intros.
replace m with (0%
nat)
by lia.
reflexivity.
-
intros.
apply le_lt_or_eq in H.
destruct H.
+
red in asc.
rewrite <-
asc.
apply IHn.
lia.
+
subst;
reflexivity.
Qed.
Lemma ascending_collection_take_union (
En:
nat ->
event σ) :
ascending_collection En ->
forall n,
event_equiv (
list_union (
collection_take En (
S n))) (
En n).
Proof.
Lemma ascending_make_disjoint_collection_take_union (
En:
nat ->
event σ) :
ascending_collection En ->
forall n,
event_equiv (
list_union (
collection_take (
make_collection_disjoint En) (
S n))) (
En n).
Proof.
Lemma is_lim_ascending (
ps:
ProbSpace σ) (
E :
nat ->
event σ) :
ascending_collection E ->
is_lim_seq (
fun n =>
ps_P (
E n)) (
ps_P (
union_of_collection E)).
Proof.
Lemma lim_ascending (
ps:
ProbSpace σ) (
E :
nat ->
event σ) :
ascending_collection E ->
Lim_seq (
fun n =>
ps_P (
E n)) = (
ps_P (
union_of_collection E)).
Proof.
Lemma event_sub_descending (
ps:
ProbSpace σ) (
E :
nat ->
event σ) :
(
forall n,
event_sub (
E (
S n)) (
E n)) ->
forall n,
event_sub (
E n) (
E 0%
nat).
Proof.
Lemma is_lim_descending (
ps:
ProbSpace σ) (
E :
nat ->
event σ) :
(
forall n,
event_sub (
E (
S n)) (
E n)) ->
is_lim_seq (
fun n =>
ps_P (
E n)) (
ps_P (
inter_of_collection E)).
Proof.
Lemma lim_descending (
ps:
ProbSpace σ) (
E :
nat ->
event σ) :
(
forall n,
event_sub (
E (
S n)) (
E n)) ->
Lim_seq (
fun n =>
ps_P (
E n)) = (
ps_P (
inter_of_collection E)).
Proof.
End ascending.
Hint Resolve ps_none ps_one :
prob.
Lemma event_complement_union {
T:
Type} {σ:
SigmaAlgebra T} (
E1 E2:
event σ) :
event_equiv (¬ (
E1 ∪
E2))
(¬
E1 ∩ ¬
E2).
Proof.
Lemma event_complement_inter {
T:
Type} {σ:
SigmaAlgebra T} (
E1 E2:
event σ) :
event_equiv (¬ (
E1 ∩
E2))
(¬
E1 ∪ ¬
E2).
Proof.
Lemma event_complement_list_union {
T:
Type} {σ:
SigmaAlgebra T} (
l:
list (
event σ)) :
event_equiv (
event_complement (
list_union l)) (
list_inter (
map event_complement l)).
Proof.
Lemma ps_zero_union {
Ts:
Type}
{
dom:
SigmaAlgebra Ts}
(
prts:
ProbSpace dom)
E1 E2 :
ps_P E1 = 0 ->
ps_P E2 = 0 ->
ps_P (
E1 ∪
E2) = 0.
Proof.
Lemma ps_one_inter {
Ts:
Type}
{
dom:
SigmaAlgebra Ts}
(
prts:
ProbSpace dom)
E1 E2 :
ps_P (
E1)=1 ->
ps_P (
E2)=1 ->
ps_P (
E1 ∩
E2)=1.
Proof.
Lemma ps_inter_r1 {
Ts:
Type}
{
dom:
SigmaAlgebra Ts}
(
prts:
ProbSpace dom)
{
A B} :
ps_P B = 1 ->
ps_P (
A ∩
B) =
ps_P A.
Proof.
intros HH.
generalize (
ps_union prts A B)
;
intros HH2.
rewrite HH in HH2.
assert (
ps_P (
A ∪
B) = 1).
{
apply Rle_antisym.
-
apply ps_le1.
-
rewrite <-
HH.
apply ps_sub.
eauto with prob.
}
rewrite H in HH2.
lra.
Qed.
Lemma ps_inter_l1 {
Ts:
Type}
{
dom:
SigmaAlgebra Ts}
(
prts:
ProbSpace dom)
{
A B} :
ps_P A = 1 ->
ps_P (
A ∩
B) =
ps_P B.
Proof.
Lemma ps_union_r0 {
Ts:
Type}
{
dom:
SigmaAlgebra Ts}
(
prts:
ProbSpace dom)
{
A B} :
ps_P B = 0 ->
ps_P (
A ∪
B) =
ps_P A.
Proof.
intros HH.
rewrite (
ps_union prts A B).
rewrite HH.
assert (
ps_P (
A ∩
B) = 0).
{
rewrite <-
HH.
apply Rle_antisym.
-
apply ps_sub.
auto with prob.
-
rewrite HH.
apply ps_pos.
}
rewrite H.
lra.
Qed.
Lemma ps_union_l0 {
Ts:
Type}
{
dom:
SigmaAlgebra Ts}
(
prts:
ProbSpace dom)
{
A B} :
ps_P A = 0 ->
ps_P (
A ∪
B) =
ps_P B.
Proof.
Lemma ps_union_sub
{
T :
Type} {σ :
SigmaAlgebra T} (
ps :
ProbSpace σ) (
A B :
event σ) :
ps_P A <=
ps_P (
A ∪
B).
Proof.
apply ps_sub.
auto with prob.
Qed.
Lemma ps_zero_countable_union {
T:
Type}
{
dom:
SigmaAlgebra T} (
prts:
ProbSpace dom)
(
coll:
nat ->
event dom) :
(
forall (
n:
nat),
ps_P (
coll n) = 0) ->
ps_P (
union_of_collection coll) = 0.
Proof.
generalize (
ps_countable_boole_inequality prts coll);
intros.
specialize (
H 0).
apply Rle_antisym.
-
apply H.
apply infinite_sum'
_ext with (
s1 :=
fun _ => 0).
+
intros;
symmetry;
apply H0.
+
apply infinite_sum'0.
-
apply ps_pos.
Qed.
Lemma ps_one_countable_inter {
T:
Type}
{
dom:
SigmaAlgebra T} (
prts:
ProbSpace dom)
(
coll:
nat ->
event dom) :
(
forall (
n:
nat),
ps_P (
coll n) = 1) ->
ps_P (
inter_of_collection coll) = 1.
Proof.
Lemma double_countable_inter_ps_one {
T:
Type}
{
dom:
SigmaAlgebra T} (
prts:
ProbSpace dom)
(
f :
nat ->
nat ->
T ->
Prop) :
(
forall (
n m :
nat),
exists (
P :
event dom),
ps_P P = 1 /\
forall (
x :
T),
P x ->
f n m x) ->
exists (
P :
event dom),
ps_P P = 1 /\
forall (
n m :
nat),
forall (
x :
T),
P x ->
f n m x.
Proof.
intros.
assert (
HH:
forall (
nm:
nat),
exists P :
event dom,
ps_P P = 1 /\ (
forall x :
T,
P x -> (
let '(
n,
m) :=
iso_b nm in f n m x))).
{
intros.
specialize (
H (
fst (
iso_b nm)) (
snd (
iso_b nm))).
match_destr.
}
destruct (
choice _ HH)
as [
coll collp].
exists (
inter_of_collection coll).
split.
-
apply ps_one_countable_inter.
intros n.
now destruct (
collp n).
-
intros n m x ic.
destruct (
collp (
iso_f (
n,
m)))
as [
_ HH2].
match_case_in HH2.
intros ??
eqq1.
rewrite eqq1 in HH2.
rewrite iso_b_f in eqq1.
invcs eqq1.
apply HH2.
apply ic.
Qed.
Section conditional_probability.
Context {
T:
Type} {σ:
SigmaAlgebra T} (Ψ:
ProbSpace σ).
Definition cond_prob
(
A B :
event σ)
:=
ps_P (
A ∩
B)/
ps_P(
B).
Lemma infinite_sum'
_scal_r {
f1 :
nat ->
R} {
sum1 :
R} (
c :
R) :
infinite_sum'
f1 sum1 ->
infinite_sum' (
fun x :
nat =>
f1 x *
c) (
sum1 *
c).
Proof.
intros.
rewrite Rmult_comm.
erewrite infinite_sum'
_ext
; [|
intros;
rewrite Rmult_comm;
reflexivity].
now apply infinite_sum'
_mult_const.
Qed.
Lemma infinite_sum'
_scal_div {
f1 :
nat ->
R} {
sum1 :
R} (
c :
R) :
infinite_sum'
f1 sum1 ->
infinite_sum' (
fun x :
nat =>
f1 x /
c) (
sum1 /
c).
Proof.
apply infinite_sum'_scal_r.
Qed.
Lemma event_inter_countable_union_distr_r (
A:
event σ) (
coll:
nat->
event σ) :
union_of_collection coll ∩
A ===
union_of_collection (
fun n => (
coll n) ∩
A).
Proof.
firstorder.
Qed.
Global Program Instance cond_prob_space (
B:
event σ) (
pf:0 <
ps_P B) :
ProbSpace σ
:= {
ps_P A :=
cond_prob A B
}.
Next Obligation.
intros ??
eqq.
unfold cond_prob.
now rewrite eqq.
Qed.
Next Obligation.
Next Obligation.
unfold cond_prob.
autorewrite with prob.
field_simplify;
lra.
Qed.
Next Obligation.
Definition event_restricted_domain (
e:
event σ) :
Type
:= {
x :
T |
e x }.
Lemma event_restricted_domain_ext (
e1 e2:
event σ) :
proj1_sig e1 =
proj1_sig e2 ->
e1 =
e2.
Proof.
Global Program Instance event_restricted_sigma (
e:
event σ) :
SigmaAlgebra (
event_restricted_domain e)
:= {
sa_sigma (
A:
pre_event (
event_restricted_domain e))
:=
sa_sigma (
fun a:
T =>
exists (
a':
event_restricted_domain e),
proj1_sig a' =
a /\
A (
a'))
}.
Next Obligation.
apply sa_countable_union in H.
eapply sa_proper;
try eapply H.
intros x.
split.
-
intros [?[?[
n ?]]];
subst.
exists n;
simpl.
eauto.
-
intros [
n [? [?
HH]]];
subst.
exists x0.
split;
trivial.
red;
eauto.
Qed.
Next Obligation.
Next Obligation.
eapply sa_proper;
try eapply (
proj2_sig e).
unfold pre_Ω;
simpl.
intros x;
simpl.
split.
-
intros [[??][??]];
simpl;
subst.
simpl.
apply e0.
-
intros.
exists (
exist _ _ H);
simpl.
tauto.
Qed.
Definition pre_event_restricted_pre_event_lift (
e:
event σ) (
A:
pre_event (
event_restricted_domain e)) :
pre_event T
:= (
fun a:
T =>
exists (
a':
event_restricted_domain e),
proj1_sig a' =
a /\
A (
a')).
Lemma sa_pre_event_restricted_event_lift (
e:
event σ) (
A:
event (
event_restricted_sigma e))
:
sa_sigma (
fun a:
T =>
exists (
a':
event_restricted_domain e),
proj1_sig a' =
a /\
A (
a')).
Proof.
Definition event_restricted_event_lift (
e:
event σ) (
A:
event(
event_restricted_sigma e)) :
event σ
:=
exist _ _ (
sa_pre_event_restricted_event_lift e A).
Definition event_restricted_pre_event (
e f:
event σ) :
pre_event (
event_restricted_domain e)
:=
fun (
a':
event_restricted_domain e) =>
f (
proj1_sig a').
Lemma sa_pre_event_restricted_event (
e f :
event σ) :
sa_sigma (
event_restricted_pre_event e f).
Proof.
Definition event_restricted_event (
e f:
event σ) :
event(
event_restricted_sigma e)
:=
exist _ _ (
sa_pre_event_restricted_event e f).
Definition event_restricted_function {
Td:
Type} (
e:
event σ) (
f :
T ->
Td) :
(
event_restricted_domain e) ->
Td
:=
fun a' =>
f (
proj1_sig a').
Instance event_restricted_event_lift_proper e :
Proper (
event_equiv ==>
event_equiv) (
event_restricted_event_lift e).
Proof.
Lemma event_restricted_event_lift_disjoint e collection :
collection_is_pairwise_disjoint collection ->
collection_is_pairwise_disjoint (
fun n :
nat =>
event_restricted_event_lift e (
collection n)).
Proof.
Lemma event_restricted_event_lift_collection e collection :
event_equiv (
event_restricted_event_lift e (
union_of_collection collection))
(
union_of_collection (
fun n :
nat =>
event_restricted_event_lift e (
collection n))).
Proof.
Lemma event_restricted_event_lift_Ω
e :
event_equiv (
event_restricted_event_lift e Ω)
e.
Proof.
intros x.
split.
-
intros [[??][??]];
simpl in *;
subst;
trivial.
-
intros.
unfold event_restricted_event_lift;
simpl.
exists (
exist _ _ H);
simpl.
unfold pre_Ω.
tauto.
Qed.
Global Program Instance event_restricted_prob_space (
e:
event σ) (
pf:0 <
ps_P e) :
ProbSpace (
event_restricted_sigma e)
:= {
ps_P A :=
cond_prob (
event_restricted_event_lift e A)
e
}.
Next Obligation.
intros ??
eqq.
unfold cond_prob.
now rewrite eqq.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
End conditional_probability.
Section sa_sub.
Context {
Ts:
Type}
{
dom:
SigmaAlgebra Ts}
(
prts:
ProbSpace dom)
{
dom2 :
SigmaAlgebra Ts}
(
sub :
sa_sub dom2 dom).
Instance prob_space_sa_sub :
ProbSpace dom2.
Proof.
End sa_sub.