src/HOL/Probability/Regularity.thy
author immler
Thu Nov 15 10:49:58 2012 +0100 (2012-11-15)
changeset 50087 635d73673b5e
child 50089 1badf63e5d97
permissions -rw-r--r--
regularity of measures, therefore:
characterization of closure with infimum distance;
characterize of compact sets as totally bounded;
added Diagonal_Subsequence to Library;
introduced (enumerable) topological basis;
rational boxes as basis of ordered euclidean space;
moved some lemmas upwards
     1 (*  Title:      HOL/Probability/Projective_Family.thy
     2     Author:     Fabian Immler, TU M√ľnchen
     3 *)
     4 
     5 theory Regularity
     6 imports Measure_Space Borel_Space
     7 begin
     8 
     9 instantiation nat::topological_space
    10 begin
    11 
    12 definition open_nat::"nat set \<Rightarrow> bool"
    13   where "open_nat s = True"
    14 
    15 instance proof qed (auto simp: open_nat_def)
    16 end
    17 
    18 instantiation nat::metric_space
    19 begin
    20 
    21 definition dist_nat::"nat \<Rightarrow> nat \<Rightarrow> real"
    22   where "dist_nat n m = (if n = m then 0 else 1)"
    23 
    24 instance proof qed (auto simp: open_nat_def dist_nat_def intro: exI[where x=1])
    25 end
    26 
    27 instance nat::complete_space
    28 proof
    29   fix X::"nat\<Rightarrow>nat" assume "Cauchy X"
    30   hence "\<exists>n. \<forall>m\<ge>n. X m = X n"
    31     by (force simp: dist_nat_def Cauchy_def split: split_if_asm dest:spec[where x=1])
    32   then guess n ..
    33   thus "convergent X"
    34     apply (intro convergentI[where L="X n"] tendstoI)
    35     unfolding eventually_sequentially dist_nat_def
    36     apply (intro exI[where x=n])
    37     apply (intro allI)
    38     apply (drule_tac x=na in spec)
    39     apply simp
    40     done
    41 qed
    42 
    43 instance nat::enumerable_basis
    44 proof
    45   have "topological_basis (range (\<lambda>n::nat. {n}))"
    46     by (intro topological_basisI) (auto simp: open_nat_def)
    47   thus "\<exists>f::nat\<Rightarrow>nat set. topological_basis (range f)" by blast
    48 qed
    49 
    50 subsection {* Regularity of Measures *}
    51 
    52 lemma ereal_approx_SUP:
    53   fixes x::ereal
    54   assumes A_notempty: "A \<noteq> {}"
    55   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
    56   assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
    57   assumes f_nonneg: "\<And>i. 0 \<le> f i"
    58   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
    59   shows "x = (SUP i : A. f i)"
    60 proof (subst eq_commute, rule ereal_SUPI)
    61   show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
    62 next
    63   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
    64   with A_notempty f_nonneg have "y \<ge> 0" by auto (metis order_trans)
    65   show "x \<le> y"
    66   proof (rule ccontr)
    67     assume "\<not> x \<le> y" hence "x > y" by simp
    68     hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<ge> 0` by auto
    69     have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `x > y` f_fin approx[where e = 1] by auto
    70     def e \<equiv> "real ((x - y) / 2)"
    71     have e: "x > y + e" "e > 0" using `x > y` y_fin x_fin by (auto simp: e_def field_simps)
    72     note e(1)
    73     also from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x \<le> f i + e" by blast
    74     note i(2)
    75     finally have "y < f i" using y_fin f_fin by (metis add_right_mono linorder_not_le)
    76     moreover have "f i \<le> y" by (rule f_le_y) fact
    77     ultimately show False by simp
    78   qed
    79 qed
    80 
    81 lemma ereal_approx_INF:
    82   fixes x::ereal
    83   assumes A_notempty: "A \<noteq> {}"
    84   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
    85   assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
    86   assumes f_nonneg: "\<And>i. 0 \<le> f i"
    87   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
    88   shows "x = (INF i : A. f i)"
    89 proof (subst eq_commute, rule ereal_INFI)
    90   show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
    91 next
    92   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
    93   with A_notempty f_fin have "y \<noteq> \<infinity>" by force
    94   show "y \<le> x"
    95   proof (rule ccontr)
    96     assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
    97     hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<noteq> \<infinity>` by auto
    98     have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
    99       apply auto by (metis ereal_infty_less_eq(2) f_le_y)
   100     def e \<equiv> "real ((y - x) / 2)"
   101     have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
   102     from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast
   103     note i(2)
   104     also note e(1)
   105     finally have "y > f i" .
   106     moreover have "y \<le> f i" by (rule f_le_y) fact
   107     ultimately show False by simp
   108   qed
   109 qed
   110 
   111 lemma INF_approx_ereal:
   112   fixes x::ereal and e::real
   113   assumes "e > 0"
   114   assumes INF: "x = (INF i : A. f i)"
   115   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   116   shows "\<exists>i \<in> A. f i < x + e"
   117 proof (rule ccontr, clarsimp)
   118   assume "\<forall>i\<in>A. \<not> f i < x + e"
   119   moreover
   120   from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
   121   ultimately
   122   have "(INF i : A. f i) = x + e" using `e > 0`
   123     by (intro ereal_INFI)
   124       (force, metis add.comm_neutral add_left_mono ereal_less(1)
   125         linorder_not_le not_less_iff_gr_or_eq)
   126   thus False using assms by auto
   127 qed
   128 
   129 lemma SUP_approx_ereal:
   130   fixes x::ereal and e::real
   131   assumes "e > 0"
   132   assumes SUP: "x = (SUP i : A. f i)"
   133   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   134   shows "\<exists>i \<in> A. x \<le> f i + e"
   135 proof (rule ccontr, clarsimp)
   136   assume "\<forall>i\<in>A. \<not> x \<le> f i + e"
   137   moreover
   138   from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
   139   ultimately
   140   have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
   141     by (intro ereal_SUPI)
   142        (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
   143         metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
   144   thus False using assms by auto
   145 qed
   146 
   147 lemma
   148   fixes M::"'a::{enumerable_basis, complete_space} measure"
   149   assumes sb: "sets M = sets borel"
   150   assumes "emeasure M (space M) \<noteq> \<infinity>"
   151   assumes "B \<in> sets borel"
   152   shows inner_regular: "emeasure M B =
   153     (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
   154   and outer_regular: "emeasure M B =
   155     (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
   156 proof -
   157   have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
   158   hence sU: "space M = UNIV" by simp
   159   interpret finite_measure M by rule fact
   160   have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow>
   161     (\<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"
   162     by (rule ereal_approx_SUP)
   163       (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
   164   have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow>
   165     (\<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"
   166     by (rule ereal_approx_INF)
   167        (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
   168   from countable_dense_setE guess x::"nat \<Rightarrow> 'a"  . note x = this
   169   {
   170     fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
   171     with x[OF this]
   172     have x: "space M = (\<Union>n. cball (x n) r)"
   173       by (auto simp add: sU) (metis dist_commute order_less_imp_le)
   174     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))"
   175       by (rule Lim_emeasure_incseq)
   176         (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
   177     also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
   178       unfolding x by force
   179     finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
   180   } note M_space = this
   181   {
   182     fix e ::real and n :: nat assume "e > 0" "n > 0"
   183     hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
   184     from M_space[OF `1/n>0`]
   185     have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
   186       unfolding emeasure_eq_measure by simp
   187     from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
   188     obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
   189       e * 2 powr -n"
   190       by auto
   191     hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
   192       measure M (space M) - e * 2 powr -real n"
   193       by (auto simp: dist_real_def)
   194     hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
   195       measure M (space M) - e * 2 powr - real n" ..
   196   } note k=this
   197   hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
   198     measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
   199     by blast
   200   then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
   201     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
   202     apply atomize_elim unfolding bchoice_iff .
   203   hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
   204     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
   205     unfolding Ball_def by blast
   206   have approx_space:
   207     "\<And>e. e > 0 \<Longrightarrow>
   208       \<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
   209       (is "\<And>e. _ \<Longrightarrow> ?thesis e")
   210   proof -
   211     fix e :: real assume "e > 0"
   212     def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
   213     have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
   214     hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
   215     from k[OF `e > 0` zero_less_Suc]
   216     have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"
   217       by (simp add: algebra_simps B_def finite_measure_compl)
   218     hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"
   219       by (simp add: finite_measure_compl)
   220     def K \<equiv> "\<Inter>n. B n"
   221     from `closed (B _)` have "closed K" by (auto simp: K_def)
   222     hence [simp]: "K \<in> sets M" by (simp add: sb)
   223     have "measure M (space M) - measure M K = measure M (space M - K)"
   224       by (simp add: finite_measure_compl)
   225     also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
   226     also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"
   227       by (rule emeasure_subadditive_countably) (auto simp: summable_def)
   228     also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
   229       using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
   230     also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
   231       by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
   232     also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
   233       unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
   234       by simp
   235     also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
   236       by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
   237     also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
   238     finally have "measure M (space M) \<le> measure M K + e" by simp
   239     hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure)
   240     moreover have "compact K"
   241       unfolding compact_eq_totally_bounded
   242     proof safe
   243       show "complete K" using `closed K` by (simp add: complete_eq_closed)
   244       fix e'::real assume "0 < e'"
   245       from nat_approx_posE[OF this] guess n . note n = this
   246       let ?k = "x ` {0..k e (Suc n)}"
   247       have "finite ?k" by simp
   248       moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
   249       ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
   250     qed
   251     ultimately
   252     show "?thesis e " by (auto simp: sU)
   253   qed
   254   have closed_in_D: "\<And>A. closed A \<Longrightarrow> ?inner A \<and> ?outer A"
   255   proof
   256     fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
   257     hence [simp]: "A \<in> sets M" by (simp add: sb)
   258     show "?inner A"
   259     proof (rule approx_inner)
   260       fix e::real assume "e > 0"
   261       from approx_space[OF this] obtain K where
   262         K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"
   263         by (auto simp: emeasure_eq_measure)
   264       hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)
   265       have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)"
   266         by (simp add: emeasure_eq_measure)
   267       also have "\<dots> = measure M (A - A \<inter> K)"
   268         by (subst finite_measure_Diff) auto
   269       also have "A - A \<inter> K = A \<union> K - K" by auto
   270       also have "measure M \<dots> = measure M (A \<union> K) - measure M K"
   271         by (subst finite_measure_Diff) auto
   272       also have "\<dots> \<le> measure M (space M) - measure M K"
   273         by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
   274       also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure)
   275       finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e"
   276         by (simp add: emeasure_eq_measure algebra_simps)
   277       moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using `closed A` `compact K` by auto
   278       ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
   279         by blast
   280     qed simp
   281     show "?outer A"
   282     proof cases
   283       assume "A \<noteq> {}"
   284       let ?G = "\<lambda>d. {x. infdist x A < d}"
   285       {
   286         fix d
   287         have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
   288         also have "open \<dots>"
   289           by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
   290         finally have "open (?G d)" .
   291       } note open_G = this
   292       from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
   293       have "A = {x. infdist x A = 0}" by auto
   294       also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
   295       proof (auto, rule ccontr)
   296         fix x
   297         assume "infdist x A \<noteq> 0"
   298         hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
   299         from nat_approx_posE[OF this] guess n .
   300         moreover
   301         assume "\<forall>i. infdist x A < 1 / real (Suc i)"
   302         hence "infdist x A < 1 / real (Suc n)" by auto
   303         ultimately show False by simp
   304       qed
   305       also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
   306       proof (rule INF_emeasure_decseq[symmetric], safe)
   307         fix i::nat
   308         from open_G[of "1 / real (Suc i)"]
   309         show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
   310       next
   311         show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
   312           by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
   313             simp: decseq_def le_eq_less_or_eq)
   314       qed simp
   315       finally
   316       have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
   317       moreover
   318       have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
   319       proof (intro INF_mono)
   320         fix m
   321         have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
   322         moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp
   323         ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.
   324           emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"
   325           by blast
   326       qed
   327       moreover
   328       have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
   329         by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
   330       ultimately show ?thesis by simp
   331     qed (auto intro!: ereal_INFI)
   332   qed
   333   let ?D = "{B \<in> sets M. ?inner B \<and> ?outer B}"
   334   interpret dynkin: dynkin_system "space M" ?D
   335   proof (rule dynkin_systemI)
   336     have "{U::'a set. space M \<subseteq> U \<and> open U} = {space M}" by (auto simp add: sU)
   337     hence "?outer (space M)" by (simp add: min_def INF_def)
   338     moreover
   339     have "?inner (space M)"
   340     proof (rule ereal_approx_SUP)
   341       fix e::real assume "0 < e"
   342       thus "\<exists>K\<in>{K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
   343         by (rule approx_space)
   344     qed (auto intro: emeasure_mono simp: sU sb intro!: exI[where x="{}"])
   345     ultimately show "space M \<in> ?D" by (simp add: sU sb)
   346   next
   347     fix B assume "B \<in> ?D" thus "B \<subseteq> space M" by (simp add: sU)
   348     from `B \<in> ?D` have [simp]: "B \<in> sets M" and "?inner B" "?outer B" by auto
   349     hence inner: "emeasure M B = (SUP K:{K. K \<subseteq> B \<and> compact K}. emeasure M K)"
   350       and outer: "emeasure M B = (INF U:{U. B \<subseteq> U \<and> open U}. emeasure M U)" by auto
   351     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
   352     also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
   353       unfolding inner by (subst INFI_ereal_cminus) force+
   354     also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
   355       by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   356     also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
   357       by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
   358     also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
   359       (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
   360       by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
   361          (rule INF_cong, auto simp add: sU intro!: INF_cong)
   362     finally have
   363       "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
   364     moreover have
   365       "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
   366       by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
   367     ultimately have "?outer (space M - B)" by simp
   368     moreover
   369     {
   370       have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
   371       also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
   372         unfolding outer by (subst SUPR_ereal_cminus) auto
   373       also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
   374         by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   375       also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
   376         by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
   377            (rule SUP_cong, auto simp: sU)
   378       also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   379       proof (safe intro!: antisym SUP_least)
   380         fix K assume "closed K" "K \<subseteq> space M - B"
   381         from closed_in_D[OF `closed K`]
   382         have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
   383         show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   384           unfolding K_inner using `K \<subseteq> space M - B`
   385           by (auto intro!: SUP_upper SUP_least)
   386       qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
   387       finally have "?inner (space M - B)" .
   388     } hence "?inner (space M - B)" .
   389     ultimately show "space M - B \<in> ?D" by auto
   390   next
   391     fix D :: "nat \<Rightarrow> _"
   392     assume "range D \<subseteq> ?D" hence "range D \<subseteq> sets M" by auto
   393     moreover assume "disjoint_family D"
   394     ultimately have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure)
   395     also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
   396       by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
   397     finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
   398       by (simp add: emeasure_eq_measure)
   399     have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
   400     moreover
   401     hence "?inner (\<Union>i. D i)"
   402     proof (rule approx_inner)
   403       fix e::real assume "e > 0"
   404       with measure_LIMSEQ
   405       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"
   406         by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
   407       hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
   408       then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
   409         unfolding choice_iff by blast
   410       have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))"
   411         by (auto simp add: emeasure_eq_measure)
   412       also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto
   413       also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
   414       also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
   415       also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
   416       finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2"
   417         using n0 by auto
   418       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)"
   419       proof
   420         fix i
   421         from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
   422         have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
   423           using `range D \<subseteq> ?D` by blast
   424         from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
   425         show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
   426           by (auto simp: emeasure_eq_measure)
   427       qed
   428       then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
   429         "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
   430         unfolding choice_iff by blast
   431       let ?K = "\<Union>i\<in>{0..<n0}. K i"
   432       have "disjoint_family_on K {0..<n0}" using K `disjoint_family D`
   433         unfolding disjoint_family_on_def by blast
   434       hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K
   435         by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
   436       have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
   437       also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
   438         using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
   439       also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))"
   440         by (simp add: setsum.distrib)
   441       also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) +  e / 2" using `0 < e`
   442         by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono)
   443       finally
   444       have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2"
   445         by auto
   446       hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
   447       moreover
   448       have "?K \<subseteq> (\<Union>i. D i)" using K by auto
   449       moreover
   450       have "compact ?K" using K by auto
   451       ultimately
   452       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
   453       thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
   454     qed
   455     moreover have "?outer (\<Union>i. D i)"
   456     proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`])
   457       fix e::real assume "e > 0"
   458       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)"
   459       proof
   460         fix i::nat
   461         from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
   462         have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
   463           using `range D \<subseteq> ?D` by blast
   464         from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
   465         show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
   466           by (auto simp: emeasure_eq_measure)
   467       qed
   468       then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
   469         "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
   470         unfolding choice_iff by blast
   471       let ?U = "\<Union>i. U i"
   472       have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U  `(\<Union>i. D i) \<in> sets M`
   473         by (subst emeasure_Diff) (auto simp: sb)
   474       also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U  `range D \<subseteq> sets M`
   475         by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
   476       also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U  `range D \<subseteq> sets M`
   477         by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
   478       also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
   479         by (intro suminf_le_pos, subst emeasure_Diff)
   480            (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
   481       also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
   482         by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
   483       also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^  Suc n))"
   484         unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
   485         by simp
   486       also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))"
   487         by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le)
   488       also have "\<dots> = e" unfolding suminf_half_series_ereal by simp
   489       finally
   490       have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure)
   491       moreover
   492       have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
   493       moreover
   494       have "open ?U" using U by auto
   495       ultimately
   496       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
   497       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" ..
   498     qed
   499     ultimately show "(\<Union>i. D i) \<in> ?D" by safe
   500   qed
   501   have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU)
   502   also have "\<dots> = dynkin (space M) (Collect closed)"
   503   proof (rule sigma_eq_dynkin)
   504     show "Collect closed \<subseteq> Pow (space M)" using Sigma_Algebra.sets_into_space by (auto simp: sU)
   505     show "Int_stable (Collect closed)" by (auto simp: Int_stable_def)
   506   qed
   507   also have "\<dots> \<subseteq> ?D" using closed_in_D
   508     by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
   509   finally have "sets borel \<subseteq> ?D" .
   510   moreover have "?D \<subseteq> sets borel" by (auto simp: sb)
   511   ultimately have "sets borel = ?D" by simp
   512   with assms show "?inner B" and "?outer B" by auto
   513 qed
   514 
   515 end
   516