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.127 +      (force, metis add.comm_neutral add_left_mono ereal_less(1)
   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 +