summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Analysis/Regularity.thy

author | wenzelm |

Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago) | |

changeset 69981 | 3dced198b9ec |

parent 69739 | 8b47c021666e |

permissions | -rw-r--r-- |

more strict AFP properties;

1 (* Title: HOL/Analysis/Regularity.thy

2 Author: Fabian Immler, TU München

3 *)

5 section \<open>Regularity of Measures\<close>

7 theory Regularity (* FIX suggestion to rename e.g. RegularityMeasures and/ or move as

8 this theory consists of 1 result only *)

9 imports Measure_Space Borel_Space

10 begin

12 theorem

13 fixes M::"'a::{second_countable_topology, complete_space} measure"

14 assumes sb: "sets M = sets borel"

15 assumes "emeasure M (space M) \<noteq> \<infinity>"

16 assumes "B \<in> sets borel"

17 shows inner_regular: "emeasure M B =

18 (SUP K \<in> {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")

19 and outer_regular: "emeasure M B =

20 (INF U \<in> {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")

21 proof -

22 have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)

23 hence sU: "space M = UNIV" by simp

24 interpret finite_measure M by rule fact

25 have approx_inner: "\<And>A. A \<in> sets M \<Longrightarrow>

26 (\<And>e. e > 0 \<Longrightarrow> \<exists>K. K \<subseteq> A \<and> compact K \<and> emeasure M A \<le> emeasure M K + ennreal e) \<Longrightarrow> ?inner A"

27 by (rule ennreal_approx_SUP)

28 (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+

29 have approx_outer: "\<And>A. A \<in> sets M \<Longrightarrow>

30 (\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ennreal e) \<Longrightarrow> ?outer A"

31 by (rule ennreal_approx_INF)

32 (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+

33 from countable_dense_setE guess X::"'a set" . note X = this

34 {

35 fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto

36 with X(2)[OF this]

37 have x: "space M = (\<Union>x\<in>X. cball x r)"

38 by (auto simp add: sU) (metis dist_commute order_less_imp_le)

39 let ?U = "\<Union>k. (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)"

40 have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M ?U"

41 by (rule Lim_emeasure_incseq) (auto intro!: borel_closed bexI simp: incseq_def Us sb)

42 also have "?U = space M"

43 proof safe

44 fix x from X(2)[OF open_ball[of x r]] \<open>r > 0\<close> obtain d where d: "d\<in>X" "d \<in> ball x r" by auto

45 show "x \<in> ?U"

46 using X(1) d

47 by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def)

48 qed (simp add: sU)

49 finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M (space M)" .

50 } note M_space = this

51 {

52 fix e ::real and n :: nat assume "e > 0" "n > 0"

53 hence "1/n > 0" "e * 2 powr - n > 0" by (auto)

54 from M_space[OF \<open>1/n>0\<close>]

55 have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) \<longlonglongrightarrow> measure M (space M)"

56 unfolding emeasure_eq_measure by (auto simp: measure_nonneg)

57 from metric_LIMSEQ_D[OF this \<open>0 < e * 2 powr -n\<close>]

58 obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <

59 e * 2 powr -n"

60 by auto

61 hence "measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>

62 measure M (space M) - e * 2 powr -real n"

63 by (auto simp: dist_real_def)

64 hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>

65 measure M (space M) - e * 2 powr - real n" ..

66 } note k=this

67 hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.

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

69 by blast

70 then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)

71 \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"

72 by metis

73 hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n

74 \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"

75 unfolding Ball_def by blast

76 have approx_space:

77 "\<exists>K \<in> {K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ennreal e"

78 (is "?thesis e") if "0 < e" for e :: real

79 proof -

80 define B where [abs_def]:

81 "B n = (\<Union>i\<in>{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n))" for n

82 have "\<And>n. closed (B n)" by (auto simp: B_def)

83 hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)

84 from k[OF \<open>e > 0\<close> zero_less_Suc]

85 have "\<And>n. measure M (space M) - measure M (B n) \<le> e * 2 powr - real (Suc n)"

86 by (simp add: algebra_simps B_def finite_measure_compl)

87 hence B_compl_le: "\<And>n::nat. measure M (space M - B n) \<le> e * 2 powr - real (Suc n)"

88 by (simp add: finite_measure_compl)

89 define K where "K = (\<Inter>n. B n)"

90 from \<open>closed (B _)\<close> have "closed K" by (auto simp: K_def)

91 hence [simp]: "K \<in> sets M" by (simp add: sb)

92 have "measure M (space M) - measure M K = measure M (space M - K)"

93 by (simp add: finite_measure_compl)

94 also have "\<dots> = emeasure M (\<Union>n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)

95 also have "\<dots> \<le> (\<Sum>n. emeasure M (space M - B n))"

96 by (rule emeasure_subadditive_countably) (auto simp: summable_def)

97 also have "\<dots> \<le> (\<Sum>n. ennreal (e*2 powr - real (Suc n)))"

98 using B_compl_le by (intro suminf_le) (simp_all add: measure_nonneg emeasure_eq_measure ennreal_leI)

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

100 by (simp add: powr_minus powr_realpow field_simps del: of_nat_Suc)

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

102 unfolding ennreal_power[symmetric]

103 using \<open>0 < e\<close>

104 by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def

105 ennreal_power[symmetric])

106 also have "\<dots> = e"

107 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto

108 finally have "measure M (space M) \<le> measure M K + e"

109 using \<open>0 < e\<close> by simp

110 hence "emeasure M (space M) \<le> emeasure M K + e"

111 using \<open>0 < e\<close> by (simp add: emeasure_eq_measure flip: ennreal_plus)

112 moreover have "compact K"

113 unfolding compact_eq_totally_bounded

114 proof safe

115 show "complete K" using \<open>closed K\<close> by (simp add: complete_eq_closed)

116 fix e'::real assume "0 < e'"

117 from nat_approx_posE[OF this] guess n . note n = this

118 let ?k = "from_nat_into X ` {0..k e (Suc n)}"

119 have "finite ?k" by simp

120 moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force

121 ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast

122 qed

123 ultimately

124 show ?thesis by (auto simp: sU)

125 qed

126 { fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)

127 hence [simp]: "A \<in> sets M" by (simp add: sb)

128 have "?inner A"

129 proof (rule approx_inner)

130 fix e::real assume "e > 0"

131 from approx_space[OF this] obtain K where

132 K: "K \<subseteq> space M" "compact K" "emeasure M (space M) \<le> emeasure M K + e"

133 by (auto simp: emeasure_eq_measure)

134 hence [simp]: "K \<in> sets M" by (simp add: sb compact_imp_closed)

135 have "measure M A - measure M (A \<inter> K) = measure M (A - A \<inter> K)"

136 by (subst finite_measure_Diff) auto

137 also have "A - A \<inter> K = A \<union> K - K" by auto

138 also have "measure M \<dots> = measure M (A \<union> K) - measure M K"

139 by (subst finite_measure_Diff) auto

140 also have "\<dots> \<le> measure M (space M) - measure M K"

141 by (simp add: emeasure_eq_measure sU sb finite_measure_mono)

142 also have "\<dots> \<le> e"

143 using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure flip: ennreal_plus)

144 finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ennreal e"

145 using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps flip: ennreal_plus)

146 moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using \<open>closed A\<close> \<open>compact K\<close> by auto

147 ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ennreal e"

148 by blast

149 qed simp

150 have "?outer A"

151 proof cases

152 assume "A \<noteq> {}"

153 let ?G = "\<lambda>d. {x. infdist x A < d}"

154 {

155 fix d

156 have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto

157 also have "open \<dots>"

158 by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident)

159 finally have "open (?G d)" .

160 } note open_G = this

161 from in_closed_iff_infdist_zero[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>]

162 have "A = {x. infdist x A = 0}" by auto

163 also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"

164 proof (auto simp del: of_nat_Suc, rule ccontr)

165 fix x

166 assume "infdist x A \<noteq> 0"

167 hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp

168 from nat_approx_posE[OF this] guess n .

169 moreover

170 assume "\<forall>i. infdist x A < 1 / real (Suc i)"

171 hence "infdist x A < 1 / real (Suc n)" by auto

172 ultimately show False by simp

173 qed

174 also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"

175 proof (rule INF_emeasure_decseq[symmetric], safe)

176 fix i::nat

177 from open_G[of "1 / real (Suc i)"]

178 show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)

179 next

180 show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"

181 by (auto intro: less_trans intro!: divide_strict_left_mono

182 simp: decseq_def le_eq_less_or_eq)

183 qed simp

184 finally

185 have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .

186 moreover

187 have "\<dots> \<ge> (INF U\<in>{U. A \<subseteq> U \<and> open U}. emeasure M U)"

188 proof (intro INF_mono)

189 fix m

190 have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto

191 moreover have "M (?G (1 / real (Suc m))) \<le> M (?G (1 / real (Suc m)))" by simp

192 ultimately show "\<exists>U\<in>{U. A \<subseteq> U \<and> open U}.

193 emeasure M U \<le> emeasure M {x. infdist x A < 1 / real (Suc m)}"

194 by blast

195 qed

196 moreover

197 have "emeasure M A \<le> (INF U\<in>{U. A \<subseteq> U \<and> open U}. emeasure M U)"

198 by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)

199 ultimately show ?thesis by simp

200 qed (auto intro!: INF_eqI)

201 note \<open>?inner A\<close> \<open>?outer A\<close> }

202 note closed_in_D = this

203 from \<open>B \<in> sets borel\<close>

204 have "Int_stable (Collect closed)" "Collect closed \<subseteq> Pow UNIV" "B \<in> sigma_sets UNIV (Collect closed)"

205 by (auto simp: Int_stable_def borel_eq_closed)

206 then show "?inner B" "?outer B"

207 proof (induct B rule: sigma_sets_induct_disjoint)

208 case empty

209 { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }

210 { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }

211 next

212 case (basic B)

213 { case 1 from basic closed_in_D show ?case by auto }

214 { case 2 from basic closed_in_D show ?case by auto }

215 next

216 case (compl B)

217 note inner = compl(2) and outer = compl(3)

218 from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed)

219 case 2

220 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)

221 also have "\<dots> = (INF K\<in>{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)"

222 by (subst ennreal_SUP_const_minus) (auto simp: less_top[symmetric] inner)

223 also have "\<dots> = (INF U\<in>{U. U \<subseteq> B \<and> compact U}. M (space M - U))"

224 by (auto simp add: emeasure_compl sb compact_imp_closed)

225 also have "\<dots> \<ge> (INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U))"

226 by (rule INF_superset_mono) (auto simp add: compact_imp_closed)

227 also have "(INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =

228 (INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"

229 apply (rule arg_cong [of _ _ Inf])

230 using sU

231 apply (auto simp add: image_iff)

232 apply (rule exI [of _ "UNIV - y" for y])

233 apply safe

234 apply (auto simp add: double_diff)

235 done

236 finally have

237 "(INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .

238 moreover have

239 "(INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"

240 by (auto simp: sb sU intro!: INF_greatest emeasure_mono)

241 ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])

243 case 1

244 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)

245 also have "\<dots> = (SUP U\<in> {U. B \<subseteq> U \<and> open U}. M (space M) - M U)"

246 unfolding outer by (subst ennreal_INF_const_minus) auto

247 also have "\<dots> = (SUP U\<in>{U. B \<subseteq> U \<and> open U}. M (space M - U))"

248 by (auto simp add: emeasure_compl sb compact_imp_closed)

249 also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"

250 unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]

251 apply (rule arg_cong [of _ _ Sup])

252 using sU apply (auto intro!: imageI)

253 done

254 also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"

255 proof (safe intro!: antisym SUP_least)

256 fix K assume "closed K" "K \<subseteq> space M - B"

257 from closed_in_D[OF \<open>closed K\<close>]

258 have K_inner: "emeasure M K = (SUP K\<in>{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp

259 show "emeasure M K \<le> (SUP K\<in>{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"

260 unfolding K_inner using \<open>K \<subseteq> space M - B\<close>

261 by (auto intro!: SUP_upper SUP_least)

262 qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)

263 finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])

264 next

265 case (union D)

266 then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed)

267 with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure)

268 also have "(\<lambda>n. \<Sum>i<n. M (D i)) \<longlonglongrightarrow> (\<Sum>i. M (D i))"

269 by (intro summable_LIMSEQ) auto

270 finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i<n. measure M (D i)) \<longlonglongrightarrow> measure M (\<Union>i. D i)"

271 by (simp add: emeasure_eq_measure measure_nonneg sum_nonneg)

272 have "(\<Union>i. D i) \<in> sets M" using \<open>range D \<subseteq> sets M\<close> by auto

274 case 1

275 show ?case

276 proof (rule approx_inner)

277 fix e::real assume "e > 0"

278 with measure_LIMSEQ

279 have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"

280 by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1)

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

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

283 unfolding choice_iff by blast

284 have "ennreal (\<Sum>i<n0. measure M (D i)) = (\<Sum>i<n0. M (D i))"

285 by (auto simp add: emeasure_eq_measure sum_nonneg measure_nonneg)

286 also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule sum_le_suminf) auto

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

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

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

290 using n0 by (auto simp: measure_nonneg sum_nonneg)

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

292 proof

293 fix i

294 from \<open>0 < e\<close> have "0 < e/(2*Suc n0)" by simp

295 have "emeasure M (D i) = (SUP K\<in>{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"

296 using union by blast

297 from SUP_approx_ennreal[OF \<open>0 < e/(2*Suc n0)\<close> _ this]

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

299 by (auto simp: emeasure_eq_measure intro: less_imp_le compact_empty)

300 qed

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

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

303 unfolding choice_iff by blast

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

305 have "disjoint_family_on K {..<n0}" using K \<open>disjoint_family D\<close>

306 unfolding disjoint_family_on_def by blast

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

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

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

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

311 using K \<open>0 < e\<close>

312 by (auto intro: sum_mono simp: emeasure_eq_measure simp flip: ennreal_plus)

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

314 by (simp add: sum.distrib)

315 also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) + e / 2" using \<open>0 < e\<close>

316 by (auto simp: field_simps intro!: mult_left_mono)

317 finally

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

319 by auto

320 hence "M (\<Union>i. D i) < M ?K + e"

321 using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff simp flip: ennreal_plus)

322 moreover

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

324 moreover

325 have "compact ?K" using K by auto

326 ultimately

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

328 thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ennreal e" ..

329 qed fact

330 case 2

331 show ?case

332 proof (rule approx_outer[OF \<open>(\<Union>i. D i) \<in> sets M\<close>])

333 fix e::real assume "e > 0"

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

335 proof

336 fix i::nat

337 from \<open>0 < e\<close> have "0 < e/(2 powr Suc i)" by simp

338 have "emeasure M (D i) = (INF U\<in>{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"

339 using union by blast

340 from INF_approx_ennreal[OF \<open>0 < e/(2 powr Suc i)\<close> this]

341 show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"

342 using \<open>0<e\<close>

343 by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus

344 finite_measure_mono sb

345 simp flip: ennreal_plus)

346 qed

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

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

349 unfolding choice_iff by blast

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

351 have "ennreal (measure M ?U - measure M (\<Union>i. D i)) = M ?U - M (\<Union>i. D i)"

352 using U(1,2)

353 by (subst ennreal_minus[symmetric])

354 (auto intro!: finite_measure_mono simp: sb measure_nonneg emeasure_eq_measure)

355 also have "\<dots> = M (?U - (\<Union>i. D i))" using U \<open>(\<Union>i. D i) \<in> sets M\<close>

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

357 also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U \<open>range D \<subseteq> sets M\<close>

358 by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff)

359 also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U \<open>range D \<subseteq> sets M\<close>

360 by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb)

361 also have "\<dots> \<le> (\<Sum>i. ennreal e/(2 powr Suc i))" using U \<open>range D \<subseteq> sets M\<close>

362 using \<open>0<e\<close>

363 by (intro suminf_le, subst emeasure_Diff)

364 (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg ennreal_minus

365 finite_measure_mono divide_ennreal ennreal_less_iff

366 intro: less_imp_le)

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

368 using \<open>0<e\<close>

369 by (simp add: powr_minus powr_realpow field_simps divide_ennreal del: of_nat_Suc)

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

371 unfolding ennreal_power[symmetric]

372 using \<open>0 < e\<close>

373 by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def

374 ennreal_power[symmetric])

375 also have "\<dots> = ennreal e"

376 by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto

377 finally have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ennreal e"

378 using \<open>0<e\<close> by (simp add: emeasure_eq_measure flip: ennreal_plus)

379 moreover

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

381 moreover

382 have "open ?U" using U by auto

383 ultimately

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

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

386 qed

387 qed

388 qed

390 end