100 ultimately show "emeasure (M i) A = emeasure (distr (PiM I M) (M i) (\<lambda>\<omega>. \<omega> i)) A" |
100 ultimately show "emeasure (M i) A = emeasure (distr (PiM I M) (M i) (\<lambda>\<omega>. \<omega> i)) A" |
101 by (auto simp: `i\<in>I` emeasure_distr measurable_component_singleton emeasure_PiM_Collect_single) |
101 by (auto simp: `i\<in>I` emeasure_distr measurable_component_singleton emeasure_PiM_Collect_single) |
102 qed simp |
102 qed simp |
103 |
103 |
104 lemma (in product_prob_space) PiM_eq: |
104 lemma (in product_prob_space) PiM_eq: |
105 assumes "sets M' = sets (PiM I M)" |
105 assumes M': "sets M' = sets (PiM I M)" |
106 assumes eq: "\<And>J F. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>j. j \<in> J \<Longrightarrow> F j \<in> sets (M j)) \<Longrightarrow> |
106 assumes eq: "\<And>J F. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>j. j \<in> J \<Longrightarrow> F j \<in> sets (M j)) \<Longrightarrow> |
107 emeasure M' (prod_emb I M J (\<Pi>\<^sub>E j\<in>J. F j)) = (\<Prod>j\<in>J. emeasure (M j) (F j))" |
107 emeasure M' (prod_emb I M J (\<Pi>\<^sub>E j\<in>J. F j)) = (\<Prod>j\<in>J. emeasure (M j) (F j))" |
108 shows "M' = (PiM I M)" |
108 shows "M' = (PiM I M)" |
109 proof (rule measure_eqI_generator_eq[symmetric, OF Int_stable_prod_algebra prod_algebra_sets_into_space]) |
109 proof (rule measure_eqI_PiM_infinite[symmetric, OF refl M']) |
110 show "sets (PiM I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)" |
110 show "finite_measure (Pi\<^sub>M I M)" |
111 by (rule sets_PiM) |
111 by standard (simp add: P.emeasure_space_1) |
112 then show "sets M' = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)" |
112 qed (simp add: eq emeasure_PiM_emb) |
113 unfolding `sets M' = sets (PiM I M)` by simp |
|
114 |
|
115 def i \<equiv> "SOME i. i \<in> I" |
|
116 have i: "I \<noteq> {} \<Longrightarrow> i \<in> I" |
|
117 unfolding i_def by (rule someI_ex) auto |
|
118 |
|
119 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))" |
|
120 then show "range A \<subseteq> prod_algebra I M" |
|
121 using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i) |
|
122 |
|
123 have A_eq: "\<And>i. A i = space (PiM I M)" |
|
124 by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI) |
|
125 show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" |
|
126 unfolding A_eq by (auto simp: space_PiM) |
|
127 show "\<And>i. emeasure (PiM I M) (A i) \<noteq> \<infinity>" |
|
128 unfolding A_eq P.emeasure_space_1 by simp |
|
129 next |
|
130 fix X assume X: "X \<in> prod_algebra I M" |
|
131 then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)" |
|
132 and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)" |
|
133 by (force elim!: prod_algebraE) |
|
134 from eq[OF J] have "emeasure M' X = (\<Prod>j\<in>J. emeasure (M j) (E j))" |
|
135 by (simp add: X) |
|
136 also have "\<dots> = emeasure (PiM I M) X" |
|
137 unfolding X using J by (intro emeasure_PiM_emb[symmetric]) auto |
|
138 finally show "emeasure (PiM I M) X = emeasure M' X" .. |
|
139 qed |
|
140 |
113 |
141 lemma (in product_prob_space) AE_component: "i \<in> I \<Longrightarrow> AE x in M i. P x \<Longrightarrow> AE x in PiM I M. P (x i)" |
114 lemma (in product_prob_space) AE_component: "i \<in> I \<Longrightarrow> AE x in M i. P x \<Longrightarrow> AE x in PiM I M. P (x i)" |
142 apply (rule AE_distrD[of "\<lambda>\<omega>. \<omega> i" "PiM I M" "M i" P]) |
115 apply (rule AE_distrD[of "\<lambda>\<omega>. \<omega> i" "PiM I M" "M i" P]) |
143 apply simp |
116 apply simp |
144 apply (subst PiM_component) |
117 apply (subst PiM_component) |