153 proof cases |
153 proof cases |
154 assume "J = {j}" then show ?thesis by simp |
154 assume "J = {j}" then show ?thesis by simp |
155 next |
155 next |
156 assume "J \<noteq> {j}" |
156 assume "J \<noteq> {j}" |
157 have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)" |
157 have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)" |
158 using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
158 using \<open>j \<in> J\<close> \<open>A j = X\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
159 also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))" |
159 also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))" |
160 proof (rule indep) |
160 proof (rule indep) |
161 show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}" |
161 show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}" |
162 using J `J \<noteq> {j}` `j \<in> J` by auto |
162 using J \<open>J \<noteq> {j}\<close> \<open>j \<in> J\<close> by auto |
163 show "\<forall>i\<in>J - {j}. A i \<in> G i" |
163 show "\<forall>i\<in>J - {j}. A i \<in> G i" |
164 using J by auto |
164 using J by auto |
165 qed |
165 qed |
166 also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))" |
166 also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))" |
167 using `A j = X` by simp |
167 using \<open>A j = X\<close> by simp |
168 also have "\<dots> = (\<Prod>i\<in>J. prob (A i))" |
168 also have "\<dots> = (\<Prod>i\<in>J. prob (A i))" |
169 unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob (A i)"] |
169 unfolding setprod.insert_remove[OF \<open>finite J\<close>, symmetric, of "\<lambda>i. prob (A i)"] |
170 using `j \<in> J` by (simp add: insert_absorb) |
170 using \<open>j \<in> J\<close> by (simp add: insert_absorb) |
171 finally show ?thesis . |
171 finally show ?thesis . |
172 qed |
172 qed |
173 next |
173 next |
174 assume "j \<notin> J" |
174 assume "j \<notin> J" |
175 with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) |
175 with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) |
189 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" |
189 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" |
190 then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" |
190 then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" |
191 using G by auto |
191 using G by auto |
192 have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = |
192 have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = |
193 prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))" |
193 prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))" |
194 using A_sets sets.sets_into_space[of _ M] X `J \<noteq> {}` |
194 using A_sets sets.sets_into_space[of _ M] X \<open>J \<noteq> {}\<close> |
195 by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
195 by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
196 also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" |
196 also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" |
197 using J `J \<noteq> {}` `j \<notin> J` A_sets X sets.sets_into_space |
197 using J \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> A_sets X sets.sets_into_space |
198 by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm) |
198 by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm) |
199 finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = |
199 finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = |
200 prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" . |
200 prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" . |
201 moreover { |
201 moreover { |
202 have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" |
202 have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" |
203 using J A `finite J` by (intro indep_setsD[OF G(1)]) auto |
203 using J A \<open>finite J\<close> by (intro indep_setsD[OF G(1)]) auto |
204 then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))" |
204 then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))" |
205 using prob_space by simp } |
205 using prob_space by simp } |
206 moreover { |
206 moreover { |
207 have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))" |
207 have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))" |
208 using J A `j \<in> K` by (intro indep_setsD[OF G']) auto |
208 using J A \<open>j \<in> K\<close> by (intro indep_setsD[OF G']) auto |
209 then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))" |
209 then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))" |
210 using `finite J` `j \<notin> J` by (auto intro!: setprod.cong) } |
210 using \<open>finite J\<close> \<open>j \<notin> J\<close> by (auto intro!: setprod.cong) } |
211 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))" |
211 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))" |
212 by (simp add: field_simps) |
212 by (simp add: field_simps) |
213 also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" |
213 also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" |
214 using X A by (simp add: finite_measure_compl) |
214 using X A by (simp add: finite_measure_compl) |
215 finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" . |
215 finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))" . |
221 proof (rule indep_sets_insert) |
221 proof (rule indep_sets_insert) |
222 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" |
222 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" |
223 then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" |
223 then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" |
224 using G by auto |
224 using G by auto |
225 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))" |
225 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))" |
226 using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
226 using \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> \<open>j \<in> K\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm) |
227 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))" |
227 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))" |
228 proof (rule finite_measure_UNION) |
228 proof (rule finite_measure_UNION) |
229 show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)" |
229 show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)" |
230 using disj by (rule disjoint_family_on_bisimulation) auto |
230 using disj by (rule disjoint_family_on_bisimulation) auto |
231 show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events" |
231 show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events" |
232 using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: sets.Int) |
232 using A_sets F \<open>finite J\<close> \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> by (auto intro!: sets.Int) |
233 qed |
233 qed |
234 moreover { fix k |
234 moreover { fix k |
235 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))" |
235 from J A \<open>j \<in> K\<close> have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))" |
236 by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: split_if_asm) |
236 by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: split_if_asm) |
237 also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)" |
237 also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)" |
238 using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto |
238 using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1)]) auto |
239 finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . } |
239 finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . } |
240 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)))" |
240 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)))" |
241 by simp |
241 by simp |
242 moreover |
242 moreover |
243 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))" |
243 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))" |
244 using disj F(1) by (intro finite_measure_UNION sums_mult2) auto |
244 using disj F(1) by (intro finite_measure_UNION sums_mult2) auto |
245 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)))" |
245 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)))" |
246 using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto |
246 using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1), symmetric]) auto |
247 ultimately |
247 ultimately |
248 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))" |
248 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))" |
249 by (auto dest!: sums_unique) |
249 by (auto dest!: sums_unique) |
250 qed (insert F, auto) |
250 qed (insert F, auto) |
251 qed (insert sets.sets_into_space, auto) |
251 qed (insert sets.sets_into_space, auto) |
252 then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}" |
252 then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}" |
253 proof (rule dynkin_system.dynkin_subset, safe) |
253 proof (rule dynkin_system.dynkin_subset, safe) |
254 fix X assume "X \<in> G j" |
254 fix X assume "X \<in> G j" |
255 then show "X \<in> events" using G `j \<in> K` by auto |
255 then show "X \<in> events" using G \<open>j \<in> K\<close> by auto |
256 from `indep_sets G K` |
256 from \<open>indep_sets G K\<close> |
257 show "indep_sets (G(j := {X})) K" |
257 show "indep_sets (G(j := {X})) K" |
258 by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto) |
258 by (rule indep_sets_mono_sets) (insert \<open>X \<in> G j\<close>, auto) |
259 qed |
259 qed |
260 have "indep_sets (G(j:=?D)) K" |
260 have "indep_sets (G(j:=?D)) K" |
261 proof (rule indep_setsI) |
261 proof (rule indep_setsI) |
262 fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events" |
262 fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events" |
263 using G(2) by auto |
263 using G(2) by auto |
659 proof (rule dynkin_systemI) |
659 proof (rule dynkin_systemI) |
660 fix D assume "D \<in> ?D" then show "D \<subseteq> space M" |
660 fix D assume "D \<in> ?D" then show "D \<subseteq> space M" |
661 using sets.sets_into_space by auto |
661 using sets.sets_into_space by auto |
662 next |
662 next |
663 show "space M \<in> ?D" |
663 show "space M \<in> ?D" |
664 using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2) |
664 using prob_space \<open>X \<subseteq> space M\<close> by (simp add: Int_absorb2) |
665 next |
665 next |
666 fix A assume A: "A \<in> ?D" |
666 fix A assume A: "A \<in> ?D" |
667 have "prob (X \<inter> (space M - A)) = prob (X - (X \<inter> A))" |
667 have "prob (X \<inter> (space M - A)) = prob (X - (X \<inter> A))" |
668 using `X \<subseteq> space M` by (auto intro!: arg_cong[where f=prob]) |
668 using \<open>X \<subseteq> space M\<close> by (auto intro!: arg_cong[where f=prob]) |
669 also have "\<dots> = prob X - prob (X \<inter> A)" |
669 also have "\<dots> = prob X - prob (X \<inter> A)" |
670 using X_in A by (intro finite_measure_Diff) auto |
670 using X_in A by (intro finite_measure_Diff) auto |
671 also have "\<dots> = prob X * prob (space M) - prob X * prob A" |
671 also have "\<dots> = prob X * prob (space M) - prob X * prob A" |
672 using A prob_space by auto |
672 using A prob_space by auto |
673 also have "\<dots> = prob X * prob (space M - A)" |
673 also have "\<dots> = prob X * prob (space M - A)" |
674 using X_in A sets.sets_into_space |
674 using X_in A sets.sets_into_space |
675 by (subst finite_measure_Diff) (auto simp: field_simps) |
675 by (subst finite_measure_Diff) (auto simp: field_simps) |
676 finally show "space M - A \<in> ?D" |
676 finally show "space M - A \<in> ?D" |
677 using A `X \<subseteq> space M` by auto |
677 using A \<open>X \<subseteq> space M\<close> by auto |
678 next |
678 next |
679 fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> ?D" |
679 fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> ?D" |
680 then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)" |
680 then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)" |
681 by auto |
681 by auto |
682 have "(\<lambda>i. prob (X \<inter> F i)) sums prob (\<Union>i. X \<inter> F i)" |
682 have "(\<lambda>i. prob (X \<inter> F i)) sums prob (\<Union>i. X \<inter> F i)" |
856 proof - |
856 proof - |
857 from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" |
857 from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" |
858 unfolding measurable_def by simp |
858 unfolding measurable_def by simp |
859 |
859 |
860 { fix i assume "i\<in>I" |
860 { fix i assume "i\<in>I" |
861 from closed[OF `i \<in> I`] |
861 from closed[OF \<open>i \<in> I\<close>] |
862 have "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} |
862 have "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} |
863 = sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> E i}" |
863 = sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> E i}" |
864 unfolding sigma_sets_vimage_commute[OF X, OF `i \<in> I`, symmetric] M'[OF `i \<in> I`] |
864 unfolding sigma_sets_vimage_commute[OF X, OF \<open>i \<in> I\<close>, symmetric] M'[OF \<open>i \<in> I\<close>] |
865 by (subst sigma_sets_sigma_sets_eq) auto } |
865 by (subst sigma_sets_sigma_sets_eq) auto } |
866 note sigma_sets_X = this |
866 note sigma_sets_X = this |
867 |
867 |
868 { fix i assume "i\<in>I" |
868 { fix i assume "i\<in>I" |
869 have "Int_stable {X i -` A \<inter> space M |A. A \<in> E i}" |
869 have "Int_stable {X i -` A \<inter> space M |A. A \<in> E i}" |
873 moreover |
873 moreover |
874 fix b assume "b \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
874 fix b assume "b \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
875 then obtain B where "b = X i -` B \<inter> space M" "B \<in> E i" by auto |
875 then obtain B where "b = X i -` B \<inter> space M" "B \<in> E i" by auto |
876 moreover |
876 moreover |
877 have "(X i -` A \<inter> space M) \<inter> (X i -` B \<inter> space M) = X i -` (A \<inter> B) \<inter> space M" by auto |
877 have "(X i -` A \<inter> space M) \<inter> (X i -` B \<inter> space M) = X i -` (A \<inter> B) \<inter> space M" by auto |
878 moreover note Int_stable[OF `i \<in> I`] |
878 moreover note Int_stable[OF \<open>i \<in> I\<close>] |
879 ultimately |
879 ultimately |
880 show "a \<inter> b \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
880 show "a \<inter> b \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
881 by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD) |
881 by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD) |
882 qed } |
882 qed } |
883 note indep_sets_X = indep_sets_sigma_sets_iff[OF this] |
883 note indep_sets_X = indep_sets_sigma_sets_iff[OF this] |
884 |
884 |
885 { fix i assume "i \<in> I" |
885 { fix i assume "i \<in> I" |
886 { fix A assume "A \<in> E i" |
886 { fix A assume "A \<in> E i" |
887 with M'[OF `i \<in> I`] have "A \<in> sets (M' i)" by auto |
887 with M'[OF \<open>i \<in> I\<close>] have "A \<in> sets (M' i)" by auto |
888 moreover |
888 moreover |
889 from rv[OF `i\<in>I`] have "X i \<in> measurable M (M' i)" by auto |
889 from rv[OF \<open>i\<in>I\<close>] have "X i \<in> measurable M (M' i)" by auto |
890 ultimately |
890 ultimately |
891 have "X i -` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) } |
891 have "X i -` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) } |
892 with X[OF `i\<in>I`] space[OF `i\<in>I`] |
892 with X[OF \<open>i\<in>I\<close>] space[OF \<open>i\<in>I\<close>] |
893 have "{X i -` A \<inter> space M |A. A \<in> E i} \<subseteq> events" |
893 have "{X i -` A \<inter> space M |A. A \<in> E i} \<subseteq> events" |
894 "space M \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
894 "space M \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
895 by (auto intro!: exI[of _ "space (M' i)"]) } |
895 by (auto intro!: exI[of _ "space (M' i)"]) } |
896 note indep_sets_finite_X = indep_sets_finite[OF I this] |
896 note indep_sets_finite_X = indep_sets_finite[OF I this] |
897 |
897 |
898 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))) = |
898 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))) = |
899 (\<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)))" |
899 (\<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)))" |
900 (is "?L = ?R") |
900 (is "?L = ?R") |
901 proof safe |
901 proof safe |
902 fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. E i)" |
902 fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. E i)" |
903 from `?L`[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A `I \<noteq> {}` |
903 from \<open>?L\<close>[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A \<open>I \<noteq> {}\<close> |
904 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))" |
904 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))" |
905 by (auto simp add: Pi_iff) |
905 by (auto simp add: Pi_iff) |
906 next |
906 next |
907 fix A assume ?R and A: "A \<in> (\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> E i})" |
907 fix A assume ?R and A: "A \<in> (\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> E i})" |
908 from A have "\<forall>i\<in>I. \<exists>B. A i = X i -` B \<inter> space M \<and> B \<in> E i" by auto |
908 from A have "\<forall>i\<in>I. \<exists>B. A i = X i -` B \<inter> space M \<and> B \<in> E i" by auto |
909 from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M" |
909 from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M" |
910 "B \<in> (\<Pi> i\<in>I. E i)" by auto |
910 "B \<in> (\<Pi> i\<in>I. E i)" by auto |
911 from `?R`[THEN bspec, OF B(2)] B(1) `I \<noteq> {}` |
911 from \<open>?R\<close>[THEN bspec, OF B(2)] B(1) \<open>I \<noteq> {}\<close> |
912 show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))" |
912 show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))" |
913 by simp |
913 by simp |
914 qed |
914 qed |
915 then show ?thesis using `I \<noteq> {}` |
915 then show ?thesis using \<open>I \<noteq> {}\<close> |
916 by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong) |
916 by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong) |
917 qed |
917 qed |
918 |
918 |
919 lemma (in prob_space) indep_vars_compose: |
919 lemma (in prob_space) indep_vars_compose: |
920 assumes "indep_vars M' X I" |
920 assumes "indep_vars M' X I" |
921 assumes rv: "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)" |
921 assumes rv: "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)" |
922 shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I" |
922 shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I" |
923 unfolding indep_vars_def |
923 unfolding indep_vars_def |
924 proof |
924 proof |
925 from rv `indep_vars M' X I` |
925 from rv \<open>indep_vars M' X I\<close> |
926 show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)" |
926 show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)" |
927 by (auto simp: indep_vars_def) |
927 by (auto simp: indep_vars_def) |
928 |
928 |
929 have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I" |
929 have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I" |
930 using `indep_vars M' X I` by (simp add: indep_vars_def) |
930 using \<open>indep_vars M' X I\<close> by (simp add: indep_vars_def) |
931 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" |
931 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" |
932 proof (rule indep_sets_mono_sets) |
932 proof (rule indep_sets_mono_sets) |
933 fix i assume "i \<in> I" |
933 fix i assume "i \<in> I" |
934 with `indep_vars M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)" |
934 with \<open>indep_vars M' X I\<close> have X: "X i \<in> space M \<rightarrow> space (M' i)" |
935 unfolding indep_vars_def measurable_def by auto |
935 unfolding indep_vars_def measurable_def by auto |
936 { fix A assume "A \<in> sets (N i)" |
936 { fix A assume "A \<in> sets (N i)" |
937 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)" |
937 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)" |
938 by (intro exI[of _ "Y i -` A \<inter> space (M' i)"]) |
938 by (intro exI[of _ "Y i -` A \<inter> space (M' i)"]) |
939 (auto simp: vimage_comp intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) } |
939 (auto simp: vimage_comp intro!: measurable_sets rv \<open>i \<in> I\<close> funcset_mem[OF X]) } |
940 then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq> |
940 then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq> |
941 sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
941 sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
942 by (intro sigma_sets_subseteq) (auto simp: vimage_comp) |
942 by (intro sigma_sets_subseteq) (auto simp: vimage_comp) |
943 qed |
943 qed |
944 qed |
944 qed |
1076 |
1076 |
1077 from E have "E \<in> sets ?P" by (auto simp: sets_PiM) |
1077 from E have "E \<in> sets ?P" by (auto simp: sets_PiM) |
1078 then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)" |
1078 then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)" |
1079 by (simp add: emeasure_distr X) |
1079 by (simp add: emeasure_distr X) |
1080 also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)" |
1080 also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)" |
1081 using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm) |
1081 using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm) |
1082 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))" |
1082 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))" |
1083 using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J] |
1083 using \<open>indep_vars M' X I\<close> J \<open>I \<noteq> {}\<close> using indep_varsD[of M' X I J] |
1084 by (auto simp: emeasure_eq_measure setprod_ereal) |
1084 by (auto simp: emeasure_eq_measure setprod_ereal) |
1085 also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" |
1085 also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" |
1086 using rv J by (simp add: emeasure_distr) |
1086 using rv J by (simp add: emeasure_distr) |
1087 also have "\<dots> = emeasure ?P' E" |
1087 also have "\<dots> = emeasure ?P' E" |
1088 using P.emeasure_PiM_emb[of J Y] J by (simp add: prod_emb_def) |
1088 using P.emeasure_PiM_emb[of J Y] J by (simp add: prod_emb_def) |
1107 qed |
1107 qed |
1108 from bchoice[OF this] obtain Y where |
1108 from bchoice[OF this] obtain Y where |
1109 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 |
1109 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 |
1110 let ?E = "prod_emb I M' J (Pi\<^sub>E J Y)" |
1110 let ?E = "prod_emb I M' J (Pi\<^sub>E J Y)" |
1111 from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M" |
1111 from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M" |
1112 using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm) |
1112 using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm) |
1113 then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)" |
1113 then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)" |
1114 by simp |
1114 by simp |
1115 also have "\<dots> = emeasure ?D ?E" |
1115 also have "\<dots> = emeasure ?D ?E" |
1116 using Y J by (intro emeasure_distr[symmetric] X sets_PiM_I) auto |
1116 using Y J by (intro emeasure_distr[symmetric] X sets_PiM_I) auto |
1117 also have "\<dots> = emeasure ?P' ?E" |
1117 also have "\<dots> = emeasure ?P' ?E" |
1118 using `?D = ?P'` by simp |
1118 using \<open>?D = ?P'\<close> by simp |
1119 also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" |
1119 also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" |
1120 using P.emeasure_PiM_emb[of J Y] J Y by (simp add: prod_emb_def) |
1120 using P.emeasure_PiM_emb[of J Y] J Y by (simp add: prod_emb_def) |
1121 also have "\<dots> = (\<Prod> i\<in>J. emeasure M (Y' i))" |
1121 also have "\<dots> = (\<Prod> i\<in>J. emeasure M (Y' i))" |
1122 using rv J Y by (simp add: emeasure_distr) |
1122 using rv J Y by (simp add: emeasure_distr) |
1123 finally have "emeasure M (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. emeasure M (Y' i))" . |
1123 finally have "emeasure M (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. emeasure M (Y' i))" . |
1220 show "indep_var S X T Y" unfolding indep_var_eq |
1220 show "indep_var S X T Y" unfolding indep_var_eq |
1221 proof (intro conjI indep_set_sigma_sets Int_stable rvs) |
1221 proof (intro conjI indep_set_sigma_sets Int_stable rvs) |
1222 show "indep_set {X -` A \<inter> space M |A. A \<in> sets S} {Y -` A \<inter> space M |A. A \<in> sets T}" |
1222 show "indep_set {X -` A \<inter> space M |A. A \<in> sets S} {Y -` A \<inter> space M |A. A \<in> sets T}" |
1223 proof (safe intro!: indep_setI) |
1223 proof (safe intro!: indep_setI) |
1224 { fix A assume "A \<in> sets S" then show "X -` A \<inter> space M \<in> sets M" |
1224 { fix A assume "A \<in> sets S" then show "X -` A \<inter> space M \<in> sets M" |
1225 using `X \<in> measurable M S` by (auto intro: measurable_sets) } |
1225 using \<open>X \<in> measurable M S\<close> by (auto intro: measurable_sets) } |
1226 { fix A assume "A \<in> sets T" then show "Y -` A \<inter> space M \<in> sets M" |
1226 { fix A assume "A \<in> sets T" then show "Y -` A \<inter> space M \<in> sets M" |
1227 using `Y \<in> measurable M T` by (auto intro: measurable_sets) } |
1227 using \<open>Y \<in> measurable M T\<close> by (auto intro: measurable_sets) } |
1228 next |
1228 next |
1229 fix A B assume ab: "A \<in> sets S" "B \<in> sets T" |
1229 fix A B assume ab: "A \<in> sets S" "B \<in> sets T" |
1230 then have "ereal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) = emeasure ?J (A \<times> B)" |
1230 then have "ereal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) = emeasure ?J (A \<times> B)" |
1231 using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"]) |
1231 using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"]) |
1232 also have "\<dots> = emeasure (?S \<Otimes>\<^sub>M ?T) (A \<times> B)" |
1232 also have "\<dots> = emeasure (?S \<Otimes>\<^sub>M ?T) (A \<times> B)" |
1233 unfolding `?S \<Otimes>\<^sub>M ?T = ?J` .. |
1233 unfolding \<open>?S \<Otimes>\<^sub>M ?T = ?J\<close> .. |
1234 also have "\<dots> = emeasure ?S A * emeasure ?T B" |
1234 also have "\<dots> = emeasure ?S A * emeasure ?T B" |
1235 using ab by (simp add: Y.emeasure_pair_measure_Times) |
1235 using ab by (simp add: Y.emeasure_pair_measure_Times) |
1236 finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) = |
1236 finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) = |
1237 prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)" |
1237 prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)" |
1238 using rvs ab by (simp add: emeasure_eq_measure emeasure_distr) |
1238 using rvs ab by (simp add: emeasure_eq_measure emeasure_distr) |
1273 have "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (Y i \<omega>)) \<partial>M)" |
1273 have "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (Y i \<omega>)) \<partial>M)" |
1274 using I(3) by (auto intro!: nn_integral_cong setprod.cong simp add: Y_def max_def) |
1274 using I(3) by (auto intro!: nn_integral_cong setprod.cong simp add: Y_def max_def) |
1275 also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))" |
1275 also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))" |
1276 by (subst nn_integral_distr) auto |
1276 by (subst nn_integral_distr) auto |
1277 also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))" |
1277 also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))" |
1278 unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] .. |
1278 unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] .. |
1279 also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. max 0 \<omega> \<partial>distr M borel (Y i)))" |
1279 also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. max 0 \<omega> \<partial>distr M borel (Y i)))" |
1280 by (rule product_nn_integral_setprod) (auto intro: `finite I`) |
1280 by (rule product_nn_integral_setprod) (auto intro: \<open>finite I\<close>) |
1281 also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)" |
1281 also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)" |
1282 by (intro setprod.cong nn_integral_cong) |
1282 by (intro setprod.cong nn_integral_cong) |
1283 (auto simp: nn_integral_distr nn_integral_max_0 Y_def rv_X) |
1283 (auto simp: nn_integral_distr nn_integral_max_0 Y_def rv_X) |
1284 finally show ?thesis . |
1284 finally show ?thesis . |
1285 qed (simp add: emeasure_space_1) |
1285 qed (simp add: emeasure_space_1) |
1315 have "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<omega>. (\<Prod>i\<in>I. Y i \<omega>) \<partial>M)" |
1315 have "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<omega>. (\<Prod>i\<in>I. Y i \<omega>) \<partial>M)" |
1316 using I(3) by (simp add: Y_def) |
1316 using I(3) by (simp add: Y_def) |
1317 also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))" |
1317 also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))" |
1318 by (subst integral_distr) auto |
1318 by (subst integral_distr) auto |
1319 also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))" |
1319 also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))" |
1320 unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] .. |
1320 unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] .. |
1321 also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))" |
1321 also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))" |
1322 by (rule product_integral_setprod) (auto intro: `finite I` simp: integrable_distr_eq int_Y) |
1322 by (rule product_integral_setprod) (auto intro: \<open>finite I\<close> simp: integrable_distr_eq int_Y) |
1323 also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)" |
1323 also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)" |
1324 by (intro setprod.cong integral_cong) |
1324 by (intro setprod.cong integral_cong) |
1325 (auto simp: integral_distr Y_def rv_X) |
1325 (auto simp: integral_distr Y_def rv_X) |
1326 finally show ?eq . |
1326 finally show ?eq . |
1327 |
1327 |
1328 have "integrable (distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x)) (\<lambda>\<omega>. (\<Prod>i\<in>I. \<omega> i))" |
1328 have "integrable (distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x)) (\<lambda>\<omega>. (\<Prod>i\<in>I. \<omega> i))" |
1329 unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] |
1329 unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] |
1330 by (intro product_integrable_setprod[OF `finite I`]) |
1330 by (intro product_integrable_setprod[OF \<open>finite I\<close>]) |
1331 (simp add: integrable_distr_eq int_Y) |
1331 (simp add: integrable_distr_eq int_Y) |
1332 then show ?int |
1332 then show ?int |
1333 by (simp add: integrable_distr_eq Y_def) |
1333 by (simp add: integrable_distr_eq Y_def) |
1334 qed (simp_all add: prob_space) |
1334 qed (simp_all add: prob_space) |
1335 |
1335 |