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