74 unfolding Ball_def by blast |
74 unfolding Ball_def by blast |
75 have approx_space: |
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" |
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 |
77 (is "?thesis e") if "0 < e" for e :: real |
78 proof - |
78 proof - |
79 def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n)" |
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 |
80 have "\<And>n. closed (B n)" by (auto simp: B_def) |
81 have "\<And>n. closed (B n)" by (auto simp: B_def) |
81 hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb) |
82 hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb) |
82 from k[OF \<open>e > 0\<close> zero_less_Suc] |
83 from k[OF \<open>e > 0\<close> zero_less_Suc] |
83 have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)" |
84 have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)" |
84 by (simp add: algebra_simps B_def finite_measure_compl) |
85 by (simp add: algebra_simps B_def finite_measure_compl) |
85 hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)" |
86 hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)" |
86 by (simp add: finite_measure_compl) |
87 by (simp add: finite_measure_compl) |
87 def K \<equiv> "\<Inter>n. B n" |
88 define K where "K = (\<Inter>n. B n)" |
88 from \<open>closed (B _)\<close> have "closed K" by (auto simp: K_def) |
89 from \<open>closed (B _)\<close> have "closed K" by (auto simp: K_def) |
89 hence [simp]: "K \<in> sets M" by (simp add: sb) |
90 hence [simp]: "K \<in> sets M" by (simp add: sb) |
90 have "measure M (space M) - measure M K = measure M (space M - K)" |
91 have "measure M (space M) - measure M K = measure M (space M - K)" |
91 by (simp add: finite_measure_compl) |
92 by (simp add: finite_measure_compl) |
92 also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure) |
93 also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure) |