author  hoelzl 
Thu, 26 May 2011 14:12:06 +0200  
changeset 42987  73e2d802ea41 
parent 42985  1fb670792708 
child 42988  d8f3fc934ff6 
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 dynkin_systemI': 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

124 
assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

125 
assumes empty: "{} \<in> sets M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

126 
assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M  A \<in> sets M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

127 
assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

128 
\<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

129 
shows "dynkin_system M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

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

131 
from Diff[OF empty] have "space M \<in> sets M" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

132 
from 1 this Diff 2 show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

133 
by (intro dynkin_systemI) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

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

135 

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

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

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

138 
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

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

140 
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

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

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

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

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

145 
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

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

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

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

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

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

151 
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

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

153 
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

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

155 
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

156 
\<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

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

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

159 
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

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

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

162 
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

163 
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

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

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

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

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

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

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

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

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

172 
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

173 
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

174 
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

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

176 
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

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

178 
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

179 
using J by 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 
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

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

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

184 
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

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

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

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

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

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

190 
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

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

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

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

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

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

196 
have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>" 
42987  197 
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

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

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

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

201 
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

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

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

204 
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

205 
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

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

207 
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

208 
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

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

210 
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

211 
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

212 
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

213 
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

214 
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

215 
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

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

217 
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

218 
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

219 
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

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

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

222 
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

223 
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

224 
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

225 
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

226 
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

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

228 
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

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

230 
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

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

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

233 
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

234 
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

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

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

237 
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

238 
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

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

240 
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

241 
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

242 
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

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

244 
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

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

246 
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

247 
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

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

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

250 
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

251 
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

252 
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

253 
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

254 
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

255 
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

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

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

258 
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

259 
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

260 
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

261 
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

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

263 
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

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

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

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

267 
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

268 
sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>" 
42987  269 
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

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

271 
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

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

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

274 
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

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

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

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

278 
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

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

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

281 
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

282 
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

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

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

285 
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

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

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

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

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

290 
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

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

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

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

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

295 
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

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

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

298 
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

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

300 
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

301 
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

302 
by (rule indep_sets_mono_sets) 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 

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

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

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

307 
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

308 
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

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

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

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

312 
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

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

314 
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

315 
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

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

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

318 

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

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

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

321 
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

322 
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

323 
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

324 

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

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

328 
proof 

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

330 
by (rule indep_sets_sigma_sets) fact 

331 
next 

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

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

334 
qed 

335 

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

336 
lemma (in prob_space) indep_sets2_eq: 
42981  337 
"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)" 
338 
unfolding indep_set_def 

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

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

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

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

342 
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

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

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

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

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

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

348 
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

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

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

351 
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

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

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

354 
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

355 
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

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

357 
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

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

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

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

361 

42981  362 
lemma (in prob_space) indep_set_sigma_sets: 
363 
assumes "indep_set A B" 

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

364 
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

365 
assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>" 
42981  366 
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

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

368 
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

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

370 
show "indep_sets (bool_case A B) UNIV" 
42981  371 
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

372 
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

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

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

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

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

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

379 

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

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

383 
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>" 

384 
assumes disjoint: "disjoint_family_on I J" 

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

386 
proof  

387 
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) }" 

388 

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

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

393 
assume "j \<in> J" 

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

395 
using sets_into_space by (intro sigma_algebra_sigma) auto 

396 

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

398 
proof (rule sigma_sets_eqI) 

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

400 
then guess i .. 

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

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

403 
next 

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

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

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

407 
by auto 

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

409 
by (safe intro!: S.finite_INT) 

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

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

412 
by (simp add: sets_sigma) 

413 
qed } 

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

415 
proof (rule indep_sets_sigma_sets) 

416 
show "indep_sets ?E J" 

417 
proof (intro indep_setsI) 

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

419 
next 

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

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

422 
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)" 

423 
by simp 

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

425 
from bchoice[OF this] obtain L 

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

427 
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" 

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

429 
by auto 

430 

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

432 
have "k = j" 

433 
proof (rule ccontr) 

434 
assume "k \<noteq> j" 

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

436 
unfolding disjoint_family_on_def by auto 

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

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

439 
qed } 

440 
note L_inj = this 

441 

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

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

444 
have "k l = j" unfolding k_def 

445 
proof (rule some_equality) 

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

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

448 
qed (insert *, simp) } 

449 
note k_simp[simp] = this 

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

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

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

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

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

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

456 
using K L L_inj by (subst setprod_UN_disjoint) auto 

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

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

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

460 
qed 

461 
next 

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

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

464 
proof (rule Int_stableI) 

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

466 
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 

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

468 
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 

469 
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 {})" 

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

471 
by (simp add: a b set_eq_iff) auto 

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

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

474 
qed 

475 
qed 

476 
ultimately show ?thesis 

477 
by (simp cong: indep_sets_cong) 

478 
qed 

479 

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

482 

483 
lemma (in prob_space) terminal_events_sets: 

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

42983  487 
shows "X \<in> events" 
42982  488 
proof  
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 
from X have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def) 

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

42983  493 
then show "X \<in> events" 
42982  494 
by induct (insert A, auto) 
495 
qed 

496 

497 
lemma (in prob_space) sigma_algebra_terminal_events: 

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

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

500 
unfolding terminal_events_def 

501 
proof (simp add: sigma_algebra_iff2, safe) 

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

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

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

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

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

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

508 
by induct (insert A.sets_into_space, auto) 

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

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

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

512 
by (intro sigma_sets.Union) auto } 

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

514 

515 
lemma (in prob_space) kolmogorov_0_1_law: 

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

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

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

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

522 
proof  

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

526 
by (rule sigma_algebra_terminal_events) fact 

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

528 

42983  529 
have X_in: "X \<in> events" 
42982  530 
by (rule terminal_events_sets) fact+ 
531 

532 
interpret D: dynkin_system ?D 

533 
proof (rule dynkin_systemI) 

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

535 
using sets_into_space by auto 

536 
next 

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

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

539 
next 

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

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

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

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

544 
using X_in A by (intro finite_measure_Diff) auto 

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

546 
using A prob_space by auto 

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

548 
using X_in A sets_into_space 

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

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

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

552 
next 

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

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

555 
by auto 

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

557 
proof (rule finite_measure_UNION) 

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

559 
using F X_in by auto 

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

561 
using dis by (rule disjoint_family_on_bisimulation) auto 

562 
qed 

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

564 
by simp 

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

566 
by (intro mult_right.sums finite_measure_UNION F dis) 

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

568 
by (auto dest!: sums_unique) 

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

570 
by auto 

571 
qed 

572 

573 
{ fix n 

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

575 
proof (rule indep_sets_collect_sigma) 

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

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

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

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

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

581 
fix m 

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

583 
unfolding Int_stable_def using A.Int by auto 

584 
qed 

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

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

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

588 
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))" 

589 
unfolding indep_set_def by simp 

590 

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

592 
proof (simp add: subset_eq, rule) 

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

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

595 
using X unfolding terminal_events_def by simp 

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

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

598 
by (auto simp add: ac_simps) 

599 
qed } 

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

601 
by auto 

602 

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

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

605 
proof (rule sigma_eq_dynkin) 

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

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

608 
by induct (insert A sets_into_space, auto) } 

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

610 
show "Int_stable ?UA" 

611 
proof (rule Int_stableI) 

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

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

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

615 
using A sets_into_space by (intro sigma_algebra_sigma) auto 

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

617 
by (intro sigma_sets_subseteq UN_mono) auto 

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

619 
moreover 

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

621 
by (intro sigma_sets_subseteq UN_mono) auto 

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

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

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

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

626 
qed 

627 
qed 

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

629 
proof (rule D.dynkin_subset) 

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

631 
qed simp 

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

633 
moreover 

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

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

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

637 
unfolding sets_sigma terminal_events_def by auto 

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

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

640 
then show ?thesis by auto 

641 
qed 

642 

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

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

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

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

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

649 
using F(1) sets_into_space 

650 
by (subst sigma_sets_singleton) auto 

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

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

653 
by (auto simp add: sigma_def) } 

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

655 
proof (rule indep_sets_sigma_sets) 

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

657 
unfolding indep_sets_singleton_iff_indep_events by fact 

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

659 
unfolding Int_stable_def by simp 

660 
qed 

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

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

663 
unfolding terminal_events_def 

664 
proof 

665 
fix j 

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

667 
using order_trans[OF F(1) space_closed] 

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

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

670 
by (intro decseq_SucI INT_decseq_offset UN_mono) auto 

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

672 
using order_trans[OF F(1) space_closed] 

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

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

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

676 
by (simp add: sets_sigma) 

677 
qed 

678 
qed 

679 

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

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

683 
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)))" 

684 
proof 

685 
assume *: "indep_sets F I" 

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

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

688 
next 

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

690 
show "indep_sets F I" 

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

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

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

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

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

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

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

698 
also 

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

700 
by (auto split: split_if_asm) 

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

702 
by auto 

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

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

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

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

707 
qed 

708 
qed 

709 

710 
lemma (in prob_space) indep_rv_finite: 

711 
fixes I :: "'i set" 

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

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

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

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

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

717 
(\<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. distribution (X j) (A j)))" 

718 
proof  

719 
from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" 

720 
unfolding measurable_def by simp 

721 

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

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

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

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

726 
by (subst sigma_sets_sigma_sets_eq) auto } 

727 
note this[simp] 

728 

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

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

731 
proof (rule Int_stableI) 

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

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

734 
moreover 

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

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

737 
moreover 

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

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

740 
ultimately 

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

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

743 
qed } 

744 
note indep_sets_sigma_sets_iff[OF this, simp] 

745 

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

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

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

749 
moreover 

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

751 
ultimately 

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

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

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

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

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

757 
note indep_sets_finite[OF I this, simp] 

758 

759 
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))) = 

760 
(\<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)))" 

761 
(is "?L = ?R") 

762 
proof safe 

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

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

765 
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))" 

766 
by (auto simp add: Pi_iff) 

767 
next 

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

769 
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 

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

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

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

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

774 
by simp 

775 
qed 

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

777 
by (simp add: rv distribution_def indep_rv_def) 

778 
qed 

779 

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

780 
end 