src/HOL/Probability/Regularity.thy
 author hoelzl Mon Nov 19 18:01:48 2012 +0100 (2012-11-19 ago) changeset 50125 4319691be975 parent 50089 1badf63e5d97 child 50244 de72bbe42190 permissions -rw-r--r--
tuned: use induction rule sigma_sets_induct_disjoint
```     1 (*  Title:      HOL/Probability/Projective_Family.thy
```
```     2     Author:     Fabian Immler, TU München
```
```     3 *)
```
```     4
```
```     5 header {* Regularity of Measures *}
```
```     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 ereal_SUPI)
```
```    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 `y \<ge> 0` by auto
```
```    28     have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `x > y` f_fin approx[where e = 1] by auto
```
```    29     def e \<equiv> "real ((x - y) / 2)"
```
```    30     have e: "x > y + e" "e > 0" using `x > y` y_fin x_fin by (auto simp: e_def field_simps)
```
```    31     note e(1)
```
```    32     also from approx[OF `e > 0`] 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 ereal_INFI)
```
```    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 `y \<noteq> \<infinity>` by auto
```
```    57     have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
```
```    58       apply auto by (metis ereal_infty_less_eq(2) f_le_y)
```
```    59     def e \<equiv> "real ((y - x) / 2)"
```
```    60     have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
```
```    61     from approx[OF `e > 0`] 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 `e > 0`
```
```    82     by (intro ereal_INFI)
```
```    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 `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
```
```   100     by (intro ereal_SUPI)
```
```   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::{enumerable_basis, 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::"nat \<Rightarrow> 'a"  . 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[OF this]
```
```   131     have x: "space M = (\<Union>n. cball (x n) r)"
```
```   132       by (auto simp add: sU) (metis dist_commute order_less_imp_le)
```
```   133     have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r))"
```
```   134       by (rule Lim_emeasure_incseq)
```
```   135         (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
```
```   136     also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
```
```   137       unfolding x by force
```
```   138     finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
```
```   139   } note M_space = this
```
```   140   {
```
```   141     fix e ::real and n :: nat assume "e > 0" "n > 0"
```
```   142     hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
```
```   143     from M_space[OF `1/n>0`]
```
```   144     have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
```
```   145       unfolding emeasure_eq_measure by simp
```
```   146     from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
```
```   147     obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
```
```   148       e * 2 powr -n"
```
```   149       by auto
```
```   150     hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
```
```   151       measure M (space M) - e * 2 powr -real n"
```
```   152       by (auto simp: dist_real_def)
```
```   153     hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
```
```   154       measure M (space M) - e * 2 powr - real n" ..
```
```   155   } note k=this
```
```   156   hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
```
```   157     measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
```
```   158     by blast
```
```   159   then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
```
```   160     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
```
```   161     apply atomize_elim unfolding bchoice_iff .
```
```   162   hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
```
```   163     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
```
```   164     unfolding Ball_def by blast
```
```   165   have approx_space:
```
```   166     "\<And>e. e > 0 \<Longrightarrow>
```
```   167       \<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
```
```   168       (is "\<And>e. _ \<Longrightarrow> ?thesis e")
```
```   169   proof -
```
```   170     fix e :: real assume "e > 0"
```
```   171     def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
```
```   172     have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
```
```   173     hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
```
```   174     from k[OF `e > 0` zero_less_Suc]
```
```   175     have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"
```
```   176       by (simp add: algebra_simps B_def finite_measure_compl)
```
```   177     hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"
```
```   178       by (simp add: finite_measure_compl)
```
```   179     def K \<equiv> "\<Inter>n. B n"
```
```   180     from `closed (B _)` have "closed K" by (auto simp: K_def)
```
```   181     hence [simp]: "K \<in> sets M" by (simp add: sb)
```
```   182     have "measure M (space M) - measure M K = measure M (space M - K)"
```
```   183       by (simp add: finite_measure_compl)
```
```   184     also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
```
```   185     also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
```
```   186       by (rule emeasure_subadditive_countably) (auto simp: summable_def)
```
```   187     also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
```
```   188       using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
```
```   189     also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
```
```   190       by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
```
```   191     also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
```
```   192       unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
```
```   193       by simp
```
```   194     also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
```
```   195       by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
```
```   196     also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
```
```   197     finally have "measure M (space M) \<le> measure M K + e" by simp
```
```   198     hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure)
```
```   199     moreover have "compact K"
```
```   200       unfolding compact_eq_totally_bounded
```
```   201     proof safe
```
```   202       show "complete K" using `closed K` by (simp add: complete_eq_closed)
```
```   203       fix e'::real assume "0 < e'"
```
```   204       from nat_approx_posE[OF this] guess n . note n = this
```
```   205       let ?k = "x ` {0..k e (Suc n)}"
```
```   206       have "finite ?k" by simp
```
```   207       moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
```
```   208       ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
```
```   209     qed
```
```   210     ultimately
```
```   211     show "?thesis e " by (auto simp: sU)
```
```   212   qed
```
```   213   { fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
```
```   214     hence [simp]: "A \<in> sets M" by (simp add: sb)
```
```   215     have "?inner A"
```
```   216     proof (rule approx_inner)
```
```   217       fix e::real assume "e > 0"
```
```   218       from approx_space[OF this] obtain K where
```
```   219         K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"
```
```   220         by (auto simp: emeasure_eq_measure)
```
```   221       hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)
```
```   222       have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)"
```
```   223         by (simp add: emeasure_eq_measure)
```
```   224       also have "\<dots> = measure M (A - A \<inter> K)"
```
```   225         by (subst finite_measure_Diff) auto
```
```   226       also have "A - A \<inter> K = A \<union> K - K" by auto
```
```   227       also have "measure M \<dots> = measure M (A \<union> K) - measure M K"
```
```   228         by (subst finite_measure_Diff) auto
```
```   229       also have "\<dots> \<le> measure M (space M) - measure M K"
```
```   230         by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
```
```   231       also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure)
```
```   232       finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e"
```
```   233         by (simp add: emeasure_eq_measure algebra_simps)
```
```   234       moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using `closed A` `compact K` by auto
```
```   235       ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
```
```   236         by blast
```
```   237     qed simp
```
```   238     have "?outer A"
```
```   239     proof cases
```
```   240       assume "A \<noteq> {}"
```
```   241       let ?G = "\<lambda>d. {x. infdist x A < d}"
```
```   242       {
```
```   243         fix d
```
```   244         have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
```
```   245         also have "open \<dots>"
```
```   246           by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
```
```   247         finally have "open (?G d)" .
```
```   248       } note open_G = this
```
```   249       from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
```
```   250       have "A = {x. infdist x A = 0}" by auto
```
```   251       also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
```
```   252       proof (auto, rule ccontr)
```
```   253         fix x
```
```   254         assume "infdist x A \<noteq> 0"
```
```   255         hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
```
```   256         from nat_approx_posE[OF this] guess n .
```
```   257         moreover
```
```   258         assume "\<forall>i. infdist x A < 1 / real (Suc i)"
```
```   259         hence "infdist x A < 1 / real (Suc n)" by auto
```
```   260         ultimately show False by simp
```
```   261       qed
```
```   262       also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
```
```   263       proof (rule INF_emeasure_decseq[symmetric], safe)
```
```   264         fix i::nat
```
```   265         from open_G[of "1 / real (Suc i)"]
```
```   266         show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
```
```   267       next
```
```   268         show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
```
```   269           by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
```
```   270             simp: decseq_def le_eq_less_or_eq)
```
```   271       qed simp
```
```   272       finally
```
```   273       have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
```
```   274       moreover
```
```   275       have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
```
```   276       proof (intro INF_mono)
```
```   277         fix m
```
```   278         have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
```
```   279         moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp
```
```   280         ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.
```
```   281           emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"
```
```   282           by blast
```
```   283       qed
```
```   284       moreover
```
```   285       have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
```
```   286         by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
```
```   287       ultimately show ?thesis by simp
```
```   288     qed (auto intro!: ereal_INFI)
```
```   289     note `?inner A` `?outer A` }
```
```   290   note closed_in_D = this
```
```   291   from `B \<in> sets borel`
```
```   292   have "Int_stable (Collect closed)" "Collect closed \<subseteq> Pow UNIV" "B \<in> sigma_sets UNIV (Collect closed)"
```
```   293     by (auto simp: Int_stable_def borel_eq_closed)
```
```   294   then show "?inner B" "?outer B"
```
```   295   proof (induct B rule: sigma_sets_induct_disjoint)
```
```   296     case empty
```
```   297     { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
```
```   298     { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
```
```   299   next
```
```   300     case (basic B)
```
```   301     { case 1 from basic closed_in_D show ?case by auto }
```
```   302     { case 2 from basic closed_in_D show ?case by auto }
```
```   303   next
```
```   304     case (compl B)
```
```   305     note inner = compl(2) and outer = compl(3)
```
```   306     from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed)
```
```   307     case 2
```
```   308     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
```
```   309     also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
```
```   310       unfolding inner by (subst INFI_ereal_cminus) force+
```
```   311     also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
```
```   312       by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
```
```   313     also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
```
```   314       by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
```
```   315     also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
```
```   316         (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
```
```   317       by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
```
```   318          (rule INF_cong, auto simp add: sU intro!: INF_cong)
```
```   319     finally have
```
```   320       "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
```
```   321     moreover have
```
```   322       "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
```
```   323       by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
```
```   324     ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
```
```   325
```
```   326     case 1
```
```   327     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
```
```   328     also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
```
```   329       unfolding outer by (subst SUPR_ereal_cminus) auto
```
```   330     also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
```
```   331       by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
```
```   332     also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
```
```   333       by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
```
```   334          (rule SUP_cong, auto simp: sU)
```
```   335     also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
```
```   336     proof (safe intro!: antisym SUP_least)
```
```   337       fix K assume "closed K" "K \<subseteq> space M - B"
```
```   338       from closed_in_D[OF `closed K`]
```
```   339       have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
```
```   340       show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
```
```   341         unfolding K_inner using `K \<subseteq> space M - B`
```
```   342         by (auto intro!: SUP_upper SUP_least)
```
```   343     qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
```
```   344     finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
```
```   345   next
```
```   346     case (union D)
```
```   347     then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed)
```
```   348     with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure)
```
```   349     also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
```
```   350       by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
```
```   351     finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
```
```   352       by (simp add: emeasure_eq_measure)
```
```   353     have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
```
```   354
```
```   355     case 1
```
```   356     show ?case
```
```   357     proof (rule approx_inner)
```
```   358       fix e::real assume "e > 0"
```
```   359       with measure_LIMSEQ
```
```   360       have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i = 0..<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
```
```   361         by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
```
```   362       hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
```
```   363       then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
```
```   364         unfolding choice_iff by blast
```
```   365       have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))"
```
```   366         by (auto simp add: emeasure_eq_measure)
```
```   367       also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto
```
```   368       also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
```
```   369       also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
```
```   370       also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
```
```   371       finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2"
```
```   372         using n0 by auto
```
```   373       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)"
```
```   374       proof
```
```   375         fix i
```
```   376         from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
```
```   377         have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
```
```   378           using union by blast
```
```   379         from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
```
```   380         show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
```
```   381           by (auto simp: emeasure_eq_measure)
```
```   382       qed
```
```   383       then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
```
```   384         "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
```
```   385         unfolding choice_iff by blast
```
```   386       let ?K = "\<Union>i\<in>{0..<n0}. K i"
```
```   387       have "disjoint_family_on K {0..<n0}" using K `disjoint_family D`
```
```   388         unfolding disjoint_family_on_def by blast
```
```   389       hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K
```
```   390         by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
```
```   391       have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
```
```   392       also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
```
```   393         using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
```
```   394       also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))"
```
```   395         by (simp add: setsum.distrib)
```
```   396       also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) +  e / 2" using `0 < e`
```
```   397         by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono)
```
```   398       finally
```
```   399       have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2"
```
```   400         by auto
```
```   401       hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
```
```   402       moreover
```
```   403       have "?K \<subseteq> (\<Union>i. D i)" using K by auto
```
```   404       moreover
```
```   405       have "compact ?K" using K by auto
```
```   406       ultimately
```
```   407       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
```
```   408       thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
```
```   409     qed fact
```
```   410     case 2
```
```   411     show ?case
```
```   412     proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`])
```
```   413       fix e::real assume "e > 0"
```
```   414       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)"
```
```   415       proof
```
```   416         fix i::nat
```
```   417         from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
```
```   418         have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
```
```   419           using union by blast
```
```   420         from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
```
```   421         show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
```
```   422           by (auto simp: emeasure_eq_measure)
```
```   423       qed
```
```   424       then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
```
```   425         "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
```
```   426         unfolding choice_iff by blast
```
```   427       let ?U = "\<Union>i. U i"
```
```   428       have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  `(\<Union>i. D i) \<in> sets M`
```
```   429         by (subst emeasure_Diff) (auto simp: sb)
```
```   430       also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  `range D \<subseteq> sets M`
```
```   431         by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
```
```   432       also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  `range D \<subseteq> sets M`
```
```   433         by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
```
```   434       also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
```
```   435         by (intro suminf_le_pos, subst emeasure_Diff)
```
```   436            (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
```
```   437       also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
```
```   438         by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
```
```   439       also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^  Suc n))"
```
```   440         unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
```
```   441         by simp
```
```   442       also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
```
```   443         by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
```
```   444       also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
```
```   445       finally
```
```   446       have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
```
```   447       moreover
```
```   448       have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
```
```   449       moreover
```
```   450       have "open ?U" using U by auto
```
```   451       ultimately
```
```   452       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
```
```   453       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" ..
```
```   454     qed
```
```   455   qed
```
```   456 qed
```
```   457
```
```   458 end
```
```   459
```