54 "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I J (x, y) i = undefined" |
54 "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I J (x, y) i = undefined" |
55 unfolding merge_def by auto |
55 unfolding merge_def by auto |
56 |
56 |
57 lemma merge_commute: |
57 lemma merge_commute: |
58 "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)" |
58 "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)" |
59 by (auto simp: merge_def intro!: ext) |
59 by (force simp: merge_def) |
60 |
60 |
61 lemma Pi_cancel_merge_range[simp]: |
61 lemma Pi_cancel_merge_range[simp]: |
62 "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A" |
62 "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A" |
63 "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A" |
63 "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A" |
64 "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A" |
64 "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A" |
428 by (auto simp: prod_emb_def) |
428 by (auto simp: prod_emb_def) |
429 then show ?thesis |
429 then show ?thesis |
430 by (auto simp add: sets_PiM intro!: sigma_sets_top) |
430 by (auto simp add: sets_PiM intro!: sigma_sets_top) |
431 next |
431 next |
432 assume "J \<noteq> {}" with assms show ?thesis |
432 assume "J \<noteq> {}" with assms show ?thesis |
433 by (auto simp add: sets_PiM prod_algebra_def intro!: sigma_sets.Basic) |
433 by (force simp add: sets_PiM prod_algebra_def) |
434 qed |
434 qed |
435 |
435 |
436 lemma measurable_PiM: |
436 lemma measurable_PiM: |
437 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))" |
437 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))" |
438 assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow> |
438 assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow> |
473 with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto |
473 with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto |
474 also have "\<dots> \<in> sets N" using B by (rule sets) |
474 also have "\<dots> \<in> sets N" using B by (rule sets) |
475 finally show "f -` A \<inter> space N \<in> sets N" . |
475 finally show "f -` A \<inter> space N \<in> sets N" . |
476 qed (auto simp: space) |
476 qed (auto simp: space) |
477 |
477 |
478 lemma sets_PiM_I_finite[simp, intro]: |
478 lemma sets_PiM_I_finite[measurable]: |
479 assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))" |
479 assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))" |
480 shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)" |
480 shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)" |
481 using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto |
481 using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto |
482 |
482 |
483 lemma measurable_component_update: |
483 lemma measurable_component_singleton[measurable (raw)]: |
484 assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I" |
|
485 shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _") |
|
486 proof (intro measurable_PiM_single) |
|
487 fix j A assume "j \<in> insert i I" "A \<in> sets (M j)" |
|
488 moreover have "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} = |
|
489 (if i = j then space (M i) \<inter> A else if x j \<in> A then space (M i) else {})" |
|
490 by auto |
|
491 ultimately show "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} \<in> sets (M i)" |
|
492 by auto |
|
493 qed (insert sets_into_space assms, auto simp: space_PiM) |
|
494 |
|
495 lemma measurable_component_singleton: |
|
496 assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)" |
484 assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)" |
497 proof (unfold measurable_def, intro CollectI conjI ballI) |
485 proof (unfold measurable_def, intro CollectI conjI ballI) |
498 fix A assume "A \<in> sets (M i)" |
486 fix A assume "A \<in> sets (M i)" |
499 then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = prod_emb I M {i} (\<Pi>\<^isub>E j\<in>{i}. A)" |
487 then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = prod_emb I M {i} (\<Pi>\<^isub>E j\<in>{i}. A)" |
500 using sets_into_space `i \<in> I` |
488 using sets_into_space `i \<in> I` |
501 by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm) |
489 by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm) |
502 then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)" |
490 then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)" |
503 using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I) |
491 using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I) |
504 qed (insert `i \<in> I`, auto simp: space_PiM) |
492 qed (insert `i \<in> I`, auto simp: space_PiM) |
505 |
493 |
506 lemma measurable_add_dim: |
494 lemma measurable_add_dim[measurable]: |
507 "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)" |
495 "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)" |
508 (is "?f \<in> measurable ?P ?I") |
496 (is "?f \<in> measurable ?P ?I") |
509 proof (rule measurable_PiM_single) |
497 proof (rule measurable_PiM_single) |
510 fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)" |
498 fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)" |
511 have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} = |
499 have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} = |
515 using A j |
503 using A j |
516 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
504 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
517 finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" . |
505 finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" . |
518 qed (auto simp: space_pair_measure space_PiM) |
506 qed (auto simp: space_pair_measure space_PiM) |
519 |
507 |
520 lemma measurable_merge: |
508 lemma measurable_component_update: |
|
509 "x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" |
|
510 by simp |
|
511 |
|
512 lemma measurable_merge[measurable]: |
521 "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)" |
513 "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)" |
522 (is "?f \<in> measurable ?P ?U") |
514 (is "?f \<in> measurable ?P ?U") |
523 proof (rule measurable_PiM_single) |
515 proof (rule measurable_PiM_single) |
524 fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J" |
516 fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J" |
525 then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} = |
517 then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} = |
529 using A |
521 using A |
530 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
522 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
531 finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" . |
523 finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" . |
532 qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def) |
524 qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def) |
533 |
525 |
534 lemma measurable_restrict: |
526 lemma measurable_restrict[measurable (raw)]: |
535 assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)" |
527 assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)" |
536 shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)" |
528 shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)" |
537 proof (rule measurable_PiM_single) |
529 proof (rule measurable_PiM_single) |
538 fix A i assume A: "i \<in> I" "A \<in> sets (M i)" |
530 fix A i assume A: "i \<in> I" "A \<in> sets (M i)" |
539 then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N" |
531 then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N" |
540 by auto |
532 by auto |
541 then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N" |
533 then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N" |
542 using A X by (auto intro!: measurable_sets) |
534 using A X by (auto intro!: measurable_sets) |
543 qed (insert X, auto dest: measurable_space) |
535 qed (insert X, auto dest: measurable_space) |
|
536 |
|
537 lemma sets_in_Pi_aux: |
|
538 "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow> |
|
539 {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)" |
|
540 by (simp add: subset_eq Pi_iff) |
|
541 |
|
542 lemma sets_in_Pi[measurable (raw)]: |
|
543 "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow> |
|
544 (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow> |
|
545 Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)" |
|
546 unfolding pred_def |
|
547 by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto |
|
548 |
|
549 lemma sets_in_extensional_aux: |
|
550 "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)" |
|
551 proof - |
|
552 have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)" |
|
553 by (auto simp add: extensional_def space_PiM) |
|
554 then show ?thesis by simp |
|
555 qed |
|
556 |
|
557 lemma sets_in_extensional[measurable (raw)]: |
|
558 "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)" |
|
559 unfolding pred_def |
|
560 by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto |
544 |
561 |
545 locale product_sigma_finite = |
562 locale product_sigma_finite = |
546 fixes M :: "'i \<Rightarrow> 'a measure" |
563 fixes M :: "'i \<Rightarrow> 'a measure" |
547 assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)" |
564 assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)" |
548 |
565 |
757 fix k |
774 fix k |
758 from F `finite I` setprod_PInf[of "I \<union> J", OF emeasure_nonneg, of M] |
775 from F `finite I` setprod_PInf[of "I \<union> J", OF emeasure_nonneg, of M] |
759 show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto |
776 show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto |
760 next |
777 next |
761 fix A assume A: "A \<in> prod_algebra (I \<union> J) M" |
778 fix A assume A: "A \<in> prod_algebra (I \<union> J) M" |
762 with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>I \<union> J. F i \<in> sets (M i)" |
779 with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)" |
763 by (auto simp add: prod_algebra_eq_finite) |
780 by (auto simp add: prod_algebra_eq_finite) |
764 let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M" |
781 let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M" |
765 let ?X = "?g -` A \<inter> space ?B" |
782 let ?X = "?g -` A \<inter> space ?B" |
766 have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)" |
783 have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)" |
767 using F[rule_format, THEN sets_into_space] by (auto simp: space_PiM) |
784 using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+ |
768 then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)" |
785 then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)" |
769 unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM) |
786 unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM) |
770 have "emeasure ?D A = emeasure ?B ?X" |
787 have "emeasure ?D A = emeasure ?B ?X" |
771 using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM) |
788 using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM) |
772 also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))" |
789 also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))" |
773 using `finite J` `finite I` F X |
790 using `finite J` `finite I` F unfolding X |
774 by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff) |
791 by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff) |
775 also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))" |
792 also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))" |
776 using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one) |
793 using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one) |
777 also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)" |
794 also have "\<dots> = emeasure ?P (Pi\<^isub>E (I \<union> J) F)" |
778 using `finite J` `finite I` F unfolding A |
795 using `finite J` `finite I` F unfolding A |
1011 by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI) |
1028 by (simp add: * insert integral_multc integral_cmult[OF prod] subset_insertI) |
1012 qed |
1029 qed |
1013 |
1030 |
1014 lemma sets_Collect_single: |
1031 lemma sets_Collect_single: |
1015 "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)" |
1032 "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)" |
1016 unfolding sets_PiM_single |
1033 by simp |
1017 by (auto intro!: sigma_sets.Basic exI[of _ i] exI[of _ A]) (auto simp: space_PiM) |
|
1018 |
1034 |
1019 lemma sigma_prod_algebra_sigma_eq_infinite: |
1035 lemma sigma_prod_algebra_sigma_eq_infinite: |
1020 fixes E :: "'i \<Rightarrow> 'a set set" |
1036 fixes E :: "'i \<Rightarrow> 'a set set" |
1021 assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)" |
1037 assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)" |
1022 and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i" |
1038 and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i" |