author  hoelzl 
Thu, 26 May 2011 17:40:01 +0200  
changeset 42988  d8f3fc934ff6 
parent 42987  73e2d802ea41 
child 42989  40adeda9a8d2 
permissions  rwrr 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

1 
(* Title: HOL/Probability/Independent_Family.thy 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

2 
Author: Johannes Hölzl, TU München 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

3 
*) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

4 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

5 
header {* Independent families of events, event sets, and random variables *} 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

6 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

7 
theory Independent_Family 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

8 
imports Probability_Measure 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

9 
begin 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

10 

42985  11 
lemma INT_decseq_offset: 
12 
assumes "decseq F" 

13 
shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)" 

14 
proof safe 

15 
fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)" 

16 
show "x \<in> F i" 

17 
proof cases 

18 
from x have "x \<in> F n" by auto 

19 
also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i" 

20 
unfolding decseq_def by simp 

21 
finally show ?thesis . 

22 
qed (insert x, simp) 

23 
qed auto 

24 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

25 
definition (in prob_space) 
42983  26 
"indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and> 
42981  27 
(\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

28 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

29 
definition (in prob_space) 
42981  30 
"indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

31 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

32 
definition (in prob_space) 
42983  33 
"indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> 
42981  34 
(\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))" 
35 

36 
definition (in prob_space) 

37 
"indep_set A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV" 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

38 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

39 
definition (in prob_space) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

40 
"indep_rv M' X I \<longleftrightarrow> 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

41 
(\<forall>i\<in>I. random_variable (M' i) (X i)) \<and> 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

42 
indep_sets (\<lambda>i. sigma_sets (space M) { X i ` A \<inter> space M  A. A \<in> sets (M' i)}) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

43 

42987  44 
lemma (in prob_space) indep_sets_cong[cong]: 
42981  45 
"I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J" 
46 
by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+ 

47 

42985  48 
lemma (in prob_space) indep_sets_singleton_iff_indep_events: 
49 
"indep_sets (\<lambda>i. {F i}) I \<longleftrightarrow> indep_events F I" 

50 
unfolding indep_sets_def indep_events_def 

51 
by (simp, intro conj_cong ball_cong all_cong imp_cong) (auto simp: Pi_iff) 

52 

42981  53 
lemma (in prob_space) indep_events_finite_index_events: 
54 
"indep_events F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_events F J)" 

55 
by (auto simp: indep_events_def) 

56 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

57 
lemma (in prob_space) indep_sets_finite_index_sets: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

58 
"indep_sets F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

59 
proof (intro iffI allI impI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

60 
assume *: "\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

61 
show "indep_sets F I" unfolding indep_sets_def 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

62 
proof (intro conjI ballI allI impI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

63 
fix i assume "i \<in> I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

64 
with *[THEN spec, of "{i}"] show "F i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

65 
by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

66 
qed (insert *, auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

67 
qed (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

68 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

69 
lemma (in prob_space) indep_sets_mono_index: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

70 
"J \<subseteq> I \<Longrightarrow> indep_sets F I \<Longrightarrow> indep_sets F J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

71 
unfolding indep_sets_def by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

72 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

73 
lemma (in prob_space) indep_sets_mono_sets: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

74 
assumes indep: "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

75 
assumes mono: "\<And>i. i\<in>I \<Longrightarrow> G i \<subseteq> F i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

76 
shows "indep_sets G I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

77 
proof  
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

78 
have "(\<forall>i\<in>I. F i \<subseteq> events) \<Longrightarrow> (\<forall>i\<in>I. G i \<subseteq> events)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

79 
using mono by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

80 
moreover have "\<And>A J. J \<subseteq> I \<Longrightarrow> A \<in> (\<Pi> j\<in>J. G j) \<Longrightarrow> A \<in> (\<Pi> j\<in>J. F j)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

81 
using mono by (auto simp: Pi_iff) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

82 
ultimately show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

83 
using indep by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

84 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

85 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

86 
lemma (in prob_space) indep_setsI: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

87 
assumes "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

88 
and "\<And>A J. J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> (\<forall>j\<in>J. A j \<in> F j) \<Longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

89 
shows "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

90 
using assms unfolding indep_sets_def by (auto simp: Pi_iff) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

91 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

92 
lemma (in prob_space) indep_setsD: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

93 
assumes "indep_sets F I" and "J \<subseteq> I" "J \<noteq> {}" "finite J" "\<forall>j\<in>J. A j \<in> F j" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

94 
shows "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

95 
using assms unfolding indep_sets_def by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

96 

42982  97 
lemma (in prob_space) indep_setI: 
98 
assumes ev: "A \<subseteq> events" "B \<subseteq> events" 

99 
and indep: "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> prob (a \<inter> b) = prob a * prob b" 

100 
shows "indep_set A B" 

101 
unfolding indep_set_def 

102 
proof (rule indep_setsI) 

103 
fix F J assume "J \<noteq> {}" "J \<subseteq> UNIV" 

104 
and F: "\<forall>j\<in>J. F j \<in> (case j of True \<Rightarrow> A  False \<Rightarrow> B)" 

105 
have "J \<in> Pow UNIV" by auto 

106 
with F `J \<noteq> {}` indep[of "F True" "F False"] 

107 
show "prob (\<Inter>j\<in>J. F j) = (\<Prod>j\<in>J. prob (F j))" 

108 
unfolding UNIV_bool Pow_insert by (auto simp: ac_simps) 

109 
qed (auto split: bool.split simp: ev) 

110 

111 
lemma (in prob_space) indep_setD: 

112 
assumes indep: "indep_set A B" and ev: "a \<in> A" "b \<in> B" 

113 
shows "prob (a \<inter> b) = prob a * prob b" 

114 
using indep[unfolded indep_set_def, THEN indep_setsD, of UNIV "bool_case a b"] ev 

115 
by (simp add: ac_simps UNIV_bool) 

116 

117 
lemma (in prob_space) 

118 
assumes indep: "indep_set A B" 

42983  119 
shows indep_setD_ev1: "A \<subseteq> events" 
120 
and indep_setD_ev2: "B \<subseteq> events" 

42982  121 
using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto 
122 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

123 
lemma (in prob_space) indep_sets_dynkin: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

124 
assumes indep: "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

125 
shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

126 
(is "indep_sets ?F I") 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

127 
proof (subst indep_sets_finite_index_sets, intro allI impI ballI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

128 
fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

129 
with indep have "indep_sets F J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

130 
by (subst (asm) indep_sets_finite_index_sets) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

131 
{ fix J K assume "indep_sets F K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

132 
let "?G S i" = "if i \<in> S then ?F i else F i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

133 
assume "finite J" "J \<subseteq> K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

134 
then have "indep_sets (?G J) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

135 
proof induct 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

136 
case (insert j J) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

137 
moreover def G \<equiv> "?G J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

138 
ultimately have G: "indep_sets G K" "\<And>i. i \<in> K \<Longrightarrow> G i \<subseteq> events" and "j \<in> K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

139 
by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

140 
let ?D = "{E\<in>events. indep_sets (G(j := {E})) K }" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

141 
{ fix X assume X: "X \<in> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

142 
assume indep: "\<And>J A. J \<noteq> {} \<Longrightarrow> J \<subseteq> K \<Longrightarrow> finite J \<Longrightarrow> j \<notin> J \<Longrightarrow> (\<forall>i\<in>J. A i \<in> G i) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

143 
\<Longrightarrow> prob ((\<Inter>i\<in>J. A i) \<inter> X) = prob X * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

144 
have "indep_sets (G(j := {X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

145 
proof (rule indep_setsI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

146 
fix i assume "i \<in> K" then show "(G(j:={X})) i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

147 
using G X by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

148 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

149 
fix A J assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "\<forall>i\<in>J. A i \<in> (G(j := {X})) i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

150 
show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

151 
proof cases 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

152 
assume "j \<in> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

153 
with J have "A j = X" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

154 
show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

155 
proof cases 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

156 
assume "J = {j}" then show ?thesis by simp 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

157 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

158 
assume "J \<noteq> {j}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

159 
have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J{j}. A i) \<inter> X)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

160 
using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

161 
also have "\<dots> = prob X * (\<Prod>i\<in>J{j}. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

162 
proof (rule indep) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

163 
show "J  {j} \<noteq> {}" "J  {j} \<subseteq> K" "finite (J  {j})" "j \<notin> J  {j}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

164 
using J `J \<noteq> {j}` `j \<in> J` by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

165 
show "\<forall>i\<in>J  {j}. A i \<in> G i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

166 
using J by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

167 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

168 
also have "\<dots> = prob (A j) * (\<Prod>i\<in>J{j}. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

169 
using `A j = X` by simp 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

170 
also have "\<dots> = (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

171 
unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob (A i)"] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

172 
using `j \<in> J` by (simp add: insert_absorb) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

173 
finally show ?thesis . 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

174 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

175 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

176 
assume "j \<notin> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

177 
with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

178 
with J show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

179 
by (intro indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

180 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

181 
qed } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

182 
note indep_sets_insert = this 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

183 
have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>" 
42987  184 
proof (rule dynkin_systemI', simp_all cong del: indep_sets_cong, safe) 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

185 
show "indep_sets (G(j := {{}})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

186 
by (rule indep_sets_insert) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

187 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

188 
fix X assume X: "X \<in> events" and G': "indep_sets (G(j := {X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

189 
show "indep_sets (G(j := {space M  X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

190 
proof (rule indep_sets_insert) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

191 
fix J A assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "j \<notin> J" and A: "\<forall>i\<in>J. A i \<in> G i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

192 
then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

193 
using G by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

194 
have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

195 
prob ((\<Inter>j\<in>J. A j)  (\<Inter>i\<in>insert j J. (A(j := X)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

196 
using A_sets sets_into_space X `J \<noteq> {}` 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

197 
by (auto intro!: arg_cong[where f=prob] split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

198 
also have "\<dots> = prob (\<Inter>j\<in>J. A j)  prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

199 
using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

200 
by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

201 
finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

202 
prob (\<Inter>j\<in>J. A j)  prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" . 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

203 
moreover { 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

204 
have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

205 
using J A `finite J` by (intro indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

206 
then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

207 
using prob_space by simp } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

208 
moreover { 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

209 
have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

210 
using J A `j \<in> K` by (intro indep_setsD[OF G']) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

211 
then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

212 
using `finite J` `j \<notin> J` by (auto intro!: setprod_cong) } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

213 
ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = (prob (space M)  prob X) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

214 
by (simp add: field_simps) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

215 
also have "\<dots> = prob (space M  X) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

216 
using X A by (simp add: finite_measure_compl) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

217 
finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = prob (space M  X) * (\<Prod>i\<in>J. prob (A i))" . 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

218 
qed (insert X, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

219 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

220 
fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F" and "range F \<subseteq> ?D" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

221 
then have F: "\<And>i. F i \<in> events" "\<And>i. indep_sets (G(j:={F i})) K" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

222 
show "indep_sets (G(j := {\<Union>k. F k})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

223 
proof (rule indep_sets_insert) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

224 
fix J A assume J: "j \<notin> J" "J \<noteq> {}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> G i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

225 
then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

226 
using G by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

227 
have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

228 
using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

229 
moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

230 
proof (rule finite_measure_UNION) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

231 
show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

232 
using disj by (rule disjoint_family_on_bisimulation) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

233 
show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

234 
using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

235 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

236 
moreover { fix k 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

237 
from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

238 
by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

239 
also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

240 
using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

241 
finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

242 
ultimately have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

243 
by simp 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

244 
moreover 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

245 
have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * prob (\<Inter>i\<in>J. A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

246 
using disj F(1) by (intro finite_measure_UNION sums_mult2) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

247 
then have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * (\<Prod>i\<in>J. prob (A i)))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

248 
using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

249 
ultimately 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

250 
show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

251 
by (auto dest!: sums_unique) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

252 
qed (insert F, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

253 
qed (insert sets_into_space, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

254 
then have mono: "sets (dynkin \<lparr>space = space M, sets = G j\<rparr>) \<subseteq> 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

255 
sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>" 
42987  256 
proof (rule dynkin_system.dynkin_subset, simp_all cong del: indep_sets_cong, safe) 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

257 
fix X assume "X \<in> G j" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

258 
then show "X \<in> events" using G `j \<in> K` by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

259 
from `indep_sets G K` 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

260 
show "indep_sets (G(j := {X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

261 
by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

262 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

263 
have "indep_sets (G(j:=?D)) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

264 
proof (rule indep_setsI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

265 
fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

266 
using G(2) by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

267 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

268 
fix A J assume J: "J\<noteq>{}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> (G(j := ?D)) i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

269 
show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

270 
proof cases 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

271 
assume "j \<in> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

272 
with A have indep: "indep_sets (G(j := {A j})) K" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

273 
from J A show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

274 
by (intro indep_setsD[OF indep]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

275 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

276 
assume "j \<notin> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

277 
with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

278 
with J show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

279 
by (intro indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

280 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

281 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

282 
then have "indep_sets (G(j:=sets (dynkin \<lparr>space = space M, sets = G j\<rparr>))) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

283 
by (rule indep_sets_mono_sets) (insert mono, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

284 
then show ?case 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

285 
by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

286 
qed (insert `indep_sets F K`, simp) } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

287 
from this[OF `indep_sets F J` `finite J` subset_refl] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

288 
show "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

289 
by (rule indep_sets_mono_sets) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

290 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

291 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

292 
lemma (in prob_space) indep_sets_sigma: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

293 
assumes indep: "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

294 
assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

295 
shows "indep_sets (\<lambda>i. sets (sigma \<lparr> space = space M, sets = F i \<rparr>)) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

296 
proof  
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

297 
from indep_sets_dynkin[OF indep] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

298 
show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

299 
proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

300 
fix i assume "i \<in> I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

301 
with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

302 
with sets_into_space show "F i \<subseteq> Pow (space M)" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

303 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

304 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

305 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

306 
lemma (in prob_space) indep_sets_sigma_sets: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

307 
assumes "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

308 
assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

309 
shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

310 
using indep_sets_sigma[OF assms] by (simp add: sets_sigma) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

311 

42987  312 
lemma (in prob_space) indep_sets_sigma_sets_iff: 
313 
assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" 

314 
shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I \<longleftrightarrow> indep_sets F I" 

315 
proof 

316 
assume "indep_sets F I" then show "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" 

317 
by (rule indep_sets_sigma_sets) fact 

318 
next 

319 
assume "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" then show "indep_sets F I" 

320 
by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic) 

321 
qed 

322 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

323 
lemma (in prob_space) indep_sets2_eq: 
42981  324 
"indep_set A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)" 
325 
unfolding indep_set_def 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

326 
proof (intro iffI ballI conjI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

327 
assume indep: "indep_sets (bool_case A B) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

328 
{ fix a b assume "a \<in> A" "b \<in> B" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

329 
with indep_setsD[OF indep, of UNIV "bool_case a b"] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

330 
show "prob (a \<inter> b) = prob a * prob b" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

331 
unfolding UNIV_bool by (simp add: ac_simps) } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

332 
from indep show "A \<subseteq> events" "B \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

333 
unfolding indep_sets_def UNIV_bool by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

334 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

335 
assume *: "A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

336 
show "indep_sets (bool_case A B) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

337 
proof (rule indep_setsI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

338 
fix i show "(case i of True \<Rightarrow> A  False \<Rightarrow> B) \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

339 
using * by (auto split: bool.split) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

340 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

341 
fix J X assume "J \<noteq> {}" "J \<subseteq> UNIV" and X: "\<forall>j\<in>J. X j \<in> (case j of True \<Rightarrow> A  False \<Rightarrow> B)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

342 
then have "J = {True} \<or> J = {False} \<or> J = {True,False}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

343 
by (auto simp: UNIV_bool) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

344 
then show "prob (\<Inter>j\<in>J. X j) = (\<Prod>j\<in>J. prob (X j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

345 
using X * by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

346 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

347 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

348 

42981  349 
lemma (in prob_space) indep_set_sigma_sets: 
350 
assumes "indep_set A B" 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

351 
assumes A: "Int_stable \<lparr> space = space M, sets = A \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

352 
assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>" 
42981  353 
shows "indep_set (sigma_sets (space M) A) (sigma_sets (space M) B)" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

354 
proof  
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

355 
have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A  False \<Rightarrow> B)) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

356 
proof (rule indep_sets_sigma_sets) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

357 
show "indep_sets (bool_case A B) UNIV" 
42981  358 
by (rule `indep_set A B`[unfolded indep_set_def]) 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

359 
fix i show "Int_stable \<lparr>space = space M, sets = case i of True \<Rightarrow> A  False \<Rightarrow> B\<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

360 
using A B by (cases i) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

361 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

362 
then show ?thesis 
42981  363 
unfolding indep_set_def 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

364 
by (rule indep_sets_mono_sets) (auto split: bool.split) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

365 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

366 

42981  367 
lemma (in prob_space) indep_sets_collect_sigma: 
368 
fixes I :: "'j \<Rightarrow> 'i set" and J :: "'j set" and E :: "'i \<Rightarrow> 'a set set" 

369 
assumes indep: "indep_sets E (\<Union>j\<in>J. I j)" 

370 
assumes Int_stable: "\<And>i j. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> Int_stable \<lparr>space = space M, sets = E i\<rparr>" 

371 
assumes disjoint: "disjoint_family_on I J" 

372 
shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J" 

373 
proof  

374 
let "?E j" = "{\<Inter>k\<in>K. E' k E' K. finite K \<and> K \<noteq> {} \<and> K \<subseteq> I j \<and> (\<forall>k\<in>K. E' k \<in> E k) }" 

375 

42983  376 
from indep have E: "\<And>j i. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> E i \<subseteq> events" 
42981  377 
unfolding indep_sets_def by auto 
378 
{ fix j 

379 
let ?S = "sigma \<lparr> space = space M, sets = (\<Union>i\<in>I j. E i) \<rparr>" 

380 
assume "j \<in> J" 

381 
from E[OF this] interpret S: sigma_algebra ?S 

382 
using sets_into_space by (intro sigma_algebra_sigma) auto 

383 

384 
have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)" 

385 
proof (rule sigma_sets_eqI) 

386 
fix A assume "A \<in> (\<Union>i\<in>I j. E i)" 

387 
then guess i .. 

388 
then show "A \<in> sigma_sets (space M) (?E j)" 

389 
by (auto intro!: sigma_sets.intros exI[of _ "{i}"] exI[of _ "\<lambda>i. A"]) 

390 
next 

391 
fix A assume "A \<in> ?E j" 

392 
then obtain E' K where "finite K" "K \<noteq> {}" "K \<subseteq> I j" "\<And>k. k \<in> K \<Longrightarrow> E' k \<in> E k" 

393 
and A: "A = (\<Inter>k\<in>K. E' k)" 

394 
by auto 

395 
then have "A \<in> sets ?S" unfolding A 

396 
by (safe intro!: S.finite_INT) 

397 
(auto simp: sets_sigma intro!: sigma_sets.Basic) 

398 
then show "A \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i)" 

399 
by (simp add: sets_sigma) 

400 
qed } 

401 
moreover have "indep_sets (\<lambda>j. sigma_sets (space M) (?E j)) J" 

402 
proof (rule indep_sets_sigma_sets) 

403 
show "indep_sets ?E J" 

404 
proof (intro indep_setsI) 

405 
fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force intro!: finite_INT) 

406 
next 

407 
fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K" 

408 
and "\<forall>j\<in>K. A j \<in> ?E j" 

409 
then have "\<forall>j\<in>K. \<exists>E' L. A j = (\<Inter>l\<in>L. E' l) \<and> finite L \<and> L \<noteq> {} \<and> L \<subseteq> I j \<and> (\<forall>l\<in>L. E' l \<in> E l)" 

410 
by simp 

411 
from bchoice[OF this] guess E' .. 

412 
from bchoice[OF this] obtain L 

413 
where A: "\<And>j. j\<in>K \<Longrightarrow> A j = (\<Inter>l\<in>L j. E' j l)" 

414 
and L: "\<And>j. j\<in>K \<Longrightarrow> finite (L j)" "\<And>j. j\<in>K \<Longrightarrow> L j \<noteq> {}" "\<And>j. j\<in>K \<Longrightarrow> L j \<subseteq> I j" 

415 
and E': "\<And>j l. j\<in>K \<Longrightarrow> l \<in> L j \<Longrightarrow> E' j l \<in> E l" 

416 
by auto 

417 

418 
{ fix k l j assume "k \<in> K" "j \<in> K" "l \<in> L j" "l \<in> L k" 

419 
have "k = j" 

420 
proof (rule ccontr) 

421 
assume "k \<noteq> j" 

422 
with disjoint `K \<subseteq> J` `k \<in> K` `j \<in> K` have "I k \<inter> I j = {}" 

423 
unfolding disjoint_family_on_def by auto 

424 
with L(2,3)[OF `j \<in> K`] L(2,3)[OF `k \<in> K`] 

425 
show False using `l \<in> L k` `l \<in> L j` by auto 

426 
qed } 

427 
note L_inj = this 

428 

429 
def k \<equiv> "\<lambda>l. (SOME k. k \<in> K \<and> l \<in> L k)" 

430 
{ fix x j l assume *: "j \<in> K" "l \<in> L j" 

431 
have "k l = j" unfolding k_def 

432 
proof (rule some_equality) 

433 
fix k assume "k \<in> K \<and> l \<in> L k" 

434 
with * L_inj show "k = j" by auto 

435 
qed (insert *, simp) } 

436 
note k_simp[simp] = this 

437 
let "?E' l" = "E' (k l) l" 

438 
have "prob (\<Inter>j\<in>K. A j) = prob (\<Inter>l\<in>(\<Union>k\<in>K. L k). ?E' l)" 

439 
by (auto simp: A intro!: arg_cong[where f=prob]) 

440 
also have "\<dots> = (\<Prod>l\<in>(\<Union>k\<in>K. L k). prob (?E' l))" 

441 
using L K E' by (intro indep_setsD[OF indep]) (simp_all add: UN_mono) 

442 
also have "\<dots> = (\<Prod>j\<in>K. \<Prod>l\<in>L j. prob (E' j l))" 

443 
using K L L_inj by (subst setprod_UN_disjoint) auto 

444 
also have "\<dots> = (\<Prod>j\<in>K. prob (A j))" 

445 
using K L E' by (auto simp add: A intro!: setprod_cong indep_setsD[OF indep, symmetric]) blast 

446 
finally show "prob (\<Inter>j\<in>K. A j) = (\<Prod>j\<in>K. prob (A j))" . 

447 
qed 

448 
next 

449 
fix j assume "j \<in> J" 

450 
show "Int_stable \<lparr> space = space M, sets = ?E j \<rparr>" 

451 
proof (rule Int_stableI) 

452 
fix a assume "a \<in> ?E j" then obtain Ka Ea 

453 
where a: "a = (\<Inter>k\<in>Ka. Ea k)" "finite Ka" "Ka \<noteq> {}" "Ka \<subseteq> I j" "\<And>k. k\<in>Ka \<Longrightarrow> Ea k \<in> E k" by auto 

454 
fix b assume "b \<in> ?E j" then obtain Kb Eb 

455 
where b: "b = (\<Inter>k\<in>Kb. Eb k)" "finite Kb" "Kb \<noteq> {}" "Kb \<subseteq> I j" "\<And>k. k\<in>Kb \<Longrightarrow> Eb k \<in> E k" by auto 

456 
let ?A = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})" 

457 
have "a \<inter> b = INTER (Ka \<union> Kb) ?A" 

458 
by (simp add: a b set_eq_iff) auto 

459 
with a b `j \<in> J` Int_stableD[OF Int_stable] show "a \<inter> b \<in> ?E j" 

460 
by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?A]) auto 

461 
qed 

462 
qed 

463 
ultimately show ?thesis 

464 
by (simp cong: indep_sets_cong) 

465 
qed 

466 

42982  467 
definition (in prob_space) terminal_events where 
468 
"terminal_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))" 

469 

470 
lemma (in prob_space) terminal_events_sets: 

42983  471 
assumes A: "\<And>i. A i \<subseteq> events" 
42982  472 
assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>" 
473 
assumes X: "X \<in> terminal_events A" 

42983  474 
shows "X \<in> events" 
42982  475 
proof  
476 
let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" 

477 
interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact 

478 
from X have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def) 

479 
from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp 

42983  480 
then show "X \<in> events" 
42982  481 
by induct (insert A, auto) 
482 
qed 

483 

484 
lemma (in prob_space) sigma_algebra_terminal_events: 

485 
assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>" 

486 
shows "sigma_algebra \<lparr> space = space M, sets = terminal_events A \<rparr>" 

487 
unfolding terminal_events_def 

488 
proof (simp add: sigma_algebra_iff2, safe) 

489 
let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" 

490 
interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact 

491 
{ fix X x assume "X \<in> ?A" "x \<in> X" 

492 
then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto 

493 
from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp 

494 
then have "X \<subseteq> space M" 

495 
by induct (insert A.sets_into_space, auto) 

496 
with `x \<in> X` show "x \<in> space M" by auto } 

497 
{ fix F :: "nat \<Rightarrow> 'a set" and n assume "range F \<subseteq> ?A" 

498 
then show "(UNION UNIV F) \<in> sigma_sets (space M) (UNION {n..} A)" 

499 
by (intro sigma_sets.Union) auto } 

500 
qed (auto intro!: sigma_sets.Compl sigma_sets.Empty) 

501 

502 
lemma (in prob_space) kolmogorov_0_1_law: 

503 
fixes A :: "nat \<Rightarrow> 'a set set" 

42983  504 
assumes A: "\<And>i. A i \<subseteq> events" 
42982  505 
assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>" 
506 
assumes indep: "indep_sets A UNIV" 

507 
and X: "X \<in> terminal_events A" 

508 
shows "prob X = 0 \<or> prob X = 1" 

509 
proof  

42983  510 
let ?D = "\<lparr> space = space M, sets = {D \<in> events. prob (X \<inter> D) = prob X * prob D} \<rparr>" 
42982  511 
interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact 
512 
interpret T: sigma_algebra "\<lparr> space = space M, sets = terminal_events A \<rparr>" 

513 
by (rule sigma_algebra_terminal_events) fact 

514 
have "X \<subseteq> space M" using T.space_closed X by auto 

515 

42983  516 
have X_in: "X \<in> events" 
42982  517 
by (rule terminal_events_sets) fact+ 
518 

519 
interpret D: dynkin_system ?D 

520 
proof (rule dynkin_systemI) 

521 
fix D assume "D \<in> sets ?D" then show "D \<subseteq> space ?D" 

522 
using sets_into_space by auto 

523 
next 

524 
show "space ?D \<in> sets ?D" 

525 
using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2) 

526 
next 

527 
fix A assume A: "A \<in> sets ?D" 

528 
have "prob (X \<inter> (space M  A)) = prob (X  (X \<inter> A))" 

529 
using `X \<subseteq> space M` by (auto intro!: arg_cong[where f=prob]) 

530 
also have "\<dots> = prob X  prob (X \<inter> A)" 

531 
using X_in A by (intro finite_measure_Diff) auto 

532 
also have "\<dots> = prob X * prob (space M)  prob X * prob A" 

533 
using A prob_space by auto 

534 
also have "\<dots> = prob X * prob (space M  A)" 

535 
using X_in A sets_into_space 

536 
by (subst finite_measure_Diff) (auto simp: field_simps) 

537 
finally show "space ?D  A \<in> sets ?D" 

538 
using A `X \<subseteq> space M` by auto 

539 
next 

540 
fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> sets ?D" 

541 
then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)" 

542 
by auto 

543 
have "(\<lambda>i. prob (X \<inter> F i)) sums prob (\<Union>i. X \<inter> F i)" 

544 
proof (rule finite_measure_UNION) 

545 
show "range (\<lambda>i. X \<inter> F i) \<subseteq> events" 

546 
using F X_in by auto 

547 
show "disjoint_family (\<lambda>i. X \<inter> F i)" 

548 
using dis by (rule disjoint_family_on_bisimulation) auto 

549 
qed 

550 
with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))" 

551 
by simp 

552 
moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))" 

553 
by (intro mult_right.sums finite_measure_UNION F dis) 

554 
ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)" 

555 
by (auto dest!: sums_unique) 

556 
with F show "(\<Union>i. F i) \<in> sets ?D" 

557 
by auto 

558 
qed 

559 

560 
{ fix n 

561 
have "indep_sets (\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) UNIV" 

562 
proof (rule indep_sets_collect_sigma) 

563 
have *: "(\<Union>b. case b of True \<Rightarrow> {..n}  False \<Rightarrow> {Suc n..}) = UNIV" (is "?U = _") 

564 
by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq) 

565 
with indep show "indep_sets A ?U" by simp 

566 
show "disjoint_family (bool_case {..n} {Suc n..})" 

567 
unfolding disjoint_family_on_def by (auto split: bool.split) 

568 
fix m 

569 
show "Int_stable \<lparr>space = space M, sets = A m\<rparr>" 

570 
unfolding Int_stable_def using A.Int by auto 

571 
qed 

572 
also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) = 

573 
bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))" 

574 
by (auto intro!: ext split: bool.split) 

575 
finally have indep: "indep_set (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))" 

576 
unfolding indep_set_def by simp 

577 

578 
have "sigma_sets (space M) (\<Union>m\<in>{..n}. A m) \<subseteq> sets ?D" 

579 
proof (simp add: subset_eq, rule) 

580 
fix D assume D: "D \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" 

581 
have "X \<in> sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m)" 

582 
using X unfolding terminal_events_def by simp 

583 
from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D 

584 
show "D \<in> events \<and> prob (X \<inter> D) = prob X * prob D" 

585 
by (auto simp add: ac_simps) 

586 
qed } 

587 
then have "(\<Union>n. sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) \<subseteq> sets ?D" (is "?A \<subseteq> _") 

588 
by auto 

589 

590 
have "sigma \<lparr> space = space M, sets = ?A \<rparr> = 

591 
dynkin \<lparr> space = space M, sets = ?A \<rparr>" (is "sigma ?UA = dynkin ?UA") 

592 
proof (rule sigma_eq_dynkin) 

593 
{ fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" 

594 
then have "B \<subseteq> space M" 

595 
by induct (insert A sets_into_space, auto) } 

596 
then show "sets ?UA \<subseteq> Pow (space ?UA)" by auto 

597 
show "Int_stable ?UA" 

598 
proof (rule Int_stableI) 

599 
fix a assume "a \<in> ?A" then guess n .. note a = this 

600 
fix b assume "b \<in> ?A" then guess m .. note b = this 

601 
interpret Amn: sigma_algebra "sigma \<lparr>space = space M, sets = (\<Union>i\<in>{..max m n}. A i)\<rparr>" 

602 
using A sets_into_space by (intro sigma_algebra_sigma) auto 

603 
have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" 

604 
by (intro sigma_sets_subseteq UN_mono) auto 

605 
with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto 

606 
moreover 

607 
have "sigma_sets (space M) (\<Union>i\<in>{..m}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" 

608 
by (intro sigma_sets_subseteq UN_mono) auto 

609 
with b have "b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto 

610 
ultimately have "a \<inter> b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" 

611 
using Amn.Int[of a b] by (simp add: sets_sigma) 

612 
then show "a \<inter> b \<in> (\<Union>n. sigma_sets (space M) (\<Union>i\<in>{..n}. A i))" by auto 

613 
qed 

614 
qed 

615 
moreover have "sets (dynkin ?UA) \<subseteq> sets ?D" 

616 
proof (rule D.dynkin_subset) 

617 
show "sets ?UA \<subseteq> sets ?D" using `?A \<subseteq> sets ?D` by auto 

618 
qed simp 

619 
ultimately have "sets (sigma ?UA) \<subseteq> sets ?D" by simp 

620 
moreover 

621 
have "\<And>n. sigma_sets (space M) (\<Union>i\<in>{n..}. A i) \<subseteq> sigma_sets (space M) ?A" 

622 
by (intro sigma_sets_subseteq UN_mono) (auto intro: sigma_sets.Basic) 

623 
then have "terminal_events A \<subseteq> sets (sigma ?UA)" 

624 
unfolding sets_sigma terminal_events_def by auto 

625 
moreover note `X \<in> terminal_events A` 

626 
ultimately have "X \<in> sets ?D" by auto 

627 
then show ?thesis by auto 

628 
qed 

629 

42985  630 
lemma (in prob_space) borel_0_1_law: 
631 
fixes F :: "nat \<Rightarrow> 'a set" 

632 
assumes F: "range F \<subseteq> events" "indep_events F UNIV" 

633 
shows "prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 1" 

634 
proof (rule kolmogorov_0_1_law[of "\<lambda>i. sigma_sets (space M) { F i }"]) 

635 
show "\<And>i. sigma_sets (space M) {F i} \<subseteq> events" 

636 
using F(1) sets_into_space 

637 
by (subst sigma_sets_singleton) auto 

638 
{ fix i show "sigma_algebra \<lparr>space = space M, sets = sigma_sets (space M) {F i}\<rparr>" 

639 
using sigma_algebra_sigma[of "\<lparr>space = space M, sets = {F i}\<rparr>"] F sets_into_space 

640 
by (auto simp add: sigma_def) } 

641 
show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV" 

642 
proof (rule indep_sets_sigma_sets) 

643 
show "indep_sets (\<lambda>i. {F i}) UNIV" 

644 
unfolding indep_sets_singleton_iff_indep_events by fact 

645 
fix i show "Int_stable \<lparr>space = space M, sets = {F i}\<rparr>" 

646 
unfolding Int_stable_def by simp 

647 
qed 

648 
let "?Q n" = "\<Union>i\<in>{n..}. F i" 

649 
show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})" 

650 
unfolding terminal_events_def 

651 
proof 

652 
fix j 

653 
interpret S: sigma_algebra "sigma \<lparr> space = space M, sets = (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})\<rparr>" 

654 
using order_trans[OF F(1) space_closed] 

655 
by (intro sigma_algebra_sigma) (simp add: sigma_sets_singleton subset_eq) 

656 
have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)" 

657 
by (intro decseq_SucI INT_decseq_offset UN_mono) auto 

658 
also have "\<dots> \<in> sets (sigma \<lparr> space = space M, sets = (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})\<rparr>)" 

659 
using order_trans[OF F(1) space_closed] 

660 
by (safe intro!: S.countable_INT S.countable_UN) 

661 
(auto simp: sets_sigma sigma_sets_singleton intro!: sigma_sets.Basic bexI) 

662 
finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" 

663 
by (simp add: sets_sigma) 

664 
qed 

665 
qed 

666 

42987  667 
lemma (in prob_space) indep_sets_finite: 
668 
assumes I: "I \<noteq> {}" "finite I" 

669 
and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events" "\<And>i. i \<in> I \<Longrightarrow> space M \<in> F i" 

670 
shows "indep_sets F I \<longleftrightarrow> (\<forall>A\<in>Pi I F. prob (\<Inter>j\<in>I. A j) = (\<Prod>j\<in>I. prob (A j)))" 

671 
proof 

672 
assume *: "indep_sets F I" 

673 
from I show "\<forall>A\<in>Pi I F. prob (\<Inter>j\<in>I. A j) = (\<Prod>j\<in>I. prob (A j))" 

674 
by (intro indep_setsD[OF *] ballI) auto 

675 
next 

676 
assume indep: "\<forall>A\<in>Pi I F. prob (\<Inter>j\<in>I. A j) = (\<Prod>j\<in>I. prob (A j))" 

677 
show "indep_sets F I" 

678 
proof (rule indep_setsI[OF F(1)]) 

679 
fix A J assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J" 

680 
assume A: "\<forall>j\<in>J. A j \<in> F j" 

681 
let "?A j" = "if j \<in> J then A j else space M" 

682 
have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)" 

683 
using subset_trans[OF F(1) space_closed] J A 

684 
by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast 

685 
also 

686 
from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _") 

687 
by (auto split: split_if_asm) 

688 
with indep have "prob (\<Inter>j\<in>I. ?A j) = (\<Prod>j\<in>I. prob (?A j))" 

689 
by auto 

690 
also have "\<dots> = (\<Prod>j\<in>J. prob (A j))" 

691 
unfolding if_distrib setprod.If_cases[OF `finite I`] 

692 
using prob_space `J \<subseteq> I` by (simp add: Int_absorb1 setprod_1) 

693 
finally show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" .. 

694 
qed 

695 
qed 

696 

697 
lemma (in prob_space) indep_rv_finite: 

698 
fixes I :: "'i set" 

699 
assumes I: "I \<noteq> {}" "finite I" 

700 
and rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (sigma (M' i)) (X i)" 

701 
and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (M' i)" 

702 
and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> sets (M' i)" 

703 
shows "indep_rv (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow> 

42988  704 
(\<forall>A\<in>(\<Pi> i\<in>I. sets (M' i)). prob (\<Inter>j\<in>I. X j ` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j ` A j \<inter> space M)))" 
42987  705 
proof  
706 
from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" 

707 
unfolding measurable_def by simp 

708 

709 
{ fix i assume "i\<in>I" 

710 
have "sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (sigma (M' i))} 

711 
= sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (M' i)}" 

712 
unfolding sigma_sets_vimage_commute[OF X, OF `i \<in> I`] 

713 
by (subst sigma_sets_sigma_sets_eq) auto } 

714 
note this[simp] 

715 

716 
{ fix i assume "i\<in>I" 

717 
have "Int_stable \<lparr>space = space M, sets = {X i ` A \<inter> space M A. A \<in> sets (M' i)}\<rparr>" 

718 
proof (rule Int_stableI) 

719 
fix a assume "a \<in> {X i ` A \<inter> space M A. A \<in> sets (M' i)}" 

720 
then obtain A where "a = X i ` A \<inter> space M" "A \<in> sets (M' i)" by auto 

721 
moreover 

722 
fix b assume "b \<in> {X i ` A \<inter> space M A. A \<in> sets (M' i)}" 

723 
then obtain B where "b = X i ` B \<inter> space M" "B \<in> sets (M' i)" by auto 

724 
moreover 

725 
have "(X i ` A \<inter> space M) \<inter> (X i ` B \<inter> space M) = X i ` (A \<inter> B) \<inter> space M" by auto 

726 
moreover note Int_stable[OF `i \<in> I`] 

727 
ultimately 

728 
show "a \<inter> b \<in> {X i ` A \<inter> space M A. A \<in> sets (M' i)}" 

729 
by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD) 

730 
qed } 

731 
note indep_sets_sigma_sets_iff[OF this, simp] 

732 

733 
{ fix i assume "i \<in> I" 

734 
{ fix A assume "A \<in> sets (M' i)" 

735 
then have "A \<in> sets (sigma (M' i))" by (auto simp: sets_sigma intro: sigma_sets.Basic) 

736 
moreover 

737 
from rv[OF `i\<in>I`] have "X i \<in> measurable M (sigma (M' i))" by auto 

738 
ultimately 

739 
have "X i ` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) } 

740 
with X[OF `i\<in>I`] space[OF `i\<in>I`] 

741 
have "{X i ` A \<inter> space M A. A \<in> sets (M' i)} \<subseteq> events" 

742 
"space M \<in> {X i ` A \<inter> space M A. A \<in> sets (M' i)}" 

743 
by (auto intro!: exI[of _ "space (M' i)"]) } 

744 
note indep_sets_finite[OF I this, simp] 

745 

746 
have "(\<forall>A\<in>\<Pi> i\<in>I. {X i ` A \<inter> space M A. A \<in> sets (M' i)}. prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))) = 

747 
(\<forall>A\<in>\<Pi> i\<in>I. sets (M' i). prob ((\<Inter>j\<in>I. X j ` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x ` A x \<inter> space M)))" 

748 
(is "?L = ?R") 

749 
proof safe 

750 
fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. sets (M' i))" 

751 
from `?L`[THEN bspec, of "\<lambda>i. X i ` A i \<inter> space M"] A `I \<noteq> {}` 

752 
show "prob ((\<Inter>j\<in>I. X j ` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x ` A x \<inter> space M))" 

753 
by (auto simp add: Pi_iff) 

754 
next 

755 
fix A assume ?R and A: "A \<in> (\<Pi> i\<in>I. {X i ` A \<inter> space M A. A \<in> sets (M' i)})" 

756 
from A have "\<forall>i\<in>I. \<exists>B. A i = X i ` B \<inter> space M \<and> B \<in> sets (M' i)" by auto 

757 
from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i ` B i \<inter> space M" 

758 
"B \<in> (\<Pi> i\<in>I. sets (M' i))" by auto 

759 
from `?R`[THEN bspec, OF B(2)] B(1) `I \<noteq> {}` 

760 
show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))" 

761 
by simp 

762 
qed 

763 
then show ?thesis using `I \<noteq> {}` 

42988  764 
by (simp add: rv indep_rv_def) 
765 
qed 

766 

767 
lemma (in prob_space) indep_rv_compose: 

768 
assumes "indep_rv M' X I" 

769 
assumes rv: 

770 
"\<And>i. i \<in> I \<Longrightarrow> sigma_algebra (N i)" 

771 
"\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)" 

772 
shows "indep_rv N (\<lambda>i. Y i \<circ> X i) I" 

773 
unfolding indep_rv_def 

774 
proof 

775 
from rv `indep_rv M' X I` 

776 
show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)" 

777 
by (auto intro!: measurable_comp simp: indep_rv_def) 

778 

779 
have "indep_sets (\<lambda>i. sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (M' i)}) I" 

780 
using `indep_rv M' X I` by (simp add: indep_rv_def) 

781 
then show "indep_sets (\<lambda>i. sigma_sets (space M) {(Y i \<circ> X i) ` A \<inter> space M A. A \<in> sets (N i)}) I" 

782 
proof (rule indep_sets_mono_sets) 

783 
fix i assume "i \<in> I" 

784 
with `indep_rv M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)" 

785 
unfolding indep_rv_def measurable_def by auto 

786 
{ fix A assume "A \<in> sets (N i)" 

787 
then have "\<exists>B. (Y i \<circ> X i) ` A \<inter> space M = X i ` B \<inter> space M \<and> B \<in> sets (M' i)" 

788 
by (intro exI[of _ "Y i ` A \<inter> space (M' i)"]) 

789 
(auto simp: vimage_compose intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) } 

790 
then show "sigma_sets (space M) {(Y i \<circ> X i) ` A \<inter> space M A. A \<in> sets (N i)} \<subseteq> 

791 
sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (M' i)}" 

792 
by (intro sigma_sets_subseteq) (auto simp: vimage_compose) 

793 
qed 

794 
qed 

795 

796 
lemma (in prob_space) indep_rvD: 

797 
assumes X: "indep_rv M' X I" 

798 
assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)" 

799 
shows "prob (\<Inter>i\<in>I. X i ` A i \<inter> space M) = (\<Prod>i\<in>I. prob (X i ` A i \<inter> space M))" 

800 
proof (rule indep_setsD) 

801 
show "indep_sets (\<lambda>i. sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (M' i)}) I" 

802 
using X by (auto simp: indep_rv_def) 

803 
show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto 

804 
show "\<forall>i\<in>I. X i ` A i \<inter> space M \<in> sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (M' i)}" 

805 
using I by (auto intro: sigma_sets.Basic) 

806 
qed 

807 

808 
lemma (in prob_space) indep_distribution_eq_measure: 

809 
assumes I: "I \<noteq> {}" "finite I" 

810 
assumes rv: "\<And>i. random_variable (M' i) (X i)" 

811 
shows "indep_rv M' X I \<longleftrightarrow> 

812 
(\<forall>A\<in>sets (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)). 

813 
distribution (\<lambda>x. \<lambda>i\<in>I. X i x) A = 

814 
finite_measure.\<mu>' (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := extreal\<circ>distribution (X i) \<rparr>)) A)" 

815 
(is "_ \<longleftrightarrow> (\<forall>X\<in>_. distribution ?D X = finite_measure.\<mu>' (Pi\<^isub>M I ?M) X)") 

816 
proof  

817 
interpret M': prob_space "?M i" for i 

818 
using rv by (rule distribution_prob_space) 

819 
interpret P: finite_product_prob_space ?M I 

820 
proof qed fact 

821 

822 
let ?D' = "(Pi\<^isub>M I ?M) \<lparr> measure := extreal \<circ> distribution ?D \<rparr>" 

823 
have "random_variable P.P ?D" 

824 
using `finite I` rv by (intro random_variable_restrict) auto 

825 
then interpret D: prob_space ?D' 

826 
by (rule distribution_prob_space) 

827 

828 
show ?thesis 

829 
proof (intro iffI ballI) 

830 
assume "indep_rv M' X I" 

831 
fix A assume "A \<in> sets P.P" 

832 
moreover 

833 
have "D.prob A = P.prob A" 

834 
proof (rule prob_space_unique_Int_stable) 

835 
show "prob_space ?D'" by default 

836 
show "prob_space (Pi\<^isub>M I ?M)" by default 

837 
show "Int_stable P.G" using M'.Int 

838 
by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def) 

839 
show "space P.G \<in> sets P.G" 

840 
using M'.top by (simp add: product_algebra_generator_def) 

841 
show "space ?D' = space P.G" "sets ?D' = sets (sigma P.G)" 

842 
by (simp_all add: product_algebra_def product_algebra_generator_def sets_sigma) 

843 
show "space P.P = space P.G" "sets P.P = sets (sigma P.G)" 

844 
by (simp_all add: product_algebra_def) 

845 
show "A \<in> sets (sigma P.G)" 

846 
using `A \<in> sets P.P` by (simp add: product_algebra_def) 

847 

848 
fix E assume E: "E \<in> sets P.G" 

849 
then have "E \<in> sets P.P" 

850 
by (simp add: sets_sigma sigma_sets.Basic product_algebra_def) 

851 
then have "D.prob E = distribution ?D E" 

852 
unfolding D.\<mu>'_def by simp 

853 
also 

854 
from E obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (M' i)" 

855 
by (auto simp: product_algebra_generator_def) 

856 
with `I \<noteq> {}` have "distribution ?D E = prob (\<Inter>i\<in>I. X i ` F i \<inter> space M)" 

857 
using `I \<noteq> {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def) 

858 
also have "\<dots> = (\<Prod>i\<in>I. prob (X i ` F i \<inter> space M))" 

859 
using `indep_rv M' X I` I F by (rule indep_rvD) 

860 
also have "\<dots> = P.prob E" 

861 
using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\<mu>'_def distribution_def) 

862 
finally show "D.prob E = P.prob E" . 

863 
qed 

864 
ultimately show "distribution ?D A = P.prob A" 

865 
by (simp add: D.\<mu>'_def) 

866 
next 

867 
assume eq: "\<forall>A\<in>sets P.P. distribution ?D A = P.prob A" 

868 
have [simp]: "\<And>i. sigma (M' i) = M' i" 

869 
using rv by (intro sigma_algebra.sigma_eq) simp 

870 
have "indep_rv (\<lambda>i. sigma (M' i)) X I" 

871 
proof (subst indep_rv_finite[OF I]) 

872 
fix i assume [simp]: "i \<in> I" 

873 
show "random_variable (sigma (M' i)) (X i)" 

874 
using rv[of i] by simp 

875 
show "Int_stable (M' i)" "space (M' i) \<in> sets (M' i)" 

876 
using M'.Int[of _ i] M'.top by (auto simp: Int_stable_def) 

877 
next 

878 
show "\<forall>A\<in>\<Pi> i\<in>I. sets (M' i). prob (\<Inter>j\<in>I. X j ` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j ` A j \<inter> space M))" 

879 
proof 

880 
fix A assume A: "A \<in> (\<Pi> i\<in>I. sets (M' i))" 

881 
then have A_in_P: "(Pi\<^isub>E I A) \<in> sets P.P" 

882 
by (auto intro!: product_algebraI) 

883 
have "prob (\<Inter>j\<in>I. X j ` A j \<inter> space M) = distribution ?D (Pi\<^isub>E I A)" 

884 
using `I \<noteq> {}`by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def) 

885 
also have "\<dots> = P.prob (Pi\<^isub>E I A)" using A_in_P eq by simp 

886 
also have "\<dots> = (\<Prod>i\<in>I. M'.prob i (A i))" 

887 
using A by (intro P.prob_times) auto 

888 
also have "\<dots> = (\<Prod>i\<in>I. prob (X i ` A i \<inter> space M))" 

889 
using A by (auto intro!: setprod_cong simp: M'.\<mu>'_def Pi_iff distribution_def) 

890 
finally show "prob (\<Inter>j\<in>I. X j ` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j ` A j \<inter> space M))" . 

891 
qed 

892 
qed 

893 
then show "indep_rv M' X I" 

894 
by simp 

895 
qed 

42987  896 
qed 
897 

42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

898 
end 