author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 50244  de72bbe42190 
child 53015  a1119cf551e8 
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 

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

11 
definition (in prob_space) 
42983  12 
"indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> 
42981  13 
(\<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))))" 
14 

15 
definition (in prob_space) 

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

17 

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

18 
definition (in prob_space) 
49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

19 
indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

20 

5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

21 
lemma (in prob_space) indep_events_def: 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

22 
"indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and> 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

23 
(\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

24 
unfolding indep_events_def_alt indep_sets_def 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

25 
apply (simp add: Ball_def Pi_iff image_subset_iff_funcset) 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

26 
apply (intro conj_cong refl arg_cong[where f=All] ext imp_cong) 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

27 
apply auto 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

28 
done 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

29 

5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

30 
definition (in prob_space) 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

31 
"indep_event A B \<longleftrightarrow> indep_events (bool_case A B) UNIV" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

32 

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

36 

37 
lemma (in prob_space) indep_events_finite_index_events: 

38 
"indep_events F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_events F J)" 

39 
by (auto simp: indep_events_def) 

40 

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

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

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

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

44 
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

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

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

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

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

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

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

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

52 

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

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

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

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

56 

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

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

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

59 
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

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

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

62 
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

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

64 
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

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

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

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

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

69 

49772  70 
lemma (in prob_space) indep_sets_mono: 
71 
assumes indep: "indep_sets F I" 

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

73 
shows "indep_sets G J" 

74 
apply (rule indep_sets_mono_sets) 

75 
apply (rule indep_sets_mono_index) 

76 
apply (fact +) 

77 
done 

78 

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

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

80 
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

81 
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

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

83 
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

84 

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

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

86 
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

87 
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

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

89 

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

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

93 
shows "indep_set A B" 

94 
unfolding indep_set_def 

95 
proof (rule indep_setsI) 

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

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

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

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

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

101 
unfolding UNIV_bool Pow_insert by (auto simp: ac_simps) 

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

103 

104 
lemma (in prob_space) indep_setD: 

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

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

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

108 
by (simp add: ac_simps UNIV_bool) 

109 

110 
lemma (in prob_space) 

111 
assumes indep: "indep_set A B" 

42983  112 
shows indep_setD_ev1: "A \<subseteq> events" 
113 
and indep_setD_ev2: "B \<subseteq> events" 

42982  114 
using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto 
115 

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

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

117 
assumes indep: "indep_sets F I" 
47694  118 
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

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

120 
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

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

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

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

124 
{ fix J K assume "indep_sets F K" 
46731  125 
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

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

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

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

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

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

131 
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

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

133 
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

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

135 
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

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

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

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

139 
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

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

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

142 
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

143 
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

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

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

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

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

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

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

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

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

152 
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

153 
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

154 
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

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

156 
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

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

158 
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

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

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

161 
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

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

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

164 
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

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

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

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

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

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

170 
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

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

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

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

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

175 
note indep_sets_insert = this 
47694  176 
have "dynkin_system (space M) ?D" 
42987  177 
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

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

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

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

181 
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

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

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

184 
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

185 
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

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

187 
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

188 
prob ((\<Inter>j\<in>J. A j)  (\<Inter>i\<in>insert j J. (A(j := X)) i))" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

189 
using A_sets sets.sets_into_space[of _ M] X `J \<noteq> {}` 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

190 
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

191 
also have "\<dots> = prob (\<Inter>j\<in>J. A j)  prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

192 
using J `J \<noteq> {}` `j \<notin> J` A_sets X sets.sets_into_space 
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

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

194 
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

195 
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

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

197 
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

198 
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

199 
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

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

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

202 
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

203 
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

204 
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

205 
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

206 
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

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

208 
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

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

210 
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

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

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

213 
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

214 
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

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

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

217 
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

218 
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

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

220 
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

221 
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

222 
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

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

224 
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

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

226 
show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

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

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

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

230 
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

231 
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

232 
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

233 
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

234 
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

235 
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

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

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

238 
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

239 
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

240 
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

241 
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

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

243 
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

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

245 
qed (insert F, auto) 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

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

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

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

250 
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

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

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

253 
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

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

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

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

257 
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

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

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

260 
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

261 
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

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

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

264 
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

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

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

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

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

269 
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

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

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

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

273 
qed 
47694  274 
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

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

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

277 
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

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

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

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

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

283 

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

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

285 
assumes indep: "indep_sets F I" 
47694  286 
assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)" 
287 
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

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

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

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

291 
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

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

293 
with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def) 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

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

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

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

297 

42987  298 
lemma (in prob_space) indep_sets_sigma_sets_iff: 
47694  299 
assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)" 
42987  300 
shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I \<longleftrightarrow> indep_sets F I" 
301 
proof 

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

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

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

307 
qed 

308 

49794  309 
definition (in prob_space) 
310 
indep_vars_def2: "indep_vars M' X I \<longleftrightarrow> 

49781  311 
(\<forall>i\<in>I. random_variable (M' i) (X i)) \<and> 
312 
indep_sets (\<lambda>i. { X i ` A \<inter> space M  A. A \<in> sets (M' i)}) I" 

49794  313 

314 
definition (in prob_space) 

315 
"indep_var Ma A Mb B \<longleftrightarrow> indep_vars (bool_case Ma Mb) (bool_case A B) UNIV" 

316 

317 
lemma (in prob_space) indep_vars_def: 

318 
"indep_vars M' X I \<longleftrightarrow> 

319 
(\<forall>i\<in>I. random_variable (M' i) (X i)) \<and> 

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

321 
unfolding indep_vars_def2 

49781  322 
apply (rule conj_cong[OF refl]) 
49794  323 
apply (rule indep_sets_sigma_sets_iff[symmetric]) 
49781  324 
apply (auto simp: Int_stable_def) 
325 
apply (rule_tac x="A \<inter> Aa" in exI) 

326 
apply auto 

327 
done 

328 

49794  329 
lemma (in prob_space) indep_var_eq: 
330 
"indep_var S X T Y \<longleftrightarrow> 

331 
(random_variable S X \<and> random_variable T Y) \<and> 

332 
indep_set 

333 
(sigma_sets (space M) { X ` A \<inter> space M  A. A \<in> sets S}) 

334 
(sigma_sets (space M) { Y ` A \<inter> space M  A. A \<in> sets T})" 

335 
unfolding indep_var_def indep_vars_def indep_set_def UNIV_bool 

336 
by (intro arg_cong2[where f="op \<and>"] arg_cong2[where f=indep_sets] ext) 

337 
(auto split: bool.split) 

338 

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

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

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

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

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

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

345 
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

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

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

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

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

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

351 
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

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

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

354 
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

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

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

357 
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

358 
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

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

360 
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

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

364 

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

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

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

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

372 
show "indep_sets (bool_case A B) UNIV" 
42981  373 
by (rule `indep_set A B`[unfolded indep_set_def]) 
47694  374 
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

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

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

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

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

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

381 

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

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

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

388 
proof  

46731  389 
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  390 

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

47694  394 
let ?S = "sigma_sets (space M) (\<Union>i\<in>I j. E i)" 
42981  395 
assume "j \<in> J" 
47694  396 
from E[OF this] interpret S: sigma_algebra "space M" ?S 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

397 
using sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto 
42981  398 

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

400 
proof (rule sigma_sets_eqI) 

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

402 
then guess i .. 

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

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

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

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

409 
by auto 

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

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

47694  416 
proof (rule indep_sets_sigma) 
42981  417 
show "indep_sets ?E J" 
418 
proof (intro indep_setsI) 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

419 
fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force intro!: sets.finite_INT) 
42981  420 
next 
421 
fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K" 

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

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

424 
by simp 

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

426 
from bchoice[OF this] obtain L 

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

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

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

430 
by auto 

431 

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

433 
have "k = j" 

434 
proof (rule ccontr) 

435 
assume "k \<noteq> j" 

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

437 
unfolding disjoint_family_on_def by auto 

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

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

440 
qed } 

441 
note L_inj = this 

442 

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

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

445 
have "k l = j" unfolding k_def 

446 
proof (rule some_equality) 

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

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

449 
qed (insert *, simp) } 

450 
note k_simp[simp] = this 

46731  451 
let ?E' = "\<lambda>l. E' (k l) l" 
42981  452 
have "prob (\<Inter>j\<in>K. A j) = prob (\<Inter>l\<in>(\<Union>k\<in>K. L k). ?E' l)" 
453 
by (auto simp: A intro!: arg_cong[where f=prob]) 

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

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

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

457 
using K L L_inj by (subst setprod_UN_disjoint) auto 

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

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

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

461 
qed 

462 
next 

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

47694  464 
show "Int_stable (?E j)" 
42981  465 
proof (rule Int_stableI) 
466 
fix a assume "a \<in> ?E j" then obtain Ka Ea 

467 
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 

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

469 
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 

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

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

472 
by (simp add: a b set_eq_iff) auto 

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

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

475 
qed 

476 
qed 

477 
ultimately show ?thesis 

478 
by (simp cong: indep_sets_cong) 

479 
qed 

480 

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

42982  483 

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

486 
shows "tail_events A \<subseteq> events" 

487 
proof 

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

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

495 

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

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

47694  502 
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

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

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

507 
by induct (insert A.sets_into_space, auto) 

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

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

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

511 
by (intro sigma_sets.Union) auto } 

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

513 

514 
lemma (in prob_space) kolmogorov_0_1_law: 

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

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  

49781  521 
have A: "\<And>i. A i \<subseteq> events" 
522 
using indep unfolding indep_sets_def by simp 

523 

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

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

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

42983  530 
have X_in: "X \<in> events" 
49772  531 
using tail_events_sets A X by auto 
42982  532 

47694  533 
interpret D: dynkin_system "space M" ?D 
42982  534 
proof (rule dynkin_systemI) 
47694  535 
fix D assume "D \<in> ?D" then show "D \<subseteq> space M" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

536 
using sets.sets_into_space by auto 
42982  537 
next 
47694  538 
show "space M \<in> ?D" 
42982  539 
using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2) 
540 
next 

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

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

545 
using X_in A by (intro finite_measure_Diff) auto 

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

547 
using A prob_space by auto 

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

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

549 
using X_in A sets.sets_into_space 
42982  550 
by (subst finite_measure_Diff) (auto simp: field_simps) 
47694  551 
finally show "space M  A \<in> ?D" 
42982  552 
using A `X \<subseteq> space M` by auto 
553 
next 

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

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

558 
proof (rule finite_measure_UNION) 

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

560 
using F X_in by auto 

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

562 
using dis by (rule disjoint_family_on_bisimulation) auto 

563 
qed 

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

565 
by simp 

566 
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

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

47694  570 
with F show "(\<Union>i. F i) \<in> ?D" 
42982  571 
by auto 
572 
qed 

573 

574 
{ fix n 

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

576 
proof (rule indep_sets_collect_sigma) 

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

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

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

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

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

582 
fix m 

47694  583 
show "Int_stable (A m)" 
42982  584 
unfolding Int_stable_def using A.Int by auto 
585 
qed 

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

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

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

590 
unfolding indep_set_def by simp 

591 

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

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

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

599 
by (auto simp add: ac_simps) 

600 
qed } 

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

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

607 
by (intro sigma_sets_subseteq UN_mono) auto 

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

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

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

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

614 
by induct (insert A sets.sets_into_space[of _ M], auto) } 
47694  615 
then show "?A \<subseteq> Pow (space M)" by auto 
616 
show "Int_stable ?A" 

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

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

47694  620 
interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

621 
using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto 
42982  622 
have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" 
623 
by (intro sigma_sets_subseteq UN_mono) auto 

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

625 
moreover 

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

627 
by (intro sigma_sets_subseteq UN_mono) auto 

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

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

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

633 
qed 

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

636 
finally show ?thesis by auto 

42982  637 
qed 
638 

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

49781  641 
assumes F2: "indep_events F UNIV" 
42985  642 
shows "prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 1" 
643 
proof (rule kolmogorov_0_1_law[of "\<lambda>i. sigma_sets (space M) { F i }"]) 

49781  644 
have F1: "range F \<subseteq> events" 
645 
using F2 by (simp add: indep_events_def subset_eq) 

47694  646 
{ fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

647 
using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets.sets_into_space 
47694  648 
by auto } 
42985  649 
show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV" 
47694  650 
proof (rule indep_sets_sigma) 
42985  651 
show "indep_sets (\<lambda>i. {F i}) UNIV" 
49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

652 
unfolding indep_events_def_alt[symmetric] by fact 
47694  653 
fix i show "Int_stable {F i}" 
42985  654 
unfolding Int_stable_def by simp 
655 
qed 

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

42985  659 
proof 
660 
fix j 

47694  661 
interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

662 
using order_trans[OF F1 sets.space_closed] 
47694  663 
by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq) 
42985  664 
have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)" 
665 
by (intro decseq_SucI INT_decseq_offset UN_mono) auto 

47694  666 
also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

667 
using order_trans[OF F1 sets.space_closed] 
42985  668 
by (safe intro!: S.countable_INT S.countable_UN) 
47694  669 
(auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI) 
42985  670 
finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" 
47694  671 
by simp 
42985  672 
qed 
673 
qed 

674 

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

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

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

679 
proof 

680 
assume *: "indep_sets F I" 

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

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

683 
next 

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

685 
show "indep_sets F I" 

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

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

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

46731  689 
let ?A = "\<lambda>j. if j \<in> J then A j else space M" 
42987  690 
have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

691 
using subset_trans[OF F(1) sets.space_closed] J A 
42987  692 
by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast 
693 
also 

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

695 
by (auto split: split_if_asm) 

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

697 
by auto 

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

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

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

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

702 
qed 

703 
qed 

704 

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

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

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

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

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

713 
(\<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  714 
proof  
715 
from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" 

716 
unfolding measurable_def by simp 

717 

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

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

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

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

42987  723 
by (subst sigma_sets_sigma_sets_eq) auto } 
47694  724 
note sigma_sets_X = this 
42987  725 

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

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

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

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

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

737 
ultimately 

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

47694  741 
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

742 

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

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

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

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

42987  753 
by (auto intro!: exI[of _ "space (M' i)"]) } 
47694  754 
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

755 

47694  756 
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))) = 
757 
(\<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  758 
(is "?L = ?R") 
759 
proof safe 

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

763 
by (auto simp add: Pi_iff) 

764 
next 

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

771 
by simp 

772 
qed 

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

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

42989  777 
lemma (in prob_space) indep_vars_compose: 
778 
assumes "indep_vars M' X I" 

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

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

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

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

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

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

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

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

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

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

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

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

801 
qed 

802 
qed 

803 

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

808 
proof (rule indep_setsD) 

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

42989  810 
using X by (auto simp: indep_vars_def) 
42988  811 
show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto 
812 
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  813 
using I by auto 
42988  814 
qed 
815 

47694  816 
lemma (in prob_space) indep_varsD: 
817 
assumes X: "indep_vars M' X I" 

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

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

820 
proof (rule indep_setsD) 

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

822 
using X by (auto simp: indep_vars_def) 

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

824 
using I by auto 

825 
qed fact+ 

826 

827 
lemma (in prob_space) indep_vars_iff_distr_eq_PiM: 

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

829 
assumes "I \<noteq> {}" 

42988  830 
assumes rv: "\<And>i. random_variable (M' i) (X i)" 
42989  831 
shows "indep_vars M' X I \<longleftrightarrow> 
47694  832 
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  833 
proof  
47694  834 
let ?P = "\<Pi>\<^isub>M i\<in>I. M' i" 
835 
let ?X = "\<lambda>x. \<lambda>i\<in>I. X i x" 

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

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

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

42988  839 

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

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

843 
interpret P: product_prob_space ?D' I .. 

844 

42988  845 
show ?thesis 
47694  846 
proof 
42989  847 
assume "indep_vars M' X I" 
47694  848 
show "?D = ?P'" 
849 
proof (rule measure_eqI_generator_eq) 

850 
show "Int_stable (prod_algebra I M')" 

851 
by (rule Int_stable_prod_algebra) 

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

853 
using prod_algebra_sets_into_space by (simp add: space_PiM) 

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

855 
by (simp add: sets_PiM space_PiM) 

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

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

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

49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49781
diff
changeset

859 
show "range ?A \<subseteq> prod_algebra I M'" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')" 
47694  860 
by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong) 
861 
{ fix i show "emeasure ?D (\<Pi>\<^isub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto } 

862 
next 

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

864 
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

865 

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

868 
by (simp add: emeasure_distr X) 

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

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

870 
using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm) 
47694  871 
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))" 
872 
using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J] 

873 
by (auto simp: emeasure_eq_measure setprod_ereal) 

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

875 
using rv J by (simp add: emeasure_distr) 

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

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

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

42988  879 
qed 
880 
next 

47694  881 
assume "?D = ?P'" 
882 
show "indep_vars M' X I" unfolding indep_vars_def 

883 
proof (intro conjI indep_setsI ballI rv) 

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

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

885 
by (auto intro!: sets.sigma_sets_subset measurable_sets rv) 
42988  886 
next 
47694  887 
fix J Y' assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J" 
888 
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)}" 

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

42988  890 
proof 
47694  891 
fix j assume "j \<in> J" 
892 
from Y'[rule_format, OF this] rv[of j] 

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

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

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50123
diff
changeset

895 
(auto dest: measurable_space simp: sets.sigma_sets_eq) 
42988  896 
qed 
47694  897 
from bchoice[OF this] obtain Y where 
898 
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 

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

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

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50104
diff
changeset

901 
using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm) 
47694  902 
then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X ` ?E \<inter> space M)" 
903 
by simp 

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

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

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

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

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

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

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

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

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

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

914 
by (auto simp: emeasure_eq_measure setprod_ereal) 

42988  915 
qed 
916 
qed 

42987  917 
qed 
918 

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

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

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

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

924 
proof  

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

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

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

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

929 
using indep unfolding indep_var_def 

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

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

932 
unfolding UNIV_bool by simp 

933 
finally show ?thesis . 

934 
qed 

935 

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

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

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

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

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

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

941 
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

942 
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

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

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

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

946 

47694  947 
lemma (in prob_space) indep_var_distribution_eq: 
948 
"indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and> 

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

950 
proof safe 

951 
assume "indep_var S X T Y" 

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

953 
by (blast dest: indep_var_rv1 indep_var_rv2)+ 

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

955 
by (rule measurable_Pair) 

956 

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

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

959 
interpret XY: pair_prob_space ?S ?T .. 

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

961 
proof (rule pair_measure_eqI) 

962 
show "sigma_finite_measure ?S" .. 

963 
show "sigma_finite_measure ?T" .. 

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

964 

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

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

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

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

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

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

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

973 
qed simp 

974 
next 

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

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

977 
by (rule measurable_Pair) 

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

978 

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

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

982 
interpret XY: pair_prob_space ?S ?T .. 

983 

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

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

985 

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

988 
proof (safe intro!: Int_stableI) 

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

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

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

992 
qed } 

993 
note Int_stable = this 

994 

995 
show "indep_var S X T Y" unfolding indep_var_eq 

996 
proof (intro conjI indep_set_sigma_sets Int_stable rvs) 

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

998 
proof (safe intro!: indep_setI) 

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

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

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

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

1003 
next 

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

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

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

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

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

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

49776  1010 
using ab by (simp add: Y.emeasure_pair_measure_Times) 
47694  1011 
finally show "prob ((X ` A \<inter> space M) \<inter> (Y ` B \<inter> space M)) = 
1012 
prob (X ` A \<inter> space M) * prob (Y ` B \<inter> space M)" 

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

1014 
qed 

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

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

1016 
qed 
42989  1017 

49795  1018 
lemma (in prob_space) distributed_joint_indep: 
1019 
assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" 

1020 
assumes X: "distributed M S X Px" and Y: "distributed M T Y Py" 

1021 
assumes indep: "indep_var S X T Y" 

1022 
shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)" 

1023 
using indep_var_distribution_eq[of S X T Y] indep 

1024 
by (intro distributed_joint_indep'[OF S T X Y]) auto 

1025 

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

1026 
end 