|
1 (* Title: HOL/Analysis/Regularity.thy |
|
2 Author: Fabian Immler, TU München |
|
3 *) |
|
4 |
|
5 section \<open>Regularity of Measures\<close> |
|
6 |
|
7 theory Regularity |
|
8 imports Measure_Space Borel_Space |
|
9 begin |
|
10 |
|
11 lemma |
|
12 fixes M::"'a::{second_countable_topology, complete_space} measure" |
|
13 assumes sb: "sets M = sets borel" |
|
14 assumes "emeasure M (space M) \<noteq> \<infinity>" |
|
15 assumes "B \<in> sets borel" |
|
16 shows inner_regular: "emeasure M B = |
|
17 (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B") |
|
18 and outer_regular: "emeasure M B = |
|
19 (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B") |
|
20 proof - |
|
21 have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel) |
|
22 hence sU: "space M = UNIV" by simp |
|
23 interpret finite_measure M by rule fact |
|
24 have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow> |
|
25 (\<And>e. e > 0 \<Longrightarrow> \<exists>K. K \<subseteq> A \<and> compact K \<and> emeasure M A \<le> emeasure M K + ennreal e) \<Longrightarrow> ?inner A" |
|
26 by (rule ennreal_approx_SUP) |
|
27 (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+ |
|
28 have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow> |
|
29 (\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ennreal e) \<Longrightarrow> ?outer A" |
|
30 by (rule ennreal_approx_INF) |
|
31 (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+ |
|
32 from countable_dense_setE guess X::"'a set" . note X = this |
|
33 { |
|
34 fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto |
|
35 with X(2)[OF this] |
|
36 have x: "space M = (\<Union>x\<in>X. cball x r)" |
|
37 by (auto simp add: sU) (metis dist_commute order_less_imp_le) |
|
38 let ?U = "\<Union>k. (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)" |
|
39 have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M ?U" |
|
40 by (rule Lim_emeasure_incseq) (auto intro!: borel_closed bexI simp: incseq_def Us sb) |
|
41 also have "?U = space M" |
|
42 proof safe |
|
43 fix x from X(2)[OF open_ball[of x r]] \<open>r > 0\<close> obtain d where d: "d\<in>X" "d \<in> ball x r" by auto |
|
44 show "x \<in> ?U" |
|
45 using X(1) d |
|
46 by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def) |
|
47 qed (simp add: sU) |
|
48 finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M (space M)" . |
|
49 } note M_space = this |
|
50 { |
|
51 fix e ::real and n :: nat assume "e > 0" "n > 0" |
|
52 hence "1/n > 0" "e * 2 powr - n > 0" by (auto) |
|
53 from M_space[OF \<open>1/n>0\<close>] |
|
54 have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) \<longlonglongrightarrow> measure M (space M)" |
|
55 unfolding emeasure_eq_measure by (auto simp: measure_nonneg) |
|
56 from metric_LIMSEQ_D[OF this \<open>0 < e * 2 powr -n\<close>] |
|
57 obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) < |
|
58 e * 2 powr -n" |
|
59 by auto |
|
60 hence "measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge> |
|
61 measure M (space M) - e * 2 powr -real n" |
|
62 by (auto simp: dist_real_def) |
|
63 hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge> |
|
64 measure M (space M) - e * 2 powr - real n" .. |
|
65 } note k=this |
|
66 hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k. |
|
67 measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n" |
|
68 by blast |
|
69 then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat) |
|
70 \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))" |
|
71 by metis |
|
72 hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n |
|
73 \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))" |
|
74 unfolding Ball_def by blast |
|
75 have approx_space: |
|
76 "\<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ennreal e" |
|
77 (is "?thesis e") if "0 < e" for e :: real |
|
78 proof - |
|
79 define B where [abs_def]: |
|
80 "B n = (\<Union>i\<in>{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n))" for n |
|
81 have "\<And>n. closed (B n)" by (auto simp: B_def) |
|
82 hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb) |
|
83 from k[OF \<open>e > 0\<close> zero_less_Suc] |
|
84 have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)" |
|
85 by (simp add: algebra_simps B_def finite_measure_compl) |
|
86 hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)" |
|
87 by (simp add: finite_measure_compl) |
|
88 define K where "K = (\<Inter>n. B n)" |
|
89 from \<open>closed (B _)\<close> have "closed K" by (auto simp: K_def) |
|
90 hence [simp]: "K \<in> sets M" by (simp add: sb) |
|
91 have "measure M (space M) - measure M K = measure M (space M - K)" |
|
92 by (simp add: finite_measure_compl) |
|
93 also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure) |
|
94 also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))" |
|
95 by (rule emeasure_subadditive_countably) (auto simp: summable_def) |
|
96 also have "\<dots> \<le> (\<Sum>n. ennreal (e*2 powr - real (Suc n)))" |
|
97 using B_compl_le by (intro suminf_le) (simp_all add: measure_nonneg emeasure_eq_measure ennreal_leI) |
|
98 also have "\<dots> \<le> (\<Sum>n. ennreal (e * (1 / 2) ^ Suc n))" |
|
99 by (simp add: powr_minus powr_realpow field_simps del: of_nat_Suc) |
|
100 also have "\<dots> = ennreal e * (\<Sum>n. ennreal ((1 / 2) ^ Suc n))" |
|
101 unfolding ennreal_power[symmetric] |
|
102 using \<open>0 < e\<close> |
|
103 by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def |
|
104 ennreal_power[symmetric]) |
|
105 also have "\<dots> = e" |
|
106 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto |
|
107 finally have "measure M (space M) \<le> measure M K + e" |
|
108 using \<open>0 < e\<close> by simp |
|
109 hence "emeasure M (space M) \<le> emeasure M K + e" |
|
110 using \<open>0 < e\<close> by (simp add: emeasure_eq_measure measure_nonneg ennreal_plus[symmetric] del: ennreal_plus) |
|
111 moreover have "compact K" |
|
112 unfolding compact_eq_totally_bounded |
|
113 proof safe |
|
114 show "complete K" using \<open>closed K\<close> by (simp add: complete_eq_closed) |
|
115 fix e'::real assume "0 < e'" |
|
116 from nat_approx_posE[OF this] guess n . note n = this |
|
117 let ?k = "from_nat_into X ` {0..k e (Suc n)}" |
|
118 have "finite ?k" by simp |
|
119 moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force |
|
120 ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast |
|
121 qed |
|
122 ultimately |
|
123 show ?thesis by (auto simp: sU) |
|
124 qed |
|
125 { fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed) |
|
126 hence [simp]: "A \<in> sets M" by (simp add: sb) |
|
127 have "?inner A" |
|
128 proof (rule approx_inner) |
|
129 fix e::real assume "e > 0" |
|
130 from approx_space[OF this] obtain K where |
|
131 K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e" |
|
132 by (auto simp: emeasure_eq_measure) |
|
133 hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed) |
|
134 have "measure M A - measure M (A \<inter> K) = measure M (A - A \<inter> K)" |
|
135 by (subst finite_measure_Diff) auto |
|
136 also have "A - A \<inter> K = A \<union> K - K" by auto |
|
137 also have "measure M \<dots> = measure M (A \<union> K) - measure M K" |
|
138 by (subst finite_measure_Diff) auto |
|
139 also have "\<dots> \<le> measure M (space M) - measure M K" |
|
140 by (simp add: emeasure_eq_measure sU sb finite_measure_mono) |
|
141 also have "\<dots> \<le> e" |
|
142 using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure ennreal_plus[symmetric] measure_nonneg del: ennreal_plus) |
|
143 finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ennreal e" |
|
144 using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps ennreal_plus[symmetric] measure_nonneg del: ennreal_plus) |
|
145 moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using \<open>closed A\<close> \<open>compact K\<close> by auto |
|
146 ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ennreal e" |
|
147 by blast |
|
148 qed simp |
|
149 have "?outer A" |
|
150 proof cases |
|
151 assume "A \<noteq> {}" |
|
152 let ?G = "\<lambda>d. {x. infdist x A < d}" |
|
153 { |
|
154 fix d |
|
155 have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto |
|
156 also have "open \<dots>" |
|
157 by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident) |
|
158 finally have "open (?G d)" . |
|
159 } note open_G = this |
|
160 from in_closed_iff_infdist_zero[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>] |
|
161 have "A = {x. infdist x A = 0}" by auto |
|
162 also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))" |
|
163 proof (auto simp del: of_nat_Suc, rule ccontr) |
|
164 fix x |
|
165 assume "infdist x A \<noteq> 0" |
|
166 hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp |
|
167 from nat_approx_posE[OF this] guess n . |
|
168 moreover |
|
169 assume "\<forall>i. infdist x A < 1 / real (Suc i)" |
|
170 hence "infdist x A < 1 / real (Suc n)" by auto |
|
171 ultimately show False by simp |
|
172 qed |
|
173 also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))" |
|
174 proof (rule INF_emeasure_decseq[symmetric], safe) |
|
175 fix i::nat |
|
176 from open_G[of "1 / real (Suc i)"] |
|
177 show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open) |
|
178 next |
|
179 show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})" |
|
180 by (auto intro: less_trans intro!: divide_strict_left_mono |
|
181 simp: decseq_def le_eq_less_or_eq) |
|
182 qed simp |
|
183 finally |
|
184 have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" . |
|
185 moreover |
|
186 have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)" |
|
187 proof (intro INF_mono) |
|
188 fix m |
|
189 have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto |
|
190 moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp |
|
191 ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}. |
|
192 emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}" |
|
193 by blast |
|
194 qed |
|
195 moreover |
|
196 have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)" |
|
197 by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb) |
|
198 ultimately show ?thesis by simp |
|
199 qed (auto intro!: INF_eqI) |
|
200 note \<open>?inner A\<close> \<open>?outer A\<close> } |
|
201 note closed_in_D = this |
|
202 from \<open>B \<in> sets borel\<close> |
|
203 have "Int_stable (Collect closed)" "Collect closed \<subseteq> Pow UNIV" "B \<in> sigma_sets UNIV (Collect closed)" |
|
204 by (auto simp: Int_stable_def borel_eq_closed) |
|
205 then show "?inner B" "?outer B" |
|
206 proof (induct B rule: sigma_sets_induct_disjoint) |
|
207 case empty |
|
208 { case 1 show ?case by (intro SUP_eqI[symmetric]) auto } |
|
209 { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) } |
|
210 next |
|
211 case (basic B) |
|
212 { case 1 from basic closed_in_D show ?case by auto } |
|
213 { case 2 from basic closed_in_D show ?case by auto } |
|
214 next |
|
215 case (compl B) |
|
216 note inner = compl(2) and outer = compl(3) |
|
217 from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed) |
|
218 case 2 |
|
219 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) |
|
220 also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)" |
|
221 by (subst ennreal_SUP_const_minus) (auto simp: less_top[symmetric] inner) |
|
222 also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))" |
|
223 by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed) |
|
224 also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))" |
|
225 by (rule INF_superset_mono) (auto simp add: compact_imp_closed) |
|
226 also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) = |
|
227 (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)" |
|
228 unfolding INF_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def] |
|
229 by (rule INF_cong) (auto simp add: sU Compl_eq_Diff_UNIV [symmetric, simp]) |
|
230 finally have |
|
231 "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" . |
|
232 moreover have |
|
233 "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)" |
|
234 by (auto simp: sb sU intro!: INF_greatest emeasure_mono) |
|
235 ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) |
|
236 |
|
237 case 1 |
|
238 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) |
|
239 also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)" |
|
240 unfolding outer by (subst ennreal_INF_const_minus) auto |
|
241 also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))" |
|
242 by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) |
|
243 also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)" |
|
244 unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def] |
|
245 by (rule SUP_cong) (auto simp add: sU) |
|
246 also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)" |
|
247 proof (safe intro!: antisym SUP_least) |
|
248 fix K assume "closed K" "K \<subseteq> space M - B" |
|
249 from closed_in_D[OF \<open>closed K\<close>] |
|
250 have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp |
|
251 show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)" |
|
252 unfolding K_inner using \<open>K \<subseteq> space M - B\<close> |
|
253 by (auto intro!: SUP_upper SUP_least) |
|
254 qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed) |
|
255 finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) |
|
256 next |
|
257 case (union D) |
|
258 then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed) |
|
259 with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure) |
|
260 also have "(\<lambda>n. \<Sum>i<n. M (D i)) \<longlonglongrightarrow> (\<Sum>i. M (D i))" |
|
261 by (intro summable_LIMSEQ) auto |
|
262 finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i<n. measure M (D i)) \<longlonglongrightarrow> measure M (\<Union>i. D i)" |
|
263 by (simp add: emeasure_eq_measure measure_nonneg setsum_nonneg) |
|
264 have "(\<Union>i. D i) \<in> sets M" using \<open>range D \<subseteq> sets M\<close> by auto |
|
265 |
|
266 case 1 |
|
267 show ?case |
|
268 proof (rule approx_inner) |
|
269 fix e::real assume "e > 0" |
|
270 with measure_LIMSEQ |
|
271 have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2" |
|
272 by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1) |
|
273 hence "\<exists>n0. \<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto |
|
274 then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2" |
|
275 unfolding choice_iff by blast |
|
276 have "ennreal (\<Sum>i<n0. measure M (D i)) = (\<Sum>i<n0. M (D i))" |
|
277 by (auto simp add: emeasure_eq_measure setsum_nonneg measure_nonneg) |
|
278 also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule setsum_le_suminf) auto |
|
279 also have "\<dots> = M (\<Union>i. D i)" by (simp add: M) |
|
280 also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure) |
|
281 finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i<n0. measure M (D i)) < e/2" |
|
282 using n0 by (auto simp: measure_nonneg setsum_nonneg) |
|
283 have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)" |
|
284 proof |
|
285 fix i |
|
286 from \<open>0 < e\<close> have "0 < e/(2*Suc n0)" by simp |
|
287 have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)" |
|
288 using union by blast |
|
289 from SUP_approx_ennreal[OF \<open>0 < e/(2*Suc n0)\<close> _ this] |
|
290 show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)" |
|
291 by (auto simp: emeasure_eq_measure intro: less_imp_le compact_empty) |
|
292 qed |
|
293 then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)" |
|
294 "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)" |
|
295 unfolding choice_iff by blast |
|
296 let ?K = "\<Union>i\<in>{..<n0}. K i" |
|
297 have "disjoint_family_on K {..<n0}" using K \<open>disjoint_family D\<close> |
|
298 unfolding disjoint_family_on_def by blast |
|
299 hence mK: "measure M ?K = (\<Sum>i<n0. measure M (K i))" using K |
|
300 by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed) |
|
301 have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (D i)) + e/2" using n0 by simp |
|
302 also have "(\<Sum>i<n0. measure M (D i)) \<le> (\<Sum>i<n0. measure M (K i) + e/(2*Suc n0))" |
|
303 using K \<open>0 < e\<close> |
|
304 by (auto intro: setsum_mono simp: emeasure_eq_measure measure_nonneg ennreal_plus[symmetric] simp del: ennreal_plus) |
|
305 also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))" |
|
306 by (simp add: setsum.distrib) |
|
307 also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) + e / 2" using \<open>0 < e\<close> |
|
308 by (auto simp: field_simps intro!: mult_left_mono) |
|
309 finally |
|
310 have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2" |
|
311 by auto |
|
312 hence "M (\<Union>i. D i) < M ?K + e" |
|
313 using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure measure_nonneg setsum_nonneg ennreal_less_iff ennreal_plus[symmetric] simp del: ennreal_plus) |
|
314 moreover |
|
315 have "?K \<subseteq> (\<Union>i. D i)" using K by auto |
|
316 moreover |
|
317 have "compact ?K" using K by auto |
|
318 ultimately |
|
319 have "?K\<subseteq>(\<Union>i. D i) \<and> compact ?K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M ?K + ennreal e" by simp |
|
320 thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ennreal e" .. |
|
321 qed fact |
|
322 case 2 |
|
323 show ?case |
|
324 proof (rule approx_outer[OF \<open>(\<Union>i. D i) \<in> sets M\<close>]) |
|
325 fix e::real assume "e > 0" |
|
326 have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)" |
|
327 proof |
|
328 fix i::nat |
|
329 from \<open>0 < e\<close> have "0 < e/(2 powr Suc i)" by simp |
|
330 have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)" |
|
331 using union by blast |
|
332 from INF_approx_ennreal[OF \<open>0 < e/(2 powr Suc i)\<close> this] |
|
333 show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)" |
|
334 using \<open>0<e\<close> |
|
335 by (auto simp: emeasure_eq_measure measure_nonneg setsum_nonneg ennreal_less_iff ennreal_plus[symmetric] ennreal_minus |
|
336 finite_measure_mono sb |
|
337 simp del: ennreal_plus) |
|
338 qed |
|
339 then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)" |
|
340 "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)" |
|
341 unfolding choice_iff by blast |
|
342 let ?U = "\<Union>i. U i" |
|
343 have "ennreal (measure M ?U - measure M (\<Union>i. D i)) = M ?U - M (\<Union>i. D i)" |
|
344 using U(1,2) |
|
345 by (subst ennreal_minus[symmetric]) |
|
346 (auto intro!: finite_measure_mono simp: sb measure_nonneg emeasure_eq_measure) |
|
347 also have "\<dots> = M (?U - (\<Union>i. D i))" using U \<open>(\<Union>i. D i) \<in> sets M\<close> |
|
348 by (subst emeasure_Diff) (auto simp: sb) |
|
349 also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U \<open>range D \<subseteq> sets M\<close> |
|
350 by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff) |
|
351 also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U \<open>range D \<subseteq> sets M\<close> |
|
352 by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb) |
|
353 also have "\<dots> \<le> (\<Sum>i. ennreal e/(2 powr Suc i))" using U \<open>range D \<subseteq> sets M\<close> |
|
354 using \<open>0<e\<close> |
|
355 by (intro suminf_le, subst emeasure_Diff) |
|
356 (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg ennreal_minus |
|
357 finite_measure_mono divide_ennreal ennreal_less_iff |
|
358 intro: less_imp_le) |
|
359 also have "\<dots> \<le> (\<Sum>n. ennreal (e * (1 / 2) ^ Suc n))" |
|
360 using \<open>0<e\<close> |
|
361 by (simp add: powr_minus powr_realpow field_simps divide_ennreal del: of_nat_Suc) |
|
362 also have "\<dots> = ennreal e * (\<Sum>n. ennreal ((1 / 2) ^ Suc n))" |
|
363 unfolding ennreal_power[symmetric] |
|
364 using \<open>0 < e\<close> |
|
365 by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def |
|
366 ennreal_power[symmetric]) |
|
367 also have "\<dots> = ennreal e" |
|
368 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto |
|
369 finally have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ennreal e" |
|
370 using \<open>0<e\<close> by (simp add: emeasure_eq_measure ennreal_plus[symmetric] measure_nonneg del: ennreal_plus) |
|
371 moreover |
|
372 have "(\<Union>i. D i) \<subseteq> ?U" using U by auto |
|
373 moreover |
|
374 have "open ?U" using U by auto |
|
375 ultimately |
|
376 have "(\<Union>i. D i) \<subseteq> ?U \<and> open ?U \<and> emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ennreal e" by simp |
|
377 thus "\<exists>B. (\<Union>i. D i) \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M (\<Union>i. D i) + ennreal e" .. |
|
378 qed |
|
379 qed |
|
380 qed |
|
381 |
|
382 end |
|
383 |