|
1 (* Title: HOL/Analysis/Embed_Measure.thy |
|
2 Author: Manuel Eberl, TU München |
|
3 |
|
4 Defines measure embeddings with injective functions, i.e. lifting a measure on some values |
|
5 to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a |
|
6 measure on the left part of the sum type 'a + 'b) |
|
7 *) |
|
8 |
|
9 section \<open>Embed Measure Spaces with a Function\<close> |
|
10 |
|
11 theory Embed_Measure |
|
12 imports Binary_Product_Measure |
|
13 begin |
|
14 |
|
15 definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where |
|
16 "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M} |
|
17 (\<lambda>A. emeasure M (f -` A \<inter> space M))" |
|
18 |
|
19 lemma space_embed_measure: "space (embed_measure M f) = f ` space M" |
|
20 unfolding embed_measure_def |
|
21 by (subst space_measure_of) (auto dest: sets.sets_into_space) |
|
22 |
|
23 lemma sets_embed_measure': |
|
24 assumes inj: "inj_on f (space M)" |
|
25 shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}" |
|
26 unfolding embed_measure_def |
|
27 proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI) |
|
28 fix s assume "s \<in> {f ` A |A. A \<in> sets M}" |
|
29 then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto |
|
30 hence "f ` space M - s = f ` (space M - s')" using inj |
|
31 by (auto dest: inj_onD sets.sets_into_space) |
|
32 also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto |
|
33 finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" . |
|
34 next |
|
35 fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}" |
|
36 then obtain A' where A': "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M" |
|
37 by (auto simp: subset_eq choice_iff) |
|
38 then have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast |
|
39 with A' show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" |
|
40 by simp blast |
|
41 qed (auto dest: sets.sets_into_space) |
|
42 |
|
43 lemma the_inv_into_vimage: |
|
44 "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A" |
|
45 by (auto simp: the_inv_into_f_f) |
|
46 |
|
47 lemma sets_embed_eq_vimage_algebra: |
|
48 assumes "inj_on f (space M)" |
|
49 shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)" |
|
50 by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image |
|
51 dest: sets.sets_into_space |
|
52 intro!: image_cong the_inv_into_vimage[symmetric]) |
|
53 |
|
54 lemma sets_embed_measure: |
|
55 assumes inj: "inj f" |
|
56 shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}" |
|
57 using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD) |
|
58 |
|
59 lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)" |
|
60 unfolding embed_measure_def |
|
61 by (intro in_measure_of) (auto dest: sets.sets_into_space) |
|
62 |
|
63 lemma measurable_embed_measure1: |
|
64 assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N" |
|
65 shows "g \<in> measurable (embed_measure M f) N" |
|
66 unfolding measurable_def |
|
67 proof safe |
|
68 fix A assume "A \<in> sets N" |
|
69 with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M" |
|
70 by (rule measurable_sets) |
|
71 then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)" |
|
72 by (rule in_sets_embed_measure) |
|
73 also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)" |
|
74 by (auto simp: space_embed_measure) |
|
75 finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" . |
|
76 qed (insert measurable_space[OF assms], auto simp: space_embed_measure) |
|
77 |
|
78 lemma measurable_embed_measure2': |
|
79 assumes "inj_on f (space M)" |
|
80 shows "f \<in> measurable M (embed_measure M f)" |
|
81 proof- |
|
82 { |
|
83 fix A assume A: "A \<in> sets M" |
|
84 also from A have "A = A \<inter> space M" by auto |
|
85 also have "... = f -` f ` A \<inter> space M" using A assms |
|
86 by (auto dest: inj_onD sets.sets_into_space) |
|
87 finally have "f -` f ` A \<inter> space M \<in> sets M" . |
|
88 } |
|
89 thus ?thesis using assms unfolding embed_measure_def |
|
90 by (intro measurable_measure_of) (auto dest: sets.sets_into_space) |
|
91 qed |
|
92 |
|
93 lemma measurable_embed_measure2: |
|
94 assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)" |
|
95 by (auto simp: inj_vimage_image_eq embed_measure_def |
|
96 intro!: measurable_measure_of dest: sets.sets_into_space) |
|
97 |
|
98 lemma embed_measure_eq_distr': |
|
99 assumes "inj_on f (space M)" |
|
100 shows "embed_measure M f = distr M (embed_measure M f) f" |
|
101 proof- |
|
102 have "distr M (embed_measure M f) f = |
|
103 measure_of (f ` space M) {f ` A |A. A \<in> sets M} |
|
104 (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def |
|
105 by (simp add: space_embed_measure sets_embed_measure'[OF assms]) |
|
106 also have "... = embed_measure M f" unfolding embed_measure_def .. |
|
107 finally show ?thesis .. |
|
108 qed |
|
109 |
|
110 lemma embed_measure_eq_distr: |
|
111 "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f" |
|
112 by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD) |
|
113 |
|
114 lemma nn_integral_embed_measure': |
|
115 "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow> |
|
116 nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))" |
|
117 apply (subst embed_measure_eq_distr', simp) |
|
118 apply (subst nn_integral_distr) |
|
119 apply (simp_all add: measurable_embed_measure2') |
|
120 done |
|
121 |
|
122 lemma nn_integral_embed_measure: |
|
123 "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow> |
|
124 nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))" |
|
125 by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp |
|
126 |
|
127 lemma emeasure_embed_measure': |
|
128 assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)" |
|
129 shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)" |
|
130 by (subst embed_measure_eq_distr'[OF assms(1)]) |
|
131 (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)]) |
|
132 |
|
133 lemma emeasure_embed_measure: |
|
134 assumes "inj f" "A \<in> sets (embed_measure M f)" |
|
135 shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)" |
|
136 using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD) |
|
137 |
|
138 lemma embed_measure_comp: |
|
139 assumes [simp]: "inj f" "inj g" |
|
140 shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)" |
|
141 proof- |
|
142 have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp) |
|
143 note measurable_embed_measure2[measurable] |
|
144 have "embed_measure (embed_measure M f) g = |
|
145 distr M (embed_measure (embed_measure M f) g) (g \<circ> f)" |
|
146 by (subst (1 2) embed_measure_eq_distr) |
|
147 (simp_all add: distr_distr sets_embed_measure cong: distr_cong) |
|
148 also have "... = embed_measure M (g \<circ> f)" |
|
149 by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong) |
|
150 (auto simp: sets_embed_measure o_def image_image[symmetric] |
|
151 intro: inj_comp cong: distr_cong) |
|
152 finally show ?thesis . |
|
153 qed |
|
154 |
|
155 lemma sigma_finite_embed_measure: |
|
156 assumes "sigma_finite_measure M" and inj: "inj f" |
|
157 shows "sigma_finite_measure (embed_measure M f)" |
|
158 proof - |
|
159 from assms(1) interpret sigma_finite_measure M . |
|
160 from sigma_finite_countable obtain A where |
|
161 A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast |
|
162 from A_props have "countable (op ` f`A)" by auto |
|
163 moreover |
|
164 from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)" |
|
165 by (auto simp: sets_embed_measure) |
|
166 moreover |
|
167 from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)" |
|
168 by (auto simp: space_embed_measure intro!: imageI) |
|
169 moreover |
|
170 from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>" |
|
171 by (intro ballI, subst emeasure_embed_measure) |
|
172 (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure) |
|
173 ultimately show ?thesis by - (standard, blast) |
|
174 qed |
|
175 |
|
176 lemma embed_measure_count_space': |
|
177 "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)" |
|
178 apply (subst distr_bij_count_space[of f A "f`A", symmetric]) |
|
179 apply (simp add: inj_on_def bij_betw_def) |
|
180 apply (subst embed_measure_eq_distr') |
|
181 apply simp |
|
182 apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff) |
|
183 apply (subst (1 2) emeasure_distr) |
|
184 apply (auto simp: space_embed_measure sets_embed_measure') |
|
185 done |
|
186 |
|
187 lemma embed_measure_count_space: |
|
188 "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)" |
|
189 by(rule embed_measure_count_space')(erule subset_inj_on, simp) |
|
190 |
|
191 lemma sets_embed_measure_alt: |
|
192 "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M" |
|
193 by (auto simp: sets_embed_measure) |
|
194 |
|
195 lemma emeasure_embed_measure_image': |
|
196 assumes "inj_on f (space M)" "X \<in> sets M" |
|
197 shows "emeasure (embed_measure M f) (f`X) = emeasure M X" |
|
198 proof- |
|
199 from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)" |
|
200 by (subst emeasure_embed_measure') (auto simp: sets_embed_measure') |
|
201 also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space) |
|
202 finally show ?thesis . |
|
203 qed |
|
204 |
|
205 lemma emeasure_embed_measure_image: |
|
206 "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X" |
|
207 by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq) |
|
208 |
|
209 lemma embed_measure_eq_iff: |
|
210 assumes "inj f" |
|
211 shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _") |
|
212 proof |
|
213 from assms have I: "inj (op` f)" by (auto intro: injI dest: injD) |
|
214 assume asm: "?M = ?N" |
|
215 hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp |
|
216 with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt) |
|
217 moreover { |
|
218 fix X assume "X \<in> sets A" |
|
219 from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp |
|
220 with \<open>X \<in> sets A\<close> and \<open>sets A = sets B\<close> and assms |
|
221 have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image) |
|
222 } |
|
223 ultimately show "A = B" by (rule measure_eqI) |
|
224 qed simp |
|
225 |
|
226 lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A" |
|
227 by (auto simp: the_inv_into_f_f) |
|
228 |
|
229 lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)" |
|
230 using map_prod_surj_on[OF refl refl] . |
|
231 |
|
232 lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)" |
|
233 by auto |
|
234 |
|
235 lemma embed_measure_prod: |
|
236 assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N" |
|
237 shows "embed_measure M f \<Otimes>\<^sub>M embed_measure N g = embed_measure (M \<Otimes>\<^sub>M N) (\<lambda>(x, y). (f x, g y))" |
|
238 (is "?L = _") |
|
239 unfolding map_prod_def[symmetric] |
|
240 proof (rule pair_measure_eqI) |
|
241 have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A" |
|
242 using f g by (auto simp: inj_on_def) |
|
243 |
|
244 note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del] |
|
245 ccSUP_insert[simp del] |
|
246 show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))" |
|
247 unfolding map_prod_def[symmetric] |
|
248 apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra |
|
249 cong: vimage_algebra_cong) |
|
250 apply (subst sets_vimage_Sup_eq[where Y="space (M \<Otimes>\<^sub>M N)"]) |
|
251 apply (simp_all add: space_pair_measure[symmetric]) |
|
252 apply (auto simp add: the_inv_into_f_f |
|
253 simp del: map_prod_simp |
|
254 del: prod_fun_imageE) [] |
|
255 apply auto [] |
|
256 apply (subst image_insert) |
|
257 apply simp |
|
258 apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq) |
|
259 apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure) |
|
260 apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq |
|
261 space_pair_measure[symmetric] map_prod_image[symmetric]) |
|
262 apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong) |
|
263 apply (auto simp: map_prod_image the_inv_into_f_f |
|
264 simp del: map_prod_simp del: prod_fun_imageE) |
|
265 apply (simp_all add: the_inv_into_f_f space_pair_measure) |
|
266 done |
|
267 |
|
268 note measurable_embed_measure2[measurable] |
|
269 fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)" |
|
270 moreover have "f -` A \<times> g -` B \<inter> space (M \<Otimes>\<^sub>M N) = (f -` A \<inter> space M) \<times> (g -` B \<inter> space N)" |
|
271 by (auto simp: space_pair_measure) |
|
272 ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B = |
|
273 emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)" |
|
274 by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure |
|
275 sigma_finite_measure.emeasure_pair_measure_Times) |
|
276 qed (insert assms, simp_all add: sigma_finite_embed_measure) |
|
277 |
|
278 lemma mono_embed_measure: |
|
279 "space M = space M' \<Longrightarrow> sets M \<subseteq> sets M' \<Longrightarrow> sets (embed_measure M f) \<subseteq> sets (embed_measure M' f)" |
|
280 unfolding embed_measure_def |
|
281 apply (subst (1 2) sets_measure_of) |
|
282 apply (blast dest: sets.sets_into_space) |
|
283 apply (blast dest: sets.sets_into_space) |
|
284 apply simp |
|
285 apply (intro sigma_sets_mono') |
|
286 apply safe |
|
287 apply (simp add: subset_eq) |
|
288 apply metis |
|
289 done |
|
290 |
|
291 lemma density_embed_measure: |
|
292 assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)" |
|
293 shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2") |
|
294 proof (rule measure_eqI) |
|
295 fix X assume X: "X \<in> sets ?M1" |
|
296 from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)" |
|
297 by (rule measurable_embed_measure2) |
|
298 from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f" |
|
299 by (subst emeasure_density) simp_all |
|
300 also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M" |
|
301 by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr) auto |
|
302 also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M" |
|
303 by (intro nn_integral_cong) (auto split: split_indicator) |
|
304 also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)" |
|
305 by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf]) |
|
306 also from X and inj have "... = emeasure ?M2 X" |
|
307 by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure) |
|
308 finally show "emeasure ?M1 X = emeasure ?M2 X" . |
|
309 qed (simp_all add: sets_embed_measure inj) |
|
310 |
|
311 lemma density_embed_measure': |
|
312 assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M" |
|
313 shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f" |
|
314 proof- |
|
315 have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f" |
|
316 by (rule density_embed_measure[OF inj]) |
|
317 (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong, |
|
318 rule inv, rule measurable_ident_sets, simp, rule Mg) |
|
319 also have "density M (g \<circ> f' \<circ> f) = density M g" |
|
320 by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv) |
|
321 finally show ?thesis . |
|
322 qed |
|
323 |
|
324 lemma inj_on_image_subset_iff: |
|
325 assumes "inj_on f C" "A \<subseteq> C" "B \<subseteq> C" |
|
326 shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B" |
|
327 proof (intro iffI subsetI) |
|
328 fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A" |
|
329 from B have "f x \<in> f ` A" by blast |
|
330 with A have "f x \<in> f ` B" by blast |
|
331 then obtain y where "f x = f y" and "y \<in> B" by blast |
|
332 with assms and B have "x = y" by (auto dest: inj_onD) |
|
333 with \<open>y \<in> B\<close> show "x \<in> B" by simp |
|
334 qed auto |
|
335 |
|
336 |
|
337 lemma AE_embed_measure': |
|
338 assumes inj: "inj_on f (space M)" |
|
339 shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))" |
|
340 proof |
|
341 let ?M = "embed_measure M f" |
|
342 assume "AE x in ?M. P x" |
|
343 then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A" |
|
344 by (force elim: AE_E) |
|
345 then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj) |
|
346 moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}" |
|
347 by (auto simp: inj space_embed_measure) |
|
348 from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'" |
|
349 by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj]) |
|
350 (insert A'_props, auto dest: sets.sets_into_space) |
|
351 moreover from A_props A'_props have "emeasure M A' = 0" |
|
352 by (simp add: emeasure_embed_measure_image' inj) |
|
353 ultimately show "AE x in M. P (f x)" by (intro AE_I) |
|
354 next |
|
355 let ?M = "embed_measure M f" |
|
356 assume "AE x in M. P (f x)" |
|
357 then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A" |
|
358 by (force elim: AE_E) |
|
359 hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A" |
|
360 by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj) |
|
361 thus "AE x in ?M. P x" by (intro AE_I) |
|
362 qed |
|
363 |
|
364 lemma AE_embed_measure: |
|
365 assumes inj: "inj f" |
|
366 shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))" |
|
367 using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD) |
|
368 |
|
369 lemma nn_integral_monotone_convergence_SUP_countable: |
|
370 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal" |
|
371 assumes nonempty: "Y \<noteq> {}" |
|
372 and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)" |
|
373 and countable: "countable B" |
|
374 shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))" |
|
375 (is "?lhs = ?rhs") |
|
376 proof - |
|
377 let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)" |
|
378 have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B" |
|
379 by(rule nn_integral_cong)(simp add: countable) |
|
380 also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)" |
|
381 by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) |
|
382 also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV" |
|
383 by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty) |
|
384 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)" |
|
385 proof(rule nn_integral_monotone_convergence_SUP_nat) |
|
386 show "Complete_Partial_Order.chain op \<le> (?f ` Y)" |
|
387 by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD) |
|
388 qed fact |
|
389 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))" |
|
390 by(simp add: nn_integral_count_space_indicator) |
|
391 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)" |
|
392 by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1) |
|
393 also have "\<dots> = ?rhs" |
|
394 by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable) |
|
395 finally show ?thesis . |
|
396 qed |
|
397 |
|
398 end |