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