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