author  haftmann 
Sat, 25 May 2013 15:44:29 +0200  
changeset 52141  eff000cab70f 
parent 51000  c9adb50f74ad 
child 56166  9a241bc276cd 
permissions  rwrr 
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" 

147 
hence "1/n > 0" "e * 2 powr  n > 0" by (auto intro: mult_pos_pos) 

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)})" 

274 
by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos 

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)" 

315 
unfolding inner by (subst INFI_ereal_cminus) force+ 

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)" 
50087  322 
by (subst INF_image[of "\<lambda>u. space M  u", symmetric]) 
323 
(rule INF_cong, auto simp add: sU intro!: INF_cong) 

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)" 
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset

334 
unfolding outer by (subst SUPR_ereal_cminus) auto 
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)" 
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset

338 
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

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) 
50087  354 
also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) > (\<Sum>i. M (D i))" 
355 
by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg) 

356 
finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) > measure M (\<Union>i. D i)" 

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 

365 
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" 

366 
by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1) 

367 
hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i))  measure M (\<Union>x. D x)\<bar> < e/2" by auto 

368 
then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i))  measure M (\<Union>i. D i)\<bar> < e/2" 

369 
unfolding choice_iff by blast 

370 
have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))" 

371 
by (auto simp add: emeasure_eq_measure) 

372 
also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto 

373 
also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg) 

374 
also have "\<dots> = M (\<Union>i. D i)" by (simp add: M) 

375 
also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure) 

376 
finally have n0: "measure M (\<Union>i. D i)  (\<Sum>i = 0..<n0. measure M (D i)) < e/2" 

377 
using n0 by auto 

378 
have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)" 

379 
proof 

380 
fix i 

381 
from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos) 

382 
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

383 
using union by blast 
50087  384 
from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this] 
385 
show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)" 

386 
by (auto simp: emeasure_eq_measure) 

387 
qed 

388 
then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)" 

389 
"\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)" 

390 
unfolding choice_iff by blast 

391 
let ?K = "\<Union>i\<in>{0..<n0}. K i" 

392 
have "disjoint_family_on K {0..<n0}" using K `disjoint_family D` 

393 
unfolding disjoint_family_on_def by blast 

394 
hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K 

395 
by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed) 

396 
have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp 

397 
also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))" 

398 
using K by (auto intro: setsum_mono simp: emeasure_eq_measure) 

399 
also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))" 

400 
by (simp add: setsum.distrib) 

401 
also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) + e / 2" using `0 < e` 

402 
by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono) 

403 
finally 

404 
have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2" 

405 
by auto 

406 
hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure) 

407 
moreover 

408 
have "?K \<subseteq> (\<Union>i. D i)" using K by auto 

409 
moreover 

410 
have "compact ?K" using K by auto 

411 
ultimately 

412 
have "?K\<subseteq>(\<Union>i. D i) \<and> compact ?K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M ?K + ereal e" by simp 

413 
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

414 
qed fact 
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset

415 
case 2 
4319691be975
tuned: use induction rule sigma_sets_induct_disjoint
hoelzl
parents:
50089
diff
changeset

416 
show ?case 
50087  417 
proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`]) 
418 
fix e::real assume "e > 0" 

419 
have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U  emeasure M (D i)" 

420 
proof 

421 
fix i::nat 

422 
from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos) 

423 
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

424 
using union by blast 
50087  425 
from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this] 
426 
show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U  emeasure M (D i)" 

427 
by (auto simp: emeasure_eq_measure) 

428 
qed 

429 
then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)" 

430 
"\<And>i. e/(2 powr Suc i) > emeasure M (U i)  emeasure M (D i)" 

431 
unfolding choice_iff by blast 

432 
let ?U = "\<Union>i. U i" 

433 
have "M ?U  M (\<Union>i. D i) = M (?U  (\<Union>i. D i))" using U `(\<Union>i. D i) \<in> sets M` 

434 
by (subst emeasure_Diff) (auto simp: sb) 

435 
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

436 
by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff) 
50087  437 
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

438 
by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb) 
50087  439 
also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M` 
440 
by (intro suminf_le_pos, subst emeasure_Diff) 

441 
(auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le) 

442 
also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))" 

443 
by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide) 

444 
also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))" 

445 
unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal 

446 
by simp 

447 
also have "\<dots> = ereal e * (\<Sum>n. ((1 / 2) ^ Suc n))" 

448 
by (rule suminf_cmult_ereal) (auto simp: `0 < e` less_imp_le) 

449 
also have "\<dots> = e" unfolding suminf_half_series_ereal by simp 

450 
finally 

451 
have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by (simp add: emeasure_eq_measure) 

452 
moreover 

453 
have "(\<Union>i. D i) \<subseteq> ?U" using U by auto 

454 
moreover 

455 
have "open ?U" using U by auto 

456 
ultimately 

457 
have "(\<Union>i. D i) \<subseteq> ?U \<and> open ?U \<and> emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by simp 

458 
thus "\<exists>B. (\<Union>i. D i) \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M (\<Union>i. D i) + ereal e" .. 

459 
qed 

460 
qed 

461 
qed 

462 

463 
end 

464 