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

src/HOL/Probability/Complete_Measure.thy

author | hoelzl |

Tue Mar 29 14:27:39 2011 +0200 (2011-03-29) | |

changeset 42146 | 5b52c6a9c627 |

parent 41983 | 2dc6e382a58b |

child 42866 | b0746bd57a41 |

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

split Product_Measure into Binary_Product_Measure and Finite_Product_Measure

1 (* Title: HOL/Probability/Complete_Measure.thy

2 Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen

3 *)

5 theory Complete_Measure

6 imports Lebesgue_Integration

7 begin

9 locale completeable_measure_space = measure_space

11 definition (in completeable_measure_space)

12 "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>

13 fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"

15 definition (in completeable_measure_space)

16 "main_part A = fst (Eps (split_completion A))"

18 definition (in completeable_measure_space)

19 "null_part A = snd (Eps (split_completion A))"

21 abbreviation (in completeable_measure_space) "\<mu>' A \<equiv> \<mu> (main_part A)"

23 definition (in completeable_measure_space) completion :: "('a, 'b) measure_space_scheme" where

24 "completion = \<lparr> space = space M,

25 sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' },

26 measure = \<mu>',

27 \<dots> = more M \<rparr>"

30 lemma (in completeable_measure_space) space_completion[simp]:

31 "space completion = space M" unfolding completion_def by simp

33 lemma (in completeable_measure_space) sets_completionE:

34 assumes "A \<in> sets completion"

35 obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"

36 using assms unfolding completion_def by auto

38 lemma (in completeable_measure_space) sets_completionI:

39 assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"

40 shows "A \<in> sets completion"

41 using assms unfolding completion_def by auto

43 lemma (in completeable_measure_space) sets_completionI_sets[intro]:

44 "A \<in> sets M \<Longrightarrow> A \<in> sets completion"

45 unfolding completion_def by force

47 lemma (in completeable_measure_space) null_sets_completion:

48 assumes "N' \<in> null_sets" "N \<subseteq> N'" shows "N \<in> sets completion"

49 apply(rule sets_completionI[of N "{}" N N'])

50 using assms by auto

52 sublocale completeable_measure_space \<subseteq> completion!: sigma_algebra completion

53 proof (unfold sigma_algebra_iff2, safe)

54 fix A x assume "A \<in> sets completion" "x \<in> A"

55 with sets_into_space show "x \<in> space completion"

56 by (auto elim!: sets_completionE)

57 next

58 fix A assume "A \<in> sets completion"

59 from this[THEN sets_completionE] guess S N N' . note A = this

60 let ?C = "space completion"

61 show "?C - A \<in> sets completion" using A

62 by (intro sets_completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"])

63 auto

64 next

65 fix A ::"nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion"

66 then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N'"

67 unfolding completion_def by (auto simp: image_subset_iff)

68 from choice[OF this] guess S ..

69 from choice[OF this] guess N ..

70 from choice[OF this] guess N' ..

71 then show "UNION UNIV A \<in> sets completion"

72 using null_sets_UN[of N']

73 by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"])

74 auto

75 qed auto

77 lemma (in completeable_measure_space) split_completion:

78 assumes "A \<in> sets completion"

79 shows "split_completion A (main_part A, null_part A)"

80 unfolding main_part_def null_part_def

81 proof (rule someI2_ex)

82 from assms[THEN sets_completionE] guess S N N' . note A = this

83 let ?P = "(S, N - S)"

84 show "\<exists>p. split_completion A p"

85 unfolding split_completion_def using A

86 proof (intro exI conjI)

87 show "A = fst ?P \<union> snd ?P" using A by auto

88 show "snd ?P \<subseteq> N'" using A by auto

89 qed auto

90 qed auto

92 lemma (in completeable_measure_space)

93 assumes "S \<in> sets completion"

94 shows main_part_sets[intro, simp]: "main_part S \<in> sets M"

95 and main_part_null_part_Un[simp]: "main_part S \<union> null_part S = S"

96 and main_part_null_part_Int[simp]: "main_part S \<inter> null_part S = {}"

97 using split_completion[OF assms] by (auto simp: split_completion_def)

99 lemma (in completeable_measure_space) null_part:

100 assumes "S \<in> sets completion" shows "\<exists>N. N\<in>null_sets \<and> null_part S \<subseteq> N"

101 using split_completion[OF assms] by (auto simp: split_completion_def)

103 lemma (in completeable_measure_space) null_part_sets[intro, simp]:

104 assumes "S \<in> sets M" shows "null_part S \<in> sets M" "\<mu> (null_part S) = 0"

105 proof -

106 have S: "S \<in> sets completion" using assms by auto

107 have "S - main_part S \<in> sets M" using assms by auto

108 moreover

109 from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]

110 have "S - main_part S = null_part S" by auto

111 ultimately show sets: "null_part S \<in> sets M" by auto

112 from null_part[OF S] guess N ..

113 with measure_eq_0[of N "null_part S"] sets

114 show "\<mu> (null_part S) = 0" by auto

115 qed

117 lemma (in completeable_measure_space) \<mu>'_set[simp]:

118 assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"

119 proof -

120 have S: "S \<in> sets completion" using assms by auto

121 then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp

122 also have "\<dots> = \<mu>' S"

123 using S assms measure_additive[of "main_part S" "null_part S"]

124 by (auto simp: measure_additive)

125 finally show ?thesis by simp

126 qed

128 lemma (in completeable_measure_space) sets_completionI_sub:

129 assumes N: "N' \<in> null_sets" "N \<subseteq> N'"

130 shows "N \<in> sets completion"

131 using assms by (intro sets_completionI[of _ "{}" N N']) auto

133 lemma (in completeable_measure_space) \<mu>_main_part_UN:

134 fixes S :: "nat \<Rightarrow> 'a set"

135 assumes "range S \<subseteq> sets completion"

136 shows "\<mu>' (\<Union>i. (S i)) = \<mu> (\<Union>i. main_part (S i))"

137 proof -

138 have S: "\<And>i. S i \<in> sets completion" using assms by auto

139 then have UN: "(\<Union>i. S i) \<in> sets completion" by auto

140 have "\<forall>i. \<exists>N. N \<in> null_sets \<and> null_part (S i) \<subseteq> N"

141 using null_part[OF S] by auto

142 from choice[OF this] guess N .. note N = this

143 then have UN_N: "(\<Union>i. N i) \<in> null_sets" by (intro null_sets_UN) auto

144 have "(\<Union>i. S i) \<in> sets completion" using S by auto

145 from null_part[OF this] guess N' .. note N' = this

146 let ?N = "(\<Union>i. N i) \<union> N'"

147 have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto

148 have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"

149 using N' by auto

150 also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"

151 unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto

152 also have "\<dots> = (\<Union>i. main_part (S i)) \<union> ?N"

153 using N by auto

154 finally have *: "main_part (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part (S i)) \<union> ?N" .

155 have "\<mu> (main_part (\<Union>i. S i)) = \<mu> (main_part (\<Union>i. S i) \<union> ?N)"

156 using null_set UN by (intro measure_Un_null_set[symmetric]) auto

157 also have "\<dots> = \<mu> ((\<Union>i. main_part (S i)) \<union> ?N)"

158 unfolding * ..

159 also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"

160 using null_set S by (intro measure_Un_null_set) auto

161 finally show ?thesis .

162 qed

164 lemma (in completeable_measure_space) \<mu>_main_part_Un:

165 assumes S: "S \<in> sets completion" and T: "T \<in> sets completion"

166 shows "\<mu>' (S \<union> T) = \<mu> (main_part S \<union> main_part T)"

167 proof -

168 have UN: "(\<Union>i. binary (main_part S) (main_part T) i) = (\<Union>i. main_part (binary S T i))"

169 unfolding binary_def by (auto split: split_if_asm)

170 show ?thesis

171 using \<mu>_main_part_UN[of "binary S T"] assms

172 unfolding range_binary_eq Un_range_binary UN by auto

173 qed

175 sublocale completeable_measure_space \<subseteq> completion!: measure_space completion

176 where "measure completion = \<mu>'"

177 proof -

178 show "measure_space completion"

179 proof

180 show "positive completion (measure completion)"

181 by (auto simp: completion_def positive_def)

182 next

183 show "countably_additive completion (measure completion)"

184 proof (intro countably_additiveI)

185 fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"

186 have "disjoint_family (\<lambda>i. main_part (A i))"

187 proof (intro disjoint_family_on_bisimulation[OF A(2)])

188 fix n m assume "A n \<inter> A m = {}"

189 then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"

190 using A by (subst (1 2) main_part_null_part_Un) auto

191 then show "main_part (A n) \<inter> main_part (A m) = {}" by auto

192 qed

193 then have "(\<Sum>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"

194 unfolding completion_def using A by (auto intro!: measure_countably_additive)

195 then show "(\<Sum>n. measure completion (A n)) = measure completion (UNION UNIV A)"

196 by (simp add: completion_def \<mu>_main_part_UN[OF A(1)])

197 qed

198 qed

199 show "measure completion = \<mu>'" unfolding completion_def by simp

200 qed

202 lemma (in completeable_measure_space) completion_ex_simple_function:

203 assumes f: "simple_function completion f"

204 shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"

205 proof -

206 let "?F x" = "f -` {x} \<inter> space M"

207 have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"

208 using completion.simple_functionD[OF f]

209 completion.simple_functionD[OF f] by simp_all

210 have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"

211 using F null_part by auto

212 from choice[OF this] obtain N where

213 N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto

214 let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"

215 have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto

216 show ?thesis unfolding simple_function_def

217 proof (safe intro!: exI[of _ ?f'])

218 have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto

219 from finite_subset[OF this] completion.simple_functionD(1)[OF f]

220 show "finite (?f' ` space M)" by auto

221 next

222 fix x assume "x \<in> space M"

223 have "?f' -` {?f' x} \<inter> space M =

224 (if x \<in> ?N then ?F undefined \<union> ?N

225 else if f x = undefined then ?F (f x) \<union> ?N

226 else ?F (f x) - ?N)"

227 using N(2) sets_into_space by (auto split: split_if_asm)

228 moreover { fix y have "?F y \<union> ?N \<in> sets M"

229 proof cases

230 assume y: "y \<in> f`space M"

231 have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"

232 using main_part_null_part_Un[OF F] by auto

233 also have "\<dots> = main_part (?F y) \<union> ?N"

234 using y N by auto

235 finally show ?thesis

236 using F sets by auto

237 next

238 assume "y \<notin> f`space M" then have "?F y = {}" by auto

239 then show ?thesis using sets by auto

240 qed }

241 moreover {

242 have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"

243 using main_part_null_part_Un[OF F] by auto

244 also have "\<dots> = main_part (?F (f x)) - ?N"

245 using N `x \<in> space M` by auto

246 finally have "?F (f x) - ?N \<in> sets M"

247 using F sets by auto }

248 ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto

249 next

250 show "AE x. f x = ?f' x"

251 by (rule AE_I', rule sets) auto

252 qed

253 qed

255 lemma (in completeable_measure_space) completion_ex_borel_measurable_pos:

256 fixes g :: "'a \<Rightarrow> extreal"

257 assumes g: "g \<in> borel_measurable completion" and "\<And>x. 0 \<le> g x"

258 shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"

259 proof -

260 from g[THEN completion.borel_measurable_implies_simple_function_sequence'] guess f . note f = this

261 from this(1)[THEN completion_ex_simple_function]

262 have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)" ..

263 from this[THEN choice] obtain f' where

264 sf: "\<And>i. simple_function M (f' i)" and

265 AE: "\<forall>i. AE x. f i x = f' i x" by auto

266 show ?thesis

267 proof (intro bexI)

268 from AE[unfolded AE_all_countable[symmetric]]

269 show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")

270 proof (elim AE_mp, safe intro!: AE_I2)

271 fix x assume eq: "\<forall>i. f i x = f' i x"

272 moreover have "g x = (SUP i. f i x)"

273 unfolding f using `0 \<le> g x` by (auto split: split_max)

274 ultimately show "g x = ?f x" by auto

275 qed

276 show "?f \<in> borel_measurable M"

277 using sf by (auto intro: borel_measurable_simple_function)

278 qed

279 qed

281 lemma (in completeable_measure_space) completion_ex_borel_measurable:

282 fixes g :: "'a \<Rightarrow> extreal"

283 assumes g: "g \<in> borel_measurable completion"

284 shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"

285 proof -

286 have "(\<lambda>x. max 0 (g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (g x)" using g by auto

287 from completion_ex_borel_measurable_pos[OF this] guess g_pos ..

288 moreover

289 have "(\<lambda>x. max 0 (- g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (- g x)" using g by auto

290 from completion_ex_borel_measurable_pos[OF this] guess g_neg ..

291 ultimately

292 show ?thesis

293 proof (safe intro!: bexI[of _ "\<lambda>x. g_pos x - g_neg x"])

294 show "AE x. max 0 (- g x) = g_neg x \<longrightarrow> max 0 (g x) = g_pos x \<longrightarrow> g x = g_pos x - g_neg x"

295 proof (intro AE_I2 impI)

296 fix x assume g: "max 0 (- g x) = g_neg x" "max 0 (g x) = g_pos x"

297 show "g x = g_pos x - g_neg x" unfolding g[symmetric]

298 by (cases "g x") (auto split: split_max)

299 qed

300 qed auto

301 qed

303 end