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

src/HOL/Probability/Embed_Measure.thy

author | haftmann |

Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) | |

changeset 60517 | f16e4fb20652 |

parent 60065 | 390de6d3a7b8 |

child 60580 | 7e741e22d7fc |

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

separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial

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

2 Author: Manuel Eberl, TU München

4 Defines measure embeddings with injective functions, i.e. lifting a measure on some values

5 to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a

6 measure on the left part of the sum type 'a + 'b)

7 *)

9 section {* Embed Measure Spaces with a Function *}

11 theory Embed_Measure

12 imports Binary_Product_Measure

13 begin

15 definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where

16 "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M}

17 (\<lambda>A. emeasure M (f -` A \<inter> space M))"

19 lemma space_embed_measure: "space (embed_measure M f) = f ` space M"

20 unfolding embed_measure_def

21 by (subst space_measure_of) (auto dest: sets.sets_into_space)

23 lemma sets_embed_measure':

24 assumes inj: "inj_on f (space M)"

25 shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"

26 unfolding embed_measure_def

27 proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI)

28 fix s assume "s \<in> {f ` A |A. A \<in> sets M}"

29 then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto

30 hence "f ` space M - s = f ` (space M - s')" using inj

31 by (auto dest: inj_onD sets.sets_into_space)

32 also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto

33 finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .

34 next

35 fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"

36 then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"

37 by (auto simp: subset_eq choice_iff)

38 moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast

39 ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" by blast

40 qed (auto dest: sets.sets_into_space)

42 lemma the_inv_into_vimage:

43 "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"

44 by (auto simp: the_inv_into_f_f)

46 lemma sets_embed_eq_vimage_algebra:

47 assumes "inj_on f (space M)"

48 shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"

49 by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image

50 dest: sets.sets_into_space

51 intro!: image_cong the_inv_into_vimage[symmetric])

53 lemma sets_embed_measure:

54 assumes inj: "inj f"

55 shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"

56 using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)

58 lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"

59 unfolding embed_measure_def

60 by (intro in_measure_of) (auto dest: sets.sets_into_space)

62 lemma measurable_embed_measure1:

63 assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N"

64 shows "g \<in> measurable (embed_measure M f) N"

65 unfolding measurable_def

66 proof safe

67 fix A assume "A \<in> sets N"

68 with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"

69 by (rule measurable_sets)

70 then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"

71 by (rule in_sets_embed_measure)

72 also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"

73 by (auto simp: space_embed_measure)

74 finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .

75 qed (insert measurable_space[OF assms], auto simp: space_embed_measure)

77 lemma measurable_embed_measure2':

78 assumes "inj_on f (space M)"

79 shows "f \<in> measurable M (embed_measure M f)"

80 proof-

81 {

82 fix A assume A: "A \<in> sets M"

83 also from this have "A = A \<inter> space M" by auto

84 also have "... = f -` f ` A \<inter> space M" using A assms

85 by (auto dest: inj_onD sets.sets_into_space)

86 finally have "f -` f ` A \<inter> space M \<in> sets M" .

87 }

88 thus ?thesis using assms unfolding embed_measure_def

89 by (intro measurable_measure_of) (auto dest: sets.sets_into_space)

90 qed

92 lemma measurable_embed_measure2:

93 assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"

94 by (auto simp: inj_vimage_image_eq embed_measure_def

95 intro!: measurable_measure_of dest: sets.sets_into_space)

97 lemma embed_measure_eq_distr':

98 assumes "inj_on f (space M)"

99 shows "embed_measure M f = distr M (embed_measure M f) f"

100 proof-

101 have "distr M (embed_measure M f) f =

102 measure_of (f ` space M) {f ` A |A. A \<in> sets M}

103 (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def

104 by (simp add: space_embed_measure sets_embed_measure'[OF assms])

105 also have "... = embed_measure M f" unfolding embed_measure_def ..

106 finally show ?thesis ..

107 qed

109 lemma embed_measure_eq_distr:

110 "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"

111 by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)

113 lemma nn_integral_embed_measure':

114 "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>

115 nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"

116 apply (subst embed_measure_eq_distr', simp)

117 apply (subst nn_integral_distr)

118 apply (simp_all add: measurable_embed_measure2')

119 done

121 lemma nn_integral_embed_measure:

122 "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>

123 nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"

124 by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp

126 lemma emeasure_embed_measure':

127 assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"

128 shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"

129 by (subst embed_measure_eq_distr'[OF assms(1)])

130 (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])

132 lemma emeasure_embed_measure:

133 assumes "inj f" "A \<in> sets (embed_measure M f)"

134 shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"

135 using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)

137 lemma embed_measure_comp:

138 assumes [simp]: "inj f" "inj g"

139 shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"

140 proof-

141 have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)

142 note measurable_embed_measure2[measurable]

143 have "embed_measure (embed_measure M f) g =

144 distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"

145 by (subst (1 2) embed_measure_eq_distr)

146 (simp_all add: distr_distr sets_embed_measure cong: distr_cong)

147 also have "... = embed_measure M (g \<circ> f)"

148 by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)

149 (auto simp: sets_embed_measure o_def image_image[symmetric]

150 intro: inj_comp cong: distr_cong)

151 finally show ?thesis .

152 qed

154 lemma sigma_finite_embed_measure:

155 assumes "sigma_finite_measure M" and inj: "inj f"

156 shows "sigma_finite_measure (embed_measure M f)"

157 proof

158 case goal1

159 from assms(1) interpret sigma_finite_measure M .

160 from sigma_finite_countable obtain A where

161 A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast

162 show ?case

163 proof (intro exI[of _ "op ` f`A"] conjI allI)

164 from A_props show "countable (op ` f`A)" by auto

165 from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)"

166 by (auto simp: sets_embed_measure)

167 from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"

168 by (auto simp: space_embed_measure intro!: imageI)

169 from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"

170 by (intro ballI, subst emeasure_embed_measure)

171 (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)

172 qed

173 qed

175 lemma embed_measure_count_space':

176 "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"

177 apply (subst distr_bij_count_space[of f A "f`A", symmetric])

178 apply (simp add: inj_on_def bij_betw_def)

179 apply (subst embed_measure_eq_distr')

180 apply simp

181 apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff)

182 apply (subst (1 2) emeasure_distr)

183 apply (auto simp: space_embed_measure sets_embed_measure')

184 done

186 lemma embed_measure_count_space:

187 "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"

188 by(rule embed_measure_count_space')(erule subset_inj_on, simp)

190 lemma sets_embed_measure_alt:

191 "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"

192 by (auto simp: sets_embed_measure)

194 lemma emeasure_embed_measure_image':

195 assumes "inj_on f (space M)" "X \<in> sets M"

196 shows "emeasure (embed_measure M f) (f`X) = emeasure M X"

197 proof-

198 from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"

199 by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')

200 also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)

201 finally show ?thesis .

202 qed

204 lemma emeasure_embed_measure_image:

205 "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"

206 by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)

208 lemma embed_measure_eq_iff:

209 assumes "inj f"

210 shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")

211 proof

212 from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)

213 assume asm: "?M = ?N"

214 hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp

215 with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)

216 moreover {

217 fix X assume "X \<in> sets A"

218 from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp

219 with `X \<in> sets A` and `sets A = sets B` and assms

220 have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)

221 }

222 ultimately show "A = B" by (rule measure_eqI)

223 qed simp

225 lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"

226 by (auto simp: the_inv_into_f_f)

228 lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"

229 using map_prod_surj_on[OF refl refl] .

231 lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"

232 by auto

234 lemma embed_measure_prod:

235 assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"

236 shows "embed_measure M f \<Otimes>\<^sub>M embed_measure N g = embed_measure (M \<Otimes>\<^sub>M N) (\<lambda>(x, y). (f x, g y))"

237 (is "?L = _")

238 unfolding map_prod_def[symmetric]

239 proof (rule pair_measure_eqI)

240 have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"

241 using f g by (auto simp: inj_on_def)

243 show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"

244 unfolding map_prod_def[symmetric]

245 apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra

246 cong: vimage_algebra_cong)

247 apply (subst vimage_algebra_Sup_sigma)

248 apply (simp_all add: space_pair_measure[symmetric])

249 apply (auto simp add: the_inv_into_f_f

250 simp del: map_prod_simp

251 del: prod_fun_imageE) []

252 apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)

253 apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)

254 apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq

255 space_pair_measure[symmetric] map_prod_image[symmetric])

256 apply (intro arg_cong[where f=sets] arg_cong[where f=Sup_sigma] arg_cong2[where f=insert] vimage_algebra_cong)

257 apply (auto simp: map_prod_image the_inv_into_f_f

258 simp del: map_prod_simp del: prod_fun_imageE)

259 apply (simp_all add: the_inv_into_f_f space_pair_measure)

260 done

262 note measurable_embed_measure2[measurable]

263 fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"

264 moreover have "f -` A \<times> g -` B \<inter> space (M \<Otimes>\<^sub>M N) = (f -` A \<inter> space M) \<times> (g -` B \<inter> space N)"

265 by (auto simp: space_pair_measure)

266 ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =

267 emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"

268 by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure

269 sigma_finite_measure.emeasure_pair_measure_Times)

270 qed (insert assms, simp_all add: sigma_finite_embed_measure)

272 lemma density_embed_measure:

273 assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"

274 shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")

275 proof (rule measure_eqI)

276 fix X assume X: "X \<in> sets ?M1"

277 from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)"

278 by (rule measurable_embed_measure2)

279 from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f"

280 by (subst emeasure_density) simp_all

281 also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"

282 by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr)

283 (auto intro!: borel_measurable_ereal_times borel_measurable_indicator)

284 also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"

285 by (intro nn_integral_cong) (auto split: split_indicator)

286 also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"

287 by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])

288 also from X and inj have "... = emeasure ?M2 X"

289 by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)

290 finally show "emeasure ?M1 X = emeasure ?M2 X" .

291 qed (simp_all add: sets_embed_measure inj)

293 lemma density_embed_measure':

294 assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"

295 shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"

296 proof-

297 have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"

298 by (rule density_embed_measure[OF inj])

299 (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong,

300 rule inv, rule measurable_ident_sets, simp, rule Mg)

301 also have "density M (g \<circ> f' \<circ> f) = density M g"

302 by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)

303 finally show ?thesis .

304 qed

306 lemma inj_on_image_subset_iff:

307 assumes "inj_on f C" "A \<subseteq> C" "B \<subseteq> C"

308 shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"

309 proof (intro iffI subsetI)

310 fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"

311 from B have "f x \<in> f ` A" by blast

312 with A have "f x \<in> f ` B" by blast

313 then obtain y where "f x = f y" and "y \<in> B" by blast

314 with assms and B have "x = y" by (auto dest: inj_onD)

315 with `y \<in> B` show "x \<in> B" by simp

316 qed auto

319 lemma AE_embed_measure':

320 assumes inj: "inj_on f (space M)"

321 shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"

322 proof

323 let ?M = "embed_measure M f"

324 assume "AE x in ?M. P x"

325 then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"

326 by (force elim: AE_E)

327 then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)

328 moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}"

329 by (auto simp: inj space_embed_measure)

330 from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"

331 by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])

332 (insert A'_props, auto dest: sets.sets_into_space)

333 moreover from A_props A'_props have "emeasure M A' = 0"

334 by (simp add: emeasure_embed_measure_image' inj)

335 ultimately show "AE x in M. P (f x)" by (intro AE_I)

336 next

337 let ?M = "embed_measure M f"

338 assume "AE x in M. P (f x)"

339 then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"

340 by (force elim: AE_E)

341 hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"

342 by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)

343 thus "AE x in ?M. P x" by (intro AE_I)

344 qed

346 lemma AE_embed_measure:

347 assumes inj: "inj f"

348 shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"

349 using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)

351 lemma nn_integral_monotone_convergence_SUP_countable:

352 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"

353 assumes nonempty: "Y \<noteq> {}"

354 and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"

355 and countable: "countable B"

356 shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"

357 (is "?lhs = ?rhs")

358 proof -

359 let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"

360 have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"

361 by(rule nn_integral_cong)(simp add: countable)

362 also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"

363 by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)

364 also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"

365 by(simp add: nn_integral_count_space_indicator ereal_indicator[symmetric] Sup_ereal_mult_right' nonempty)

366 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)" using nonempty

367 proof(rule nn_integral_monotone_convergence_SUP_nat)

368 show "Complete_Partial_Order.chain op \<le> (?f ` Y)"

369 by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)

370 qed

371 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"

372 by(simp add: nn_integral_count_space_indicator)

373 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"

374 by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)

375 also have "\<dots> = ?rhs"

376 by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)

377 finally show ?thesis .

378 qed

380 end