author | immler |
Tue, 27 Nov 2012 11:29:47 +0100 | |
changeset 50244 | de72bbe42190 |
parent 50125 | 4319691be975 |
child 50245 | dea9363887a6 |
permissions | -rw-r--r-- |
50087 | 1 |
(* Title: HOL/Probability/Projective_Family.thy |
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)" |
|
19 |
proof (subst eq_commute, rule ereal_SUPI) |
|
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)" |
|
48 |
proof (subst eq_commute, rule ereal_INFI) |
|
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` |
|
82 |
by (intro ereal_INFI) |
|
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>` |
|
100 |
by (intro ereal_SUPI) |
|
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 |
|
107 |
fixes M::"'a::{enumerable_basis, complete_space} measure" |
|
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)+ |
|
127 |
from countable_dense_setE guess x::"nat \<Rightarrow> 'a" . note x = this |
|
128 |
{ |
|
129 |
fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto |
|
130 |
with x[OF this] |
|
131 |
have x: "space M = (\<Union>n. cball (x n) r)" |
|
132 |
by (auto simp add: sU) (metis dist_commute order_less_imp_le) |
|
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))" |
|
134 |
by (rule Lim_emeasure_incseq) |
|
135 |
(auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb) |
|
136 |
also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M" |
|
137 |
unfolding x by force |
|
138 |
finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" . |
|
139 |
} note M_space = this |
|
140 |
{ |
|
141 |
fix e ::real and n :: nat assume "e > 0" "n > 0" |
|
142 |
hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos) |
|
143 |
from M_space[OF `1/n>0`] |
|
144 |
have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)" |
|
145 |
unfolding emeasure_eq_measure by simp |
|
146 |
from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`] |
|
147 |
obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) < |
|
148 |
e * 2 powr -n" |
|
149 |
by auto |
|
150 |
hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> |
|
151 |
measure M (space M) - e * 2 powr -real n" |
|
152 |
by (auto simp: dist_real_def) |
|
153 |
hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> |
|
154 |
measure M (space M) - e * 2 powr - real n" .. |
|
155 |
} note k=this |
|
156 |
hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k. |
|
157 |
measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n" |
|
158 |
by blast |
|
159 |
then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat) |
|
160 |
\<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))" |
|
161 |
apply atomize_elim unfolding bchoice_iff . |
|
162 |
hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n |
|
163 |
\<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))" |
|
164 |
unfolding Ball_def by blast |
|
165 |
have approx_space: |
|
166 |
"\<And>e. e > 0 \<Longrightarrow> |
|
167 |
\<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e" |
|
168 |
(is "\<And>e. _ \<Longrightarrow> ?thesis e") |
|
169 |
proof - |
|
170 |
fix e :: real assume "e > 0" |
|
171 |
def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)" |
|
172 |
have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball) |
|
173 |
hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb) |
|
174 |
from k[OF `e > 0` zero_less_Suc] |
|
175 |
have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)" |
|
176 |
by (simp add: algebra_simps B_def finite_measure_compl) |
|
177 |
hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)" |
|
178 |
by (simp add: finite_measure_compl) |
|
179 |
def K \<equiv> "\<Inter>n. B n" |
|
180 |
from `closed (B _)` have "closed K" by (auto simp: K_def) |
|
181 |
hence [simp]: "K \<in> sets M" by (simp add: sb) |
|
182 |
have "measure M (space M) - measure M K = measure M (space M - K)" |
|
183 |
by (simp add: finite_measure_compl) |
|
184 |
also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure) |
|
185 |
also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))" |
|
186 |
by (rule emeasure_subadditive_countably) (auto simp: summable_def) |
|
187 |
also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))" |
|
188 |
using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure) |
|
189 |
also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))" |
|
190 |
by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide) |
|
191 |
also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))" |
|
192 |
unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal |
|
193 |
by simp |
|
194 |
also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))" |
|
195 |
by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le) |
|
196 |
also have "\<dots> = e" unfolding suminf_half_series_ereal by simp |
|
197 |
finally have "measure M (space M) \<le> measure M K + e" by simp |
|
198 |
hence "emeasure M (space M) \<le> emeasure M K + e" by (simp add: emeasure_eq_measure) |
|
199 |
moreover have "compact K" |
|
200 |
unfolding compact_eq_totally_bounded |
|
201 |
proof safe |
|
202 |
show "complete K" using `closed K` by (simp add: complete_eq_closed) |
|
203 |
fix e'::real assume "0 < e'" |
|
204 |
from nat_approx_posE[OF this] guess n . note n = this |
|
205 |
let ?k = "x ` {0..k e (Suc n)}" |
|
206 |
have "finite ?k" by simp |
|
207 |
moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force |
|
208 |
ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast |
|
209 |
qed |
|
210 |
ultimately |
|
211 |
show "?thesis e " by (auto simp: sU) |
|
212 |
qed |
|
50125
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
213 |
{ fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed) |
50087 | 214 |
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
|
215 |
have "?inner A" |
50087 | 216 |
proof (rule approx_inner) |
217 |
fix e::real assume "e > 0" |
|
218 |
from approx_space[OF this] obtain K where |
|
219 |
K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e" |
|
220 |
by (auto simp: emeasure_eq_measure) |
|
221 |
hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed) |
|
222 |
have "M A - M (A \<inter> K) = measure M A - measure M (A \<inter> K)" |
|
223 |
by (simp add: emeasure_eq_measure) |
|
224 |
also have "\<dots> = measure M (A - A \<inter> K)" |
|
225 |
by (subst finite_measure_Diff) auto |
|
226 |
also have "A - A \<inter> K = A \<union> K - K" by auto |
|
227 |
also have "measure M \<dots> = measure M (A \<union> K) - measure M K" |
|
228 |
by (subst finite_measure_Diff) auto |
|
229 |
also have "\<dots> \<le> measure M (space M) - measure M K" |
|
230 |
by (simp add: emeasure_eq_measure sU sb finite_measure_mono) |
|
231 |
also have "\<dots> \<le> e" using K by (simp add: emeasure_eq_measure) |
|
232 |
finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ereal e" |
|
233 |
by (simp add: emeasure_eq_measure algebra_simps) |
|
234 |
moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using `closed A` `compact K` by auto |
|
235 |
ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e" |
|
236 |
by blast |
|
237 |
qed simp |
|
50125
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
238 |
have "?outer A" |
50087 | 239 |
proof cases |
240 |
assume "A \<noteq> {}" |
|
241 |
let ?G = "\<lambda>d. {x. infdist x A < d}" |
|
242 |
{ |
|
243 |
fix d |
|
244 |
have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto |
|
245 |
also have "open \<dots>" |
|
246 |
by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id) |
|
247 |
finally have "open (?G d)" . |
|
248 |
} note open_G = this |
|
249 |
from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`] |
|
250 |
have "A = {x. infdist x A = 0}" by auto |
|
251 |
also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))" |
|
252 |
proof (auto, rule ccontr) |
|
253 |
fix x |
|
254 |
assume "infdist x A \<noteq> 0" |
|
255 |
hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp |
|
256 |
from nat_approx_posE[OF this] guess n . |
|
257 |
moreover |
|
258 |
assume "\<forall>i. infdist x A < 1 / real (Suc i)" |
|
259 |
hence "infdist x A < 1 / real (Suc n)" by auto |
|
260 |
ultimately show False by simp |
|
261 |
qed |
|
262 |
also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))" |
|
263 |
proof (rule INF_emeasure_decseq[symmetric], safe) |
|
264 |
fix i::nat |
|
265 |
from open_G[of "1 / real (Suc i)"] |
|
266 |
show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open) |
|
267 |
next |
|
268 |
show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})" |
|
269 |
by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos |
|
270 |
simp: decseq_def le_eq_less_or_eq) |
|
271 |
qed simp |
|
272 |
finally |
|
273 |
have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" . |
|
274 |
moreover |
|
275 |
have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)" |
|
276 |
proof (intro INF_mono) |
|
277 |
fix m |
|
278 |
have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto |
|
279 |
moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp |
|
280 |
ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}. |
|
281 |
emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}" |
|
282 |
by blast |
|
283 |
qed |
|
284 |
moreover |
|
285 |
have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)" |
|
286 |
by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb) |
|
287 |
ultimately show ?thesis by simp |
|
288 |
qed (auto intro!: ereal_INFI) |
|
50125
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
289 |
note `?inner A` `?outer A` } |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
290 |
note closed_in_D = this |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
291 |
from `B \<in> sets borel` |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
292 |
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
|
293 |
by (auto simp: Int_stable_def borel_eq_closed) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
294 |
then show "?inner B" "?outer B" |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
295 |
proof (induct B rule: sigma_sets_induct_disjoint) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
296 |
case empty |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
297 |
{ case 1 show ?case by (intro ereal_SUPI[symmetric]) auto } |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
298 |
{ case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) } |
50087 | 299 |
next |
50125
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
300 |
case (basic B) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
301 |
{ 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
|
302 |
{ 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
|
303 |
next |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
304 |
case (compl B) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
305 |
note inner = compl(2) and outer = compl(3) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
306 |
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
|
307 |
case 2 |
50087 | 308 |
have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) |
309 |
also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)" |
|
310 |
unfolding inner by (subst INFI_ereal_cminus) force+ |
|
311 |
also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))" |
|
312 |
by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed) |
|
313 |
also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))" |
|
314 |
by (rule INF_superset_mono) (auto simp add: compact_imp_closed) |
|
315 |
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
|
316 |
(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)" |
50087 | 317 |
by (subst INF_image[of "\<lambda>u. space M - u", symmetric]) |
318 |
(rule INF_cong, auto simp add: sU intro!: INF_cong) |
|
319 |
finally have |
|
320 |
"(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" . |
|
321 |
moreover have |
|
322 |
"(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)" |
|
323 |
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
|
324 |
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
|
325 |
|
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
326 |
case 1 |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
327 |
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
|
328 |
also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)" |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
329 |
unfolding outer by (subst SUPR_ereal_cminus) auto |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
330 |
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
|
331 |
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
|
332 |
also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)" |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
333 |
by (subst SUP_image[of "\<lambda>u. space M - u", symmetric]) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
334 |
(rule SUP_cong, auto simp: sU) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
335 |
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
|
336 |
proof (safe intro!: antisym SUP_least) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
337 |
fix K assume "closed K" "K \<subseteq> space M - B" |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
338 |
from closed_in_D[OF `closed K`] |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
339 |
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
|
340 |
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
|
341 |
unfolding K_inner using `K \<subseteq> space M - B` |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
342 |
by (auto intro!: SUP_upper SUP_least) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
343 |
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
|
344 |
finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) |
50087 | 345 |
next |
50125
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
346 |
case (union D) |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
347 |
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
|
348 |
with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure) |
50087 | 349 |
also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))" |
350 |
by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg) |
|
351 |
finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)" |
|
352 |
by (simp add: emeasure_eq_measure) |
|
353 |
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
|
354 |
|
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
355 |
case 1 |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
356 |
show ?case |
50087 | 357 |
proof (rule approx_inner) |
358 |
fix e::real assume "e > 0" |
|
359 |
with measure_LIMSEQ |
|
360 |
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" |
|
361 |
by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1) |
|
362 |
hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto |
|
363 |
then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2" |
|
364 |
unfolding choice_iff by blast |
|
365 |
have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))" |
|
366 |
by (auto simp add: emeasure_eq_measure) |
|
367 |
also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto |
|
368 |
also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg) |
|
369 |
also have "\<dots> = M (\<Union>i. D i)" by (simp add: M) |
|
370 |
also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure) |
|
371 |
finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2" |
|
372 |
using n0 by auto |
|
373 |
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)" |
|
374 |
proof |
|
375 |
fix i |
|
376 |
from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos) |
|
377 |
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
|
378 |
using union by blast |
50087 | 379 |
from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this] |
380 |
show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)" |
|
381 |
by (auto simp: emeasure_eq_measure) |
|
382 |
qed |
|
383 |
then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)" |
|
384 |
"\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)" |
|
385 |
unfolding choice_iff by blast |
|
386 |
let ?K = "\<Union>i\<in>{0..<n0}. K i" |
|
387 |
have "disjoint_family_on K {0..<n0}" using K `disjoint_family D` |
|
388 |
unfolding disjoint_family_on_def by blast |
|
389 |
hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K |
|
390 |
by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed) |
|
391 |
have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp |
|
392 |
also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))" |
|
393 |
using K by (auto intro: setsum_mono simp: emeasure_eq_measure) |
|
394 |
also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))" |
|
395 |
by (simp add: setsum.distrib) |
|
396 |
also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) + e / 2" using `0 < e` |
|
397 |
by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono) |
|
398 |
finally |
|
399 |
have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2" |
|
400 |
by auto |
|
401 |
hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure) |
|
402 |
moreover |
|
403 |
have "?K \<subseteq> (\<Union>i. D i)" using K by auto |
|
404 |
moreover |
|
405 |
have "compact ?K" using K by auto |
|
406 |
ultimately |
|
407 |
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 |
|
408 |
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
|
409 |
qed fact |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
410 |
case 2 |
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset
|
411 |
show ?case |
50087 | 412 |
proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`]) |
413 |
fix e::real assume "e > 0" |
|
414 |
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)" |
|
415 |
proof |
|
416 |
fix i::nat |
|
417 |
from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos) |
|
418 |
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
|
419 |
using union by blast |
50087 | 420 |
from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this] |
421 |
show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)" |
|
422 |
by (auto simp: emeasure_eq_measure) |
|
423 |
qed |
|
424 |
then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)" |
|
425 |
"\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)" |
|
426 |
unfolding choice_iff by blast |
|
427 |
let ?U = "\<Union>i. U i" |
|
428 |
have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U `(\<Union>i. D i) \<in> sets M` |
|
429 |
by (subst emeasure_Diff) (auto simp: sb) |
|
430 |
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
|
431 |
by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff) |
50087 | 432 |
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
|
433 |
by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb) |
50087 | 434 |
also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M` |
435 |
by (intro suminf_le_pos, subst emeasure_Diff) |
|
436 |
(auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le) |
|
437 |
also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))" |
|
438 |
by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide) |
|
439 |
also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))" |
|
440 |
unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal |
|
441 |
by simp |
|
442 |
also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))" |
|
443 |
by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le) |
|
444 |
also have "\<dots> = e" unfolding suminf_half_series_ereal by simp |
|
445 |
finally |
|
446 |
have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure) |
|
447 |
moreover |
|
448 |
have "(\<Union>i. D i) \<subseteq> ?U" using U by auto |
|
449 |
moreover |
|
450 |
have "open ?U" using U by auto |
|
451 |
ultimately |
|
452 |
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 |
|
453 |
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" .. |
|
454 |
qed |
|
455 |
qed |
|
456 |
qed |
|
457 |
||
458 |
end |
|
459 |