290 with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) |
289 with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) |
291 with J show ?thesis |
290 with J show ?thesis |
292 by (intro indep_setsD[OF G(1)]) auto |
291 by (intro indep_setsD[OF G(1)]) auto |
293 qed |
292 qed |
294 qed |
293 qed |
295 then have "indep_sets (G(j:=sets (dynkin \<lparr>space = space M, sets = G j\<rparr>))) K" |
294 then have "indep_sets (G(j := dynkin (space M) (G j))) K" |
296 by (rule indep_sets_mono_sets) (insert mono, auto) |
295 by (rule indep_sets_mono_sets) (insert mono, auto) |
297 then show ?case |
296 then show ?case |
298 by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def) |
297 by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def) |
299 qed (insert `indep_sets F K`, simp) } |
298 qed (insert `indep_sets F K`, simp) } |
300 from this[OF `indep_sets F J` `finite J` subset_refl] |
299 from this[OF `indep_sets F J` `finite J` subset_refl] |
301 show "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) J" |
300 show "indep_sets ?F J" |
302 by (rule indep_sets_mono_sets) auto |
301 by (rule indep_sets_mono_sets) auto |
303 qed |
302 qed |
304 |
303 |
305 lemma (in prob_space) indep_sets_sigma: |
304 lemma (in prob_space) indep_sets_sigma: |
306 assumes indep: "indep_sets F I" |
305 assumes indep: "indep_sets F I" |
307 assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" |
306 assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)" |
308 shows "indep_sets (\<lambda>i. sets (sigma \<lparr> space = space M, sets = F i \<rparr>)) I" |
307 shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" |
309 proof - |
308 proof - |
310 from indep_sets_dynkin[OF indep] |
309 from indep_sets_dynkin[OF indep] |
311 show ?thesis |
310 show ?thesis |
312 proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable) |
311 proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable) |
313 fix i assume "i \<in> I" |
312 fix i assume "i \<in> I" |
314 with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def) |
313 with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def) |
315 with sets_into_space show "F i \<subseteq> Pow (space M)" by auto |
314 with sets_into_space show "F i \<subseteq> Pow (space M)" by auto |
316 qed |
315 qed |
317 qed |
316 qed |
318 |
317 |
319 lemma (in prob_space) indep_sets_sigma_sets: |
|
320 assumes "indep_sets F I" |
|
321 assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" |
|
322 shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" |
|
323 using indep_sets_sigma[OF assms] by (simp add: sets_sigma) |
|
324 |
|
325 lemma (in prob_space) indep_sets_sigma_sets_iff: |
318 lemma (in prob_space) indep_sets_sigma_sets_iff: |
326 assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" |
319 assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)" |
327 shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I \<longleftrightarrow> indep_sets F I" |
320 shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I \<longleftrightarrow> indep_sets F I" |
328 proof |
321 proof |
329 assume "indep_sets F I" then show "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" |
322 assume "indep_sets F I" then show "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" |
330 by (rule indep_sets_sigma_sets) fact |
323 by (rule indep_sets_sigma) fact |
331 next |
324 next |
332 assume "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" then show "indep_sets F I" |
325 assume "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" then show "indep_sets F I" |
333 by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic) |
326 by (rule indep_sets_mono_sets) (intro subsetI sigma_sets.Basic) |
334 qed |
327 qed |
335 |
328 |
359 qed |
352 qed |
360 qed |
353 qed |
361 |
354 |
362 lemma (in prob_space) indep_set_sigma_sets: |
355 lemma (in prob_space) indep_set_sigma_sets: |
363 assumes "indep_set A B" |
356 assumes "indep_set A B" |
364 assumes A: "Int_stable \<lparr> space = space M, sets = A \<rparr>" |
357 assumes A: "Int_stable A" and B: "Int_stable B" |
365 assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>" |
|
366 shows "indep_set (sigma_sets (space M) A) (sigma_sets (space M) B)" |
358 shows "indep_set (sigma_sets (space M) A) (sigma_sets (space M) B)" |
367 proof - |
359 proof - |
368 have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV" |
360 have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV" |
369 proof (rule indep_sets_sigma_sets) |
361 proof (rule indep_sets_sigma) |
370 show "indep_sets (bool_case A B) UNIV" |
362 show "indep_sets (bool_case A B) UNIV" |
371 by (rule `indep_set A B`[unfolded indep_set_def]) |
363 by (rule `indep_set A B`[unfolded indep_set_def]) |
372 fix i show "Int_stable \<lparr>space = space M, sets = case i of True \<Rightarrow> A | False \<Rightarrow> B\<rparr>" |
364 fix i show "Int_stable (case i of True \<Rightarrow> A | False \<Rightarrow> B)" |
373 using A B by (cases i) auto |
365 using A B by (cases i) auto |
374 qed |
366 qed |
375 then show ?thesis |
367 then show ?thesis |
376 unfolding indep_set_def |
368 unfolding indep_set_def |
377 by (rule indep_sets_mono_sets) (auto split: bool.split) |
369 by (rule indep_sets_mono_sets) (auto split: bool.split) |
378 qed |
370 qed |
379 |
371 |
380 lemma (in prob_space) indep_sets_collect_sigma: |
372 lemma (in prob_space) indep_sets_collect_sigma: |
381 fixes I :: "'j \<Rightarrow> 'i set" and J :: "'j set" and E :: "'i \<Rightarrow> 'a set set" |
373 fixes I :: "'j \<Rightarrow> 'i set" and J :: "'j set" and E :: "'i \<Rightarrow> 'a set set" |
382 assumes indep: "indep_sets E (\<Union>j\<in>J. I j)" |
374 assumes indep: "indep_sets E (\<Union>j\<in>J. I j)" |
383 assumes Int_stable: "\<And>i j. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> Int_stable \<lparr>space = space M, sets = E i\<rparr>" |
375 assumes Int_stable: "\<And>i j. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> Int_stable (E i)" |
384 assumes disjoint: "disjoint_family_on I J" |
376 assumes disjoint: "disjoint_family_on I J" |
385 shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J" |
377 shows "indep_sets (\<lambda>j. sigma_sets (space M) (\<Union>i\<in>I j. E i)) J" |
386 proof - |
378 proof - |
387 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) }" |
379 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) }" |
388 |
380 |
389 from indep have E: "\<And>j i. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> E i \<subseteq> events" |
381 from indep have E: "\<And>j i. j \<in> J \<Longrightarrow> i \<in> I j \<Longrightarrow> E i \<subseteq> events" |
390 unfolding indep_sets_def by auto |
382 unfolding indep_sets_def by auto |
391 { fix j |
383 { fix j |
392 let ?S = "sigma \<lparr> space = space M, sets = (\<Union>i\<in>I j. E i) \<rparr>" |
384 let ?S = "sigma_sets (space M) (\<Union>i\<in>I j. E i)" |
393 assume "j \<in> J" |
385 assume "j \<in> J" |
394 from E[OF this] interpret S: sigma_algebra ?S |
386 from E[OF this] interpret S: sigma_algebra "space M" ?S |
395 using sets_into_space by (intro sigma_algebra_sigma) auto |
387 using sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto |
396 |
388 |
397 have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)" |
389 have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)" |
398 proof (rule sigma_sets_eqI) |
390 proof (rule sigma_sets_eqI) |
399 fix A assume "A \<in> (\<Union>i\<in>I j. E i)" |
391 fix A assume "A \<in> (\<Union>i\<in>I j. E i)" |
400 then guess i .. |
392 then guess i .. |
401 then show "A \<in> sigma_sets (space M) (?E j)" |
393 then show "A \<in> sigma_sets (space M) (?E j)" |
402 by (auto intro!: sigma_sets.intros exI[of _ "{i}"] exI[of _ "\<lambda>i. A"]) |
394 by (auto intro!: sigma_sets.intros(2-) exI[of _ "{i}"] exI[of _ "\<lambda>i. A"]) |
403 next |
395 next |
404 fix A assume "A \<in> ?E j" |
396 fix A assume "A \<in> ?E j" |
405 then obtain E' K where "finite K" "K \<noteq> {}" "K \<subseteq> I j" "\<And>k. k \<in> K \<Longrightarrow> E' k \<in> E k" |
397 then obtain E' K where "finite K" "K \<noteq> {}" "K \<subseteq> I j" "\<And>k. k \<in> K \<Longrightarrow> E' k \<in> E k" |
406 and A: "A = (\<Inter>k\<in>K. E' k)" |
398 and A: "A = (\<Inter>k\<in>K. E' k)" |
407 by auto |
399 by auto |
408 then have "A \<in> sets ?S" unfolding A |
400 then have "A \<in> ?S" unfolding A |
409 by (safe intro!: S.finite_INT) |
401 by (safe intro!: S.finite_INT) auto |
410 (auto simp: sets_sigma intro!: sigma_sets.Basic) |
|
411 then show "A \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i)" |
402 then show "A \<in> sigma_sets (space M) (\<Union>i\<in>I j. E i)" |
412 by (simp add: sets_sigma) |
403 by simp |
413 qed } |
404 qed } |
414 moreover have "indep_sets (\<lambda>j. sigma_sets (space M) (?E j)) J" |
405 moreover have "indep_sets (\<lambda>j. sigma_sets (space M) (?E j)) J" |
415 proof (rule indep_sets_sigma_sets) |
406 proof (rule indep_sets_sigma) |
416 show "indep_sets ?E J" |
407 show "indep_sets ?E J" |
417 proof (intro indep_setsI) |
408 proof (intro indep_setsI) |
418 fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force intro!: finite_INT) |
409 fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force intro!: finite_INT) |
419 next |
410 next |
420 fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K" |
411 fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K" |
480 definition (in prob_space) terminal_events where |
471 definition (in prob_space) terminal_events where |
481 "terminal_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))" |
472 "terminal_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))" |
482 |
473 |
483 lemma (in prob_space) terminal_events_sets: |
474 lemma (in prob_space) terminal_events_sets: |
484 assumes A: "\<And>i. A i \<subseteq> events" |
475 assumes A: "\<And>i. A i \<subseteq> events" |
485 assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>" |
476 assumes "\<And>i::nat. sigma_algebra (space M) (A i)" |
486 assumes X: "X \<in> terminal_events A" |
477 assumes X: "X \<in> terminal_events A" |
487 shows "X \<in> events" |
478 shows "X \<in> events" |
488 proof - |
479 proof - |
489 let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" |
480 let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" |
490 interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact |
481 interpret A: sigma_algebra "space M" "A i" for i by fact |
491 from X have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def) |
482 from X have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: terminal_events_def) |
492 from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp |
483 from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp |
493 then show "X \<in> events" |
484 then show "X \<in> events" |
494 by induct (insert A, auto) |
485 by induct (insert A, auto) |
495 qed |
486 qed |
496 |
487 |
497 lemma (in prob_space) sigma_algebra_terminal_events: |
488 lemma (in prob_space) sigma_algebra_terminal_events: |
498 assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>" |
489 assumes "\<And>i::nat. sigma_algebra (space M) (A i)" |
499 shows "sigma_algebra \<lparr> space = space M, sets = terminal_events A \<rparr>" |
490 shows "sigma_algebra (space M) (terminal_events A)" |
500 unfolding terminal_events_def |
491 unfolding terminal_events_def |
501 proof (simp add: sigma_algebra_iff2, safe) |
492 proof (simp add: sigma_algebra_iff2, safe) |
502 let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" |
493 let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))" |
503 interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact |
494 interpret A: sigma_algebra "space M" "A i" for i by fact |
504 { fix X x assume "X \<in> ?A" "x \<in> X" |
495 { fix X x assume "X \<in> ?A" "x \<in> X" |
505 then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto |
496 then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto |
506 from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp |
497 from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp |
507 then have "X \<subseteq> space M" |
498 then have "X \<subseteq> space M" |
508 by induct (insert A.sets_into_space, auto) |
499 by induct (insert A.sets_into_space, auto) |
513 qed (auto intro!: sigma_sets.Compl sigma_sets.Empty) |
504 qed (auto intro!: sigma_sets.Compl sigma_sets.Empty) |
514 |
505 |
515 lemma (in prob_space) kolmogorov_0_1_law: |
506 lemma (in prob_space) kolmogorov_0_1_law: |
516 fixes A :: "nat \<Rightarrow> 'a set set" |
507 fixes A :: "nat \<Rightarrow> 'a set set" |
517 assumes A: "\<And>i. A i \<subseteq> events" |
508 assumes A: "\<And>i. A i \<subseteq> events" |
518 assumes "\<And>i::nat. sigma_algebra \<lparr>space = space M, sets = A i\<rparr>" |
509 assumes "\<And>i::nat. sigma_algebra (space M) (A i)" |
519 assumes indep: "indep_sets A UNIV" |
510 assumes indep: "indep_sets A UNIV" |
520 and X: "X \<in> terminal_events A" |
511 and X: "X \<in> terminal_events A" |
521 shows "prob X = 0 \<or> prob X = 1" |
512 shows "prob X = 0 \<or> prob X = 1" |
522 proof - |
513 proof - |
523 let ?D = "\<lparr> space = space M, sets = {D \<in> events. prob (X \<inter> D) = prob X * prob D} \<rparr>" |
514 let ?D = "{D \<in> events. prob (X \<inter> D) = prob X * prob D}" |
524 interpret A: sigma_algebra "\<lparr>space = space M, sets = A i\<rparr>" for i by fact |
515 interpret A: sigma_algebra "space M" "A i" for i by fact |
525 interpret T: sigma_algebra "\<lparr> space = space M, sets = terminal_events A \<rparr>" |
516 interpret T: sigma_algebra "space M" "terminal_events A" |
526 by (rule sigma_algebra_terminal_events) fact |
517 by (rule sigma_algebra_terminal_events) fact |
527 have "X \<subseteq> space M" using T.space_closed X by auto |
518 have "X \<subseteq> space M" using T.space_closed X by auto |
528 |
519 |
529 have X_in: "X \<in> events" |
520 have X_in: "X \<in> events" |
530 by (rule terminal_events_sets) fact+ |
521 by (rule terminal_events_sets) fact+ |
531 |
522 |
532 interpret D: dynkin_system ?D |
523 interpret D: dynkin_system "space M" ?D |
533 proof (rule dynkin_systemI) |
524 proof (rule dynkin_systemI) |
534 fix D assume "D \<in> sets ?D" then show "D \<subseteq> space ?D" |
525 fix D assume "D \<in> ?D" then show "D \<subseteq> space M" |
535 using sets_into_space by auto |
526 using sets_into_space by auto |
536 next |
527 next |
537 show "space ?D \<in> sets ?D" |
528 show "space M \<in> ?D" |
538 using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2) |
529 using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2) |
539 next |
530 next |
540 fix A assume A: "A \<in> sets ?D" |
531 fix A assume A: "A \<in> ?D" |
541 have "prob (X \<inter> (space M - A)) = prob (X - (X \<inter> A))" |
532 have "prob (X \<inter> (space M - A)) = prob (X - (X \<inter> A))" |
542 using `X \<subseteq> space M` by (auto intro!: arg_cong[where f=prob]) |
533 using `X \<subseteq> space M` by (auto intro!: arg_cong[where f=prob]) |
543 also have "\<dots> = prob X - prob (X \<inter> A)" |
534 also have "\<dots> = prob X - prob (X \<inter> A)" |
544 using X_in A by (intro finite_measure_Diff) auto |
535 using X_in A by (intro finite_measure_Diff) auto |
545 also have "\<dots> = prob X * prob (space M) - prob X * prob A" |
536 also have "\<dots> = prob X * prob (space M) - prob X * prob A" |
546 using A prob_space by auto |
537 using A prob_space by auto |
547 also have "\<dots> = prob X * prob (space M - A)" |
538 also have "\<dots> = prob X * prob (space M - A)" |
548 using X_in A sets_into_space |
539 using X_in A sets_into_space |
549 by (subst finite_measure_Diff) (auto simp: field_simps) |
540 by (subst finite_measure_Diff) (auto simp: field_simps) |
550 finally show "space ?D - A \<in> sets ?D" |
541 finally show "space M - A \<in> ?D" |
551 using A `X \<subseteq> space M` by auto |
542 using A `X \<subseteq> space M` by auto |
552 next |
543 next |
553 fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> sets ?D" |
544 fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> ?D" |
554 then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)" |
545 then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)" |
555 by auto |
546 by auto |
556 have "(\<lambda>i. prob (X \<inter> F i)) sums prob (\<Union>i. X \<inter> F i)" |
547 have "(\<lambda>i. prob (X \<inter> F i)) sums prob (\<Union>i. X \<inter> F i)" |
557 proof (rule finite_measure_UNION) |
548 proof (rule finite_measure_UNION) |
558 show "range (\<lambda>i. X \<inter> F i) \<subseteq> events" |
549 show "range (\<lambda>i. X \<inter> F i) \<subseteq> events" |
577 by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq) |
568 by (simp split: bool.split add: set_eq_iff) (metis not_less_eq_eq) |
578 with indep show "indep_sets A ?U" by simp |
569 with indep show "indep_sets A ?U" by simp |
579 show "disjoint_family (bool_case {..n} {Suc n..})" |
570 show "disjoint_family (bool_case {..n} {Suc n..})" |
580 unfolding disjoint_family_on_def by (auto split: bool.split) |
571 unfolding disjoint_family_on_def by (auto split: bool.split) |
581 fix m |
572 fix m |
582 show "Int_stable \<lparr>space = space M, sets = A m\<rparr>" |
573 show "Int_stable (A m)" |
583 unfolding Int_stable_def using A.Int by auto |
574 unfolding Int_stable_def using A.Int by auto |
584 qed |
575 qed |
585 also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) = |
576 also have "(\<lambda>b. sigma_sets (space M) (\<Union>m\<in>bool_case {..n} {Suc n..} b. A m)) = |
586 bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))" |
577 bool_case (sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) (sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m))" |
587 by (auto intro!: ext split: bool.split) |
578 by (auto intro!: ext split: bool.split) |
588 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))" |
579 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))" |
589 unfolding indep_set_def by simp |
580 unfolding indep_set_def by simp |
590 |
581 |
591 have "sigma_sets (space M) (\<Union>m\<in>{..n}. A m) \<subseteq> sets ?D" |
582 have "sigma_sets (space M) (\<Union>m\<in>{..n}. A m) \<subseteq> ?D" |
592 proof (simp add: subset_eq, rule) |
583 proof (simp add: subset_eq, rule) |
593 fix D assume D: "D \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" |
584 fix D assume D: "D \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" |
594 have "X \<in> sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m)" |
585 have "X \<in> sigma_sets (space M) (\<Union>m\<in>{Suc n..}. A m)" |
595 using X unfolding terminal_events_def by simp |
586 using X unfolding terminal_events_def by simp |
596 from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D |
587 from indep_setD[OF indep D this] indep_setD_ev1[OF indep] D |
597 show "D \<in> events \<and> prob (X \<inter> D) = prob X * prob D" |
588 show "D \<in> events \<and> prob (X \<inter> D) = prob X * prob D" |
598 by (auto simp add: ac_simps) |
589 by (auto simp add: ac_simps) |
599 qed } |
590 qed } |
600 then have "(\<Union>n. sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) \<subseteq> sets ?D" (is "?A \<subseteq> _") |
591 then have "(\<Union>n. sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) \<subseteq> ?D" (is "?A \<subseteq> _") |
601 by auto |
592 by auto |
602 |
593 |
603 have "sigma \<lparr> space = space M, sets = ?A \<rparr> = |
594 note `X \<in> terminal_events A` |
604 dynkin \<lparr> space = space M, sets = ?A \<rparr>" (is "sigma ?UA = dynkin ?UA") |
595 also { |
|
596 have "\<And>n. sigma_sets (space M) (\<Union>i\<in>{n..}. A i) \<subseteq> sigma_sets (space M) ?A" |
|
597 by (intro sigma_sets_subseteq UN_mono) auto |
|
598 then have "terminal_events A \<subseteq> sigma_sets (space M) ?A" |
|
599 unfolding terminal_events_def by auto } |
|
600 also have "sigma_sets (space M) ?A = dynkin (space M) ?A" |
605 proof (rule sigma_eq_dynkin) |
601 proof (rule sigma_eq_dynkin) |
606 { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" |
602 { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)" |
607 then have "B \<subseteq> space M" |
603 then have "B \<subseteq> space M" |
608 by induct (insert A sets_into_space, auto) } |
604 by induct (insert A sets_into_space[of _ M], auto) } |
609 then show "sets ?UA \<subseteq> Pow (space ?UA)" by auto |
605 then show "?A \<subseteq> Pow (space M)" by auto |
610 show "Int_stable ?UA" |
606 show "Int_stable ?A" |
611 proof (rule Int_stableI) |
607 proof (rule Int_stableI) |
612 fix a assume "a \<in> ?A" then guess n .. note a = this |
608 fix a assume "a \<in> ?A" then guess n .. note a = this |
613 fix b assume "b \<in> ?A" then guess m .. note b = this |
609 fix b assume "b \<in> ?A" then guess m .. note b = this |
614 interpret Amn: sigma_algebra "sigma \<lparr>space = space M, sets = (\<Union>i\<in>{..max m n}. A i)\<rparr>" |
610 interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" |
615 using A sets_into_space by (intro sigma_algebra_sigma) auto |
611 using A sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto |
616 have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" |
612 have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" |
617 by (intro sigma_sets_subseteq UN_mono) auto |
613 by (intro sigma_sets_subseteq UN_mono) auto |
618 with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto |
614 with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto |
619 moreover |
615 moreover |
620 have "sigma_sets (space M) (\<Union>i\<in>{..m}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" |
616 have "sigma_sets (space M) (\<Union>i\<in>{..m}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" |
621 by (intro sigma_sets_subseteq UN_mono) auto |
617 by (intro sigma_sets_subseteq UN_mono) auto |
622 with b have "b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto |
618 with b have "b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto |
623 ultimately have "a \<inter> b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" |
619 ultimately have "a \<inter> b \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" |
624 using Amn.Int[of a b] by (simp add: sets_sigma) |
620 using Amn.Int[of a b] by simp |
625 then show "a \<inter> b \<in> (\<Union>n. sigma_sets (space M) (\<Union>i\<in>{..n}. A i))" by auto |
621 then show "a \<inter> b \<in> (\<Union>n. sigma_sets (space M) (\<Union>i\<in>{..n}. A i))" by auto |
626 qed |
622 qed |
627 qed |
623 qed |
628 moreover have "sets (dynkin ?UA) \<subseteq> sets ?D" |
624 also have "dynkin (space M) ?A \<subseteq> ?D" |
629 proof (rule D.dynkin_subset) |
625 using `?A \<subseteq> ?D` by (auto intro!: D.dynkin_subset) |
630 show "sets ?UA \<subseteq> sets ?D" using `?A \<subseteq> sets ?D` by auto |
626 finally show ?thesis by auto |
631 qed simp |
|
632 ultimately have "sets (sigma ?UA) \<subseteq> sets ?D" by simp |
|
633 moreover |
|
634 have "\<And>n. sigma_sets (space M) (\<Union>i\<in>{n..}. A i) \<subseteq> sigma_sets (space M) ?A" |
|
635 by (intro sigma_sets_subseteq UN_mono) (auto intro: sigma_sets.Basic) |
|
636 then have "terminal_events A \<subseteq> sets (sigma ?UA)" |
|
637 unfolding sets_sigma terminal_events_def by auto |
|
638 moreover note `X \<in> terminal_events A` |
|
639 ultimately have "X \<in> sets ?D" by auto |
|
640 then show ?thesis by auto |
|
641 qed |
627 qed |
642 |
628 |
643 lemma (in prob_space) borel_0_1_law: |
629 lemma (in prob_space) borel_0_1_law: |
644 fixes F :: "nat \<Rightarrow> 'a set" |
630 fixes F :: "nat \<Rightarrow> 'a set" |
645 assumes F: "range F \<subseteq> events" "indep_events F UNIV" |
631 assumes F: "range F \<subseteq> events" "indep_events F UNIV" |
646 shows "prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 1" |
632 shows "prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. F m) = 1" |
647 proof (rule kolmogorov_0_1_law[of "\<lambda>i. sigma_sets (space M) { F i }"]) |
633 proof (rule kolmogorov_0_1_law[of "\<lambda>i. sigma_sets (space M) { F i }"]) |
648 show "\<And>i. sigma_sets (space M) {F i} \<subseteq> events" |
634 show "\<And>i. sigma_sets (space M) {F i} \<subseteq> events" |
649 using F(1) sets_into_space |
635 using F(1) sets_into_space |
650 by (subst sigma_sets_singleton) auto |
636 by (subst sigma_sets_singleton) auto |
651 { fix i show "sigma_algebra \<lparr>space = space M, sets = sigma_sets (space M) {F i}\<rparr>" |
637 { fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})" |
652 using sigma_algebra_sigma[of "\<lparr>space = space M, sets = {F i}\<rparr>"] F sets_into_space |
638 using sigma_algebra_sigma_sets[of "{F i}" "space M"] F sets_into_space |
653 by (auto simp add: sigma_def) } |
639 by auto } |
654 show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV" |
640 show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV" |
655 proof (rule indep_sets_sigma_sets) |
641 proof (rule indep_sets_sigma) |
656 show "indep_sets (\<lambda>i. {F i}) UNIV" |
642 show "indep_sets (\<lambda>i. {F i}) UNIV" |
657 unfolding indep_sets_singleton_iff_indep_events by fact |
643 unfolding indep_sets_singleton_iff_indep_events by fact |
658 fix i show "Int_stable \<lparr>space = space M, sets = {F i}\<rparr>" |
644 fix i show "Int_stable {F i}" |
659 unfolding Int_stable_def by simp |
645 unfolding Int_stable_def by simp |
660 qed |
646 qed |
661 let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i" |
647 let ?Q = "\<lambda>n. \<Union>i\<in>{n..}. F i" |
662 show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})" |
648 show "(\<Inter>n. \<Union>m\<in>{n..}. F m) \<in> terminal_events (\<lambda>i. sigma_sets (space M) {F i})" |
663 unfolding terminal_events_def |
649 unfolding terminal_events_def |
664 proof |
650 proof |
665 fix j |
651 fix j |
666 interpret S: sigma_algebra "sigma \<lparr> space = space M, sets = (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})\<rparr>" |
652 interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" |
667 using order_trans[OF F(1) space_closed] |
653 using order_trans[OF F(1) space_closed] |
668 by (intro sigma_algebra_sigma) (simp add: sigma_sets_singleton subset_eq) |
654 by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq) |
669 have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)" |
655 have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)" |
670 by (intro decseq_SucI INT_decseq_offset UN_mono) auto |
656 by (intro decseq_SucI INT_decseq_offset UN_mono) auto |
671 also have "\<dots> \<in> sets (sigma \<lparr> space = space M, sets = (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})\<rparr>)" |
657 also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" |
672 using order_trans[OF F(1) space_closed] |
658 using order_trans[OF F(1) space_closed] |
673 by (safe intro!: S.countable_INT S.countable_UN) |
659 by (safe intro!: S.countable_INT S.countable_UN) |
674 (auto simp: sets_sigma sigma_sets_singleton intro!: sigma_sets.Basic bexI) |
660 (auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI) |
675 finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" |
661 finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})" |
676 by (simp add: sets_sigma) |
662 by simp |
677 qed |
663 qed |
678 qed |
664 qed |
679 |
665 |
680 lemma (in prob_space) indep_sets_finite: |
666 lemma (in prob_space) indep_sets_finite: |
681 assumes I: "I \<noteq> {}" "finite I" |
667 assumes I: "I \<noteq> {}" "finite I" |
708 qed |
694 qed |
709 |
695 |
710 lemma (in prob_space) indep_vars_finite: |
696 lemma (in prob_space) indep_vars_finite: |
711 fixes I :: "'i set" |
697 fixes I :: "'i set" |
712 assumes I: "I \<noteq> {}" "finite I" |
698 assumes I: "I \<noteq> {}" "finite I" |
713 and rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (sigma (M' i)) (X i)" |
699 and M': "\<And>i. i \<in> I \<Longrightarrow> sets (M' i) = sigma_sets (space (M' i)) (E i)" |
714 and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (M' i)" |
700 and rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (M' i) (X i)" |
715 and space: "\<And>i. i \<in> I \<Longrightarrow> space (M' i) \<in> sets (M' i)" |
701 and Int_stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (E i)" |
716 shows "indep_vars (\<lambda>i. sigma (M' i)) X I \<longleftrightarrow> |
702 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))" |
717 (\<forall>A\<in>(\<Pi> i\<in>I. sets (M' 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)))" |
703 shows "indep_vars M' X I \<longleftrightarrow> |
|
704 (\<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)))" |
718 proof - |
705 proof - |
719 from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" |
706 from rv have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> space M \<rightarrow> space (M' i)" |
720 unfolding measurable_def by simp |
707 unfolding measurable_def by simp |
721 |
708 |
722 { fix i assume "i\<in>I" |
709 { fix i assume "i\<in>I" |
723 have "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (sigma (M' i))} |
710 from closed[OF `i \<in> I`] |
724 = sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
711 have "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} |
725 unfolding sigma_sets_vimage_commute[OF X, OF `i \<in> I`] |
712 = sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> E i}" |
|
713 unfolding sigma_sets_vimage_commute[OF X, OF `i \<in> I`, symmetric] M'[OF `i \<in> I`] |
726 by (subst sigma_sets_sigma_sets_eq) auto } |
714 by (subst sigma_sets_sigma_sets_eq) auto } |
727 note this[simp] |
715 note sigma_sets_X = this |
728 |
716 |
729 { fix i assume "i\<in>I" |
717 { fix i assume "i\<in>I" |
730 have "Int_stable \<lparr>space = space M, sets = {X i -` A \<inter> space M |A. A \<in> sets (M' i)}\<rparr>" |
718 have "Int_stable {X i -` A \<inter> space M |A. A \<in> E i}" |
731 proof (rule Int_stableI) |
719 proof (rule Int_stableI) |
732 fix a assume "a \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
720 fix a assume "a \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
733 then obtain A where "a = X i -` A \<inter> space M" "A \<in> sets (M' i)" by auto |
721 then obtain A where "a = X i -` A \<inter> space M" "A \<in> E i" by auto |
734 moreover |
722 moreover |
735 fix b assume "b \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
723 fix b assume "b \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
736 then obtain B where "b = X i -` B \<inter> space M" "B \<in> sets (M' i)" by auto |
724 then obtain B where "b = X i -` B \<inter> space M" "B \<in> E i" by auto |
737 moreover |
725 moreover |
738 have "(X i -` A \<inter> space M) \<inter> (X i -` B \<inter> space M) = X i -` (A \<inter> B) \<inter> space M" by auto |
726 have "(X i -` A \<inter> space M) \<inter> (X i -` B \<inter> space M) = X i -` (A \<inter> B) \<inter> space M" by auto |
739 moreover note Int_stable[OF `i \<in> I`] |
727 moreover note Int_stable[OF `i \<in> I`] |
740 ultimately |
728 ultimately |
741 show "a \<inter> b \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
729 show "a \<inter> b \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
742 by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD) |
730 by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD) |
743 qed } |
731 qed } |
744 note indep_sets_sigma_sets_iff[OF this, simp] |
732 note indep_sets_X = indep_sets_sigma_sets_iff[OF this] |
745 |
733 |
746 { fix i assume "i \<in> I" |
734 { fix i assume "i \<in> I" |
747 { fix A assume "A \<in> sets (M' i)" |
735 { fix A assume "A \<in> E i" |
748 then have "A \<in> sets (sigma (M' i))" by (auto simp: sets_sigma intro: sigma_sets.Basic) |
736 with M'[OF `i \<in> I`] have "A \<in> sets (M' i)" by auto |
749 moreover |
737 moreover |
750 from rv[OF `i\<in>I`] have "X i \<in> measurable M (sigma (M' i))" by auto |
738 from rv[OF `i\<in>I`] have "X i \<in> measurable M (M' i)" by auto |
751 ultimately |
739 ultimately |
752 have "X i -` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) } |
740 have "X i -` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) } |
753 with X[OF `i\<in>I`] space[OF `i\<in>I`] |
741 with X[OF `i\<in>I`] space[OF `i\<in>I`] |
754 have "{X i -` A \<inter> space M |A. A \<in> sets (M' i)} \<subseteq> events" |
742 have "{X i -` A \<inter> space M |A. A \<in> E i} \<subseteq> events" |
755 "space M \<in> {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
743 "space M \<in> {X i -` A \<inter> space M |A. A \<in> E i}" |
756 by (auto intro!: exI[of _ "space (M' i)"]) } |
744 by (auto intro!: exI[of _ "space (M' i)"]) } |
757 note indep_sets_finite[OF I this, simp] |
745 note indep_sets_finite_X = indep_sets_finite[OF I this] |
758 |
746 |
759 have "(\<forall>A\<in>\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}. prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))) = |
747 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))) = |
760 (\<forall>A\<in>\<Pi> i\<in>I. sets (M' 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)))" |
748 (\<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)))" |
761 (is "?L = ?R") |
749 (is "?L = ?R") |
762 proof safe |
750 proof safe |
763 fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. sets (M' i))" |
751 fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. E i)" |
764 from `?L`[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A `I \<noteq> {}` |
752 from `?L`[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A `I \<noteq> {}` |
765 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))" |
753 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))" |
766 by (auto simp add: Pi_iff) |
754 by (auto simp add: Pi_iff) |
767 next |
755 next |
768 fix A assume ?R and A: "A \<in> (\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> sets (M' i)})" |
756 fix A assume ?R and A: "A \<in> (\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> E i})" |
769 from A have "\<forall>i\<in>I. \<exists>B. A i = X i -` B \<inter> space M \<and> B \<in> sets (M' i)" by auto |
757 from A have "\<forall>i\<in>I. \<exists>B. A i = X i -` B \<inter> space M \<and> B \<in> E i" by auto |
770 from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M" |
758 from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M" |
771 "B \<in> (\<Pi> i\<in>I. sets (M' i))" by auto |
759 "B \<in> (\<Pi> i\<in>I. E i)" by auto |
772 from `?R`[THEN bspec, OF B(2)] B(1) `I \<noteq> {}` |
760 from `?R`[THEN bspec, OF B(2)] B(1) `I \<noteq> {}` |
773 show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))" |
761 show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))" |
774 by simp |
762 by simp |
775 qed |
763 qed |
776 then show ?thesis using `I \<noteq> {}` |
764 then show ?thesis using `I \<noteq> {}` |
777 by (simp add: rv indep_vars_def) |
765 by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong) |
778 qed |
766 qed |
779 |
767 |
780 lemma (in prob_space) indep_vars_compose: |
768 lemma (in prob_space) indep_vars_compose: |
781 assumes "indep_vars M' X I" |
769 assumes "indep_vars M' X I" |
782 assumes rv: |
770 assumes rv: "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)" |
783 "\<And>i. i \<in> I \<Longrightarrow> sigma_algebra (N i)" |
|
784 "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)" |
|
785 shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I" |
771 shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I" |
786 unfolding indep_vars_def |
772 unfolding indep_vars_def |
787 proof |
773 proof |
788 from rv `indep_vars M' X I` |
774 from rv `indep_vars M' X I` |
789 show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)" |
775 show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)" |
790 by (auto intro!: measurable_comp simp: indep_vars_def) |
776 by (auto simp: indep_vars_def) |
791 |
777 |
792 have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I" |
778 have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I" |
793 using `indep_vars M' X I` by (simp add: indep_vars_def) |
779 using `indep_vars M' X I` by (simp add: indep_vars_def) |
794 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" |
780 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" |
795 proof (rule indep_sets_mono_sets) |
781 proof (rule indep_sets_mono_sets) |
804 sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
790 sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}" |
805 by (intro sigma_sets_subseteq) (auto simp: vimage_compose) |
791 by (intro sigma_sets_subseteq) (auto simp: vimage_compose) |
806 qed |
792 qed |
807 qed |
793 qed |
808 |
794 |
809 lemma (in prob_space) indep_varsD: |
795 lemma (in prob_space) indep_varsD_finite: |
810 assumes X: "indep_vars M' X I" |
796 assumes X: "indep_vars M' X I" |
811 assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)" |
797 assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)" |
812 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))" |
798 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))" |
813 proof (rule indep_setsD) |
799 proof (rule indep_setsD) |
814 show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I" |
800 show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I" |
815 using X by (auto simp: indep_vars_def) |
801 using X by (auto simp: indep_vars_def) |
816 show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto |
802 show "I \<subseteq> I" "I \<noteq> {}" "finite I" using I by auto |
817 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)}" |
803 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)}" |
818 using I by (auto intro: sigma_sets.Basic) |
804 using I by auto |
819 qed |
805 qed |
820 |
806 |
821 lemma (in prob_space) indep_distribution_eq_measure: |
807 lemma (in prob_space) indep_varsD: |
822 assumes I: "I \<noteq> {}" "finite I" |
808 assumes X: "indep_vars M' X I" |
|
809 assumes I: "J \<noteq> {}" "finite J" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M' i)" |
|
810 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))" |
|
811 proof (rule indep_setsD) |
|
812 show "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I" |
|
813 using X by (auto simp: indep_vars_def) |
|
814 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)}" |
|
815 using I by auto |
|
816 qed fact+ |
|
817 |
|
818 lemma prod_algebra_cong: |
|
819 assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))" |
|
820 shows "prod_algebra I M = prod_algebra J N" |
|
821 proof - |
|
822 have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)" |
|
823 using sets_eq_imp_space_eq[OF sets] by auto |
|
824 with sets show ?thesis unfolding `I = J` |
|
825 by (intro antisym prod_algebra_mono) auto |
|
826 qed |
|
827 |
|
828 lemma space_in_prod_algebra: |
|
829 "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M" |
|
830 proof cases |
|
831 assume "I = {}" then show ?thesis |
|
832 by (auto simp add: prod_algebra_def image_iff prod_emb_def) |
|
833 next |
|
834 assume "I \<noteq> {}" |
|
835 then obtain i where "i \<in> I" by auto |
|
836 then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))" |
|
837 by (auto simp: prod_emb_def Pi_iff) |
|
838 also have "\<dots> \<in> prod_algebra I M" |
|
839 using `i \<in> I` by (intro prod_algebraI) auto |
|
840 finally show ?thesis . |
|
841 qed |
|
842 |
|
843 lemma (in prob_space) indep_vars_iff_distr_eq_PiM: |
|
844 fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b" |
|
845 assumes "I \<noteq> {}" |
823 assumes rv: "\<And>i. random_variable (M' i) (X i)" |
846 assumes rv: "\<And>i. random_variable (M' i) (X i)" |
824 shows "indep_vars M' X I \<longleftrightarrow> |
847 shows "indep_vars M' X I \<longleftrightarrow> |
825 (\<forall>A\<in>sets (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := ereal\<circ>distribution (X i) \<rparr>)). |
848 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))" |
826 distribution (\<lambda>x. \<lambda>i\<in>I. X i x) A = |
849 proof - |
827 finite_measure.\<mu>' (\<Pi>\<^isub>M i\<in>I. (M' i \<lparr> measure := ereal\<circ>distribution (X i) \<rparr>)) A)" |
850 let ?P = "\<Pi>\<^isub>M i\<in>I. M' i" |
828 (is "_ \<longleftrightarrow> (\<forall>X\<in>_. distribution ?D X = finite_measure.\<mu>' (Pi\<^isub>M I ?M) X)") |
851 let ?X = "\<lambda>x. \<lambda>i\<in>I. X i x" |
829 proof - |
852 let ?D = "distr M ?P ?X" |
830 interpret M': prob_space "?M i" for i |
853 have X: "random_variable ?P ?X" by (intro measurable_restrict rv) |
831 using rv by (rule distribution_prob_space) |
854 interpret D: prob_space ?D by (intro prob_space_distr X) |
832 interpret P: finite_product_prob_space ?M I |
855 |
833 proof qed fact |
856 let ?D' = "\<lambda>i. distr M (M' i) (X i)" |
834 |
857 let ?P' = "\<Pi>\<^isub>M i\<in>I. distr M (M' i) (X i)" |
835 let ?D' = "(Pi\<^isub>M I ?M) \<lparr> measure := ereal \<circ> distribution ?D \<rparr>" |
858 interpret D': prob_space "?D' i" for i by (intro prob_space_distr rv) |
836 have "random_variable P.P ?D" |
859 interpret P: product_prob_space ?D' I .. |
837 using `finite I` rv by (intro random_variable_restrict) auto |
860 |
838 then interpret D: prob_space ?D' |
|
839 by (rule distribution_prob_space) |
|
840 |
|
841 show ?thesis |
861 show ?thesis |
842 proof (intro iffI ballI) |
862 proof |
843 assume "indep_vars M' X I" |
863 assume "indep_vars M' X I" |
844 fix A assume "A \<in> sets P.P" |
864 show "?D = ?P'" |
845 moreover |
865 proof (rule measure_eqI_generator_eq) |
846 have "D.prob A = P.prob A" |
866 show "Int_stable (prod_algebra I M')" |
847 proof (rule prob_space_unique_Int_stable) |
867 by (rule Int_stable_prod_algebra) |
848 show "prob_space ?D'" by unfold_locales |
868 show "prod_algebra I M' \<subseteq> Pow (space ?P)" |
849 show "prob_space (Pi\<^isub>M I ?M)" by unfold_locales |
869 using prod_algebra_sets_into_space by (simp add: space_PiM) |
850 show "Int_stable P.G" using M'.Int |
870 show "sets ?D = sigma_sets (space ?P) (prod_algebra I M')" |
851 by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def) |
871 by (simp add: sets_PiM space_PiM) |
852 show "space P.G \<in> sets P.G" |
872 show "sets ?P' = sigma_sets (space ?P) (prod_algebra I M')" |
853 using M'.top by (simp add: product_algebra_generator_def) |
873 by (simp add: sets_PiM space_PiM cong: prod_algebra_cong) |
854 show "space ?D' = space P.G" "sets ?D' = sets (sigma P.G)" |
874 let ?A = "\<lambda>i. \<Pi>\<^isub>E i\<in>I. space (M' i)" |
855 by (simp_all add: product_algebra_def product_algebra_generator_def sets_sigma) |
875 show "range ?A \<subseteq> prod_algebra I M'" "incseq ?A" "(\<Union>i. ?A i) = space (Pi\<^isub>M I M')" |
856 show "space P.P = space P.G" "sets P.P = sets (sigma P.G)" |
876 by (auto simp: space_PiM intro!: space_in_prod_algebra cong: prod_algebra_cong) |
857 by (simp_all add: product_algebra_def) |
877 { fix i show "emeasure ?D (\<Pi>\<^isub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto } |
858 show "A \<in> sets (sigma P.G)" |
878 next |
859 using `A \<in> sets P.P` by (simp add: product_algebra_def) |
879 fix E assume E: "E \<in> prod_algebra I M'" |
860 |
880 from prod_algebraE[OF E] guess J Y . note J = this |
861 fix E assume E: "E \<in> sets P.G" |
881 |
862 then have "E \<in> sets P.P" |
882 from E have "E \<in> sets ?P" by (auto simp: sets_PiM) |
863 by (simp add: sets_sigma sigma_sets.Basic product_algebra_def) |
883 then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)" |
864 then have "D.prob E = distribution ?D E" |
884 by (simp add: emeasure_distr X) |
865 unfolding D.\<mu>'_def by simp |
885 also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)" |
866 also |
886 using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm) |
867 from E obtain F where "E = Pi\<^isub>E I F" and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets (M' i)" |
887 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))" |
868 by (auto simp: product_algebra_generator_def) |
888 using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J] |
869 with `I \<noteq> {}` have "distribution ?D E = prob (\<Inter>i\<in>I. X i -` F i \<inter> space M)" |
889 by (auto simp: emeasure_eq_measure setprod_ereal) |
870 using `I \<noteq> {}` by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def) |
890 also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" |
871 also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` F i \<inter> space M))" |
891 using rv J by (simp add: emeasure_distr) |
872 using `indep_vars M' X I` I F by (rule indep_varsD) |
892 also have "\<dots> = emeasure ?P' E" |
873 also have "\<dots> = P.prob E" |
893 using P.emeasure_PiM_emb[of J Y] J by (simp add: prod_emb_def) |
874 using F by (simp add: `E = Pi\<^isub>E I F` P.prob_times M'.\<mu>'_def distribution_def) |
894 finally show "emeasure ?D E = emeasure ?P' E" . |
875 finally show "D.prob E = P.prob E" . |
|
876 qed |
895 qed |
877 ultimately show "distribution ?D A = P.prob A" |
|
878 by (simp add: D.\<mu>'_def) |
|
879 next |
896 next |
880 assume eq: "\<forall>A\<in>sets P.P. distribution ?D A = P.prob A" |
897 assume "?D = ?P'" |
881 have [simp]: "\<And>i. sigma (M' i) = M' i" |
898 show "indep_vars M' X I" unfolding indep_vars_def |
882 using rv by (intro sigma_algebra.sigma_eq) simp |
899 proof (intro conjI indep_setsI ballI rv) |
883 have "indep_vars (\<lambda>i. sigma (M' i)) X I" |
900 fix i show "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} \<subseteq> events" |
884 proof (subst indep_vars_finite[OF I]) |
901 by (auto intro!: sigma_sets_subset measurable_sets rv) |
885 fix i assume [simp]: "i \<in> I" |
|
886 show "random_variable (sigma (M' i)) (X i)" |
|
887 using rv[of i] by simp |
|
888 show "Int_stable (M' i)" "space (M' i) \<in> sets (M' i)" |
|
889 using M'.Int[of _ i] M'.top by (auto simp: Int_stable_def) |
|
890 next |
902 next |
891 show "\<forall>A\<in>\<Pi> i\<in>I. sets (M' 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))" |
903 fix J Y' assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J" |
|
904 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)}" |
|
905 have "\<forall>j\<in>J. \<exists>Y. Y' j = X j -` Y \<inter> space M \<and> Y \<in> sets (M' j)" |
892 proof |
906 proof |
893 fix A assume A: "A \<in> (\<Pi> i\<in>I. sets (M' i))" |
907 fix j assume "j \<in> J" |
894 then have A_in_P: "(Pi\<^isub>E I A) \<in> sets P.P" |
908 from Y'[rule_format, OF this] rv[of j] |
895 by (auto intro!: product_algebraI) |
909 show "\<exists>Y. Y' j = X j -` Y \<inter> space M \<and> Y \<in> sets (M' j)" |
896 have "prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = distribution ?D (Pi\<^isub>E I A)" |
910 by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"]) |
897 using `I \<noteq> {}`by (auto intro!: arg_cong[where f=prob] simp: Pi_iff distribution_def) |
911 (auto dest: measurable_space simp: sigma_sets_eq) |
898 also have "\<dots> = P.prob (Pi\<^isub>E I A)" using A_in_P eq by simp |
|
899 also have "\<dots> = (\<Prod>i\<in>I. M'.prob i (A i))" |
|
900 using A by (intro P.prob_times) auto |
|
901 also have "\<dots> = (\<Prod>i\<in>I. prob (X i -` A i \<inter> space M))" |
|
902 using A by (auto intro!: setprod_cong simp: M'.\<mu>'_def Pi_iff distribution_def) |
|
903 finally show "prob (\<Inter>j\<in>I. X j -` A j \<inter> space M) = (\<Prod>j\<in>I. prob (X j -` A j \<inter> space M))" . |
|
904 qed |
912 qed |
|
913 from bchoice[OF this] obtain Y where |
|
914 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 |
|
915 let ?E = "prod_emb I M' J (Pi\<^isub>E J Y)" |
|
916 from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M" |
|
917 using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def Pi_iff split: split_if_asm) |
|
918 then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)" |
|
919 by simp |
|
920 also have "\<dots> = emeasure ?D ?E" |
|
921 using Y J by (intro emeasure_distr[symmetric] X sets_PiM_I) auto |
|
922 also have "\<dots> = emeasure ?P' ?E" |
|
923 using `?D = ?P'` by simp |
|
924 also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))" |
|
925 using P.emeasure_PiM_emb[of J Y] J Y by (simp add: prod_emb_def) |
|
926 also have "\<dots> = (\<Prod> i\<in>J. emeasure M (Y' i))" |
|
927 using rv J Y by (simp add: emeasure_distr) |
|
928 finally have "emeasure M (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. emeasure M (Y' i))" . |
|
929 then show "prob (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. prob (Y' i))" |
|
930 by (auto simp: emeasure_eq_measure setprod_ereal) |
905 qed |
931 qed |
906 then show "indep_vars M' X I" |
|
907 by simp |
|
908 qed |
932 qed |
909 qed |
933 qed |
910 |
934 |
911 lemma (in prob_space) indep_varD: |
935 lemma (in prob_space) indep_varD: |
912 assumes indep: "indep_var Ma A Mb B" |
936 assumes indep: "indep_var Ma A Mb B" |
934 using assms unfolding indep_var_def indep_vars_def by auto |
958 using assms unfolding indep_var_def indep_vars_def by auto |
935 then show "random_variable S X" "random_variable T Y" |
959 then show "random_variable S X" "random_variable T Y" |
936 unfolding UNIV_bool by auto |
960 unfolding UNIV_bool by auto |
937 qed |
961 qed |
938 |
962 |
939 lemma (in prob_space) indep_var_distributionD: |
963 lemma measurable_bool_case[simp, intro]: |
940 assumes indep: "indep_var S X T Y" |
964 "(\<lambda>(x, y). bool_case x y) \<in> measurable (M \<Otimes>\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))" |
941 defines "P \<equiv> S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>" |
965 (is "?f \<in> measurable ?B ?P") |
942 assumes "A \<in> sets P" |
966 proof (rule measurable_PiM_single) |
943 shows "joint_distribution X Y A = finite_measure.\<mu>' P A" |
967 show "?f \<in> space ?B \<rightarrow> (\<Pi>\<^isub>E i\<in>UNIV. space (bool_case M N i))" |
944 proof - |
968 by (auto simp: space_pair_measure extensional_def split: bool.split) |
945 from indep have rvs: "random_variable S X" "random_variable T Y" |
969 fix i A assume "A \<in> sets (case i of True \<Rightarrow> M | False \<Rightarrow> N)" |
|
970 moreover then have "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} |
|
971 = (case i of True \<Rightarrow> A \<times> space N | False \<Rightarrow> space M \<times> A)" |
|
972 by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space) |
|
973 ultimately show "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} \<in> sets ?B" |
|
974 by (auto split: bool.split) |
|
975 qed |
|
976 |
|
977 lemma borel_measurable_indicator': |
|
978 "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M" |
|
979 using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def) |
|
980 |
|
981 lemma (in product_sigma_finite) distr_component: |
|
982 "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P") |
|
983 proof (intro measure_eqI[symmetric]) |
|
984 interpret I: finite_product_sigma_finite M "{i}" by default simp |
|
985 |
|
986 have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x" |
|
987 by (auto simp: extensional_def restrict_def) |
|
988 |
|
989 fix A assume A: "A \<in> sets ?P" |
|
990 then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" |
|
991 by simp |
|
992 also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) x \<partial>M i)" |
|
993 apply (subst product_positive_integral_singleton[symmetric]) |
|
994 apply (force intro!: measurable_restrict measurable_sets A) |
|
995 apply (auto intro!: positive_integral_cong simp: space_PiM indicator_def simp: eq) |
|
996 done |
|
997 also have "\<dots> = emeasure (M i) ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i))" |
|
998 by (force intro!: measurable_restrict measurable_sets A positive_integral_indicator) |
|
999 also have "\<dots> = emeasure ?D A" |
|
1000 using A by (auto intro!: emeasure_distr[symmetric] measurable_restrict) |
|
1001 finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" . |
|
1002 qed simp |
|
1003 |
|
1004 lemma pair_measure_eqI: |
|
1005 assumes "sigma_finite_measure M1" "sigma_finite_measure M2" |
|
1006 assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M" |
|
1007 assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)" |
|
1008 shows "M1 \<Otimes>\<^isub>M M2 = M" |
|
1009 proof - |
|
1010 interpret M1: sigma_finite_measure M1 by fact |
|
1011 interpret M2: sigma_finite_measure M2 by fact |
|
1012 interpret pair_sigma_finite M1 M2 by default |
|
1013 from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this |
|
1014 let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}" |
|
1015 let ?P = "M1 \<Otimes>\<^isub>M M2" |
|
1016 show ?thesis |
|
1017 proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]]) |
|
1018 show "?E \<subseteq> Pow (space ?P)" |
|
1019 using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure) |
|
1020 show "sets ?P = sigma_sets (space ?P) ?E" |
|
1021 by (simp add: sets_pair_measure space_pair_measure) |
|
1022 then show "sets M = sigma_sets (space ?P) ?E" |
|
1023 using sets[symmetric] by simp |
|
1024 next |
|
1025 show "range F \<subseteq> ?E" "incseq F" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>" |
|
1026 using F by (auto simp: space_pair_measure) |
|
1027 next |
|
1028 fix X assume "X \<in> ?E" |
|
1029 then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto |
|
1030 then have "emeasure ?P X = emeasure M1 A * emeasure M2 B" |
|
1031 by (simp add: emeasure_pair_measure_Times) |
|
1032 also have "\<dots> = emeasure M (A \<times> B)" |
|
1033 using A B emeasure by auto |
|
1034 finally show "emeasure ?P X = emeasure M X" |
|
1035 by simp |
|
1036 qed |
|
1037 qed |
|
1038 |
|
1039 lemma pair_measure_eq_distr_PiM: |
|
1040 fixes M1 :: "'a measure" and M2 :: "'a measure" |
|
1041 assumes "sigma_finite_measure M1" "sigma_finite_measure M2" |
|
1042 shows "(M1 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. (x True, x False))" |
|
1043 (is "?P = ?D") |
|
1044 proof (rule pair_measure_eqI[OF assms]) |
|
1045 interpret B: product_sigma_finite "bool_case M1 M2" |
|
1046 unfolding product_sigma_finite_def using assms by (auto split: bool.split) |
|
1047 let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)" |
|
1048 |
|
1049 have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)" |
|
1050 by auto |
|
1051 fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2" |
|
1052 have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))" |
|
1053 by (simp add: UNIV_bool ac_simps) |
|
1054 also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))" |
|
1055 using A B by (subst B.emeasure_PiM) (auto split: bool.split) |
|
1056 also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B" |
|
1057 using A[THEN sets_into_space] B[THEN sets_into_space] |
|
1058 by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split) |
|
1059 finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)" |
|
1060 using A B |
|
1061 measurable_component_singleton[of True UNIV "bool_case M1 M2"] |
|
1062 measurable_component_singleton[of False UNIV "bool_case M1 M2"] |
|
1063 by (subst emeasure_distr) (auto simp: measurable_pair_iff) |
|
1064 qed simp |
|
1065 |
|
1066 lemma measurable_Pair: |
|
1067 assumes rvs: "X \<in> measurable M S" "Y \<in> measurable M T" |
|
1068 shows "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)" |
|
1069 proof - |
|
1070 have [simp]: "fst \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. X x)" "snd \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. Y x)" |
|
1071 by auto |
|
1072 show " (\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)" |
|
1073 by (auto simp: measurable_pair_iff rvs) |
|
1074 qed |
|
1075 |
|
1076 lemma (in prob_space) indep_var_distribution_eq: |
|
1077 "indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and> |
|
1078 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") |
|
1079 proof safe |
|
1080 assume "indep_var S X T Y" |
|
1081 then show rvs: "random_variable S X" "random_variable T Y" |
946 by (blast dest: indep_var_rv1 indep_var_rv2)+ |
1082 by (blast dest: indep_var_rv1 indep_var_rv2)+ |
947 |
1083 then have XY: "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" |
948 let ?S = "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" |
1084 by (rule measurable_Pair) |
949 let ?T = "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>" |
1085 |
950 interpret X: prob_space ?S by (rule distribution_prob_space) fact |
1086 interpret X: prob_space ?S by (rule prob_space_distr) fact |
951 interpret Y: prob_space ?T by (rule distribution_prob_space) fact |
1087 interpret Y: prob_space ?T by (rule prob_space_distr) fact |
952 interpret XY: pair_prob_space ?S ?T by default |
1088 interpret XY: pair_prob_space ?S ?T .. |
953 |
1089 show "?S \<Otimes>\<^isub>M ?T = ?J" |
954 let ?J = "XY.P\<lparr> measure := ereal \<circ> joint_distribution X Y \<rparr>" |
1090 proof (rule pair_measure_eqI) |
955 interpret J: prob_space ?J |
1091 show "sigma_finite_measure ?S" .. |
956 by (rule joint_distribution_prob_space) (simp_all add: rvs) |
1092 show "sigma_finite_measure ?T" .. |
957 |
1093 |
958 have "finite_measure.\<mu>' (XY.P\<lparr> measure := ereal \<circ> joint_distribution X Y \<rparr>) A = XY.\<mu>' A" |
1094 fix A B assume A: "A \<in> sets ?S" and B: "B \<in> sets ?T" |
959 proof (rule prob_space_unique_Int_stable) |
1095 have "emeasure ?J (A \<times> B) = emeasure M ((\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M)" |
960 show "Int_stable (pair_measure_generator ?S ?T)" (is "Int_stable ?P") |
1096 using A B by (intro emeasure_distr[OF XY]) auto |
961 by fact |
1097 also have "\<dots> = emeasure M (X -` A \<inter> space M) * emeasure M (Y -` B \<inter> space M)" |
962 show "space ?P \<in> sets ?P" |
1098 using indep_varD[OF `indep_var S X T Y`, of A B] A B by (simp add: emeasure_eq_measure) |
963 unfolding space_pair_measure[simplified pair_measure_def space_sigma] |
1099 also have "\<dots> = emeasure ?S A * emeasure ?T B" |
964 using X.top Y.top by (auto intro!: pair_measure_generatorI) |
1100 using rvs A B by (simp add: emeasure_distr) |
965 |
1101 finally show "emeasure ?S A * emeasure ?T B = emeasure ?J (A \<times> B)" by simp |
966 show "prob_space ?J" by unfold_locales |
1102 qed simp |
967 show "space ?J = space ?P" |
1103 next |
968 by (simp add: pair_measure_generator_def space_pair_measure) |
1104 assume rvs: "random_variable S X" "random_variable T Y" |
969 show "sets ?J = sets (sigma ?P)" |
1105 then have XY: "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" |
970 by (simp add: pair_measure_def) |
1106 by (rule measurable_Pair) |
971 |
1107 |
972 show "prob_space XY.P" by unfold_locales |
1108 let ?S = "distr M S X" and ?T = "distr M T Y" |
973 show "space XY.P = space ?P" "sets XY.P = sets (sigma ?P)" |
1109 interpret X: prob_space ?S by (rule prob_space_distr) fact |
974 by (simp_all add: pair_measure_generator_def pair_measure_def) |
1110 interpret Y: prob_space ?T by (rule prob_space_distr) fact |
975 |
1111 interpret XY: pair_prob_space ?S ?T .. |
976 show "A \<in> sets (sigma ?P)" |
1112 |
977 using `A \<in> sets P` unfolding P_def pair_measure_def by simp |
1113 assume "?S \<Otimes>\<^isub>M ?T = ?J" |
978 |
1114 |
979 fix X assume "X \<in> sets ?P" |
1115 { fix S and X |
980 then obtain A B where "A \<in> sets S" "B \<in> sets T" "X = A \<times> B" |
1116 have "Int_stable {X -` A \<inter> space M |A. A \<in> sets S}" |
981 by (auto simp: sets_pair_measure_generator) |
1117 proof (safe intro!: Int_stableI) |
982 then show "J.\<mu>' X = XY.\<mu>' X" |
1118 fix A B assume "A \<in> sets S" "B \<in> sets S" |
983 unfolding J.\<mu>'_def XY.\<mu>'_def using indep |
1119 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" |
984 by (simp add: XY.pair_measure_times) |
1120 by (intro exI[of _ "A \<inter> B"]) auto |
985 (simp add: distribution_def indep_varD) |
1121 qed } |
986 qed |
1122 note Int_stable = this |
987 then show ?thesis |
1123 |
988 using `A \<in> sets P` unfolding P_def J.\<mu>'_def XY.\<mu>'_def by simp |
1124 show "indep_var S X T Y" unfolding indep_var_eq |
|
1125 proof (intro conjI indep_set_sigma_sets Int_stable rvs) |
|
1126 show "indep_set {X -` A \<inter> space M |A. A \<in> sets S} {Y -` A \<inter> space M |A. A \<in> sets T}" |
|
1127 proof (safe intro!: indep_setI) |
|
1128 { fix A assume "A \<in> sets S" then show "X -` A \<inter> space M \<in> sets M" |
|
1129 using `X \<in> measurable M S` by (auto intro: measurable_sets) } |
|
1130 { fix A assume "A \<in> sets T" then show "Y -` A \<inter> space M \<in> sets M" |
|
1131 using `Y \<in> measurable M T` by (auto intro: measurable_sets) } |
|
1132 next |
|
1133 fix A B assume ab: "A \<in> sets S" "B \<in> sets T" |
|
1134 then have "ereal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) = emeasure ?J (A \<times> B)" |
|
1135 using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"]) |
|
1136 also have "\<dots> = emeasure (?S \<Otimes>\<^isub>M ?T) (A \<times> B)" |
|
1137 unfolding `?S \<Otimes>\<^isub>M ?T = ?J` .. |
|
1138 also have "\<dots> = emeasure ?S A * emeasure ?T B" |
|
1139 using ab by (simp add: XY.emeasure_pair_measure_Times) |
|
1140 finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) = |
|
1141 prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)" |
|
1142 using rvs ab by (simp add: emeasure_eq_measure emeasure_distr) |
|
1143 qed |
|
1144 qed |
989 qed |
1145 qed |
990 |
1146 |
991 end |
1147 end |