105 also have "\<dots> = e" |
105 also have "\<dots> = e" |
106 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto |
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" |
107 finally have "measure M (space M) \<le> measure M K + e" |
108 using \<open>0 < e\<close> by simp |
108 using \<open>0 < e\<close> by simp |
109 hence "emeasure M (space M) \<le> emeasure M K + e" |
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) |
110 using \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus) |
111 moreover have "compact K" |
111 moreover have "compact K" |
112 unfolding compact_eq_totally_bounded |
112 unfolding compact_eq_totally_bounded |
113 proof safe |
113 proof safe |
114 show "complete K" using \<open>closed K\<close> by (simp add: complete_eq_closed) |
114 show "complete K" using \<open>closed K\<close> by (simp add: complete_eq_closed) |
115 fix e'::real assume "0 < e'" |
115 fix e'::real assume "0 < e'" |
137 also have "measure M \<dots> = measure M (A \<union> K) - measure M K" |
137 also have "measure M \<dots> = measure M (A \<union> K) - measure M K" |
138 by (subst finite_measure_Diff) auto |
138 by (subst finite_measure_Diff) auto |
139 also have "\<dots> \<le> measure M (space M) - measure M K" |
139 also have "\<dots> \<le> measure M (space M) - measure M K" |
140 by (simp add: emeasure_eq_measure sU sb finite_measure_mono) |
140 by (simp add: emeasure_eq_measure sU sb finite_measure_mono) |
141 also have "\<dots> \<le> e" |
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) |
142 using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus) |
143 finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ennreal e" |
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) |
144 using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps reorient: 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 |
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" |
146 ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ennreal e" |
147 by blast |
147 by blast |
148 qed simp |
148 qed simp |
149 have "?outer A" |
149 have "?outer A" |
299 hence mK: "measure M ?K = (\<Sum>i<n0. measure M (K i))" using K |
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) |
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 |
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))" |
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> |
303 using K \<open>0 < e\<close> |
304 by (auto intro: sum_mono simp: emeasure_eq_measure measure_nonneg ennreal_plus[symmetric] simp del: ennreal_plus) |
304 by (auto intro: sum_mono simp: emeasure_eq_measure reorient: ennreal_plus) |
305 also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))" |
305 also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))" |
306 by (simp add: sum.distrib) |
306 by (simp add: sum.distrib) |
307 also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) + e / 2" using \<open>0 < e\<close> |
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) |
308 by (auto simp: field_simps intro!: mult_left_mono) |
309 finally |
309 finally |
310 have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2" |
310 have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2" |
311 by auto |
311 by auto |
312 hence "M (\<Union>i. D i) < M ?K + e" |
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 sum_nonneg ennreal_less_iff ennreal_plus[symmetric] simp del: ennreal_plus) |
313 using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff reorient: ennreal_plus) |
314 moreover |
314 moreover |
315 have "?K \<subseteq> (\<Union>i. D i)" using K by auto |
315 have "?K \<subseteq> (\<Union>i. D i)" using K by auto |
316 moreover |
316 moreover |
317 have "compact ?K" using K by auto |
317 have "compact ?K" using K by auto |
318 ultimately |
318 ultimately |
330 have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)" |
330 have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)" |
331 using union by blast |
331 using union by blast |
332 from INF_approx_ennreal[OF \<open>0 < e/(2 powr Suc i)\<close> this] |
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)" |
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> |
334 using \<open>0<e\<close> |
335 by (auto simp: emeasure_eq_measure measure_nonneg sum_nonneg ennreal_less_iff ennreal_plus[symmetric] ennreal_minus |
335 by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus |
336 finite_measure_mono sb |
336 finite_measure_mono sb |
337 simp del: ennreal_plus) |
337 reorient: ennreal_plus) |
338 qed |
338 qed |
339 then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)" |
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)" |
340 "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)" |
341 unfolding choice_iff by blast |
341 unfolding choice_iff by blast |
342 let ?U = "\<Union>i. U i" |
342 let ?U = "\<Union>i. U i" |
365 by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def |
365 by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def |
366 ennreal_power[symmetric]) |
366 ennreal_power[symmetric]) |
367 also have "\<dots> = ennreal e" |
367 also have "\<dots> = ennreal e" |
368 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto |
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" |
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) |
370 using \<open>0<e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus) |
371 moreover |
371 moreover |
372 have "(\<Union>i. D i) \<subseteq> ?U" using U by auto |
372 have "(\<Union>i. D i) \<subseteq> ?U" using U by auto |
373 moreover |
373 moreover |
374 have "open ?U" using U by auto |
374 have "open ?U" using U by auto |
375 ultimately |
375 ultimately |