114 subsubsection%important \<open>Products\<close> |
114 subsubsection%important \<open>Products\<close> |
115 |
115 |
116 definition%important prod_emb where |
116 definition%important prod_emb where |
117 "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
117 "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
118 |
118 |
119 lemma%important prod_emb_iff: |
119 lemma prod_emb_iff: |
120 "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))" |
120 "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))" |
121 unfolding%unimportant prod_emb_def PiE_def by auto |
121 unfolding%unimportant prod_emb_def PiE_def by auto |
122 |
122 |
123 lemma%unimportant |
123 lemma |
124 shows prod_emb_empty[simp]: "prod_emb M L K {} = {}" |
124 shows prod_emb_empty[simp]: "prod_emb M L K {} = {}" |
125 and prod_emb_Un[simp]: "prod_emb M L K (A \<union> B) = prod_emb M L K A \<union> prod_emb M L K B" |
125 and prod_emb_Un[simp]: "prod_emb M L K (A \<union> B) = prod_emb M L K A \<union> prod_emb M L K B" |
126 and prod_emb_Int: "prod_emb M L K (A \<inter> B) = prod_emb M L K A \<inter> prod_emb M L K B" |
126 and prod_emb_Int: "prod_emb M L K (A \<inter> B) = prod_emb M L K A \<inter> prod_emb M L K B" |
127 and prod_emb_UN[simp]: "prod_emb M L K (\<Union>i\<in>I. F i) = (\<Union>i\<in>I. prod_emb M L K (F i))" |
127 and prod_emb_UN[simp]: "prod_emb M L K (\<Union>i\<in>I. F i) = (\<Union>i\<in>I. prod_emb M L K (F i))" |
128 and prod_emb_INT[simp]: "I \<noteq> {} \<Longrightarrow> prod_emb M L K (\<Inter>i\<in>I. F i) = (\<Inter>i\<in>I. prod_emb M L K (F i))" |
128 and prod_emb_INT[simp]: "I \<noteq> {} \<Longrightarrow> prod_emb M L K (\<Inter>i\<in>I. F i) = (\<Inter>i\<in>I. prod_emb M L K (F i))" |
129 and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B" |
129 and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B" |
130 by%unimportant (auto simp: prod_emb_def) |
130 by (auto simp: prod_emb_def) |
131 |
131 |
132 lemma%unimportant prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> |
132 lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> |
133 prod_emb I M J (\<Pi>\<^sub>E i\<in>J. E i) = (\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i))" |
133 prod_emb I M J (\<Pi>\<^sub>E i\<in>J. E i) = (\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i))" |
134 by (force simp: prod_emb_def PiE_iff if_split_mem2) |
134 by (force simp: prod_emb_def PiE_iff if_split_mem2) |
135 |
135 |
136 lemma%unimportant prod_emb_PiE_same_index[simp]: |
136 lemma prod_emb_PiE_same_index[simp]: |
137 "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E" |
137 "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E" |
138 by (auto simp: prod_emb_def PiE_iff) |
138 by (auto simp: prod_emb_def PiE_iff) |
139 |
139 |
140 lemma%unimportant prod_emb_trans[simp]: |
140 lemma prod_emb_trans[simp]: |
141 "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X" |
141 "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X" |
142 by (auto simp add: Int_absorb1 prod_emb_def PiE_def) |
142 by (auto simp add: Int_absorb1 prod_emb_def PiE_def) |
143 |
143 |
144 lemma%unimportant prod_emb_Pi: |
144 lemma prod_emb_Pi: |
145 assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K" |
145 assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K" |
146 shows "prod_emb K M J (Pi\<^sub>E J X) = (\<Pi>\<^sub>E i\<in>K. if i \<in> J then X i else space (M i))" |
146 shows "prod_emb K M J (Pi\<^sub>E J X) = (\<Pi>\<^sub>E i\<in>K. if i \<in> J then X i else space (M i))" |
147 using assms sets.space_closed |
147 using assms sets.space_closed |
148 by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+ |
148 by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+ |
149 |
149 |
150 lemma%unimportant prod_emb_id: |
150 lemma prod_emb_id: |
151 "B \<subseteq> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B" |
151 "B \<subseteq> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B" |
152 by (auto simp: prod_emb_def subset_eq extensional_restrict) |
152 by (auto simp: prod_emb_def subset_eq extensional_restrict) |
153 |
153 |
154 lemma%unimportant prod_emb_mono: |
154 lemma prod_emb_mono: |
155 "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G" |
155 "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G" |
156 by (auto simp: prod_emb_def) |
156 by (auto simp: prod_emb_def) |
157 |
157 |
158 definition%important PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where |
158 definition%important PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where |
159 "PiM I M = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i)) |
159 "PiM I M = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i)) |
230 by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff) |
230 by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff) |
231 from X I show "A \<in> ?L" unfolding A |
231 from X I show "A \<in> ?L" unfolding A |
232 by (auto simp: prod_algebra_def) |
232 by (auto simp: prod_algebra_def) |
233 qed |
233 qed |
234 |
234 |
235 lemma%unimportant prod_algebraI: |
235 lemma prod_algebraI: |
236 "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)) |
236 "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)) |
237 \<Longrightarrow> prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> prod_algebra I M" |
237 \<Longrightarrow> prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> prod_algebra I M" |
238 by (auto simp: prod_algebra_def) |
238 by (auto simp: prod_algebra_def) |
239 |
239 |
240 lemma%unimportant prod_algebraI_finite: |
240 lemma prod_algebraI_finite: |
241 "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>E I E) \<in> prod_algebra I M" |
241 "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>E I E) \<in> prod_algebra I M" |
242 using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp |
242 using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp |
243 |
243 |
244 lemma%unimportant Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}" |
244 lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}" |
245 proof (safe intro!: Int_stableI) |
245 proof (safe intro!: Int_stableI) |
246 fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)" |
246 fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)" |
247 then show "\<exists>G. Pi\<^sub>E J E \<inter> Pi\<^sub>E J F = Pi\<^sub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))" |
247 then show "\<exists>G. Pi\<^sub>E J E \<inter> Pi\<^sub>E J F = Pi\<^sub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))" |
248 by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int) |
248 by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int) |
249 qed |
249 qed |
250 |
250 |
251 lemma%unimportant prod_algebraE: |
251 lemma prod_algebraE: |
252 assumes A: "A \<in> prod_algebra I M" |
252 assumes A: "A \<in> prod_algebra I M" |
253 obtains J E where "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)" |
253 obtains J E where "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)" |
254 "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)" |
254 "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)" |
255 using A by (auto simp: prod_algebra_def) |
255 using A by (auto simp: prod_algebra_def) |
256 |
256 |
257 lemma%important prod_algebraE_all: |
257 lemma prod_algebraE_all: |
258 assumes A: "A \<in> prod_algebra I M" |
258 assumes A: "A \<in> prod_algebra I M" |
259 obtains E where "A = Pi\<^sub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))" |
259 obtains E where "A = Pi\<^sub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))" |
260 proof%unimportant - |
260 proof - |
261 from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)" |
261 from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)" |
262 and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))" |
262 and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))" |
263 by (auto simp: prod_algebra_def) |
263 by (auto simp: prod_algebra_def) |
264 from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)" |
264 from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)" |
265 using sets.sets_into_space by auto |
265 using sets.sets_into_space by auto |
339 also have "\<dots> \<in> prod_algebra I M" |
338 also have "\<dots> \<in> prod_algebra I M" |
340 using \<open>i \<in> I\<close> by (intro prod_algebraI) auto |
339 using \<open>i \<in> I\<close> by (intro prod_algebraI) auto |
341 finally show ?thesis . |
340 finally show ?thesis . |
342 qed |
341 qed |
343 |
342 |
344 lemma%unimportant space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" |
343 lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" |
345 using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp |
344 using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp |
346 |
345 |
347 lemma%unimportant prod_emb_subset_PiM[simp]: "prod_emb I M K X \<subseteq> space (PiM I M)" |
346 lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \<subseteq> space (PiM I M)" |
348 by (auto simp: prod_emb_def space_PiM) |
347 by (auto simp: prod_emb_def space_PiM) |
349 |
348 |
350 lemma%unimportant space_PiM_empty_iff[simp]: "space (PiM I M) = {} \<longleftrightarrow> (\<exists>i\<in>I. space (M i) = {})" |
349 lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \<longleftrightarrow> (\<exists>i\<in>I. space (M i) = {})" |
351 by (auto simp: space_PiM PiE_eq_empty_iff) |
350 by (auto simp: space_PiM PiE_eq_empty_iff) |
352 |
351 |
353 lemma%unimportant undefined_in_PiM_empty[simp]: "(\<lambda>x. undefined) \<in> space (PiM {} M)" |
352 lemma undefined_in_PiM_empty[simp]: "(\<lambda>x. undefined) \<in> space (PiM {} M)" |
354 by (auto simp: space_PiM) |
353 by (auto simp: space_PiM) |
355 |
354 |
356 lemma%unimportant sets_PiM: "sets (\<Pi>\<^sub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)" |
355 lemma sets_PiM: "sets (\<Pi>\<^sub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)" |
357 using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp |
356 using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp |
358 |
357 |
359 lemma%important sets_PiM_single: "sets (PiM I M) = |
358 proposition sets_PiM_single: "sets (PiM I M) = |
360 sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {{f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> sets (M i)}" |
359 sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {{f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> sets (M i)}" |
361 (is "_ = sigma_sets ?\<Omega> ?R") |
360 (is "_ = sigma_sets ?\<Omega> ?R") |
362 unfolding sets_PiM |
361 unfolding sets_PiM |
363 proof%unimportant (rule sigma_sets_eqI) |
362 proof (rule sigma_sets_eqI) |
364 interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto |
363 interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto |
365 fix A assume "A \<in> prod_algebra I M" |
364 fix A assume "A \<in> prod_algebra I M" |
366 from prod_algebraE[OF this] guess J X . note X = this |
365 from prod_algebraE[OF this] guess J X . note X = this |
367 show "A \<in> sigma_sets ?\<Omega> ?R" |
366 show "A \<in> sigma_sets ?\<Omega> ?R" |
368 proof cases |
367 proof cases |
493 qed |
492 qed |
494 qed |
493 qed |
495 finally show "?thesis" . |
494 finally show "?thesis" . |
496 qed |
495 qed |
497 |
496 |
498 lemma%unimportant sets_PiM_in_sets: |
497 lemma sets_PiM_in_sets: |
499 assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))" |
498 assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))" |
500 assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N" |
499 assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N" |
501 shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N" |
500 shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N" |
502 unfolding sets_PiM_single space[symmetric] |
501 unfolding sets_PiM_single space[symmetric] |
503 by (intro sets.sigma_sets_subset subsetI) (auto intro: sets) |
502 by (intro sets.sigma_sets_subset subsetI) (auto intro: sets) |
504 |
503 |
505 lemma%unimportant sets_PiM_cong[measurable_cong]: |
504 lemma sets_PiM_cong[measurable_cong]: |
506 assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" |
505 assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" |
507 using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) |
506 using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) |
508 |
507 |
509 lemma%important sets_PiM_I: |
508 lemma sets_PiM_I: |
510 assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)" |
509 assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)" |
511 shows "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)" |
510 shows "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)" |
512 proof%unimportant cases |
511 proof cases |
513 assume "J = {}" |
512 assume "J = {}" |
514 then have "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) = (\<Pi>\<^sub>E j\<in>I. space (M j))" |
513 then have "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) = (\<Pi>\<^sub>E j\<in>I. space (M j))" |
515 by (auto simp: prod_emb_def) |
514 by (auto simp: prod_emb_def) |
516 then show ?thesis |
515 then show ?thesis |
517 by (auto simp add: sets_PiM intro!: sigma_sets_top) |
516 by (auto simp add: sets_PiM intro!: sigma_sets_top) |
518 next |
517 next |
519 assume "J \<noteq> {}" with assms show ?thesis |
518 assume "J \<noteq> {}" with assms show ?thesis |
520 by (force simp add: sets_PiM prod_algebra_def) |
519 by (force simp add: sets_PiM prod_algebra_def) |
521 qed |
520 qed |
522 |
521 |
523 lemma%unimportant measurable_PiM: |
522 proposition measurable_PiM: |
524 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
523 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
525 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> |
524 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> |
526 f -` prod_emb I M J (Pi\<^sub>E J X) \<inter> space N \<in> sets N" |
525 f -` prod_emb I M J (Pi\<^sub>E J X) \<inter> space N \<in> sets N" |
527 shows "f \<in> measurable N (PiM I M)" |
526 shows "f \<in> measurable N (PiM I M)" |
528 using sets_PiM prod_algebra_sets_into_space space |
527 using sets_PiM prod_algebra_sets_into_space space |
530 fix A assume "A \<in> prod_algebra I M" |
529 fix A assume "A \<in> prod_algebra I M" |
531 from prod_algebraE[OF this] guess J X . |
530 from prod_algebraE[OF this] guess J X . |
532 with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto |
531 with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto |
533 qed |
532 qed |
534 |
533 |
535 lemma%important measurable_PiM_Collect: |
534 lemma measurable_PiM_Collect: |
536 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
535 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
537 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> |
536 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> |
538 {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N" |
537 {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N" |
539 shows "f \<in> measurable N (PiM I M)" |
538 shows "f \<in> measurable N (PiM I M)" |
540 using sets_PiM prod_algebra_sets_into_space space |
539 using sets_PiM prod_algebra_sets_into_space space |
541 proof%unimportant (rule measurable_sigma_sets) |
540 proof (rule measurable_sigma_sets) |
542 fix A assume "A \<in> prod_algebra I M" |
541 fix A assume "A \<in> prod_algebra I M" |
543 from prod_algebraE[OF this] guess J X . note X = this |
542 from prod_algebraE[OF this] guess J X . note X = this |
544 then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}" |
543 then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}" |
545 using space by (auto simp: prod_emb_def del: PiE_I) |
544 using space by (auto simp: prod_emb_def del: PiE_I) |
546 also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets) |
545 also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets) |
547 finally show "f -` A \<inter> space N \<in> sets N" . |
546 finally show "f -` A \<inter> space N \<in> sets N" . |
548 qed |
547 qed |
549 |
548 |
550 lemma%unimportant measurable_PiM_single: |
549 lemma measurable_PiM_single: |
551 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
550 assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
552 assumes sets: "\<And>A i. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {\<omega> \<in> space N. f \<omega> i \<in> A} \<in> sets N" |
551 assumes sets: "\<And>A i. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {\<omega> \<in> space N. f \<omega> i \<in> A} \<in> sets N" |
553 shows "f \<in> measurable N (PiM I M)" |
552 shows "f \<in> measurable N (PiM I M)" |
554 using sets_PiM_single |
553 using sets_PiM_single |
555 proof (rule measurable_sigma_sets) |
554 proof (rule measurable_sigma_sets) |
559 with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto |
558 with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto |
560 also have "\<dots> \<in> sets N" using B by (rule sets) |
559 also have "\<dots> \<in> sets N" using B by (rule sets) |
561 finally show "f -` A \<inter> space N \<in> sets N" . |
560 finally show "f -` A \<inter> space N \<in> sets N" . |
562 qed (auto simp: space) |
561 qed (auto simp: space) |
563 |
562 |
564 lemma%important measurable_PiM_single': |
563 lemma measurable_PiM_single': |
565 assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)" |
564 assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)" |
566 and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
565 and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
567 shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^sub>M I M)" |
566 shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^sub>M I M)" |
568 proof%unimportant (rule measurable_PiM_single) |
567 proof (rule measurable_PiM_single) |
569 fix A i assume A: "i \<in> I" "A \<in> sets (M i)" |
568 fix A i assume A: "i \<in> I" "A \<in> sets (M i)" |
570 then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N" |
569 then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N" |
571 by auto |
570 by auto |
572 then show "{\<omega> \<in> space N. f i \<omega> \<in> A} \<in> sets N" |
571 then show "{\<omega> \<in> space N. f i \<omega> \<in> A} \<in> sets N" |
573 using A f by (auto intro!: measurable_sets) |
572 using A f by (auto intro!: measurable_sets) |
574 qed fact |
573 qed fact |
575 |
574 |
576 lemma%unimportant sets_PiM_I_finite[measurable]: |
575 lemma sets_PiM_I_finite[measurable]: |
577 assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))" |
576 assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))" |
578 shows "(\<Pi>\<^sub>E j\<in>I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)" |
577 shows "(\<Pi>\<^sub>E j\<in>I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)" |
579 using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto |
578 using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto |
580 |
579 |
581 lemma%unimportant measurable_component_singleton[measurable (raw)]: |
580 lemma measurable_component_singleton[measurable (raw)]: |
582 assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)" |
581 assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)" |
583 proof (unfold measurable_def, intro CollectI conjI ballI) |
582 proof (unfold measurable_def, intro CollectI conjI ballI) |
584 fix A assume "A \<in> sets (M i)" |
583 fix A assume "A \<in> sets (M i)" |
585 then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) = prod_emb I M {i} (\<Pi>\<^sub>E j\<in>{i}. A)" |
584 then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) = prod_emb I M {i} (\<Pi>\<^sub>E j\<in>{i}. A)" |
586 using sets.sets_into_space \<open>i \<in> I\<close> |
585 using sets.sets_into_space \<open>i \<in> I\<close> |
587 by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm) |
586 by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm) |
588 then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)" |
587 then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)" |
589 using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I) |
588 using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I) |
590 qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM) |
589 qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM) |
591 |
590 |
592 lemma%unimportant measurable_component_singleton'[measurable_dest]: |
591 lemma measurable_component_singleton'[measurable_dest]: |
593 assumes f: "f \<in> measurable N (Pi\<^sub>M I M)" |
592 assumes f: "f \<in> measurable N (Pi\<^sub>M I M)" |
594 assumes g: "g \<in> measurable L N" |
593 assumes g: "g \<in> measurable L N" |
595 assumes i: "i \<in> I" |
594 assumes i: "i \<in> I" |
596 shows "(\<lambda>x. (f (g x)) i) \<in> measurable L (M i)" |
595 shows "(\<lambda>x. (f (g x)) i) \<in> measurable L (M i)" |
597 using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] . |
596 using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] . |
598 |
597 |
599 lemma%unimportant measurable_PiM_component_rev: |
598 lemma measurable_PiM_component_rev: |
600 "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N" |
599 "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N" |
601 by simp |
600 by simp |
602 |
601 |
603 lemma%unimportant measurable_case_nat[measurable (raw)]: |
602 lemma measurable_case_nat[measurable (raw)]: |
604 assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N" |
603 assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N" |
605 "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N" |
604 "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N" |
606 shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N" |
605 shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N" |
607 by (cases i) simp_all |
606 by (cases i) simp_all |
608 |
607 |
609 lemma%unimportant measurable_case_nat'[measurable (raw)]: |
608 lemma measurable_case_nat'[measurable (raw)]: |
610 assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)" |
609 assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)" |
611 shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)" |
610 shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)" |
612 using fg[THEN measurable_space] |
611 using fg[THEN measurable_space] |
613 by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split) |
612 by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split) |
614 |
613 |
615 lemma%unimportant measurable_add_dim[measurable]: |
614 lemma measurable_add_dim[measurable]: |
616 "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M)" |
615 "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M)" |
617 (is "?f \<in> measurable ?P ?I") |
616 (is "?f \<in> measurable ?P ?I") |
618 proof (rule measurable_PiM_single) |
617 proof (rule measurable_PiM_single) |
619 fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)" |
618 fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)" |
620 have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} = |
619 have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} = |
624 using A j |
623 using A j |
625 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
624 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
626 finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" . |
625 finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" . |
627 qed (auto simp: space_pair_measure space_PiM PiE_def) |
626 qed (auto simp: space_pair_measure space_PiM PiE_def) |
628 |
627 |
629 lemma%important measurable_fun_upd: |
628 proposition measurable_fun_upd: |
630 assumes I: "I = J \<union> {i}" |
629 assumes I: "I = J \<union> {i}" |
631 assumes f[measurable]: "f \<in> measurable N (PiM J M)" |
630 assumes f[measurable]: "f \<in> measurable N (PiM J M)" |
632 assumes h[measurable]: "h \<in> measurable N (M i)" |
631 assumes h[measurable]: "h \<in> measurable N (M i)" |
633 shows "(\<lambda>x. (f x) (i := h x)) \<in> measurable N (PiM I M)" |
632 shows "(\<lambda>x. (f x) (i := h x)) \<in> measurable N (PiM I M)" |
634 proof%unimportant (intro measurable_PiM_single') |
633 proof (intro measurable_PiM_single') |
635 fix j assume "j \<in> I" then show "(\<lambda>\<omega>. ((f \<omega>)(i := h \<omega>)) j) \<in> measurable N (M j)" |
634 fix j assume "j \<in> I" then show "(\<lambda>\<omega>. ((f \<omega>)(i := h \<omega>)) j) \<in> measurable N (M j)" |
636 unfolding I by (cases "j = i") auto |
635 unfolding I by (cases "j = i") auto |
637 next |
636 next |
638 show "(\<lambda>x. (f x)(i := h x)) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
637 show "(\<lambda>x. (f x)(i := h x)) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))" |
639 using I f[THEN measurable_space] h[THEN measurable_space] |
638 using I f[THEN measurable_space] h[THEN measurable_space] |
640 by (auto simp: space_PiM PiE_iff extensional_def) |
639 by (auto simp: space_PiM PiE_iff extensional_def) |
641 qed |
640 qed |
642 |
641 |
643 lemma%unimportant measurable_component_update: |
642 lemma measurable_component_update: |
644 "x \<in> space (Pi\<^sub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^sub>M (insert i I) M)" |
643 "x \<in> space (Pi\<^sub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^sub>M (insert i I) M)" |
645 by simp |
644 by simp |
646 |
645 |
647 lemma%important measurable_merge[measurable]: |
646 lemma measurable_merge[measurable]: |
648 "merge I J \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M)" |
647 "merge I J \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M)" |
649 (is "?f \<in> measurable ?P ?U") |
648 (is "?f \<in> measurable ?P ?U") |
650 proof%unimportant (rule measurable_PiM_single) |
649 proof (rule measurable_PiM_single) |
651 fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J" |
650 fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J" |
652 then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} = |
651 then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} = |
653 (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)" |
652 (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)" |
654 by (auto simp: merge_def) |
653 by (auto simp: merge_def) |
655 also have "\<dots> \<in> sets ?P" |
654 also have "\<dots> \<in> sets ?P" |
656 using A |
655 using A |
657 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
656 by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton]) |
658 finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" . |
657 finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" . |
659 qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def) |
658 qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def) |
660 |
659 |
661 lemma%unimportant measurable_restrict[measurable (raw)]: |
660 lemma measurable_restrict[measurable (raw)]: |
662 assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)" |
661 assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)" |
663 shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^sub>M I M)" |
662 shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^sub>M I M)" |
664 proof (rule measurable_PiM_single) |
663 proof (rule measurable_PiM_single) |
665 fix A i assume A: "i \<in> I" "A \<in> sets (M i)" |
664 fix A i assume A: "i \<in> I" "A \<in> sets (M i)" |
666 then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N" |
665 then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N" |
667 by auto |
666 by auto |
668 then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N" |
667 then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N" |
669 using A X by (auto intro!: measurable_sets) |
668 using A X by (auto intro!: measurable_sets) |
670 qed (insert X, auto simp add: PiE_def dest: measurable_space) |
669 qed (insert X, auto simp add: PiE_def dest: measurable_space) |
671 |
670 |
672 lemma%unimportant measurable_abs_UNIV: |
671 lemma measurable_abs_UNIV: |
673 "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)" |
672 "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)" |
674 by (intro measurable_PiM_single) (auto dest: measurable_space) |
673 by (intro measurable_PiM_single) (auto dest: measurable_space) |
675 |
674 |
676 lemma%unimportant measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" |
675 lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" |
677 by (intro measurable_restrict measurable_component_singleton) auto |
676 by (intro measurable_restrict measurable_component_singleton) auto |
678 |
677 |
679 lemma%unimportant measurable_restrict_subset': |
678 lemma measurable_restrict_subset': |
680 assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)" |
679 assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)" |
681 shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)" |
680 shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)" |
682 proof- |
681 proof- |
683 from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" |
682 from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" |
684 by (rule measurable_restrict_subset) |
683 by (rule measurable_restrict_subset) |
685 also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)" |
684 also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)" |
686 by (intro sets_PiM_cong measurable_cong_sets) simp_all |
685 by (intro sets_PiM_cong measurable_cong_sets) simp_all |
687 finally show ?thesis . |
686 finally show ?thesis . |
688 qed |
687 qed |
689 |
688 |
690 lemma%unimportant measurable_prod_emb[intro, simp]: |
689 lemma measurable_prod_emb[intro, simp]: |
691 "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)" |
690 "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)" |
692 unfolding prod_emb_def space_PiM[symmetric] |
691 unfolding prod_emb_def space_PiM[symmetric] |
693 by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton) |
692 by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton) |
694 |
693 |
695 lemma%unimportant merge_in_prod_emb: |
694 lemma merge_in_prod_emb: |
696 assumes "y \<in> space (PiM I M)" "x \<in> X" and X: "X \<in> sets (Pi\<^sub>M J M)" and "J \<subseteq> I" |
695 assumes "y \<in> space (PiM I M)" "x \<in> X" and X: "X \<in> sets (Pi\<^sub>M J M)" and "J \<subseteq> I" |
697 shows "merge J I (x, y) \<in> prod_emb I M J X" |
696 shows "merge J I (x, y) \<in> prod_emb I M J X" |
698 using assms sets.sets_into_space[OF X] |
697 using assms sets.sets_into_space[OF X] |
699 by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff |
698 by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff |
700 cong: if_cong restrict_cong) |
699 cong: if_cong restrict_cong) |
701 (simp add: extensional_def) |
700 (simp add: extensional_def) |
702 |
701 |
703 lemma%unimportant prod_emb_eq_emptyD: |
702 lemma prod_emb_eq_emptyD: |
704 assumes J: "J \<subseteq> I" and ne: "space (PiM I M) \<noteq> {}" and X: "X \<in> sets (Pi\<^sub>M J M)" |
703 assumes J: "J \<subseteq> I" and ne: "space (PiM I M) \<noteq> {}" and X: "X \<in> sets (Pi\<^sub>M J M)" |
705 and *: "prod_emb I M J X = {}" |
704 and *: "prod_emb I M J X = {}" |
706 shows "X = {}" |
705 shows "X = {}" |
707 proof safe |
706 proof safe |
708 fix x assume "x \<in> X" |
707 fix x assume "x \<in> X" |
709 obtain \<omega> where "\<omega> \<in> space (PiM I M)" |
708 obtain \<omega> where "\<omega> \<in> space (PiM I M)" |
710 using ne by blast |
709 using ne by blast |
711 from merge_in_prod_emb[OF this \<open>x\<in>X\<close> X J] * show "x \<in> {}" by auto |
710 from merge_in_prod_emb[OF this \<open>x\<in>X\<close> X J] * show "x \<in> {}" by auto |
712 qed |
711 qed |
713 |
712 |
714 lemma%unimportant sets_in_Pi_aux: |
713 lemma sets_in_Pi_aux: |
715 "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow> |
714 "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow> |
716 {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)" |
715 {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)" |
717 by (simp add: subset_eq Pi_iff) |
716 by (simp add: subset_eq Pi_iff) |
718 |
717 |
719 lemma%unimportant sets_in_Pi[measurable (raw)]: |
718 lemma sets_in_Pi[measurable (raw)]: |
720 "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow> |
719 "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow> |
721 (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow> |
720 (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow> |
722 Measurable.pred N (\<lambda>x. f x \<in> Pi I F)" |
721 Measurable.pred N (\<lambda>x. f x \<in> Pi I F)" |
723 unfolding pred_def |
722 unfolding pred_def |
724 by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto |
723 by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto |
725 |
724 |
726 lemma%unimportant sets_in_extensional_aux: |
725 lemma sets_in_extensional_aux: |
727 "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)" |
726 "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)" |
728 proof - |
727 proof - |
729 have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)" |
728 have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)" |
730 by (auto simp add: extensional_def space_PiM) |
729 by (auto simp add: extensional_def space_PiM) |
731 then show ?thesis by simp |
730 then show ?thesis by simp |
732 qed |
731 qed |
733 |
732 |
734 lemma%unimportant sets_in_extensional[measurable (raw)]: |
733 lemma sets_in_extensional[measurable (raw)]: |
735 "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)" |
734 "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)" |
736 unfolding pred_def |
735 unfolding pred_def |
737 by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto |
736 by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto |
738 |
737 |
739 lemma%unimportant sets_PiM_I_countable: |
738 lemma sets_PiM_I_countable: |
740 assumes I: "countable I" and E: "\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i)" shows "Pi\<^sub>E I E \<in> sets (Pi\<^sub>M I M)" |
739 assumes I: "countable I" and E: "\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i)" shows "Pi\<^sub>E I E \<in> sets (Pi\<^sub>M I M)" |
741 proof cases |
740 proof cases |
742 assume "I \<noteq> {}" |
741 assume "I \<noteq> {}" |
743 then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))" |
742 then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))" |
744 using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff) |
743 using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff) |
745 also have "\<dots> \<in> sets (PiM I M)" |
744 also have "\<dots> \<in> sets (PiM I M)" |
746 using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E) |
745 using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E) |
747 finally show ?thesis . |
746 finally show ?thesis . |
748 qed (simp add: sets_PiM_empty) |
747 qed (simp add: sets_PiM_empty) |
749 |
748 |
750 lemma%important sets_PiM_D_countable: |
749 lemma sets_PiM_D_countable: |
751 assumes A: "A \<in> PiM I M" |
750 assumes A: "A \<in> PiM I M" |
752 shows "\<exists>J\<subseteq>I. \<exists>X\<in>PiM J M. countable J \<and> A = prod_emb I M J X" |
751 shows "\<exists>J\<subseteq>I. \<exists>X\<in>PiM J M. countable J \<and> A = prod_emb I M J X" |
753 using A[unfolded sets_PiM_single] |
752 using A[unfolded sets_PiM_single] |
754 proof%unimportant induction |
753 proof induction |
755 case (Basic A) |
754 case (Basic A) |
756 then obtain i X where *: "i \<in> I" "X \<in> sets (M i)" and "A = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> X}" |
755 then obtain i X where *: "i \<in> I" "X \<in> sets (M i)" and "A = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> X}" |
757 by auto |
756 by auto |
758 then have A: "A = prod_emb I M {i} (\<Pi>\<^sub>E _\<in>{i}. X)" |
757 then have A: "A = prod_emb I M {i} (\<Pi>\<^sub>E _\<in>{i}. X)" |
759 by (auto simp: prod_emb_def) |
758 by (auto simp: prod_emb_def) |
781 with J show "\<Union>(K ` UNIV) = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))" |
780 with J show "\<Union>(K ` UNIV) = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))" |
782 by (simp add: K[abs_def] SUP_upper) |
781 by (simp add: K[abs_def] SUP_upper) |
783 qed(auto intro: X) |
782 qed(auto intro: X) |
784 qed |
783 qed |
785 |
784 |
786 lemma%important measure_eqI_PiM_finite: |
785 proposition measure_eqI_PiM_finite: |
787 assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M" |
786 assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M" |
788 assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)" |
787 assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)" |
789 assumes A: "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = space (PiM I M)" "\<And>i::nat. P (A i) \<noteq> \<infinity>" |
788 assumes A: "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = space (PiM I M)" "\<And>i::nat. P (A i) \<noteq> \<infinity>" |
790 shows "P = Q" |
789 shows "P = Q" |
791 proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) |
790 proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) |
792 show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>" |
791 show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>" |
793 unfolding space_PiM[symmetric] by fact+ |
792 unfolding space_PiM[symmetric] by fact+ |
794 fix X assume "X \<in> prod_algebra I M" |
793 fix X assume "X \<in> prod_algebra I M" |
795 then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)" |
794 then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)" |
796 and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)" |
795 and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)" |
797 by (force elim!: prod_algebraE) |
796 by (force elim!: prod_algebraE) |
798 then show "emeasure P X = emeasure Q X" |
797 then show "emeasure P X = emeasure Q X" |
799 unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq) |
798 unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq) |
800 qed (simp_all add: sets_PiM) |
799 qed (simp_all add: sets_PiM) |
801 |
800 |
802 lemma%important measure_eqI_PiM_infinite: |
801 proposition measure_eqI_PiM_infinite: |
803 assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M" |
802 assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M" |
804 assumes eq: "\<And>A J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> |
803 assumes eq: "\<And>A J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> |
805 P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))" |
804 P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))" |
806 assumes A: "finite_measure P" |
805 assumes A: "finite_measure P" |
807 shows "P = Q" |
806 shows "P = Q" |
808 proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) |
807 proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) |
809 interpret finite_measure P by fact |
808 interpret finite_measure P by fact |
810 define i where "i = (SOME i. i \<in> I)" |
809 define i where "i = (SOME i. i \<in> I)" |
811 have i: "I \<noteq> {} \<Longrightarrow> i \<in> I" |
810 have i: "I \<noteq> {} \<Longrightarrow> i \<in> I" |
812 unfolding i_def by (rule someI_ex) auto |
811 unfolding i_def by (rule someI_ex) auto |
813 define A where "A n = |
812 define A where "A n = |