634 also have "?p' = (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))" |
634 also have "?p' = (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))" |
635 using J E[rule_format, THEN sets.sets_into_space] |
635 using J E[rule_format, THEN sets.sets_into_space] |
636 by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+ |
636 by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+ |
637 also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) = |
637 also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) = |
638 (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))" |
638 (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))" |
639 using E by (subst insert) (auto intro!: setprod_cong) |
639 using E by (subst insert) (auto intro!: setprod.cong) |
640 also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) * |
640 also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) * |
641 emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)" |
641 emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)" |
642 using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod_cong) |
642 using insert by (auto simp: mult_commute intro!: arg_cong2[where f="op *"] setprod.cong) |
643 also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)" |
643 also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)" |
644 using insert(1,2) J E by (intro setprod_mono_one_right) auto |
644 using insert(1,2) J E by (intro setprod.mono_neutral_right) auto |
645 finally show "?\<mu> ?p = \<dots>" . |
645 finally show "?\<mu> ?p = \<dots>" . |
646 |
646 |
647 show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))" |
647 show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))" |
648 using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def) |
648 using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def) |
649 next |
649 next |
651 using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all |
651 using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all |
652 next |
652 next |
653 show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and> |
653 show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and> |
654 insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))" |
654 insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))" |
655 using insert by auto |
655 using insert by auto |
656 qed (auto intro!: setprod_cong) |
656 qed (auto intro!: setprod.cong) |
657 with insert show ?case |
657 with insert show ?case |
658 by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space) |
658 by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space) |
659 qed simp |
659 qed simp |
660 |
660 |
661 lemma (in product_sigma_finite) sigma_finite: |
661 lemma (in product_sigma_finite) sigma_finite: |
762 using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM) |
762 using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM) |
763 also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))" |
763 also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))" |
764 using `finite J` `finite I` F unfolding X |
764 using `finite J` `finite I` F unfolding X |
765 by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times) |
765 by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times) |
766 also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))" |
766 also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))" |
767 using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod_Un_one) |
767 using `finite J` `finite I` `I \<inter> J = {}` by (simp add: setprod.union_inter_neutral) |
768 also have "\<dots> = emeasure ?P (Pi\<^sub>E (I \<union> J) F)" |
768 also have "\<dots> = emeasure ?P (Pi\<^sub>E (I \<union> J) F)" |
769 using `finite J` `finite I` F unfolding A |
769 using `finite J` `finite I` F unfolding A |
770 by (intro IJ.measure_times[symmetric]) auto |
770 by (intro IJ.measure_times[symmetric]) auto |
771 finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp |
771 finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp |
772 qed |
772 qed |
847 using assms proof induct |
847 using assms proof induct |
848 case (insert i I) |
848 case (insert i I) |
849 note `finite I`[intro, simp] |
849 note `finite I`[intro, simp] |
850 interpret I: finite_product_sigma_finite M I by default auto |
850 interpret I: finite_product_sigma_finite M I by default auto |
851 have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))" |
851 have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))" |
852 using insert by (auto intro!: setprod_cong) |
852 using insert by (auto intro!: setprod.cong) |
853 have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^sub>M J M)" |
853 have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^sub>M J M)" |
854 using sets.sets_into_space insert |
854 using sets.sets_into_space insert |
855 by (intro borel_measurable_ereal_setprod |
855 by (intro borel_measurable_ereal_setprod |
856 measurable_comp[OF measurable_component_singleton, unfolded comp_def]) |
856 measurable_comp[OF measurable_component_singleton, unfolded comp_def]) |
857 auto |
857 auto |