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

src/HOL/Probability/Complete_Measure.thy

author | hoelzl |

Wed Dec 01 21:03:02 2010 +0100 (2010-12-01) | |

changeset 40871 | 688f6ff859e1 |

parent 40859 | de0b30e6c2d2 |

child 41023 | 9118eb4eb8dc |

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

Generalized simple_functionD and less_SUP_iff.

Moved theorems to appropriate places.

Moved theorems to appropriate places.

1 (* Title: Complete_Measure.thy

2 Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen

3 *)

4 theory Complete_Measure

5 imports Product_Measure

6 begin

8 locale completeable_measure_space = measure_space

10 definition (in completeable_measure_space) completion :: "'a algebra" where

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

12 sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' } \<rparr>"

14 lemma (in completeable_measure_space) space_completion[simp]:

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

17 lemma (in completeable_measure_space) sets_completionE:

18 assumes "A \<in> sets completion"

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

20 using assms unfolding completion_def by auto

22 lemma (in completeable_measure_space) sets_completionI:

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

24 shows "A \<in> sets completion"

25 using assms unfolding completion_def by auto

27 lemma (in completeable_measure_space) sets_completionI_sets[intro]:

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

29 unfolding completion_def by force

31 lemma (in completeable_measure_space) null_sets_completion:

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

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

34 using assms by auto

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

37 proof (unfold sigma_algebra_iff2, safe)

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

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

40 by (auto elim!: sets_completionE)

41 next

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

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

44 let ?C = "space completion"

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

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

47 auto

48 next

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

50 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'"

51 unfolding completion_def by (auto simp: image_subset_iff)

52 from choice[OF this] guess S ..

53 from choice[OF this] guess N ..

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

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

56 using null_sets_UN[of N']

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

58 auto

59 qed auto

61 definition (in completeable_measure_space)

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

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

65 definition (in completeable_measure_space)

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

68 definition (in completeable_measure_space)

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

71 lemma (in completeable_measure_space) split_completion:

72 assumes "A \<in> sets completion"

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

74 unfolding main_part_def null_part_def

75 proof (rule someI2_ex)

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

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

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

79 unfolding split_completion_def using A

80 proof (intro exI conjI)

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

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

83 qed auto

84 qed auto

86 lemma (in completeable_measure_space)

87 assumes "S \<in> sets completion"

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

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

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

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

93 lemma (in completeable_measure_space) null_part:

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

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

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

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

99 proof -

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

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

102 moreover

103 from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]

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

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

106 from null_part[OF S] guess N ..

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

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

109 qed

111 definition (in completeable_measure_space) "\<mu>' A = \<mu> (main_part A)"

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

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

115 proof -

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

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

118 also have "\<dots> = \<mu> (main_part S)"

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

120 by (auto simp: measure_additive)

121 finally show ?thesis unfolding \<mu>'_def by simp

122 qed

124 lemma (in completeable_measure_space) sets_completionI_sub:

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

126 shows "N \<in> sets completion"

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

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

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

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

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

133 proof -

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

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

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

137 using null_part[OF S] by auto

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

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

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

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

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

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

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

145 using N' by auto

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

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

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

149 using N by auto

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

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

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

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

154 unfolding * ..

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

156 using null_set S by (intro measure_Un_null_set) auto

157 finally show ?thesis unfolding \<mu>'_def .

158 qed

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

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

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

163 proof -

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

165 unfolding binary_def by (auto split: split_if_asm)

166 show ?thesis

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

168 unfolding range_binary_eq Un_range_binary UN by auto

169 qed

171 sublocale completeable_measure_space \<subseteq> completion!: measure_space completion \<mu>'

172 proof

173 show "\<mu>' {} = 0" by auto

174 next

175 show "countably_additive completion \<mu>'"

176 proof (unfold countably_additive_def, intro allI conjI impI)

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

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

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

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

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

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

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

184 qed

185 then have "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu> (\<Union>i. main_part (A i))"

186 unfolding \<mu>'_def using A by (intro measure_countably_additive) auto

187 then show "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu>' (UNION UNIV A)"

188 unfolding \<mu>_main_part_UN[OF A(1)] .

189 qed

190 qed

192 lemma (in completeable_measure_space) completion_ex_simple_function:

193 assumes f: "completion.simple_function f"

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

195 proof -

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

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

198 using completion.simple_functionD[OF f]

199 completion.simple_functionD[OF f] by simp_all

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

201 using F null_part by auto

202 from choice[OF this] obtain N where

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

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

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

206 show ?thesis unfolding simple_function_def

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

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

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

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

211 next

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

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

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

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

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

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

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

219 proof cases

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

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

222 using main_part_null_part_Un[OF F] by auto

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

224 using y N by auto

225 finally show ?thesis

226 using F sets by auto

227 next

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

229 then show ?thesis using sets by auto

230 qed }

231 moreover {

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

233 using main_part_null_part_Un[OF F] by auto

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

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

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

237 using F sets by auto }

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

239 next

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

241 by (rule AE_I', rule sets) auto

242 qed

243 qed

245 lemma (in completeable_measure_space) completion_ex_borel_measurable:

246 fixes g :: "'a \<Rightarrow> pinfreal"

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

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

249 proof -

250 from g[THEN completion.borel_measurable_implies_simple_function_sequence]

251 obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto

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

253 using completion_ex_simple_function by auto

254 from this[THEN choice] obtain f' where

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

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

257 show ?thesis

258 proof (intro bexI)

259 from AE[unfolded all_AE_countable]

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

261 proof (rule AE_mp, safe intro!: AE_cong)

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

263 have "g x = (SUP i. f i x)"

264 using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto

265 then show "g x = ?f x"

266 using eq unfolding SUPR_fun_expand by auto

267 qed

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

269 using sf by (auto intro!: borel_measurable_SUP

270 intro: borel_measurable_simple_function)

271 qed

272 qed

274 end