|
1 (* Title: HOL/Probability/Independent_Family.thy |
|
2 Author: Johannes Hölzl, TU München |
|
3 *) |
|
4 |
|
5 header {* Independent families of events, event sets, and random variables *} |
|
6 |
|
7 theory Independent_Family |
|
8 imports Probability_Measure |
|
9 begin |
|
10 |
|
11 definition (in prob_space) |
|
12 "indep_events A I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))" |
|
13 |
|
14 definition (in prob_space) |
|
15 "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> |
|
16 (\<forall>A\<in>(\<Pi> j\<in>J. F j). prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))" |
|
17 |
|
18 definition (in prob_space) |
|
19 "indep_sets2 A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV" |
|
20 |
|
21 definition (in prob_space) |
|
22 "indep_rv M' X I \<longleftrightarrow> |
|
23 (\<forall>i\<in>I. random_variable (M' i) (X i)) \<and> |
|
24 indep_sets (\<lambda>i. sigma_sets (space M) { X i -` A \<inter> space M | A. A \<in> sets (M' i)}) I" |
|
25 |
|
26 lemma (in prob_space) indep_sets_finite_index_sets: |
|
27 "indep_sets F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J)" |
|
28 proof (intro iffI allI impI) |
|
29 assume *: "\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J" |
|
30 show "indep_sets F I" unfolding indep_sets_def |
|
31 proof (intro conjI ballI allI impI) |
|
32 fix i assume "i \<in> I" |
|
33 with *[THEN spec, of "{i}"] show "F i \<subseteq> events" |
|
34 by (auto simp: indep_sets_def) |
|
35 qed (insert *, auto simp: indep_sets_def) |
|
36 qed (auto simp: indep_sets_def) |
|
37 |
|
38 lemma (in prob_space) indep_sets_mono_index: |
|
39 "J \<subseteq> I \<Longrightarrow> indep_sets F I \<Longrightarrow> indep_sets F J" |
|
40 unfolding indep_sets_def by auto |
|
41 |
|
42 lemma (in prob_space) indep_sets_mono_sets: |
|
43 assumes indep: "indep_sets F I" |
|
44 assumes mono: "\<And>i. i\<in>I \<Longrightarrow> G i \<subseteq> F i" |
|
45 shows "indep_sets G I" |
|
46 proof - |
|
47 have "(\<forall>i\<in>I. F i \<subseteq> events) \<Longrightarrow> (\<forall>i\<in>I. G i \<subseteq> events)" |
|
48 using mono by auto |
|
49 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)" |
|
50 using mono by (auto simp: Pi_iff) |
|
51 ultimately show ?thesis |
|
52 using indep by (auto simp: indep_sets_def) |
|
53 qed |
|
54 |
|
55 lemma (in prob_space) indep_setsI: |
|
56 assumes "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events" |
|
57 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))" |
|
58 shows "indep_sets F I" |
|
59 using assms unfolding indep_sets_def by (auto simp: Pi_iff) |
|
60 |
|
61 lemma (in prob_space) indep_setsD: |
|
62 assumes "indep_sets F I" and "J \<subseteq> I" "J \<noteq> {}" "finite J" "\<forall>j\<in>J. A j \<in> F j" |
|
63 shows "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" |
|
64 using assms unfolding indep_sets_def by auto |
|
65 |
|
66 lemma dynkin_systemI': |
|
67 assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" |
|
68 assumes empty: "{} \<in> sets M" |
|
69 assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M - A \<in> sets M" |
|
70 assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M |
|
71 \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" |
|
72 shows "dynkin_system M" |
|
73 proof - |
|
74 from Diff[OF empty] have "space M \<in> sets M" by auto |
|
75 from 1 this Diff 2 show ?thesis |
|
76 by (intro dynkin_systemI) auto |
|
77 qed |
|
78 |
|
79 lemma (in prob_space) indep_sets_dynkin: |
|
80 assumes indep: "indep_sets F I" |
|
81 shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I" |
|
82 (is "indep_sets ?F I") |
|
83 proof (subst indep_sets_finite_index_sets, intro allI impI ballI) |
|
84 fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}" |
|
85 with indep have "indep_sets F J" |
|
86 by (subst (asm) indep_sets_finite_index_sets) auto |
|
87 { fix J K assume "indep_sets F K" |
|
88 let "?G S i" = "if i \<in> S then ?F i else F i" |
|
89 assume "finite J" "J \<subseteq> K" |
|
90 then have "indep_sets (?G J) K" |
|
91 proof induct |
|
92 case (insert j J) |
|
93 moreover def G \<equiv> "?G J" |
|
94 ultimately have G: "indep_sets G K" "\<And>i. i \<in> K \<Longrightarrow> G i \<subseteq> events" and "j \<in> K" |
|
95 by (auto simp: indep_sets_def) |
|
96 let ?D = "{E\<in>events. indep_sets (G(j := {E})) K }" |
|
97 { fix X assume X: "X \<in> events" |
|
98 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) |
|
99 \<Longrightarrow> prob ((\<Inter>i\<in>J. A i) \<inter> X) = prob X * (\<Prod>i\<in>J. prob (A i))" |
|
100 have "indep_sets (G(j := {X})) K" |
|
101 proof (rule indep_setsI) |
|
102 fix i assume "i \<in> K" then show "(G(j:={X})) i \<subseteq> events" |
|
103 using G X by auto |
|
104 next |
|
105 fix A J assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "\<forall>i\<in>J. A i \<in> (G(j := {X})) i" |
|
106 show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" |
|
107 proof cases |
|
108 assume "j \<in> J" |
|
109 with J have "A j = X" by auto |
|
110 show ?thesis |
|
111 proof cases |
|
112 assume "J = {j}" then show ?thesis by simp |
|
113 next |
|
114 assume "J \<noteq> {j}" |
|
115 have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)" |
|
116 using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
|
117 also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))" |
|
118 proof (rule indep) |
|
119 show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}" |
|
120 using J `J \<noteq> {j}` `j \<in> J` by auto |
|
121 show "\<forall>i\<in>J - {j}. A i \<in> G i" |
|
122 using J by auto |
|
123 qed |
|
124 also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))" |
|
125 using `A j = X` by simp |
|
126 also have "\<dots> = (\<Prod>i\<in>J. prob (A i))" |
|
127 unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob (A i)"] |
|
128 using `j \<in> J` by (simp add: insert_absorb) |
|
129 finally show ?thesis . |
|
130 qed |
|
131 next |
|
132 assume "j \<notin> J" |
|
133 with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) |
|
134 with J show ?thesis |
|
135 by (intro indep_setsD[OF G(1)]) auto |
|
136 qed |
|
137 qed } |
|
138 note indep_sets_insert = this |
|
139 have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>" |
|
140 proof (rule dynkin_systemI', simp_all, safe) |
|
141 show "indep_sets (G(j := {{}})) K" |
|
142 by (rule indep_sets_insert) auto |
|
143 next |
|
144 fix X assume X: "X \<in> events" and G': "indep_sets (G(j := {X})) K" |
|
145 show "indep_sets (G(j := {space M - X})) K" |
|
146 proof (rule indep_sets_insert) |
|
147 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" |
|
148 then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" |
|
149 using G by auto |
|
150 have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = |
|
151 prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))" |
|
152 using A_sets sets_into_space X `J \<noteq> {}` |
|
153 by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
|
154 also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" |
|
155 using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space |
|
156 by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm) |
|
157 finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = |
|
158 prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" . |
|
159 moreover { |
|
160 have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" |
|
161 using J A `finite J` by (intro indep_setsD[OF G(1)]) auto |
|
162 then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))" |
|
163 using prob_space by simp } |
|
164 moreover { |
|
165 have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))" |
|
166 using J A `j \<in> K` by (intro indep_setsD[OF G']) auto |
|
167 then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))" |
|
168 using `finite J` `j \<notin> J` by (auto intro!: setprod_cong) } |
|
169 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))" |
|
170 by (simp add: field_simps) |
|
171 also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" |
|
172 using X A by (simp add: finite_measure_compl) |
|
173 finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" . |
|
174 qed (insert X, auto) |
|
175 next |
|
176 fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F" and "range F \<subseteq> ?D" |
|
177 then have F: "\<And>i. F i \<in> events" "\<And>i. indep_sets (G(j:={F i})) K" by auto |
|
178 show "indep_sets (G(j := {\<Union>k. F k})) K" |
|
179 proof (rule indep_sets_insert) |
|
180 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" |
|
181 then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" |
|
182 using G by auto |
|
183 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))" |
|
184 using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
|
185 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))" |
|
186 proof (rule finite_measure_UNION) |
|
187 show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)" |
|
188 using disj by (rule disjoint_family_on_bisimulation) auto |
|
189 show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events" |
|
190 using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int) |
|
191 qed |
|
192 moreover { fix k |
|
193 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))" |
|
194 by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm) |
|
195 also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)" |
|
196 using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto |
|
197 finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . } |
|
198 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)))" |
|
199 by simp |
|
200 moreover |
|
201 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))" |
|
202 using disj F(1) by (intro finite_measure_UNION sums_mult2) auto |
|
203 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)))" |
|
204 using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto |
|
205 ultimately |
|
206 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))" |
|
207 by (auto dest!: sums_unique) |
|
208 qed (insert F, auto) |
|
209 qed (insert sets_into_space, auto) |
|
210 then have mono: "sets (dynkin \<lparr>space = space M, sets = G j\<rparr>) \<subseteq> |
|
211 sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>" |
|
212 proof (rule dynkin_system.dynkin_subset, simp_all, safe) |
|
213 fix X assume "X \<in> G j" |
|
214 then show "X \<in> events" using G `j \<in> K` by auto |
|
215 from `indep_sets G K` |
|
216 show "indep_sets (G(j := {X})) K" |
|
217 by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto) |
|
218 qed |
|
219 have "indep_sets (G(j:=?D)) K" |
|
220 proof (rule indep_setsI) |
|
221 fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events" |
|
222 using G(2) by auto |
|
223 next |
|
224 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" |
|
225 show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" |
|
226 proof cases |
|
227 assume "j \<in> J" |
|
228 with A have indep: "indep_sets (G(j := {A j})) K" by auto |
|
229 from J A show ?thesis |
|
230 by (intro indep_setsD[OF indep]) auto |
|
231 next |
|
232 assume "j \<notin> J" |
|
233 with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) |
|
234 with J show ?thesis |
|
235 by (intro indep_setsD[OF G(1)]) auto |
|
236 qed |
|
237 qed |
|
238 then have "indep_sets (G(j:=sets (dynkin \<lparr>space = space M, sets = G j\<rparr>))) K" |
|
239 by (rule indep_sets_mono_sets) (insert mono, auto) |
|
240 then show ?case |
|
241 by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def) |
|
242 qed (insert `indep_sets F K`, simp) } |
|
243 from this[OF `indep_sets F J` `finite J` subset_refl] |
|
244 show "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) J" |
|
245 by (rule indep_sets_mono_sets) auto |
|
246 qed |
|
247 |
|
248 lemma (in prob_space) indep_sets_sigma: |
|
249 assumes indep: "indep_sets F I" |
|
250 assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" |
|
251 shows "indep_sets (\<lambda>i. sets (sigma \<lparr> space = space M, sets = F i \<rparr>)) I" |
|
252 proof - |
|
253 from indep_sets_dynkin[OF indep] |
|
254 show ?thesis |
|
255 proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable) |
|
256 fix i assume "i \<in> I" |
|
257 with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def) |
|
258 with sets_into_space show "F i \<subseteq> Pow (space M)" by auto |
|
259 qed |
|
260 qed |
|
261 |
|
262 lemma (in prob_space) indep_sets_sigma_sets: |
|
263 assumes "indep_sets F I" |
|
264 assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" |
|
265 shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" |
|
266 using indep_sets_sigma[OF assms] by (simp add: sets_sigma) |
|
267 |
|
268 lemma (in prob_space) indep_sets2_eq: |
|
269 "indep_sets2 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)" |
|
270 unfolding indep_sets2_def |
|
271 proof (intro iffI ballI conjI) |
|
272 assume indep: "indep_sets (bool_case A B) UNIV" |
|
273 { fix a b assume "a \<in> A" "b \<in> B" |
|
274 with indep_setsD[OF indep, of UNIV "bool_case a b"] |
|
275 show "prob (a \<inter> b) = prob a * prob b" |
|
276 unfolding UNIV_bool by (simp add: ac_simps) } |
|
277 from indep show "A \<subseteq> events" "B \<subseteq> events" |
|
278 unfolding indep_sets_def UNIV_bool by auto |
|
279 next |
|
280 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)" |
|
281 show "indep_sets (bool_case A B) UNIV" |
|
282 proof (rule indep_setsI) |
|
283 fix i show "(case i of True \<Rightarrow> A | False \<Rightarrow> B) \<subseteq> events" |
|
284 using * by (auto split: bool.split) |
|
285 next |
|
286 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)" |
|
287 then have "J = {True} \<or> J = {False} \<or> J = {True,False}" |
|
288 by (auto simp: UNIV_bool) |
|
289 then show "prob (\<Inter>j\<in>J. X j) = (\<Prod>j\<in>J. prob (X j))" |
|
290 using X * by auto |
|
291 qed |
|
292 qed |
|
293 |
|
294 lemma (in prob_space) indep_sets2_sigma_sets: |
|
295 assumes "indep_sets2 A B" |
|
296 assumes A: "Int_stable \<lparr> space = space M, sets = A \<rparr>" |
|
297 assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>" |
|
298 shows "indep_sets2 (sigma_sets (space M) A) (sigma_sets (space M) B)" |
|
299 proof - |
|
300 have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV" |
|
301 proof (rule indep_sets_sigma_sets) |
|
302 show "indep_sets (bool_case A B) UNIV" |
|
303 by (rule `indep_sets2 A B`[unfolded indep_sets2_def]) |
|
304 fix i show "Int_stable \<lparr>space = space M, sets = case i of True \<Rightarrow> A | False \<Rightarrow> B\<rparr>" |
|
305 using A B by (cases i) auto |
|
306 qed |
|
307 then show ?thesis |
|
308 unfolding indep_sets2_def |
|
309 by (rule indep_sets_mono_sets) (auto split: bool.split) |
|
310 qed |
|
311 |
|
312 end |