src/HOL/Probability/Regularity.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62343 24106dc44def
child 62533 bc25f3916a99
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Probability/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 ereal_approx_SUP:
    12   fixes x::ereal
    13   assumes A_notempty: "A \<noteq> {}"
    14   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
    15   assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
    16   assumes f_nonneg: "\<And>i. 0 \<le> f i"
    17   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
    18   shows "x = (SUP i : A. f i)"
    19 proof (subst eq_commute, rule SUP_eqI)
    20   show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
    21 next
    22   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
    23   with A_notempty f_nonneg have "y \<ge> 0" by auto (metis order_trans)
    24   show "x \<le> y"
    25   proof (rule ccontr)
    26     assume "\<not> x \<le> y" hence "x > y" by simp
    27     hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using \<open>y \<ge> 0\<close> by auto
    28     have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using \<open>x > y\<close> f_fin approx[where e = 1] by auto
    29     def e \<equiv> "real_of_ereal ((x - y) / 2)"
    30     have e: "x > y + e" "e > 0" using \<open>x > y\<close> y_fin x_fin by (auto simp: e_def field_simps)
    31     note e(1)
    32     also from approx[OF \<open>e > 0\<close>] obtain i where i: "i \<in> A" "x \<le> f i + e" by blast
    33     note i(2)
    34     finally have "y < f i" using y_fin f_fin by (metis add_right_mono linorder_not_le)
    35     moreover have "f i \<le> y" by (rule f_le_y) fact
    36     ultimately show False by simp
    37   qed
    38 qed
    39 
    40 lemma ereal_approx_INF:
    41   fixes x::ereal
    42   assumes A_notempty: "A \<noteq> {}"
    43   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
    44   assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
    45   assumes f_nonneg: "\<And>i. 0 \<le> f i"
    46   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
    47   shows "x = (INF i : A. f i)"
    48 proof (subst eq_commute, rule INF_eqI)
    49   show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
    50 next
    51   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
    52   with A_notempty f_fin have "y \<noteq> \<infinity>" by force
    53   show "y \<le> x"
    54   proof (rule ccontr)
    55     assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
    56     hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using \<open>y \<noteq> \<infinity>\<close> by auto
    57     have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using \<open>y > x\<close> f_fin f_nonneg approx[where e = 1] A_notempty
    58       by auto
    59     def e \<equiv> "real_of_ereal ((y - x) / 2)"
    60     have e: "y > x + e" "e > 0" using \<open>y > x\<close> y_fin x_fin by (auto simp: e_def field_simps)
    61     from approx[OF \<open>e > 0\<close>] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast
    62     note i(2)
    63     also note e(1)
    64     finally have "y > f i" .
    65     moreover have "y \<le> f i" by (rule f_le_y) fact
    66     ultimately show False by simp
    67   qed
    68 qed
    69 
    70 lemma INF_approx_ereal:
    71   fixes x::ereal and e::real
    72   assumes "e > 0"
    73   assumes INF: "x = (INF i : A. f i)"
    74   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
    75   shows "\<exists>i \<in> A. f i < x + e"
    76 proof (rule ccontr, clarsimp)
    77   assume "\<forall>i\<in>A. \<not> f i < x + e"
    78   moreover
    79   from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
    80   ultimately
    81   have "(INF i : A. f i) = x + e" using \<open>e > 0\<close>
    82     by (intro INF_eqI)
    83       (force, metis add.comm_neutral add_left_mono ereal_less(1)
    84         linorder_not_le not_less_iff_gr_or_eq)
    85   thus False using assms by auto
    86 qed
    87 
    88 lemma SUP_approx_ereal:
    89   fixes x::ereal and e::real
    90   assumes "e > 0"
    91   assumes SUP: "x = (SUP i : A. f i)"
    92   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
    93   shows "\<exists>i \<in> A. x \<le> f i + e"
    94 proof (rule ccontr, clarsimp)
    95   assume "\<forall>i\<in>A. \<not> x \<le> f i + e"
    96   moreover
    97   from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
    98   ultimately
    99   have "(SUP i : A. f i) = x - e" using \<open>e > 0\<close> \<open>\<bar>x\<bar> \<noteq> \<infinity>\<close>
   100     by (intro SUP_eqI)
   101        (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
   102         metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
   103   thus False using assms by auto
   104 qed
   105 
   106 lemma
   107   fixes M::"'a::{second_countable_topology, complete_space} measure"
   108   assumes sb: "sets M = sets borel"
   109   assumes "emeasure M (space M) \<noteq> \<infinity>"
   110   assumes "B \<in> sets borel"
   111   shows inner_regular: "emeasure M B =
   112     (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
   113   and outer_regular: "emeasure M B =
   114     (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
   115 proof -
   116   have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
   117   hence sU: "space M = UNIV" by simp
   118   interpret finite_measure M by rule fact
   119   have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow>
   120     (\<And>e. e > 0 \<Longrightarrow> \<exists>K. K \<subseteq> A \<and> compact K \<and> emeasure M A \<le> emeasure M K + ereal e) \<Longrightarrow> ?inner A"
   121     by (rule ereal_approx_SUP)
   122       (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
   123   have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow>
   124     (\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ereal e) \<Longrightarrow> ?outer A"
   125     by (rule ereal_approx_INF)
   126        (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
   127   from countable_dense_setE guess X::"'a set"  . note X = this
   128   {
   129     fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
   130     with X(2)[OF this]
   131     have x: "space M = (\<Union>x\<in>X. cball x r)"
   132       by (auto simp add: sU) (metis dist_commute order_less_imp_le)
   133     let ?U = "\<Union>k. (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)"
   134     have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M ?U"
   135       by (rule Lim_emeasure_incseq)
   136         (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
   137     also have "?U = space M"
   138     proof safe
   139       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
   140       show "x \<in> ?U"
   141         using X(1) d
   142         by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def)
   143     qed (simp add: sU)
   144     finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M (space M)" .
   145   } note M_space = this
   146   {
   147     fix e ::real and n :: nat assume "e > 0" "n > 0"
   148     hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
   149     from M_space[OF \<open>1/n>0\<close>]
   150     have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) \<longlonglongrightarrow> measure M (space M)"
   151       unfolding emeasure_eq_measure by simp
   152     from metric_LIMSEQ_D[OF this \<open>0 < e * 2 powr -n\<close>]
   153     obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <
   154       e * 2 powr -n"
   155       by auto
   156     hence "measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
   157       measure M (space M) - e * 2 powr -real n"
   158       by (auto simp: dist_real_def)
   159     hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
   160       measure M (space M) - e * 2 powr - real n" ..
   161   } note k=this
   162   hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
   163     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"
   164     by blast
   165   then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
   166     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
   167     by metis
   168   hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
   169     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
   170     unfolding Ball_def by blast
   171   have approx_space:
   172     "\<And>e. e > 0 \<Longrightarrow>
   173       \<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
   174       (is "\<And>e. _ \<Longrightarrow> ?thesis e")
   175   proof -
   176     fix e :: real assume "e > 0"
   177     def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n)"
   178     have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
   179     hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
   180     from k[OF \<open>e > 0\<close> zero_less_Suc]
   181     have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"
   182       by (simp add: algebra_simps B_def finite_measure_compl)
   183     hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"
   184       by (simp add: finite_measure_compl)
   185     def K \<equiv> "\<Inter>n. B n"
   186     from \<open>closed (B _)\<close> have "closed K" by (auto simp: K_def)
   187     hence [simp]: "K \<in> sets M" by (simp add: sb)
   188     have "measure M (space M) - measure M K = measure M (space M - K)"
   189       by (simp add: finite_measure_compl)
   190     also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
   191     also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
   192       by (rule emeasure_subadditive_countably) (auto simp: summable_def)
   193     also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
   194       using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
   195     also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
   196       by (simp add: Transcendental.powr_minus powr_realpow field_simps del: of_nat_Suc)
   197     also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
   198       unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
   199       by simp
   200     also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
   201       by (rule suminf_cmult_ereal) (auto simp: \<open>0 < e\<close> less_imp_le)
   202     also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
   203     finally have "measure M (space M) \<le> measure M K + e" by simp
   204     hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure)
   205     moreover have "compact K"
   206       unfolding compact_eq_totally_bounded
   207     proof safe
   208       show "complete K" using \<open>closed K\<close> by (simp add: complete_eq_closed)
   209       fix e'::real assume "0 < e'"
   210       from nat_approx_posE[OF this] guess n . note n = this
   211       let ?k = "from_nat_into X ` {0..k e (Suc n)}"
   212       have "finite ?k" by simp
   213       moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
   214       ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast
   215     qed
   216     ultimately
   217     show "?thesis e " by (auto simp: sU)
   218   qed
   219   { fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
   220     hence [simp]: "A \<in> sets M" by (simp add: sb)
   221     have "?inner A"
   222     proof (rule approx_inner)
   223       fix e::real assume "e > 0"
   224       from approx_space[OF this] obtain K where
   225         K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"
   226         by (auto simp: emeasure_eq_measure)
   227       hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)
   228       have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)"
   229         by (simp add: emeasure_eq_measure)
   230       also have "\<dots> = measure M (A - A \<inter> K)"
   231         by (subst finite_measure_Diff) auto
   232       also have "A - A \<inter> K = A \<union> K - K" by auto
   233       also have "measure M \<dots> = measure M (A \<union> K) - measure M K"
   234         by (subst finite_measure_Diff) auto
   235       also have "\<dots> \<le> measure M (space M) - measure M K"
   236         by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
   237       also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure)
   238       finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e"
   239         by (simp add: emeasure_eq_measure algebra_simps)
   240       moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using \<open>closed A\<close> \<open>compact K\<close> by auto
   241       ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
   242         by blast
   243     qed simp
   244     have "?outer A"
   245     proof cases
   246       assume "A \<noteq> {}"
   247       let ?G = "\<lambda>d. {x. infdist x A < d}"
   248       {
   249         fix d
   250         have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
   251         also have "open \<dots>"
   252           by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
   253         finally have "open (?G d)" .
   254       } note open_G = this
   255       from in_closed_iff_infdist_zero[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>]
   256       have "A = {x. infdist x A = 0}" by auto
   257       also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
   258       proof (auto simp del: of_nat_Suc, rule ccontr)
   259         fix x
   260         assume "infdist x A \<noteq> 0"
   261         hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
   262         from nat_approx_posE[OF this] guess n .
   263         moreover
   264         assume "\<forall>i. infdist x A < 1 / real (Suc i)"
   265         hence "infdist x A < 1 / real (Suc n)" by auto
   266         ultimately show False by simp
   267       qed
   268       also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
   269       proof (rule INF_emeasure_decseq[symmetric], safe)
   270         fix i::nat
   271         from open_G[of "1 / real (Suc i)"]
   272         show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
   273       next
   274         show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
   275           by (auto intro: less_trans intro!: divide_strict_left_mono
   276             simp: decseq_def le_eq_less_or_eq)
   277       qed simp
   278       finally
   279       have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
   280       moreover
   281       have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
   282       proof (intro INF_mono)
   283         fix m
   284         have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
   285         moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp
   286         ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.
   287           emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"
   288           by blast
   289       qed
   290       moreover
   291       have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
   292         by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
   293       ultimately show ?thesis by simp
   294     qed (auto intro!: INF_eqI)
   295     note \<open>?inner A\<close> \<open>?outer A\<close> }
   296   note closed_in_D = this
   297   from \<open>B \<in> sets borel\<close>
   298   have "Int_stable (Collect closed)" "Collect closed \<subseteq> Pow UNIV" "B \<in> sigma_sets UNIV (Collect closed)"
   299     by (auto simp: Int_stable_def borel_eq_closed)
   300   then show "?inner B" "?outer B"
   301   proof (induct B rule: sigma_sets_induct_disjoint)
   302     case empty
   303     { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
   304     { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
   305   next
   306     case (basic B)
   307     { case 1 from basic closed_in_D show ?case by auto }
   308     { case 2 from basic closed_in_D show ?case by auto }
   309   next
   310     case (compl B)
   311     note inner = compl(2) and outer = compl(3)
   312     from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed)
   313     case 2
   314     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
   315     also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
   316       unfolding inner by (subst INF_ereal_minus_right) force+
   317     also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
   318       by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   319     also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
   320       by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
   321     also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
   322         (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
   323       unfolding INF_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
   324         by (rule INF_cong) (auto simp add: sU open_Compl Compl_eq_Diff_UNIV [symmetric, simp])
   325     finally have
   326       "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
   327     moreover have
   328       "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
   329       by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
   330     ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
   331 
   332     case 1
   333     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
   334     also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
   335       unfolding outer by (subst SUP_ereal_minus_right) auto
   336     also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
   337       by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   338     also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
   339       unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
   340         by (rule SUP_cong) (auto simp add: sU)
   341     also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   342     proof (safe intro!: antisym SUP_least)
   343       fix K assume "closed K" "K \<subseteq> space M - B"
   344       from closed_in_D[OF \<open>closed K\<close>]
   345       have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
   346       show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   347         unfolding K_inner using \<open>K \<subseteq> space M - B\<close>
   348         by (auto intro!: SUP_upper SUP_least)
   349     qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
   350     finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
   351   next
   352     case (union D)
   353     then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed)
   354     with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure)
   355     also have "(\<lambda>n. \<Sum>i<n. M (D i)) \<longlonglongrightarrow> (\<Sum>i. M (D i))"
   356       by (intro summable_LIMSEQ summable_ereal_pos emeasure_nonneg)
   357     finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i<n. measure M (D i)) \<longlonglongrightarrow> measure M (\<Union>i. D i)"
   358       by (simp add: emeasure_eq_measure)
   359     have "(\<Union>i. D i) \<in> sets M" using \<open>range D \<subseteq> sets M\<close> by auto
   360 
   361     case 1
   362     show ?case
   363     proof (rule approx_inner)
   364       fix e::real assume "e > 0"
   365       with measure_LIMSEQ
   366       have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
   367         by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1)
   368       hence "\<exists>n0. \<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
   369       then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
   370         unfolding choice_iff by blast
   371       have "ereal (\<Sum>i<n0. measure M (D i)) = (\<Sum>i<n0. M (D i))"
   372         by (auto simp add: emeasure_eq_measure)
   373       also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
   374       also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
   375       also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
   376       finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i<n0. measure M (D i)) < e/2"
   377         using n0 by auto
   378       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)"
   379       proof
   380         fix i
   381         from \<open>0 < e\<close> have "0 < e/(2*Suc n0)" by simp
   382         have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
   383           using union by blast
   384         from SUP_approx_ereal[OF \<open>0 < e/(2*Suc n0)\<close> this]
   385         show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
   386           by (auto simp: emeasure_eq_measure)
   387       qed
   388       then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
   389         "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
   390         unfolding choice_iff by blast
   391       let ?K = "\<Union>i\<in>{..<n0}. K i"
   392       have "disjoint_family_on K {..<n0}" using K \<open>disjoint_family D\<close>
   393         unfolding disjoint_family_on_def by blast
   394       hence mK: "measure M ?K = (\<Sum>i<n0. measure M (K i))" using K
   395         by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
   396       have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (D i)) + e/2" using n0 by simp
   397       also have "(\<Sum>i<n0. measure M (D i)) \<le> (\<Sum>i<n0. measure M (K i) + e/(2*Suc n0))"
   398         using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
   399       also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))"
   400         by (simp add: setsum.distrib)
   401       also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) +  e / 2" using \<open>0 < e\<close>
   402         by (auto simp: field_simps intro!: mult_left_mono)
   403       finally
   404       have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2"
   405         by auto
   406       hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
   407       moreover
   408       have "?K \<subseteq> (\<Union>i. D i)" using K by auto
   409       moreover
   410       have "compact ?K" using K by auto
   411       ultimately
   412       have "?K\<subseteq>(\<Union>i. D i) \<and> compact ?K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M ?K + ereal e" by simp
   413       thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
   414     qed fact
   415     case 2
   416     show ?case
   417     proof (rule approx_outer[OF \<open>(\<Union>i. D i) \<in> sets M\<close>])
   418       fix e::real assume "e > 0"
   419       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)"
   420       proof
   421         fix i::nat
   422         from \<open>0 < e\<close> have "0 < e/(2 powr Suc i)" by simp
   423         have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
   424           using union by blast
   425         from INF_approx_ereal[OF \<open>0 < e/(2 powr Suc i)\<close> this]
   426         show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
   427           by (auto simp: emeasure_eq_measure)
   428       qed
   429       then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
   430         "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
   431         unfolding choice_iff by blast
   432       let ?U = "\<Union>i. U i"
   433       have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  \<open>(\<Union>i. D i) \<in> sets M\<close>
   434         by (subst emeasure_Diff) (auto simp: sb)
   435       also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  \<open>range D \<subseteq> sets M\<close>
   436         by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff)
   437       also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  \<open>range D \<subseteq> sets M\<close>
   438         by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb)
   439       also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U \<open>range D \<subseteq> sets M\<close>
   440         by (intro suminf_le_pos, subst emeasure_Diff)
   441            (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
   442       also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
   443         by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide del: of_nat_Suc)
   444       also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^  Suc n))"
   445         unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
   446         by simp
   447       also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
   448         by (rule suminf_cmult_ereal) (auto simp: \<open>0 < e\<close> less_imp_le)
   449       also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
   450       finally
   451       have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
   452       moreover
   453       have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
   454       moreover
   455       have "open ?U" using U by auto
   456       ultimately
   457       have "(\<Union>i. D i) \<subseteq> ?U \<and> open ?U \<and> emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by simp
   458       thus "\<exists>B. (\<Union>i. D i) \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M (\<Union>i. D i) + ereal e" ..
   459     qed
   460   qed
   461 qed
   462 
   463 end
   464