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