266 show ?thesis |
266 show ?thesis |
267 unfolding * ** using S P disj |
267 unfolding * ** using S P disj |
268 by (intro finite_measure_UNION) auto |
268 by (intro finite_measure_UNION) auto |
269 qed |
269 qed |
270 |
270 |
|
271 lemma (in prob_space) prob_EX_countable: |
|
272 assumes sets: "\<And>i. i \<in> I \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" and I: "countable I" |
|
273 assumes disj: "AE x in M. \<forall>i\<in>I. \<forall>j\<in>I. P i x \<longrightarrow> P j x \<longrightarrow> i = j" |
|
274 shows "\<P>(x in M. \<exists>i\<in>I. P i x) = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)" |
|
275 proof - |
|
276 let ?N= "\<lambda>x. \<exists>!i\<in>I. P i x" |
|
277 have "ereal (\<P>(x in M. \<exists>i\<in>I. P i x)) = \<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x))" |
|
278 unfolding ereal.inject |
|
279 proof (rule prob_eq_AE) |
|
280 show "AE x in M. (\<exists>i\<in>I. P i x) = (\<exists>i\<in>I. P i x \<and> ?N x)" |
|
281 using disj by eventually_elim blast |
|
282 qed (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+ |
|
283 also have "\<P>(x in M. (\<exists>i\<in>I. P i x \<and> ?N x)) = emeasure M (\<Union>i\<in>I. {x\<in>space M. P i x \<and> ?N x})" |
|
284 unfolding emeasure_eq_measure by (auto intro!: arg_cong[where f=prob]) |
|
285 also have "\<dots> = (\<integral>\<^sup>+i. emeasure M {x\<in>space M. P i x \<and> ?N x} \<partial>count_space I)" |
|
286 by (rule emeasure_UN_countable) |
|
287 (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets |
|
288 simp: disjoint_family_on_def) |
|
289 also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)" |
|
290 unfolding emeasure_eq_measure using disj |
|
291 by (intro positive_integral_cong ereal.inject[THEN iffD2] prob_eq_AE) |
|
292 (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+ |
|
293 finally show ?thesis . |
|
294 qed |
|
295 |
271 lemma (in prob_space) cond_prob_eq_AE: |
296 lemma (in prob_space) cond_prob_eq_AE: |
272 assumes P: "AE x in M. Q x \<longrightarrow> P x \<longleftrightarrow> P' x" "{x\<in>space M. P x} \<in> events" "{x\<in>space M. P' x} \<in> events" |
297 assumes P: "AE x in M. Q x \<longrightarrow> P x \<longleftrightarrow> P' x" "{x\<in>space M. P x} \<in> events" "{x\<in>space M. P' x} \<in> events" |
273 assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events" |
298 assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events" |
274 shows "cond_prob M P Q = cond_prob M P' Q'" |
299 shows "cond_prob M P Q = cond_prob M P' Q'" |
275 using P Q |
300 using P Q |