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