src/HOL/Probability/Regularity.thy
 changeset 50087 635d73673b5e child 50089 1badf63e5d97
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Probability/Regularity.thy	Thu Nov 15 10:49:58 2012 +0100
1.3 @@ -0,0 +1,516 @@
1.4 +(*  Title:      HOL/Probability/Projective_Family.thy
1.5 +    Author:     Fabian Immler, TU München
1.6 +*)
1.7 +
1.8 +theory Regularity
1.9 +imports Measure_Space Borel_Space
1.10 +begin
1.11 +
1.12 +instantiation nat::topological_space
1.13 +begin
1.14 +
1.15 +definition open_nat::"nat set \<Rightarrow> bool"
1.16 +  where "open_nat s = True"
1.17 +
1.18 +instance proof qed (auto simp: open_nat_def)
1.19 +end
1.20 +
1.21 +instantiation nat::metric_space
1.22 +begin
1.23 +
1.24 +definition dist_nat::"nat \<Rightarrow> nat \<Rightarrow> real"
1.25 +  where "dist_nat n m = (if n = m then 0 else 1)"
1.26 +
1.27 +instance proof qed (auto simp: open_nat_def dist_nat_def intro: exI[where x=1])
1.28 +end
1.29 +
1.30 +instance nat::complete_space
1.31 +proof
1.32 +  fix X::"nat\<Rightarrow>nat" assume "Cauchy X"
1.33 +  hence "\<exists>n. \<forall>m\<ge>n. X m = X n"
1.34 +    by (force simp: dist_nat_def Cauchy_def split: split_if_asm dest:spec[where x=1])
1.35 +  then guess n ..
1.36 +  thus "convergent X"
1.37 +    apply (intro convergentI[where L="X n"] tendstoI)
1.38 +    unfolding eventually_sequentially dist_nat_def
1.39 +    apply (intro exI[where x=n])
1.40 +    apply (intro allI)
1.41 +    apply (drule_tac x=na in spec)
1.42 +    apply simp
1.43 +    done
1.44 +qed
1.45 +
1.46 +instance nat::enumerable_basis
1.47 +proof
1.48 +  have "topological_basis (range (\<lambda>n::nat. {n}))"
1.49 +    by (intro topological_basisI) (auto simp: open_nat_def)
1.50 +  thus "\<exists>f::nat\<Rightarrow>nat set. topological_basis (range f)" by blast
1.51 +qed
1.52 +
1.53 +subsection {* Regularity of Measures *}
1.54 +
1.55 +lemma ereal_approx_SUP:
1.56 +  fixes x::ereal
1.57 +  assumes A_notempty: "A \<noteq> {}"
1.58 +  assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
1.59 +  assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
1.60 +  assumes f_nonneg: "\<And>i. 0 \<le> f i"
1.61 +  assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
1.62 +  shows "x = (SUP i : A. f i)"
1.63 +proof (subst eq_commute, rule ereal_SUPI)
1.64 +  show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
1.65 +next
1.66 +  fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
1.67 +  with A_notempty f_nonneg have "y \<ge> 0" by auto (metis order_trans)
1.68 +  show "x \<le> y"
1.69 +  proof (rule ccontr)
1.70 +    assume "\<not> x \<le> y" hence "x > y" by simp
1.71 +    hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<ge> 0` by auto
1.72 +    have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `x > y` f_fin approx[where e = 1] by auto
1.73 +    def e \<equiv> "real ((x - y) / 2)"
1.74 +    have e: "x > y + e" "e > 0" using `x > y` y_fin x_fin by (auto simp: e_def field_simps)
1.75 +    note e(1)
1.76 +    also from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x \<le> f i + e" by blast
1.77 +    note i(2)
1.78 +    finally have "y < f i" using y_fin f_fin by (metis add_right_mono linorder_not_le)
1.79 +    moreover have "f i \<le> y" by (rule f_le_y) fact
1.80 +    ultimately show False by simp
1.81 +  qed
1.82 +qed
1.83 +
1.84 +lemma ereal_approx_INF:
1.85 +  fixes x::ereal
1.86 +  assumes A_notempty: "A \<noteq> {}"
1.87 +  assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
1.88 +  assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
1.89 +  assumes f_nonneg: "\<And>i. 0 \<le> f i"
1.90 +  assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
1.91 +  shows "x = (INF i : A. f i)"
1.92 +proof (subst eq_commute, rule ereal_INFI)
1.93 +  show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
1.94 +next
1.95 +  fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
1.96 +  with A_notempty f_fin have "y \<noteq> \<infinity>" by force
1.97 +  show "y \<le> x"
1.98 +  proof (rule ccontr)
1.99 +    assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
1.100 +    hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<noteq> \<infinity>` by auto
1.101 +    have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
1.102 +      apply auto by (metis ereal_infty_less_eq(2) f_le_y)
1.103 +    def e \<equiv> "real ((y - x) / 2)"
1.104 +    have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
1.105 +    from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast
1.106 +    note i(2)
1.107 +    also note e(1)
1.108 +    finally have "y > f i" .
1.109 +    moreover have "y \<le> f i" by (rule f_le_y) fact
1.110 +    ultimately show False by simp
1.111 +  qed
1.112 +qed
1.113 +
1.114 +lemma INF_approx_ereal:
1.115 +  fixes x::ereal and e::real
1.116 +  assumes "e > 0"
1.117 +  assumes INF: "x = (INF i : A. f i)"
1.118 +  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
1.119 +  shows "\<exists>i \<in> A. f i < x + e"
1.120 +proof (rule ccontr, clarsimp)
1.121 +  assume "\<forall>i\<in>A. \<not> f i < x + e"
1.122 +  moreover
1.123 +  from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
1.124 +  ultimately
1.125 +  have "(INF i : A. f i) = x + e" using `e > 0`
1.126 +    by (intro ereal_INFI)
1.128 +        linorder_not_le not_less_iff_gr_or_eq)
1.129 +  thus False using assms by auto
1.130 +qed
1.131 +
1.132 +lemma SUP_approx_ereal:
1.133 +  fixes x::ereal and e::real
1.134 +  assumes "e > 0"
1.135 +  assumes SUP: "x = (SUP i : A. f i)"
1.136 +  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
1.137 +  shows "\<exists>i \<in> A. x \<le> f i + e"
1.138 +proof (rule ccontr, clarsimp)
1.139 +  assume "\<forall>i\<in>A. \<not> x \<le> f i + e"
1.140 +  moreover
1.141 +  from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
1.142 +  ultimately
1.143 +  have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
1.144 +    by (intro ereal_SUPI)
1.145 +       (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
1.146 +        metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
1.147 +  thus False using assms by auto
1.148 +qed
1.149 +
1.150 +lemma
1.151 +  fixes M::"'a::{enumerable_basis, complete_space} measure"
1.152 +  assumes sb: "sets M = sets borel"
1.153 +  assumes "emeasure M (space M) \<noteq> \<infinity>"
1.154 +  assumes "B \<in> sets borel"
1.155 +  shows inner_regular: "emeasure M B =
1.156 +    (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
1.157 +  and outer_regular: "emeasure M B =
1.158 +    (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
1.159 +proof -
1.160 +  have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
1.161 +  hence sU: "space M = UNIV" by simp
1.162 +  interpret finite_measure M by rule fact
1.163 +  have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow>
1.164 +    (\<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"
1.165 +    by (rule ereal_approx_SUP)
1.166 +      (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
1.167 +  have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow>
1.168 +    (\<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"
1.169 +    by (rule ereal_approx_INF)
1.170 +       (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
1.171 +  from countable_dense_setE guess x::"nat \<Rightarrow> 'a"  . note x = this
1.172 +  {
1.173 +    fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
1.174 +    with x[OF this]
1.175 +    have x: "space M = (\<Union>n. cball (x n) r)"
1.176 +      by (auto simp add: sU) (metis dist_commute order_less_imp_le)
1.177 +    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))"
1.178 +      by (rule Lim_emeasure_incseq)
1.179 +        (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
1.180 +    also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
1.181 +      unfolding x by force
1.182 +    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
1.183 +  } note M_space = this
1.184 +  {
1.185 +    fix e ::real and n :: nat assume "e > 0" "n > 0"
1.186 +    hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
1.187 +    from M_space[OF `1/n>0`]
1.188 +    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
1.189 +      unfolding emeasure_eq_measure by simp
1.190 +    from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
1.191 +    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
1.192 +      e * 2 powr -n"
1.193 +      by auto
1.194 +    hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
1.195 +      measure M (space M) - e * 2 powr -real n"
1.196 +      by (auto simp: dist_real_def)
1.197 +    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
1.198 +      measure M (space M) - e * 2 powr - real n" ..
1.199 +  } note k=this
1.200 +  hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
1.201 +    measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
1.202 +    by blast
1.203 +  then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
1.204 +    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
1.205 +    apply atomize_elim unfolding bchoice_iff .
1.206 +  hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
1.207 +    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
1.208 +    unfolding Ball_def by blast
1.209 +  have approx_space:
1.210 +    "\<And>e. e > 0 \<Longrightarrow>
1.211 +      \<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
1.212 +      (is "\<And>e. _ \<Longrightarrow> ?thesis e")
1.213 +  proof -
1.214 +    fix e :: real assume "e > 0"
1.215 +    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
1.216 +    have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
1.217 +    hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
1.218 +    from k[OF `e > 0` zero_less_Suc]
1.219 +    have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"
1.220 +      by (simp add: algebra_simps B_def finite_measure_compl)
1.221 +    hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"
1.222 +      by (simp add: finite_measure_compl)
1.223 +    def K \<equiv> "\<Inter>n. B n"
1.224 +    from `closed (B _)` have "closed K" by (auto simp: K_def)
1.225 +    hence [simp]: "K \<in> sets M" by (simp add: sb)
1.226 +    have "measure M (space M) - measure M K = measure M (space M - K)"
1.227 +      by (simp add: finite_measure_compl)
1.228 +    also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
1.229 +    also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
1.230 +      by (rule emeasure_subadditive_countably) (auto simp: summable_def)
1.231 +    also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
1.232 +      using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
1.233 +    also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
1.234 +      by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
1.235 +    also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
1.236 +      unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
1.237 +      by simp
1.238 +    also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
1.239 +      by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
1.240 +    also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
1.241 +    finally have "measure M (space M) \<le> measure M K + e" by simp
1.242 +    hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure)
1.243 +    moreover have "compact K"
1.244 +      unfolding compact_eq_totally_bounded
1.245 +    proof safe
1.246 +      show "complete K" using `closed K` by (simp add: complete_eq_closed)
1.247 +      fix e'::real assume "0 < e'"
1.248 +      from nat_approx_posE[OF this] guess n . note n = this
1.249 +      let ?k = "x ` {0..k e (Suc n)}"
1.250 +      have "finite ?k" by simp
1.251 +      moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
1.252 +      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
1.253 +    qed
1.254 +    ultimately
1.255 +    show "?thesis e " by (auto simp: sU)
1.256 +  qed
1.257 +  have closed_in_D: "\<And>A. closed A \<Longrightarrow> ?inner A \<and> ?outer A"
1.258 +  proof
1.259 +    fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
1.260 +    hence [simp]: "A \<in> sets M" by (simp add: sb)
1.261 +    show "?inner A"
1.262 +    proof (rule approx_inner)
1.263 +      fix e::real assume "e > 0"
1.264 +      from approx_space[OF this] obtain K where
1.265 +        K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"
1.266 +        by (auto simp: emeasure_eq_measure)
1.267 +      hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)
1.268 +      have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)"
1.269 +        by (simp add: emeasure_eq_measure)
1.270 +      also have "\<dots> = measure M (A - A \<inter> K)"
1.271 +        by (subst finite_measure_Diff) auto
1.272 +      also have "A - A \<inter> K = A \<union> K - K" by auto
1.273 +      also have "measure M \<dots> = measure M (A \<union> K) - measure M K"
1.274 +        by (subst finite_measure_Diff) auto
1.275 +      also have "\<dots> \<le> measure M (space M) - measure M K"
1.276 +        by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
1.277 +      also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure)
1.278 +      finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e"
1.279 +        by (simp add: emeasure_eq_measure algebra_simps)
1.280 +      moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using `closed A` `compact K` by auto
1.281 +      ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
1.282 +        by blast
1.283 +    qed simp
1.284 +    show "?outer A"
1.285 +    proof cases
1.286 +      assume "A \<noteq> {}"
1.287 +      let ?G = "\<lambda>d. {x. infdist x A < d}"
1.288 +      {
1.289 +        fix d
1.290 +        have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
1.291 +        also have "open \<dots>"
1.292 +          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
1.293 +        finally have "open (?G d)" .
1.294 +      } note open_G = this
1.295 +      from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
1.296 +      have "A = {x. infdist x A = 0}" by auto
1.297 +      also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
1.298 +      proof (auto, rule ccontr)
1.299 +        fix x
1.300 +        assume "infdist x A \<noteq> 0"
1.301 +        hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
1.302 +        from nat_approx_posE[OF this] guess n .
1.303 +        moreover
1.304 +        assume "\<forall>i. infdist x A < 1 / real (Suc i)"
1.305 +        hence "infdist x A < 1 / real (Suc n)" by auto
1.306 +        ultimately show False by simp
1.307 +      qed
1.308 +      also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
1.309 +      proof (rule INF_emeasure_decseq[symmetric], safe)
1.310 +        fix i::nat
1.311 +        from open_G[of "1 / real (Suc i)"]
1.312 +        show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
1.313 +      next
1.314 +        show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
1.315 +          by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
1.316 +            simp: decseq_def le_eq_less_or_eq)
1.317 +      qed simp
1.318 +      finally
1.319 +      have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
1.320 +      moreover
1.321 +      have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
1.322 +      proof (intro INF_mono)
1.323 +        fix m
1.324 +        have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
1.325 +        moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp
1.326 +        ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.
1.327 +          emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"
1.328 +          by blast
1.329 +      qed
1.330 +      moreover
1.331 +      have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
1.332 +        by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
1.333 +      ultimately show ?thesis by simp
1.334 +    qed (auto intro!: ereal_INFI)
1.335 +  qed
1.336 +  let ?D = "{B \<in> sets M. ?inner B \<and> ?outer B}"
1.337 +  interpret dynkin: dynkin_system "space M" ?D
1.338 +  proof (rule dynkin_systemI)
1.339 +    have "{U::'a set. space M \<subseteq> U \<and> open U} = {space M}" by (auto simp add: sU)
1.340 +    hence "?outer (space M)" by (simp add: min_def INF_def)
1.341 +    moreover
1.342 +    have "?inner (space M)"
1.343 +    proof (rule ereal_approx_SUP)
1.344 +      fix e::real assume "0 < e"
1.345 +      thus "\<exists>K\<in>{K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
1.346 +        by (rule approx_space)
1.347 +    qed (auto intro: emeasure_mono simp: sU sb intro!: exI[where x="{}"])
1.348 +    ultimately show "space M \<in> ?D" by (simp add: sU sb)
1.349 +  next
1.350 +    fix B assume "B \<in> ?D" thus "B \<subseteq> space M" by (simp add: sU)
1.351 +    from `B \<in> ?D` have [simp]: "B \<in> sets M" and "?inner B" "?outer B" by auto
1.352 +    hence inner: "emeasure M B = (SUP K:{K. K \<subseteq> B \<and> compact K}. emeasure M K)"
1.353 +      and outer: "emeasure M B = (INF U:{U. B \<subseteq> U \<and> open U}. emeasure M U)" by auto
1.354 +    have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
1.355 +    also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
1.356 +      unfolding inner by (subst INFI_ereal_cminus) force+
1.357 +    also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
1.358 +      by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
1.359 +    also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
1.360 +      by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
1.361 +    also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
1.362 +      (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
1.363 +      by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
1.364 +         (rule INF_cong, auto simp add: sU intro!: INF_cong)
1.365 +    finally have
1.366 +      "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
1.367 +    moreover have
1.368 +      "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
1.369 +      by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
1.370 +    ultimately have "?outer (space M - B)" by simp
1.371 +    moreover
1.372 +    {
1.373 +      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
1.374 +      also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
1.375 +        unfolding outer by (subst SUPR_ereal_cminus) auto
1.376 +      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
1.377 +        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
1.378 +      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
1.379 +        by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
1.380 +           (rule SUP_cong, auto simp: sU)
1.381 +      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
1.382 +      proof (safe intro!: antisym SUP_least)
1.383 +        fix K assume "closed K" "K \<subseteq> space M - B"
1.384 +        from closed_in_D[OF `closed K`]
1.385 +        have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
1.386 +        show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
1.387 +          unfolding K_inner using `K \<subseteq> space M - B`
1.388 +          by (auto intro!: SUP_upper SUP_least)
1.389 +      qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
1.390 +      finally have "?inner (space M - B)" .
1.391 +    } hence "?inner (space M - B)" .
1.392 +    ultimately show "space M - B \<in> ?D" by auto
1.393 +  next
1.394 +    fix D :: "nat \<Rightarrow> _"
1.395 +    assume "range D \<subseteq> ?D" hence "range D \<subseteq> sets M" by auto
1.396 +    moreover assume "disjoint_family D"
1.397 +    ultimately have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure)
1.398 +    also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
1.399 +      by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
1.400 +    finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
1.401 +      by (simp add: emeasure_eq_measure)
1.402 +    have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
1.403 +    moreover
1.404 +    hence "?inner (\<Union>i. D i)"
1.405 +    proof (rule approx_inner)
1.406 +      fix e::real assume "e > 0"
1.407 +      with measure_LIMSEQ
1.408 +      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"
1.409 +        by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
1.410 +      hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
1.411 +      then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
1.412 +        unfolding choice_iff by blast
1.413 +      have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))"
1.414 +        by (auto simp add: emeasure_eq_measure)
1.415 +      also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto
1.416 +      also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
1.417 +      also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
1.418 +      also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
1.419 +      finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2"
1.420 +        using n0 by auto
1.421 +      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)"
1.422 +      proof
1.423 +        fix i
1.424 +        from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
1.425 +        have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
1.426 +          using `range D \<subseteq> ?D` by blast
1.427 +        from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
1.428 +        show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
1.429 +          by (auto simp: emeasure_eq_measure)
1.430 +      qed
1.431 +      then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
1.432 +        "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
1.433 +        unfolding choice_iff by blast
1.434 +      let ?K = "\<Union>i\<in>{0..<n0}. K i"
1.435 +      have "disjoint_family_on K {0..<n0}" using K `disjoint_family D`
1.436 +        unfolding disjoint_family_on_def by blast
1.437 +      hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K
1.438 +        by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
1.439 +      have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
1.440 +      also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
1.441 +        using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
1.442 +      also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))"
1.443 +        by (simp add: setsum.distrib)
1.444 +      also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) +  e / 2" using `0 < e`
1.445 +        by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono)
1.446 +      finally
1.447 +      have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2"
1.448 +        by auto
1.449 +      hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
1.450 +      moreover
1.451 +      have "?K \<subseteq> (\<Union>i. D i)" using K by auto
1.452 +      moreover
1.453 +      have "compact ?K" using K by auto
1.454 +      ultimately
1.455 +      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
1.456 +      thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
1.457 +    qed
1.458 +    moreover have "?outer (\<Union>i. D i)"
1.459 +    proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`])
1.460 +      fix e::real assume "e > 0"
1.461 +      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)"
1.462 +      proof
1.463 +        fix i::nat
1.464 +        from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
1.465 +        have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
1.466 +          using `range D \<subseteq> ?D` by blast
1.467 +        from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
1.468 +        show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
1.469 +          by (auto simp: emeasure_eq_measure)
1.470 +      qed
1.471 +      then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
1.472 +        "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
1.473 +        unfolding choice_iff by blast
1.474 +      let ?U = "\<Union>i. U i"
1.475 +      have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  `(\<Union>i. D i) \<in> sets M`
1.476 +        by (subst emeasure_Diff) (auto simp: sb)
1.477 +      also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  `range D \<subseteq> sets M`
1.478 +        by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
1.479 +      also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  `range D \<subseteq> sets M`
1.480 +        by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
1.481 +      also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
1.482 +        by (intro suminf_le_pos, subst emeasure_Diff)
1.483 +           (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
1.484 +      also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
1.485 +        by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
1.486 +      also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^  Suc n))"
1.487 +        unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
1.488 +        by simp
1.489 +      also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
1.490 +        by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
1.491 +      also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
1.492 +      finally
1.493 +      have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
1.494 +      moreover
1.495 +      have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
1.496 +      moreover
1.497 +      have "open ?U" using U by auto
1.498 +      ultimately
1.499 +      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
1.500 +      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" ..
1.501 +    qed
1.502 +    ultimately show "(\<Union>i. D i) \<in> ?D" by safe
1.503 +  qed
1.504 +  have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU)
1.505 +  also have "\<dots> = dynkin (space M) (Collect closed)"
1.506 +  proof (rule sigma_eq_dynkin)
1.507 +    show "Collect closed \<subseteq> Pow (space M)" using Sigma_Algebra.sets_into_space by (auto simp: sU)
1.508 +    show "Int_stable (Collect closed)" by (auto simp: Int_stable_def)
1.509 +  qed
1.510 +  also have "\<dots> \<subseteq> ?D" using closed_in_D
1.511 +    by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
1.512 +  finally have "sets borel \<subseteq> ?D" .
1.513 +  moreover have "?D \<subseteq> sets borel" by (auto simp: sb)
1.514 +  ultimately have "sets borel = ?D" by simp
1.515 +  with assms show "?inner B" and "?outer B" by auto
1.516 +qed
1.517 +
1.518 +end
1.519 +
```