author  hoelzl 
Wed, 10 Oct 2012 12:12:14 +0200  
changeset 49772  75660d89c339 
parent 47694  05663f75964c 
child 49776  199d1d5bb17e 
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 
47694  8 
imports Probability_Measure Infinite_Product_Measure 
42861
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) 
42989  40 
"indep_vars M' X I \<longleftrightarrow> 
42861
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 

42989  44 
definition (in prob_space) 
45 
"indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV" 

46 

47694  47 
lemma (in prob_space) indep_sets_cong: 
42981  48 
"I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i = G i) \<Longrightarrow> indep_sets F I \<longleftrightarrow> indep_sets G J" 
49 
by (simp add: indep_sets_def, intro conj_cong all_cong imp_cong ball_cong) blast+ 

50 

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

53 
unfolding indep_sets_def indep_events_def 

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

55 

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

58 
by (auto simp: indep_events_def) 

59 

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

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

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

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

63 
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

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

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

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

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

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

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

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

71 

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

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

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

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

75 

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

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

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

78 
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

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

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

81 
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

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

83 
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

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

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

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

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

88 

49772  89 
lemma (in prob_space) indep_sets_mono: 
90 
assumes indep: "indep_sets F I" 

91 
assumes mono: "J \<subseteq> I" "\<And>i. i\<in>J \<Longrightarrow> G i \<subseteq> F i" 

92 
shows "indep_sets G J" 

93 
apply (rule indep_sets_mono_sets) 

94 
apply (rule indep_sets_mono_index) 

95 
apply (fact +) 

96 
done 

97 

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

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

99 
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

100 
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

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

102 
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

103 

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

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

105 
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

106 
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

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

108 

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

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

112 
shows "indep_set A B" 

113 
unfolding indep_set_def 

114 
proof (rule indep_setsI) 

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

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

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

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

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

120 
unfolding UNIV_bool Pow_insert by (auto simp: ac_simps) 

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

122 

123 
lemma (in prob_space) indep_setD: 

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

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

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

127 
by (simp add: ac_simps UNIV_bool) 

128 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

129 
lemma (in prob_space) indep_var_eq: 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

130 
"indep_var S X T Y \<longleftrightarrow> 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

131 
(random_variable S X \<and> random_variable T Y) \<and> 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

132 
indep_set 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

133 
(sigma_sets (space M) { X ` A \<inter> space M  A. A \<in> sets S}) 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

134 
(sigma_sets (space M) { Y ` A \<inter> space M  A. A \<in> sets T})" 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

135 
unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

136 
by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext) 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

137 
(auto split: bool.split) 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

138 

42982  139 
lemma (in prob_space) 
140 
assumes indep: "indep_set A B" 

42983  141 
shows indep_setD_ev1: "A \<subseteq> events" 
142 
and indep_setD_ev2: "B \<subseteq> events" 

42982  143 
using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto 
144 

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

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

146 
assumes indep: "indep_sets F I" 
47694  147 
shows "indep_sets (\<lambda>i. dynkin (space M) (F i)) I" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

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

149 
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

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

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

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

153 
{ fix J K assume "indep_sets F K" 
46731  154 
let ?G = "\<lambda>S i. if i \<in> S then ?F i else F i" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

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

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

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

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

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

160 
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

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

162 
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

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

164 
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

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

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

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

168 
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

169 
using G X by auto 
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 
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

172 
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

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

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

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

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

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

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

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

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

181 
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

182 
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

183 
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

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

185 
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

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

187 
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

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

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

190 
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

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

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

193 
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

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

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

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

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

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

199 
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

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

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

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

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

204 
note indep_sets_insert = this 
47694  205 
have "dynkin_system (space M) ?D" 
42987  206 
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

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

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

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

210 
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

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

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

213 
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

214 
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

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

216 
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

217 
prob ((\<Inter>j\<in>J. A j)  (\<Inter>i\<in>insert j J. (A(j := X)) i))" 
47694  218 
using A_sets sets_into_space[of _ M] X `J \<noteq> {}` 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

219 
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

220 
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

221 
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

222 
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

223 
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

224 
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

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

226 
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

227 
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

228 
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

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

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

231 
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

232 
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

233 
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

234 
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

235 
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

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

237 
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

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

239 
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

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

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

242 
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

243 
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

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

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

246 
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

247 
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

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

249 
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

250 
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

251 
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

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

253 
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

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

255 
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

256 
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

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

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

259 
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

260 
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

261 
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

262 
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

263 
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

264 
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

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

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

267 
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

268 
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

269 
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

270 
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

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

272 
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

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

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

275 
qed (insert sets_into_space, auto) 
47694  276 
then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}" 
277 
proof (rule dynkin_system.dynkin_subset, safe) 

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

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

279 
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

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

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

282 
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

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

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

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

286 
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

287 
using G(2) by 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 
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

290 
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

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

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

293 
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

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

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

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

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

298 
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

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

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

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

302 
qed 
47694  303 
then have "indep_sets (G(j := dynkin (space M) (G j))) K" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

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

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

306 
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

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

308 
from this[OF `indep_sets F J` `finite J` subset_refl] 
47694  309 
show "indep_sets ?F J" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

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

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

312 

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

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

314 
assumes indep: "indep_sets F I" 
47694  315 
assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)" 
316 
shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" 

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

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

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

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

320 
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

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

322 
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

323 
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

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

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

326 

42987  327 
lemma (in prob_space) indep_sets_sigma_sets_iff: 
47694  328 
assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)" 
42987  329 
shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I \<longleftrightarrow> indep_sets F I" 
330 
proof 

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

47694  332 
by (rule indep_sets_sigma) fact 
42987  333 
next 
334 
assume "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" then show "indep_sets F I" 

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

336 
qed 

337 

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

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

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

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

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

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

344 
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

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

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

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

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

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

350 
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

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

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

353 
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

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

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

356 
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

357 
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

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

359 
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

360 
using X * by 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 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

363 

42981  364 
lemma (in prob_space) indep_set_sigma_sets: 
365 
assumes "indep_set A B" 

47694  366 
assumes A: "Int_stable A" and B: "Int_stable B" 
42981  367 
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

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

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

371 
show "indep_sets (bool_case A B) UNIV" 
42981  372 
by (rule `indep_set A B`[unfolded indep_set_def]) 
47694  373 
fix i show "Int_stable (case i of True \<Rightarrow> A  False \<Rightarrow> B)" 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

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

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

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

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

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

380 

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

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

47694  384 
assumes Int_stable: "\<And>i j. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> Int_stable (E i)" 
42981  385 
assumes disjoint: "disjoint_family_on I J" 
386 
shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J" 

387 
proof  

46731  388 
let ?E = "\<lambda>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) }" 
42981  389 

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

47694  393 
let ?S = "sigma_sets (space M) (\<Union>i\<in>I j. E i)" 
42981  394 
assume "j \<in> J" 
47694  395 
from E[OF this] interpret S: sigma_algebra "space M" ?S 
396 
using sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto 

42981  397 

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

399 
proof (rule sigma_sets_eqI) 

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

401 
then guess i .. 

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

47694  403 
by (auto intro!: sigma_sets.intros(2) exI[of _ "{i}"] exI[of _ "\<lambda>i. A"]) 
42981  404 
next 
405 
fix A assume "A \<in> ?E j" 

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

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

408 
by auto 

47694  409 
then have "A \<in> ?S" unfolding A 
410 
by (safe intro!: S.finite_INT) auto 

42981  411 
then show "A \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i)" 
47694  412 
by simp 
42981  413 
qed } 
414 
moreover have "indep_sets (\<lambda>j. sigma_sets (space M) (?E j)) J" 

47694  415 
proof (rule indep_sets_sigma) 
42981  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 

46731  450 
let ?E' = "\<lambda>l. E' (k l) l" 
42981  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" 

47694  463 
show "Int_stable (?E j)" 
42981  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 

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

42982  482 

49772  483 
lemma (in prob_space) tail_events_sets: 
484 
assumes A: "\<And>i::nat. A i \<subseteq> events" 

485 
shows "tail_events A \<subseteq> events" 

486 
proof 

487 
fix X assume X: "X \<in> tail_events A" 

42982  488 
let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" 
49772  489 
from X have "\<And>n::nat. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def) 
42982  490 
from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp 
42983  491 
then show "X \<in> events" 
42982  492 
by induct (insert A, auto) 
493 
qed 

494 

49772  495 
lemma (in prob_space) sigma_algebra_tail_events: 
47694  496 
assumes "\<And>i::nat. sigma_algebra (space M) (A i)" 
49772  497 
shows "sigma_algebra (space M) (tail_events A)" 
498 
unfolding tail_events_def 

42982  499 
proof (simp add: sigma_algebra_iff2, safe) 
500 
let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" 

47694  501 
interpret A: sigma_algebra "space M" "A i" for i by fact 
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

502 
{ fix X x assume "X \<in> ?A" "x \<in> X" 
42982  503 
then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto 
504 
from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp 

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

506 
by induct (insert A.sets_into_space, auto) 

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

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

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

510 
by (intro sigma_sets.Union) auto } 

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

512 

513 
lemma (in prob_space) kolmogorov_0_1_law: 

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

42983  515 
assumes A: "\<And>i. A i \<subseteq> events" 
47694  516 
assumes "\<And>i::nat. sigma_algebra (space M) (A i)" 
42982  517 
assumes indep: "indep_sets A UNIV" 
49772  518 
and X: "X \<in> tail_events A" 
42982  519 
shows "prob X = 0 \<or> prob X = 1" 
520 
proof  

47694  521 
let ?D = "{D \<in> events. prob (X \<inter> D) = prob X * prob D}" 
522 
interpret A: sigma_algebra "space M" "A i" for i by fact 

49772  523 
interpret T: sigma_algebra "space M" "tail_events A" 
524 
by (rule sigma_algebra_tail_events) fact 

42982  525 
have "X \<subseteq> space M" using T.space_closed X by auto 
526 

42983  527 
have X_in: "X \<in> events" 
49772  528 
using tail_events_sets A X by auto 
42982  529 

47694  530 
interpret D: dynkin_system "space M" ?D 
42982  531 
proof (rule dynkin_systemI) 
47694  532 
fix D assume "D \<in> ?D" then show "D \<subseteq> space M" 
42982  533 
using sets_into_space by auto 
534 
next 

47694  535 
show "space M \<in> ?D" 
42982  536 
using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2) 
537 
next 

47694  538 
fix A assume A: "A \<in> ?D" 
42982  539 
have "prob (X \<inter> (space M  A)) = prob (X  (X \<inter> A))" 
540 
using `X \<subseteq> space M` by (auto intro!: arg_cong[where f=prob]) 

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

542 
using X_in A by (intro finite_measure_Diff) auto 

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

544 
using A prob_space by auto 

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

546 
using X_in A sets_into_space 

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

47694  548 
finally show "space M  A \<in> ?D" 
42982  549 
using A `X \<subseteq> space M` by auto 
550 
next 

47694  551 
fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> ?D" 
42982  552 
then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)" 
553 
by auto 

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

555 
proof (rule finite_measure_UNION) 

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

557 
using F X_in by auto 

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

559 
using dis by (rule disjoint_family_on_bisimulation) auto 

560 
qed 

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

562 
by simp 

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

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
43920
diff
changeset

564 
by (intro sums_mult finite_measure_UNION F dis) 
42982  565 
ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)" 
566 
by (auto dest!: sums_unique) 

47694  567 
with F show "(\<Union>i. F i) \<in> ?D" 
42982  568 
by auto 
569 
qed 

570 

571 
{ fix n 

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

573 
proof (rule indep_sets_collect_sigma) 

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

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

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

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

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

579 
fix m 

47694  580 
show "Int_stable (A m)" 
42982  581 
unfolding Int_stable_def using A.Int by auto 
582 
qed 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

583 
also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) = 
42982  584 
bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))" 
585 
by (auto intro!: ext split: bool.split) 

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

587 
unfolding indep_set_def by simp 

588 

47694  589 
have "sigma_sets (space M) (\<Union>m\<in>{..n}. A m) \<subseteq> ?D" 
42982  590 
proof (simp add: subset_eq, rule) 
591 
fix D assume D: "D \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" 

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

49772  593 
using X unfolding tail_events_def by simp 
42982  594 
from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D 
595 
show "D \<in> events \<and> prob (X \<inter> D) = prob X * prob D" 

596 
by (auto simp add: ac_simps) 

597 
qed } 

47694  598 
then have "(\<Union>n. sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) \<subseteq> ?D" (is "?A \<subseteq> _") 
42982  599 
by auto 
600 

49772  601 
note `X \<in> tail_events A` 
47694  602 
also { 
603 
have "\<And>n. sigma_sets (space M) (\<Union>i\<in>{n..}. A i) \<subseteq> sigma_sets (space M) ?A" 

604 
by (intro sigma_sets_subseteq UN_mono) auto 

49772  605 
then have "tail_events A \<subseteq> sigma_sets (space M) ?A" 
606 
unfolding tail_events_def by auto } 

47694  607 
also have "sigma_sets (space M) ?A = dynkin (space M) ?A" 
42982  608 
proof (rule sigma_eq_dynkin) 
609 
{ fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" 

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

47694  611 
by induct (insert A sets_into_space[of _ M], auto) } 
612 
then show "?A \<subseteq> Pow (space M)" by auto 

613 
show "Int_stable ?A" 

42982  614 
proof (rule Int_stableI) 
615 
fix a assume "a \<in> ?A" then guess n .. note a = this 

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

47694  617 
interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" 
618 
using A sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto 

42982  619 
have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" 
620 
by (intro sigma_sets_subseteq UN_mono) auto 

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

622 
moreover 

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

624 
by (intro sigma_sets_subseteq UN_mono) auto 

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

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

47694  627 
using Amn.Int[of a b] by simp 
42982  628 
then show "a \<inter> b \<in> (\<Union>n. sigma_sets (space M) (\<Union>i\<in>{..n}. A i))" by auto 
629 
qed 

630 
qed 

47694  631 
also have "dynkin (space M) ?A \<subseteq> ?D" 
632 
using `?A \<subseteq> ?D` by (auto intro!: D.dynkin_subset) 

633 
finally show ?thesis by auto 

42982  634 
qed 
635 

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

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

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

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

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

642 
using F(1) sets_into_space 

643 
by (subst sigma_sets_singleton) auto 

47694  644 
{ fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})" 
645 
using sigma_algebra_sigma_sets[of "{F i}" "space M"] F sets_into_space 

646 
by auto } 

42985  647 
show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV" 
47694  648 
proof (rule indep_sets_sigma) 
42985  649 
show "indep_sets (\<lambda>i. {F i}) UNIV" 
650 
unfolding indep_sets_singleton_iff_indep_events by fact 

47694  651 
fix i show "Int_stable {F i}" 
42985  652 
unfolding Int_stable_def by simp 
653 
qed 

46731  654 
let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i" 
49772  655 
show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> tail_events (\<lambda>i. sigma_sets (space M) {F i})" 
656 
unfolding tail_events_def 

42985  657 
proof 
658 
fix j 

47694  659 
interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" 
42985  660 
using order_trans[OF F(1) space_closed] 
47694  661 
by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq) 
42985  662 
have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)" 
663 
by (intro decseq_SucI INT_decseq_offset UN_mono) auto 

47694  664 
also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" 
42985  665 
using order_trans[OF F(1) space_closed] 
666 
by (safe intro!: S.countable_INT S.countable_UN) 

47694  667 
(auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI) 
42985  668 
finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" 
47694  669 
by simp 
42985  670 
qed 
671 
qed 

672 

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

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

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

677 
proof 

678 
assume *: "indep_sets F I" 

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

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

681 
next 

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

683 
show "indep_sets F I" 

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

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

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

46731  687 
let ?A = "\<lambda>j. if j \<in> J then A j else space M" 
42987  688 
have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)" 
689 
using subset_trans[OF F(1) space_closed] J A 

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

691 
also 

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

693 
by (auto split: split_if_asm) 

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

695 
by auto 

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

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

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

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

700 
qed 

701 
qed 

702 

42989  703 
lemma (in prob_space) indep_vars_finite: 
42987  704 
fixes I :: "'i set" 
705 
assumes I: "I \<noteq> {}" "finite I" 

47694  706 
and M': "\<And>i. i \<in> I \<Longrightarrow> sets (M' i) = sigma_sets (space (M' i)) (E i)" 
707 
and rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (M' i) (X i)" 

708 
and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (E i)" 

709 
and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> E i" and closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M' i))" 

710 
shows "indep_vars M' X I \<longleftrightarrow> 

711 
(\<forall>A\<in>(\<Pi> i\<in>I. E 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  712 
proof  
713 
from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" 

714 
unfolding measurable_def by simp 

715 

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

47694  717 
from closed[OF `i \<in> I`] 
718 
have "sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (M' i)} 

719 
= sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> E i}" 

720 
unfolding sigma_sets_vimage_commute[OF X, OF `i \<in> I`, symmetric] M'[OF `i \<in> I`] 

42987  721 
by (subst sigma_sets_sigma_sets_eq) auto } 
47694  722 
note sigma_sets_X = this 
42987  723 

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

47694  725 
have "Int_stable {X i ` A \<inter> space M A. A \<in> E i}" 
42987  726 
proof (rule Int_stableI) 
47694  727 
fix a assume "a \<in> {X i ` A \<inter> space M A. A \<in> E i}" 
728 
then obtain A where "a = X i ` A \<inter> space M" "A \<in> E i" by auto 

42987  729 
moreover 
47694  730 
fix b assume "b \<in> {X i ` A \<inter> space M A. A \<in> E i}" 
731 
then obtain B where "b = X i ` B \<inter> space M" "B \<in> E i" by auto 

42987  732 
moreover 
733 
have "(X i ` A \<inter> space M) \<inter> (X i ` B \<inter> space M) = X i ` (A \<inter> B) \<inter> space M" by auto 

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

735 
ultimately 

47694  736 
show "a \<inter> b \<in> {X i ` A \<inter> space M A. A \<in> E i}" 
42987  737 
by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD) 
738 
qed } 

47694  739 
note indep_sets_X = indep_sets_sigma_sets_iff[OF this] 
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

740 

42987  741 
{ fix i assume "i \<in> I" 
47694  742 
{ fix A assume "A \<in> E i" 
743 
with M'[OF `i \<in> I`] have "A \<in> sets (M' i)" by auto 

42987  744 
moreover 
47694  745 
from rv[OF `i\<in>I`] have "X i \<in> measurable M (M' i)" by auto 
42987  746 
ultimately 
747 
have "X i ` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) } 

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

47694  749 
have "{X i ` A \<inter> space M A. A \<in> E i} \<subseteq> events" 
750 
"space M \<in> {X i ` A \<inter> space M A. A \<in> E i}" 

42987  751 
by (auto intro!: exI[of _ "space (M' i)"]) } 
47694  752 
note indep_sets_finite_X = indep_sets_finite[OF I this] 
43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

753 

47694  754 
have "(\<forall>A\<in>\<Pi> i\<in>I. {X i ` A \<inter> space M A. A \<in> E i}. prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))) = 
755 
(\<forall>A\<in>\<Pi> i\<in>I. E 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)))" 

42987  756 
(is "?L = ?R") 
757 
proof safe 

47694  758 
fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. E i)" 
42987  759 
from `?L`[THEN bspec, of "\<lambda>i. X i ` A i \<inter> space M"] A `I \<noteq> {}` 
760 
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))" 

761 
by (auto simp add: Pi_iff) 

762 
next 

47694  763 
fix A assume ?R and A: "A \<in> (\<Pi> i\<in>I. {X i ` A \<inter> space M A. A \<in> E i})" 
764 
from A have "\<forall>i\<in>I. \<exists>B. A i = X i ` B \<inter> space M \<and> B \<in> E i" by auto 

42987  765 
from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i ` B i \<inter> space M" 
47694  766 
"B \<in> (\<Pi> i\<in>I. E i)" by auto 
42987  767 
from `?R`[THEN bspec, OF B(2)] B(1) `I \<noteq> {}` 
768 
show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))" 

769 
by simp 

770 
qed 

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

47694  772 
by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong) 
42988  773 
qed 
774 

42989  775 
lemma (in prob_space) indep_vars_compose: 
776 
assumes "indep_vars M' X I" 

47694  777 
assumes rv: "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)" 
42989  778 
shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I" 
779 
unfolding indep_vars_def 

42988  780 
proof 
42989  781 
from rv `indep_vars M' X I` 
42988  782 
show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)" 
47694  783 
by (auto simp: indep_vars_def) 
42988  784 

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

42989  786 
using `indep_vars M' X I` by (simp add: indep_vars_def) 
42988  787 
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" 
788 
proof (rule indep_sets_mono_sets) 

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

42989  790 
with `indep_vars M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)" 
791 
unfolding indep_vars_def measurable_def by auto 

42988  792 
{ fix A assume "A \<in> sets (N i)" 
793 
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)" 

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

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

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

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

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

799 
qed 

800 
qed 

801 

47694  802 
lemma (in prob_space) indep_varsD_finite: 
42989  803 
assumes X: "indep_vars M' X I" 
42988  804 
assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)" 
805 
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))" 

806 
proof (rule indep_setsD) 

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

42989  808 
using X by (auto simp: indep_vars_def) 
42988  809 
show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto 
810 
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)}" 

47694  811 
using I by auto 
42988  812 
qed 
813 

47694  814 
lemma (in prob_space) indep_varsD: 
815 
assumes X: "indep_vars M' X I" 

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

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

818 
proof (rule indep_setsD) 

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

820 
using X by (auto simp: indep_vars_def) 

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

822 
using I by auto 

823 
qed fact+ 

824 

825 
lemma prod_algebra_cong: 

826 
assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))" 

827 
shows "prod_algebra I M = prod_algebra J N" 

828 
proof  

829 
have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)" 

830 
using sets_eq_imp_space_eq[OF sets] by auto 

831 
with sets show ?thesis unfolding `I = J` 

832 
by (intro antisym prod_algebra_mono) auto 

833 
qed 

834 

835 
lemma space_in_prod_algebra: 

836 
"(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M" 

837 
proof cases 

838 
assume "I = {}" then show ?thesis 

839 
by (auto simp add: prod_algebra_def image_iff prod_emb_def) 

840 
next 

841 
assume "I \<noteq> {}" 

842 
then obtain i where "i \<in> I" by auto 

843 
then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))" 

844 
by (auto simp: prod_emb_def Pi_iff) 

845 
also have "\<dots> \<in> prod_algebra I M" 

846 
using `i \<in> I` by (intro prod_algebraI) auto 

847 
finally show ?thesis . 

848 
qed 

849 

850 
lemma (in prob_space) indep_vars_iff_distr_eq_PiM: 

851 
fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b" 

852 
assumes "I \<noteq> {}" 

42988  853 
assumes rv: "\<And>i. random_variable (M' i) (X i)" 
42989  854 
shows "indep_vars M' X I \<longleftrightarrow> 
47694  855 
distr M (\<Pi>\<^isub>M i\<in>I. M' i) (\<lambda>x. \<lambda>i\<in>I. X i x) = (\<Pi>\<^isub>M i\<in>I. distr M (M' i) (X i))" 
42988  856 
proof  
47694  857 
let ?P = "\<Pi>\<^isub>M i\<in>I. M' i" 
858 
let ?X = "\<lambda>x. \<lambda>i\<in>I. X i x" 

859 
let ?D = "distr M ?P ?X" 

860 
have X: "random_variable ?P ?X" by (intro measurable_restrict rv) 

861 
interpret D: prob_space ?D by (intro prob_space_distr X) 

42988  862 

47694  863 
let ?D' = "\<lambda>i. distr M (M' i) (X i)" 
864 
let ?P' = "\<Pi>\<^isub>M i\<in>I. distr M (M' i) (X i)" 

865 
interpret D': prob_space "?D' i" for i by (intro prob_space_distr rv) 

866 
interpret P: product_prob_space ?D' I .. 

867 

42988  868 
show ?thesis 
47694  869 
proof 
42989  870 
assume "indep_vars M' X I" 
47694  871 
show "?D = ?P'" 
872 
proof (rule measure_eqI_generator_eq) 

873 
show "Int_stable (prod_algebra I M')" 

874 
by (rule Int_stable_prod_algebra) 

875 
show "prod_algebra I M' \<subseteq> Pow (space ?P)" 

876 
using prod_algebra_sets_into_space by (simp add: space_PiM) 

877 
show "sets ?D = sigma_sets (space ?P) (prod_algebra I M')" 

878 
by (simp add: sets_PiM space_PiM) 

879 
show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')" 

880 
by (simp add: sets_PiM space_PiM cong: prod_algebra_cong) 

881 
let ?A = "\<lambda>i. \<Pi>\<^isub>E i\<in>I. space (M' i)" 

882 
show "range ?A \<subseteq> prod_algebra I M'" "incseq ?A" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')" 

883 
by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong) 

884 
{ fix i show "emeasure ?D (\<Pi>\<^isub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto } 

885 
next 

886 
fix E assume E: "E \<in> prod_algebra I M'" 

887 
from prod_algebraE[OF E] guess J Y . note J = this 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

888 

47694  889 
from E have "E \<in> sets ?P" by (auto simp: sets_PiM) 
890 
then have "emeasure ?D E = emeasure M (?X ` E \<inter> space M)" 

891 
by (simp add: emeasure_distr X) 

892 
also have "?X ` E \<inter> space M = (\<Inter>i\<in>J. X i ` Y i \<inter> space M)" 

893 
using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm) 

894 
also have "emeasure M (\<Inter>i\<in>J. X i ` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i ` Y i \<inter> space M))" 

895 
using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J] 

896 
by (auto simp: emeasure_eq_measure setprod_ereal) 

897 
also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" 

898 
using rv J by (simp add: emeasure_distr) 

899 
also have "\<dots> = emeasure ?P' E" 

900 
using P.emeasure_PiM_emb[of J Y] J by (simp add: prod_emb_def) 

901 
finally show "emeasure ?D E = emeasure ?P' E" . 

42988  902 
qed 
903 
next 

47694  904 
assume "?D = ?P'" 
905 
show "indep_vars M' X I" unfolding indep_vars_def 

906 
proof (intro conjI indep_setsI ballI rv) 

907 
fix i show "sigma_sets (space M) {X i ` A \<inter> space M A. A \<in> sets (M' i)} \<subseteq> events" 

908 
by (auto intro!: sigma_sets_subset measurable_sets rv) 

42988  909 
next 
47694  910 
fix J Y' assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J" 
911 
assume Y': "\<forall>j\<in>J. Y' j \<in> sigma_sets (space M) {X j ` A \<inter> space M A. A \<in> sets (M' j)}" 

912 
have "\<forall>j\<in>J. \<exists>Y. Y' j = X j ` Y \<inter> space M \<and> Y \<in> sets (M' j)" 

42988  913 
proof 
47694  914 
fix j assume "j \<in> J" 
915 
from Y'[rule_format, OF this] rv[of j] 

916 
show "\<exists>Y. Y' j = X j ` Y \<inter> space M \<and> Y \<in> sets (M' j)" 

917 
by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"]) 

918 
(auto dest: measurable_space simp: sigma_sets_eq) 

42988  919 
qed 
47694  920 
from bchoice[OF this] obtain Y where 
921 
Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j ` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto 

922 
let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)" 

923 
from Y have "(\<Inter>j\<in>J. Y' j) = ?X ` ?E \<inter> space M" 

924 
using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm) 

925 
then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X ` ?E \<inter> space M)" 

926 
by simp 

927 
also have "\<dots> = emeasure ?D ?E" 

928 
using Y J by (intro emeasure_distr[symmetric] X sets_PiM_I) auto 

929 
also have "\<dots> = emeasure ?P' ?E" 

930 
using `?D = ?P'` by simp 

931 
also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" 

932 
using P.emeasure_PiM_emb[of J Y] J Y by (simp add: prod_emb_def) 

933 
also have "\<dots> = (\<Prod> i\<in>J. emeasure M (Y' i))" 

934 
using rv J Y by (simp add: emeasure_distr) 

935 
finally have "emeasure M (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. emeasure M (Y' i))" . 

936 
then show "prob (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. prob (Y' i))" 

937 
by (auto simp: emeasure_eq_measure setprod_ereal) 

42988  938 
qed 
939 
qed 

42987  940 
qed 
941 

42989  942 
lemma (in prob_space) indep_varD: 
943 
assumes indep: "indep_var Ma A Mb B" 

944 
assumes sets: "Xa \<in> sets Ma" "Xb \<in> sets Mb" 

945 
shows "prob ((\<lambda>x. (A x, B x)) ` (Xa \<times> Xb) \<inter> space M) = 

946 
prob (A ` Xa \<inter> space M) * prob (B ` Xb \<inter> space M)" 

947 
proof  

948 
have "prob ((\<lambda>x. (A x, B x)) ` (Xa \<times> Xb) \<inter> space M) = 

949 
prob (\<Inter>i\<in>UNIV. (bool_case A B i ` bool_case Xa Xb i \<inter> space M))" 

950 
by (auto intro!: arg_cong[where f=prob] simp: UNIV_bool) 

951 
also have "\<dots> = (\<Prod>i\<in>UNIV. prob (bool_case A B i ` bool_case Xa Xb i \<inter> space M))" 

952 
using indep unfolding indep_var_def 

953 
by (rule indep_varsD) (auto split: bool.split intro: sets) 

954 
also have "\<dots> = prob (A ` Xa \<inter> space M) * prob (B ` Xb \<inter> space M)" 

955 
unfolding UNIV_bool by simp 

956 
finally show ?thesis . 

957 
qed 

958 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

959 
lemma (in prob_space) 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

960 
assumes "indep_var S X T Y" 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

961 
shows indep_var_rv1: "random_variable S X" 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

962 
and indep_var_rv2: "random_variable T Y" 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

963 
proof  
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

964 
have "\<forall>i\<in>UNIV. random_variable (bool_case S T i) (bool_case X Y i)" 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

965 
using assms unfolding indep_var_def indep_vars_def by auto 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

966 
then show "random_variable S X" "random_variable T Y" 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

967 
unfolding UNIV_bool by auto 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

968 
qed 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

969 

47694  970 
lemma measurable_bool_case[simp, intro]: 
971 
"(\<lambda>(x, y). bool_case x y) \<in> measurable (M \<Otimes>\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))" 

972 
(is "?f \<in> measurable ?B ?P") 

973 
proof (rule measurable_PiM_single) 

974 
show "?f \<in> space ?B \<rightarrow> (\<Pi>\<^isub>E i\<in>UNIV. space (bool_case M N i))" 

975 
by (auto simp: space_pair_measure extensional_def split: bool.split) 

976 
fix i A assume "A \<in> sets (case i of True \<Rightarrow> M  False \<Rightarrow> N)" 

977 
moreover then have "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} 

978 
= (case i of True \<Rightarrow> A \<times> space N  False \<Rightarrow> space M \<times> A)" 

979 
by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space) 

980 
ultimately show "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} \<in> sets ?B" 

981 
by (auto split: bool.split) 

982 
qed 

983 

984 
lemma borel_measurable_indicator': 

985 
"A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M" 

986 
using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def) 

987 

988 
lemma (in product_sigma_finite) distr_component: 

989 
"distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P") 

990 
proof (intro measure_eqI[symmetric]) 

991 
interpret I: finite_product_sigma_finite M "{i}" by default simp 

992 

993 
have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x" 

994 
by (auto simp: extensional_def restrict_def) 

995 

996 
fix A assume A: "A \<in> sets ?P" 

997 
then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" 

998 
by simp 

999 
also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) ` A \<inter> space (M i)) x \<partial>M i)" 

1000 
apply (subst product_positive_integral_singleton[symmetric]) 

1001 
apply (force intro!: measurable_restrict measurable_sets A) 

1002 
apply (auto intro!: positive_integral_cong simp: space_PiM indicator_def simp: eq) 

1003 
done 

1004 
also have "\<dots> = emeasure (M i) ((\<lambda>x. \<lambda>i\<in>{i}. x) ` A \<inter> space (M i))" 

1005 
by (force intro!: measurable_restrict measurable_sets A positive_integral_indicator) 

1006 
also have "\<dots> = emeasure ?D A" 

1007 
using A by (auto intro!: emeasure_distr[symmetric] measurable_restrict) 

1008 
finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" . 

1009 
qed simp 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1010 

47694  1011 
lemma pair_measure_eqI: 
1012 
assumes "sigma_finite_measure M1" "sigma_finite_measure M2" 

1013 
assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M" 

1014 
assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)" 

1015 
shows "M1 \<Otimes>\<^isub>M M2 = M" 

1016 
proof  

1017 
interpret M1: sigma_finite_measure M1 by fact 

1018 
interpret M2: sigma_finite_measure M2 by fact 

1019 
interpret pair_sigma_finite M1 M2 by default 

1020 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 

1021 
let ?E = "{a \<times> b a b. a \<in> sets M1 \<and> b \<in> sets M2}" 

1022 
let ?P = "M1 \<Otimes>\<^isub>M M2" 

1023 
show ?thesis 

1024 
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) 

1025 
show "?E \<subseteq> Pow (space ?P)" 

1026 
using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure) 

1027 
show "sets ?P = sigma_sets (space ?P) ?E" 

1028 
by (simp add: sets_pair_measure space_pair_measure) 

1029 
then show "sets M = sigma_sets (space ?P) ?E" 

1030 
using sets[symmetric] by simp 

1031 
next 

1032 
show "range F \<subseteq> ?E" "incseq F" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>" 

1033 
using F by (auto simp: space_pair_measure) 

1034 
next 

1035 
fix X assume "X \<in> ?E" 

1036 
then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto 

1037 
then have "emeasure ?P X = emeasure M1 A * emeasure M2 B" 

1038 
by (simp add: emeasure_pair_measure_Times) 

1039 
also have "\<dots> = emeasure M (A \<times> B)" 

1040 
using A B emeasure by auto 

1041 
finally show "emeasure ?P X = emeasure M X" 

1042 
by simp 

1043 
qed 

1044 
qed 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1045 

47694  1046 
lemma pair_measure_eq_distr_PiM: 
1047 
fixes M1 :: "'a measure" and M2 :: "'a measure" 

1048 
assumes "sigma_finite_measure M1" "sigma_finite_measure M2" 

1049 
shows "(M1 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. (x True, x False))" 

1050 
(is "?P = ?D") 

1051 
proof (rule pair_measure_eqI[OF assms]) 

1052 
interpret B: product_sigma_finite "bool_case M1 M2" 

1053 
unfolding product_sigma_finite_def using assms by (auto split: bool.split) 

1054 
let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)" 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1055 

47694  1056 
have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)" 
1057 
by auto 

1058 
fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2" 

1059 
have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))" 

1060 
by (simp add: UNIV_bool ac_simps) 

1061 
also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))" 

1062 
using A B by (subst B.emeasure_PiM) (auto split: bool.split) 

1063 
also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) ` (A \<times> B) \<inter> space ?B" 

1064 
using A[THEN sets_into_space] B[THEN sets_into_space] 

1065 
by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split) 

1066 
finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)" 

1067 
using A B 

1068 
measurable_component_singleton[of True UNIV "bool_case M1 M2"] 

1069 
measurable_component_singleton[of False UNIV "bool_case M1 M2"] 

1070 
by (subst emeasure_distr) (auto simp: measurable_pair_iff) 

1071 
qed simp 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1072 

47694  1073 
lemma measurable_Pair: 
1074 
assumes rvs: "X \<in> measurable M S" "Y \<in> measurable M T" 

1075 
shows "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)" 

1076 
proof  

1077 
have [simp]: "fst \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. X x)" "snd \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. Y x)" 

1078 
by auto 

1079 
show " (\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)" 

1080 
by (auto simp: measurable_pair_iff rvs) 

1081 
qed 

1082 

1083 
lemma (in prob_space) indep_var_distribution_eq: 

1084 
"indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and> 

1085 
distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" (is "_ \<longleftrightarrow> _ \<and> _ \<and> ?S \<Otimes>\<^isub>M ?T = ?J") 

1086 
proof safe 

1087 
assume "indep_var S X T Y" 

1088 
then show rvs: "random_variable S X" "random_variable T Y" 

1089 
by (blast dest: indep_var_rv1 indep_var_rv2)+ 

1090 
then have XY: "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" 

1091 
by (rule measurable_Pair) 

1092 

1093 
interpret X: prob_space ?S by (rule prob_space_distr) fact 

1094 
interpret Y: prob_space ?T by (rule prob_space_distr) fact 

1095 
interpret XY: pair_prob_space ?S ?T .. 

1096 
show "?S \<Otimes>\<^isub>M ?T = ?J" 

1097 
proof (rule pair_measure_eqI) 

1098 
show "sigma_finite_measure ?S" .. 

1099 
show "sigma_finite_measure ?T" .. 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1100 

47694  1101 
fix A B assume A: "A \<in> sets ?S" and B: "B \<in> sets ?T" 
1102 
have "emeasure ?J (A \<times> B) = emeasure M ((\<lambda>x. (X x, Y x)) ` (A \<times> B) \<inter> space M)" 

1103 
using A B by (intro emeasure_distr[OF XY]) auto 

1104 
also have "\<dots> = emeasure M (X ` A \<inter> space M) * emeasure M (Y ` B \<inter> space M)" 

1105 
using indep_varD[OF `indep_var S X T Y`, of A B] A B by (simp add: emeasure_eq_measure) 

1106 
also have "\<dots> = emeasure ?S A * emeasure ?T B" 

1107 
using rvs A B by (simp add: emeasure_distr) 

1108 
finally show "emeasure ?S A * emeasure ?T B = emeasure ?J (A \<times> B)" by simp 

1109 
qed simp 

1110 
next 

1111 
assume rvs: "random_variable S X" "random_variable T Y" 

1112 
then have XY: "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" 

1113 
by (rule measurable_Pair) 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1114 

47694  1115 
let ?S = "distr M S X" and ?T = "distr M T Y" 
1116 
interpret X: prob_space ?S by (rule prob_space_distr) fact 

1117 
interpret Y: prob_space ?T by (rule prob_space_distr) fact 

1118 
interpret XY: pair_prob_space ?S ?T .. 

1119 

1120 
assume "?S \<Otimes>\<^isub>M ?T = ?J" 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1121 

47694  1122 
{ fix S and X 
1123 
have "Int_stable {X ` A \<inter> space M A. A \<in> sets S}" 

1124 
proof (safe intro!: Int_stableI) 

1125 
fix A B assume "A \<in> sets S" "B \<in> sets S" 

1126 
then show "\<exists>C. (X ` A \<inter> space M) \<inter> (X ` B \<inter> space M) = (X ` C \<inter> space M) \<and> C \<in> sets S" 

1127 
by (intro exI[of _ "A \<inter> B"]) auto 

1128 
qed } 

1129 
note Int_stable = this 

1130 

1131 
show "indep_var S X T Y" unfolding indep_var_eq 

1132 
proof (intro conjI indep_set_sigma_sets Int_stable rvs) 

1133 
show "indep_set {X ` A \<inter> space M A. A \<in> sets S} {Y ` A \<inter> space M A. A \<in> sets T}" 

1134 
proof (safe intro!: indep_setI) 

1135 
{ fix A assume "A \<in> sets S" then show "X ` A \<inter> space M \<in> sets M" 

1136 
using `X \<in> measurable M S` by (auto intro: measurable_sets) } 

1137 
{ fix A assume "A \<in> sets T" then show "Y ` A \<inter> space M \<in> sets M" 

1138 
using `Y \<in> measurable M T` by (auto intro: measurable_sets) } 

1139 
next 

1140 
fix A B assume ab: "A \<in> sets S" "B \<in> sets T" 

1141 
then have "ereal (prob ((X ` A \<inter> space M) \<inter> (Y ` B \<inter> space M))) = emeasure ?J (A \<times> B)" 

1142 
using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"]) 

1143 
also have "\<dots> = emeasure (?S \<Otimes>\<^isub>M ?T) (A \<times> B)" 

1144 
unfolding `?S \<Otimes>\<^isub>M ?T = ?J` .. 

1145 
also have "\<dots> = emeasure ?S A * emeasure ?T B" 

1146 
using ab by (simp add: XY.emeasure_pair_measure_Times) 

1147 
finally show "prob ((X ` A \<inter> space M) \<inter> (Y ` B \<inter> space M)) = 

1148 
prob (X ` A \<inter> space M) * prob (Y ` B \<inter> space M)" 

1149 
using rvs ab by (simp add: emeasure_eq_measure emeasure_distr) 

1150 
qed 

43340
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1151 
qed 
60e181c4eae4
lemma: independence is equal to mutual information = 0
hoelzl
parents:
42989
diff
changeset

1152 
qed 
42989  1153 

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

1154 
end 