author  hoelzl 
Fri, 26 Mar 2010 18:03:01 +0100  
changeset 35977  30d42bfd0174 
parent 35929  90f38c8831e2 
child 36624  25153c08655e 
permissions  rwrr 
35582  1 
theory Probability_Space 
2 
imports Lebesgue 

3 
begin 

4 

5 
locale prob_space = measure_space + 

6 
assumes prob_space: "measure M (space M) = 1" 

7 
begin 

8 

9 
abbreviation "events \<equiv> sets M" 

10 
abbreviation "prob \<equiv> measure M" 

11 
abbreviation "prob_preserving \<equiv> measure_preserving" 

12 
abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s" 

13 
abbreviation "expectation \<equiv> integral" 

14 

15 
definition 

16 
"indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B" 

17 

18 
definition 

19 
"indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)" 

20 

21 
definition 

22 
"distribution X = (\<lambda>s. prob ((X ` s) \<inter> (space M)))" 

23 

24 
definition 

25 
"probably e \<longleftrightarrow> e \<in> events \<and> prob e = 1" 

26 

27 
definition 

28 
"possibly e \<longleftrightarrow> e \<in> events \<and> prob e \<noteq> 0" 

29 

30 
definition 

31 
"joint_distribution X Y \<equiv> (\<lambda>a. prob ((\<lambda>x. (X x, Y x)) ` a \<inter> space M))" 

32 

33 
definition 

34 
"conditional_expectation X s \<equiv> THE f. random_variable borel_space f \<and> 

35 
(\<forall> g \<in> s. integral (\<lambda>x. f x * indicator_fn g x) = 

36 
integral (\<lambda>x. X x * indicator_fn g x))" 

37 

38 
definition 

39 
"conditional_prob e1 e2 \<equiv> conditional_expectation (indicator_fn e1) e2" 

40 

35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset

41 
lemma positive': "positive M prob" 
35582  42 
unfolding positive_def using positive empty_measure by blast 
43 

44 
lemma prob_compl: 

45 
assumes "s \<in> events" 

46 
shows "prob (space M  s) = 1  prob s" 

47 
using assms 

48 
proof  

49 
have "prob ((space M  s) \<union> s) = prob (space M  s) + prob s" 

50 
using assms additive[unfolded additive_def] by blast 

51 
thus ?thesis by (simp add:Un_absorb2[OF sets_into_space[OF assms]] prob_space) 

52 
qed 

53 

54 
lemma indep_space: 

55 
assumes "s \<in> events" 

56 
shows "indep (space M) s" 

57 
using assms prob_space 

58 
unfolding indep_def by auto 

59 

60 

61 
lemma prob_space_increasing: 

62 
"increasing M prob" 

35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset

63 
by (rule additive_increasing[OF positive' additive]) 
35582  64 

65 
lemma prob_subadditive: 

66 
assumes "s \<in> events" "t \<in> events" 

67 
shows "prob (s \<union> t) \<le> prob s + prob t" 

68 
using assms 

69 
proof  

70 
have "prob (s \<union> t) = prob ((s  t) \<union> t)" by simp 

71 
also have "\<dots> = prob (s  t) + prob t" 

72 
using additive[unfolded additive_def, rule_format, of "st" "t"] 

73 
assms by blast 

74 
also have "\<dots> \<le> prob s + prob t" 

75 
using prob_space_increasing[unfolded increasing_def, rule_format] assms 

76 
by auto 

77 
finally show ?thesis by simp 

78 
qed 

79 

80 
lemma prob_zero_union: 

81 
assumes "s \<in> events" "t \<in> events" "prob t = 0" 

82 
shows "prob (s \<union> t) = prob s" 

83 
using assms 

84 
proof  

85 
have "prob (s \<union> t) \<le> prob s" 

86 
using prob_subadditive[of s t] assms by auto 

87 
moreover have "prob (s \<union> t) \<ge> prob s" 

88 
using prob_space_increasing[unfolded increasing_def, rule_format] 

89 
assms by auto 

90 
ultimately show ?thesis by simp 

91 
qed 

92 

93 
lemma prob_eq_compl: 

94 
assumes "s \<in> events" "t \<in> events" 

95 
assumes "prob (space M  s) = prob (space M  t)" 

96 
shows "prob s = prob t" 

97 
using assms prob_compl by auto 

98 

99 
lemma prob_one_inter: 

100 
assumes events:"s \<in> events" "t \<in> events" 

101 
assumes "prob t = 1" 

102 
shows "prob (s \<inter> t) = prob s" 

103 
using assms 

104 
proof  

105 
have "prob ((space M  s) \<union> (space M  t)) = prob (space M  s)" 

106 
using prob_compl[of "t"] prob_zero_union assms by auto 

107 
then show "prob (s \<inter> t) = prob s" 

108 
using prob_eq_compl[of "s \<inter> t"] events by (simp only: Diff_Int) auto 

109 
qed 

110 

111 
lemma prob_eq_bigunion_image: 

112 
assumes "range f \<subseteq> events" "range g \<subseteq> events" 

113 
assumes "disjoint_family f" "disjoint_family g" 

114 
assumes "\<And> n :: nat. prob (f n) = prob (g n)" 

115 
shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))" 

116 
using assms 

117 
proof  

118 
have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" 

119 
using ca[unfolded countably_additive_def] assms by blast 

120 
have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))" 

121 
using ca[unfolded countably_additive_def] assms by blast 

122 
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp 

123 
qed 

124 

125 
lemma prob_countably_subadditive: 

126 
assumes "range f \<subseteq> events" 

127 
assumes "summable (prob \<circ> f)" 

128 
shows "prob (\<Union>i. f i) \<le> (\<Sum> i. prob (f i))" 

129 
using assms 

130 
proof  

131 
def f' == "\<lambda> i. f i  (\<Union> j \<in> {0 ..< i}. f j)" 

132 
have "(\<Union> i. f' i) \<subseteq> (\<Union> i. f i)" unfolding f'_def by auto 

133 
moreover have "(\<Union> i. f' i) \<supseteq> (\<Union> i. f i)" 

134 
proof (rule subsetI) 

135 
fix x assume "x \<in> (\<Union> i. f i)" 

136 
then obtain k where "x \<in> f k" by blast 

137 
hence k: "k \<in> {m. x \<in> f m}" by simp 

138 
have "\<exists> l. x \<in> f l \<and> (\<forall> l' < l. x \<notin> f l')" 

139 
using wfE_min[of "{(x, y). x < y}" "k" "{m. x \<in> f m}", 

140 
OF wf_less k] by auto 

141 
thus "x \<in> (\<Union> i. f' i)" unfolding f'_def by auto 

142 
qed 

143 
ultimately have uf'f: "(\<Union> i. f' i) = (\<Union> i. f i)" by (rule equalityI) 

144 

145 
have df': "\<And> i j. i < j \<Longrightarrow> f' i \<inter> f' j = {}" 

146 
unfolding f'_def by auto 

147 
have "\<And> i j. i \<noteq> j \<Longrightarrow> f' i \<inter> f' j = {}" 

148 
apply (drule iffD1[OF nat_neq_iff]) 

149 
using df' by auto 

150 
hence df: "disjoint_family f'" unfolding disjoint_family_on_def by simp 

151 

152 
have rf': "\<And> i. f' i \<in> events" 

153 
proof  

154 
fix i :: nat 

155 
have "(\<Union> {f j  j. j \<in> {0 ..< i}}) = (\<Union> j \<in> {0 ..< i}. f j)" by blast 

156 
hence "(\<Union> {f j  j. j \<in> {0 ..< i}}) \<in> events 

157 
\<Longrightarrow> (\<Union> j \<in> {0 ..< i}. f j) \<in> events" by auto 

158 
thus "f' i \<in> events" 

159 
unfolding f'_def 

160 
using assms finite_union[of "{f j  j. j \<in> {0 ..< i}}"] 

161 
Diff[of "f i" "\<Union> j \<in> {0 ..< i}. f j"] by auto 

162 
qed 

163 
hence uf': "(\<Union> range f') \<in> events" by auto 

164 

165 
have "\<And> i. prob (f' i) \<le> prob (f i)" 

166 
using prob_space_increasing[unfolded increasing_def, rule_format, OF rf'] 

167 
assms rf' unfolding f'_def by blast 

168 

169 
hence absinc: "\<And> i. \<bar> prob (f' i) \<bar> \<le> prob (f i)" 

35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset

170 
using abs_of_nonneg positive'[unfolded positive_def] 
35582  171 
assms rf' by auto 
172 

173 
have "prob (\<Union> i. f i) = prob (\<Union> i. f' i)" using uf'f by simp 

174 

175 
also have "\<dots> = (\<Sum> i. prob (f' i))" 

176 
using ca[unfolded countably_additive_def, rule_format] 

177 
sums_unique rf' uf' df 

178 
by auto 

179 

180 
also have "\<dots> \<le> (\<Sum> i. prob (f i))" 

181 
using summable_le2[of "\<lambda> i. prob (f' i)" "\<lambda> i. prob (f i)", 

182 
rule_format, OF absinc] 

183 
assms[unfolded o_def] by auto 

184 

185 
finally show ?thesis by auto 

186 
qed 

187 

188 
lemma prob_countably_zero: 

189 
assumes "range c \<subseteq> events" 

190 
assumes "\<And> i. prob (c i) = 0" 

191 
shows "(prob (\<Union> i :: nat. c i) = 0)" 

192 
using assms 

193 
proof  

194 
have leq0: "0 \<le> prob (\<Union> i. c i)" 

35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset

195 
using assms positive'[unfolded positive_def, rule_format] 
35582  196 
by auto 
197 

198 
have "prob (\<Union> i. c i) \<le> (\<Sum> i. prob (c i))" 

199 
using prob_countably_subadditive[of c, unfolded o_def] 

200 
assms sums_zero sums_summable by auto 

201 

202 
also have "\<dots> = 0" 

203 
using assms sums_zero 

204 
sums_unique[of "\<lambda> i. prob (c i)" "0"] by auto 

205 

206 
finally show "prob (\<Union> i. c i) = 0" 

207 
using leq0 by auto 

208 
qed 

209 

210 
lemma indep_sym: 

211 
"indep a b \<Longrightarrow> indep b a" 

212 
unfolding indep_def using Int_commute[of a b] by auto 

213 

214 
lemma indep_refl: 

215 
assumes "a \<in> events" 

216 
shows "indep a a = (prob a = 0) \<or> (prob a = 1)" 

217 
using assms unfolding indep_def by auto 

218 

219 
lemma prob_equiprobable_finite_unions: 

220 
assumes "s \<in> events" 

221 
assumes "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events" 

222 
assumes "finite s" 

223 
assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})" 

224 
shows "prob s = of_nat (card s) * prob {SOME x. x \<in> s}" 

225 
using assms 

226 
proof (cases "s = {}") 

227 
case True thus ?thesis by simp 

228 
next 

229 
case False hence " \<exists> x. x \<in> s" by blast 

230 
from someI_ex[OF this] assms 

231 
have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast 

232 
have "prob s = (\<Sum> x \<in> s. prob {x})" 

233 
using assms measure_real_sum_image by blast 

234 
also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto 

235 
also have "\<dots> = of_nat (card s) * prob {(SOME x. x \<in> s)}" 

236 
using setsum_constant assms by auto 

237 
finally show ?thesis by simp 

238 
qed 

239 

240 
lemma prob_real_sum_image_fn: 

241 
assumes "e \<in> events" 

242 
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events" 

243 
assumes "finite s" 

244 
assumes "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}" 

245 
assumes "space M \<subseteq> (\<Union> i \<in> s. f i)" 

246 
shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))" 

247 
using assms 

248 
proof  

249 
let ?S = "{0 ..< card s}" 

250 
obtain g where "g ` ?S = s \<and> inj_on g ?S" 

251 
using ex_bij_betw_nat_finite[unfolded bij_betw_def, of s] assms by auto 

252 
moreover hence gs: "g ` ?S = s" by simp 

253 
ultimately have ginj: "inj_on g ?S" by simp 

254 
let ?f' = "\<lambda> i. e \<inter> f (g i)" 

255 
have f': "?f' \<in> ?S \<rightarrow> events" 

256 
using gs assms by blast 

257 
hence "\<And> i j. \<lbrakk>i \<in> ?S ; j \<in> ?S ; i \<noteq> j\<rbrakk> 

258 
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" using assms ginj[unfolded inj_on_def] gs f' by blast 

259 
hence df': "\<And> i j. \<lbrakk>i < card s ; j < card s ; i \<noteq> j\<rbrakk> 

260 
\<Longrightarrow> ?f' i \<inter> ?f' j = {}" by simp 

261 

262 
have "e = e \<inter> space M" using assms sets_into_space by simp 

263 
also hence "\<dots> = e \<inter> (\<Union> x \<in> s. f x)" using assms by blast 

264 
also have "\<dots> = (\<Union> x \<in> g ` ?S. e \<inter> f x)" using gs by simp 

265 
also have "\<dots> = (\<Union> i \<in> ?S. ?f' i)" by simp 

266 
finally have "prob e = prob (\<Union> i \<in> ?S. ?f' i)" by simp 

267 
also have "\<dots> = (\<Sum> i \<in> ?S. prob (?f' i))" 

268 
apply (subst measure_finitely_additive'') 

269 
using f' df' assms by (auto simp: disjoint_family_on_def) 

270 
also have "\<dots> = (\<Sum> x \<in> g ` ?S. prob (e \<inter> f x))" 

271 
using setsum_reindex[of g "?S" "\<lambda> x. prob (e \<inter> f x)"] 

272 
ginj by simp 

273 
also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" using gs by simp 

274 
finally show ?thesis by simp 

275 
qed 

276 

277 
lemma distribution_prob_space: 

278 
assumes "random_variable s X" 

279 
shows "prob_space \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>" 

280 
using assms 

281 
proof  

282 
let ?N = "\<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>" 

283 
interpret s: sigma_algebra "s" using assms[unfolded measurable_def] by auto 

284 
hence sigN: "sigma_algebra ?N" using s.sigma_algebra_extend by auto 

285 

286 
have pos: "\<And> e. e \<in> sets s \<Longrightarrow> distribution X e \<ge> 0" 

287 
unfolding distribution_def 

35929
90f38c8831e2
Unhide measure_space.positive defined in Caratheodory.
hoelzl
parents:
35582
diff
changeset

288 
using positive'[unfolded positive_def] 
35582  289 
assms[unfolded measurable_def] by auto 
290 

291 
have cas: "countably_additive ?N (distribution X)" 

292 
proof  

293 
{ 

294 
fix f :: "nat \<Rightarrow> 'c \<Rightarrow> bool" 

295 
let ?g = "\<lambda> n. X ` f n \<inter> space M" 

296 
assume asm: "range f \<subseteq> sets s" "UNION UNIV f \<in> sets s" "disjoint_family f" 

297 
hence "range ?g \<subseteq> events" 

298 
using assms unfolding measurable_def by blast 

299 
from ca[unfolded countably_additive_def, 

300 
rule_format, of ?g, OF this] countable_UN[OF this] asm 

301 
have "(\<lambda> n. prob (?g n)) sums prob (UNION UNIV ?g)" 

302 
unfolding disjoint_family_on_def by blast 

303 
moreover have "(X ` (\<Union> n. f n)) = (\<Union> n. X ` f n)" by blast 

304 
ultimately have "(\<lambda> n. distribution X (f n)) sums distribution X (UNION UNIV f)" 

305 
unfolding distribution_def by simp 

306 
} thus ?thesis unfolding countably_additive_def by simp 

307 
qed 

308 

309 
have ds0: "distribution X {} = 0" 

310 
unfolding distribution_def by simp 

311 

312 
have "X ` space s \<inter> space M = space M" 

313 
using assms[unfolded measurable_def] by auto 

314 
hence ds1: "distribution X (space s) = 1" 

315 
unfolding measurable_def distribution_def using prob_space by simp 

316 

317 
from ds0 ds1 cas pos sigN 

318 
show "prob_space ?N" 

319 
unfolding prob_space_def prob_space_axioms_def 

320 
measure_space_def measure_space_axioms_def by simp 

321 
qed 

322 

323 
lemma distribution_lebesgue_thm1: 

324 
assumes "random_variable s X" 

325 
assumes "A \<in> sets s" 

326 
shows "distribution X A = expectation (indicator_fn (X ` A \<inter> space M))" 

327 
unfolding distribution_def 

328 
using assms unfolding measurable_def 

329 
using integral_indicator_fn by auto 

330 

331 
lemma distribution_lebesgue_thm2: 

332 
assumes "random_variable s X" "A \<in> sets s" 

333 
shows "distribution X A = measure_space.integral \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr> (indicator_fn A)" 

334 
(is "_ = measure_space.integral ?M _") 

335 
proof  

336 
interpret S: prob_space ?M using assms(1) by (rule distribution_prob_space) 

337 

338 
show ?thesis 

339 
using S.integral_indicator_fn(1) 

340 
using assms unfolding distribution_def by auto 

341 
qed 

342 

343 
lemma finite_expectation1: 

344 
assumes "finite (space M)" "random_variable borel_space X" 

345 
shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X ` {r} \<inter> space M))" 

346 
using assms integral_finite measurable_def 

347 
unfolding borel_measurable_def by auto 

348 

349 
lemma finite_expectation: 

350 
assumes "finite (space M) \<and> random_variable borel_space X" 

351 
shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})" 

352 
using assms unfolding distribution_def using finite_expectation1 by auto 

353 
lemma prob_x_eq_1_imp_prob_y_eq_0: 

354 
assumes "{x} \<in> events" 

355 
assumes "(prob {x} = 1)" 

356 
assumes "{y} \<in> events" 

357 
assumes "y \<noteq> x" 

358 
shows "prob {y} = 0" 

359 
using prob_one_inter[of "{y}" "{x}"] assms by auto 

360 

361 
lemma distribution_x_eq_1_imp_distribution_y_eq_0: 

362 
assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X" 

363 
assumes "(distribution X {x} = 1)" 

364 
assumes "y \<noteq> x" 

365 
shows "distribution X {y} = 0" 

366 
proof  

367 
let ?S = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr>" 

368 
let ?M = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M)), measure = distribution X\<rparr>" 

369 
interpret S: prob_space ?M 

370 
using distribution_prob_space[OF X] by auto 

371 
{ assume "{x} \<notin> sets ?M" 

372 
hence "x \<notin> X ` space M" by auto 

373 
hence "X ` {x} \<inter> space M = {}" by auto 

374 
hence "distribution X {x} = 0" unfolding distribution_def by auto 

375 
hence "False" using assms by auto } 

376 
hence x: "{x} \<in> sets ?M" by auto 

377 
{ assume "{y} \<notin> sets ?M" 

378 
hence "y \<notin> X ` space M" by auto 

379 
hence "X ` {y} \<inter> space M = {}" by auto 

380 
hence "distribution X {y} = 0" unfolding distribution_def by auto } 

381 
moreover 

382 
{ assume "{y} \<in> sets ?M" 

383 
hence "distribution X {y} = 0" using assms S.prob_x_eq_1_imp_prob_y_eq_0[OF x] by auto } 

384 
ultimately show ?thesis by auto 

385 
qed 

386 

35977  387 

35582  388 
end 
389 

35977  390 
locale finite_prob_space = prob_space + finite_measure_space 
391 

392 
lemma (in finite_prob_space) finite_marginal_product_space_POW2: 

393 
assumes "finite s1" "finite s2" 

394 
shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>" 

395 
(is "finite_measure_space ?M") 

396 
proof (rule finite_Pow_additivity_sufficient) 

397 
show "positive ?M (measure ?M)" 

398 
unfolding positive_def using positive'[unfolded positive_def] assms sets_eq_Pow 

399 
by (simp add: joint_distribution_def) 

400 

401 
show "additive ?M (measure ?M)" unfolding additive_def 

402 
proof safe 

403 
fix x y 

404 
have A: "((\<lambda>x. (X x, Y x)) ` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto 

405 
have B: "((\<lambda>x. (X x, Y x)) ` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto 

406 
assume "x \<inter> y = {}" 

407 
from additive[unfolded additive_def, rule_format, OF A B] this 

408 
show "measure ?M (x \<union> y) = measure ?M x + measure ?M y" 

409 
apply (simp add: joint_distribution_def) 

410 
apply (subst Int_Un_distrib2) 

411 
by auto 

412 
qed 

413 

414 
show "finite (space ?M)" 

415 
using assms by auto 

416 

417 
show "sets ?M = Pow (space ?M)" 

418 
by simp 

419 
qed 

420 

421 
lemma (in finite_prob_space) finite_marginal_product_space_POW: 

422 
shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M, 

423 
sets = Pow (X ` space M \<times> Y ` space M), 

424 
measure = joint_distribution X Y\<rparr>" 

425 
(is "finite_measure_space ?M") 

426 
using finite_space by (auto intro!: finite_marginal_product_space_POW2) 

427 

35582  428 
end 