438 from \<open>i \<in> I\<close> J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j" |
438 from \<open>i \<in> I\<close> J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j" |
439 by auto |
439 by auto |
440 obtain S where S: "\<And>i. i \<in> j \<Longrightarrow> S i \<subseteq> E i" "\<And>i. i \<in> j \<Longrightarrow> countable (S i)" |
440 obtain S where S: "\<And>i. i \<in> j \<Longrightarrow> S i \<subseteq> E i" "\<And>i. i \<in> j \<Longrightarrow> countable (S i)" |
441 "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)" |
441 "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)" |
442 by (metis subset_eq \<Omega>_cover \<open>j \<subseteq> I\<close>) |
442 by (metis subset_eq \<Omega>_cover \<open>j \<subseteq> I\<close>) |
443 def A' \<equiv> "\<lambda>n. n(i := A)" |
443 define A' where "A' n = n(i := A)" for n |
444 then have A'_i: "\<And>n. A' n i = A" |
444 then have A'_i: "\<And>n. A' n i = A" |
445 by simp |
445 by simp |
446 { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S" |
446 { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S" |
447 then have "A' n \<in> Pi j E" |
447 then have "A' n \<in> Pi j E" |
448 unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def \<open>A \<in> E i\<close> ) |
448 unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def \<open>A \<in> E i\<close> ) |
802 P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))" |
802 P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))" |
803 assumes A: "finite_measure P" |
803 assumes A: "finite_measure P" |
804 shows "P = Q" |
804 shows "P = Q" |
805 proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) |
805 proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) |
806 interpret finite_measure P by fact |
806 interpret finite_measure P by fact |
807 def i \<equiv> "SOME i. i \<in> I" |
807 define i where "i = (SOME i. i \<in> I)" |
808 have i: "I \<noteq> {} \<Longrightarrow> i \<in> I" |
808 have i: "I \<noteq> {} \<Longrightarrow> i \<in> I" |
809 unfolding i_def by (rule someI_ex) auto |
809 unfolding i_def by (rule someI_ex) auto |
810 def A \<equiv> "\<lambda>n::nat. if I = {} then prod_emb I M {} (\<Pi>\<^sub>E i\<in>{}. {}) else prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))" |
810 define A where "A n = |
|
811 (if I = {} then prod_emb I M {} (\<Pi>\<^sub>E i\<in>{}. {}) else prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)))" |
|
812 for n :: nat |
811 then show "range A \<subseteq> prod_algebra I M" |
813 then show "range A \<subseteq> prod_algebra I M" |
812 using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i) |
814 using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i) |
813 have "\<And>i. A i = space (PiM I M)" |
815 have "\<And>i. A i = space (PiM I M)" |
814 by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI) |
816 by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI) |
815 then show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. emeasure P (A i) \<noteq> \<infinity>" |
817 then show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. emeasure P (A i) \<noteq> \<infinity>" |
952 from sigma_finite_pairs guess C .. note C = this |
954 from sigma_finite_pairs guess C .. note C = this |
953 show ?thesis |
955 show ?thesis |
954 proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric]) |
956 proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric]) |
955 show "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>M I M) (Pi\<^sub>E I A) = P (Pi\<^sub>E I A)" for A |
957 show "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>M I M) (Pi\<^sub>E I A) = P (Pi\<^sub>E I A)" for A |
956 by (simp add: eq emeasure_PiM) |
958 by (simp add: eq emeasure_PiM) |
957 def A \<equiv> "\<lambda>n. \<Pi>\<^sub>E i\<in>I. C i n" |
959 define A where "A n = (\<Pi>\<^sub>E i\<in>I. C i n)" for n |
958 with C show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>" "(\<Union>i. A i) = space (PiM I M)" |
960 with C show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>" "(\<Union>i. A i) = space (PiM I M)" |
959 by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_setprod_eq_top) |
961 by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_setprod_eq_top) |
960 qed |
962 qed |
961 qed |
963 qed |
962 |
964 |