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