1(* interactive mode 2app load ["boolLib", "bossLib", "arithmeticTheory", "realTheory", 3 "seqTheory", "pred_setTheory", "res_quanTheory", "listTheory", 4 "rich_listTheory", "pairTheory", "combinTheory", "realLib", "formalizeUseful", 5 "subtypeTheory", "extra_pred_setTheory", "extra_boolTheory", "optionTheory", 6 "extra_realTheory", "extra_numTheory", 7 "measureTheory", "simpLib", "borelTheory", "lebesgueTheory"]; 8 9 10quietdec := true; 11*) 12 13open HolKernel Parse boolLib bossLib arithmeticTheory realTheory 14 seqTheory pred_setTheory res_quanTheory listTheory 15 rich_listTheory pairTheory combinTheory realLib formalizeUseful 16 subtypeTheory extra_pred_setTheory extra_boolTheory optionTheory 17 extra_realTheory extra_numTheory 18 measureTheory simpLib borelTheory lebesgueTheory; 19 20open real_sigmaTheory; 21 22val _ = new_theory "probability"; 23 24(* ------------------------------------------------------------------------- *) 25(* Tools. *) 26(* ------------------------------------------------------------------------- *) 27 28val Strip = rpt (POP_ASSUM MP_TAC) >> rpt STRIP_TAC; 29val Simplify = RW_TAC arith_ss; 30val Suff = PARSE_TAC SUFF_TAC; 31val Know = PARSE_TAC KNOW_TAC; 32val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 33val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 34val Cond = 35 DISCH_THEN 36 (fn mp_th => 37 let 38 val cond = fst (dest_imp (concl mp_th)) 39 in 40 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 41 end); 42 43val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 44 45(* ------------------------------------------------------------------------- *) 46(* Basic probability theory definitions. *) 47(* ------------------------------------------------------------------------- *) 48 49val p_space_def = Define `p_space = m_space`; 50 51val events_def = Define `events = measurable_sets`; 52 53val prob_def = Define `prob = measure`; 54 55val prob_preserving_def = Define `prob_preserving = measure_preserving`; 56 57val prob_space_def = Define 58 `prob_space p = measure_space p /\ (measure p (p_space p) = 1)`; 59 60val indep_def = Define 61 `indep p a b = 62 a IN events p /\ b IN events p /\ 63 (prob p (a INTER b) = prob p a * prob p b)`; 64 65val indep_families_def = Define 66 `indep_families p q r = !s t. s IN q /\ t IN r ==> indep p s t`; 67 68(* ?????????????????????????????????????????????????????? 69 70val indep_function_def = Define 71 `indep_function p = 72 {f | 73 indep_families p (IMAGE (PREIMAGE (FST o f)) UNIV) 74 (IMAGE (PREIMAGE (SND o f)) (events p))}`; 75 76?????????????????????????????????????????????????????? *) 77 78val probably_def = Define `probably p e = (e IN events p) /\ (prob p e = 1)`; 79 80val possibly_def = Define `possibly p e = (e IN events p) /\ ~(prob p e = 0)`; 81 82val random_variable_def = Define 83 `random_variable X p s = prob_space p /\ X IN measurable (p_space p, events p) s`; 84 85val real_random_variable_def = Define 86 `real_random_variable X p = prob_space p /\ X IN borel_measurable (p_space p, events p)`; 87 88val distribution_def = Define 89 `distribution p X = (\s. prob p ((PREIMAGE X s) INTER (p_space p)))`; 90 91val joint_distribution_def = Define 92 `joint_distribution p X Y = (\a. prob p (PREIMAGE (\x. (X x, Y x)) a INTER p_space p))`; 93 94val expectation_def = Define 95 `expectation = integral`; 96 97val conditional_expectation_def = Define 98 `conditional_expectation p X s = 99 @f. real_random_variable f p /\ 100 !g. g IN s ==> 101 (integral p (\x. f x * indicator_fn g x) = 102 integral p (\x. X x * indicator_fn g x))`; 103 104val conditional_prob_def = Define 105 `conditional_prob p e1 e2 = conditional_expectation p (indicator_fn e1) e2`; 106 107val rv_conditional_expectation_def = Define 108 `rv_conditional_expectation p s X Y = conditional_expectation p X (IMAGE (\a. (PREIMAGE Y a) INTER p_space p) (subsets s))`; 109 110(* ------------------------------------------------------------------------- *) 111(* Basic probability theorems, leading to: *) 112(* 1. s IN events p ==> (prob p (COMPL s) = 1 - prob p s) *) 113(* ------------------------------------------------------------------------- *) 114 115(* new definitions in terms of prob & events *) 116 117val POSITIVE_PROB = store_thm 118 ("POSITIVE_PROB", 119 ``!p. positive p = (prob p {} = 0) /\ !s. s IN events p ==> 0 <= prob p s``, 120 RW_TAC std_ss [positive_def, prob_def, events_def]); 121 122val INCREASING_PROB = store_thm 123 ("INCREASING_PROB", 124 ``!p. 125 increasing p = 126 !s t. 127 s IN events p /\ t IN events p /\ s SUBSET t ==> 128 prob p s <= prob p t``, 129 RW_TAC std_ss [increasing_def, prob_def, events_def]); 130 131val ADDITIVE_PROB = store_thm 132 ("ADDITIVE_PROB", 133 ``!p. 134 additive p = 135 !s t. 136 s IN events p /\ t IN events p /\ DISJOINT s t ==> 137 (prob p (s UNION t) = prob p s + prob p t)``, 138 RW_TAC std_ss [additive_def, prob_def, events_def]); 139 140val COUNTABLY_ADDITIVE_PROB = store_thm 141 ("COUNTABLY_ADDITIVE_PROB", 142 ``!p. 143 countably_additive p = 144 !f. 145 f IN (UNIV -> events p) /\ 146 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 147 BIGUNION (IMAGE f UNIV) IN events p ==> 148 prob p o f sums prob p (BIGUNION (IMAGE f UNIV))``, 149 RW_TAC std_ss [countably_additive_def, prob_def, events_def]); 150 151(* properties of prob spaces *) 152 153val PROB_SPACE = store_thm 154 ("PROB_SPACE", 155 ``!p. 156 prob_space p = 157 sigma_algebra (p_space p, events p) /\ positive p /\ countably_additive p /\ 158 (prob p (p_space p) = 1)``, 159 RW_TAC std_ss [prob_space_def, prob_def, events_def, measure_space_def, p_space_def] 160 >> PROVE_TAC []); 161 162val EVENTS_SIGMA_ALGEBRA = store_thm 163 ("EVENTS_SIGMA_ALGEBRA", 164 ``!p. prob_space p ==> sigma_algebra (p_space p, events p)``, 165 RW_TAC std_ss [PROB_SPACE]); 166 167val EVENTS_ALGEBRA = store_thm 168 ("EVENTS_ALGEBRA", 169 ``!p. prob_space p ==> algebra (p_space p, events p)``, 170 PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA, EVENTS_SIGMA_ALGEBRA]); 171 172val PROB_EMPTY = store_thm 173 ("PROB_EMPTY", 174 ``!p. prob_space p ==> (prob p {} = 0)``, 175 PROVE_TAC [PROB_SPACE, POSITIVE_PROB]); 176 177val PROB_UNIV = store_thm 178 ("PROB_UNIV", 179 ``!p. prob_space p ==> (prob p (p_space p) = 1)``, 180 RW_TAC std_ss [PROB_SPACE]); 181 182val PROB_SPACE_POSITIVE = store_thm 183 ("PROB_SPACE_POSITIVE", 184 ``!p. prob_space p ==> positive p``, 185 RW_TAC std_ss [PROB_SPACE]); 186 187val PROB_SPACE_COUNTABLY_ADDITIVE = store_thm 188 ("PROB_SPACE_COUNTABLY_ADDITIVE", 189 ``!p. prob_space p ==> countably_additive p``, 190 RW_TAC std_ss [PROB_SPACE]); 191 192val PROB_SPACE_ADDITIVE = store_thm 193 ("PROB_SPACE_ADDITIVE", 194 ``!p. prob_space p ==> additive p``, 195 PROVE_TAC [PROB_SPACE_COUNTABLY_ADDITIVE, COUNTABLY_ADDITIVE_ADDITIVE, 196 PROB_SPACE_POSITIVE, EVENTS_ALGEBRA, events_def, p_space_def]); 197 198val PROB_SPACE_INCREASING = store_thm 199 ("PROB_SPACE_INCREASING", 200 ``!p. prob_space p ==> increasing p``, 201 PROVE_TAC [ADDITIVE_INCREASING, EVENTS_ALGEBRA, PROB_SPACE_ADDITIVE, 202 PROB_SPACE_POSITIVE, events_def, p_space_def]); 203 204(* handy theorems for use with MATCH_MP_TAC *) 205 206val PROB_POSITIVE = store_thm 207 ("PROB_POSITIVE", 208 ``!p s. prob_space p /\ s IN events p ==> 0 <= prob p s``, 209 PROVE_TAC [POSITIVE_PROB, PROB_SPACE_POSITIVE]); 210 211val PROB_INCREASING = store_thm 212 ("PROB_INCREASING", 213 ``!p s t. 214 prob_space p /\ s IN events p /\ t IN events p /\ s SUBSET t ==> 215 prob p s <= prob p t``, 216 PROVE_TAC [INCREASING_PROB, PROB_SPACE_INCREASING]); 217 218val PROB_ADDITIVE = store_thm 219 ("PROB_ADDITIVE", 220 ``!p s t u. 221 prob_space p /\ s IN events p /\ t IN events p /\ 222 DISJOINT s t /\ (u = s UNION t) ==> 223 (prob p u = prob p s + prob p t)``, 224 PROVE_TAC [ADDITIVE_PROB, PROB_SPACE_ADDITIVE]); 225 226val PROB_COUNTABLY_ADDITIVE = store_thm 227 ("PROB_COUNTABLY_ADDITIVE", 228 ``!p s f. 229 prob_space p /\ f IN (UNIV -> events p) /\ 230 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 231 (s = BIGUNION (IMAGE f UNIV)) ==> 232 prob p o f sums prob p s``, 233 RW_TAC std_ss [] 234 >> Suff `BIGUNION (IMAGE f UNIV) IN events p` 235 >- PROVE_TAC [COUNTABLY_ADDITIVE_PROB, PROB_SPACE_COUNTABLY_ADDITIVE] 236 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 237 Q.SPECL [`(p_space p, events p)`,`f`]) SIGMA_ALGEBRA_ENUM 238 >> PROVE_TAC [EVENTS_SIGMA_ALGEBRA]); 239 240(* more properties of prob_spaces *) 241 242val PROB_COMPL = store_thm 243 ("PROB_COMPL", 244 ``!p s. 245 prob_space p /\ s IN events p ==> (prob p (p_space p DIFF s) = 1 - prob p s)``, 246 RW_TAC std_ss [] 247 >> MP_TAC (Q.SPEC `p` PROB_UNIV) 248 >> ASM_REWRITE_TAC [] 249 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap o GSYM) 250 >> REWRITE_TAC [prob_def, p_space_def] 251 >> MATCH_MP_TAC MEASURE_COMPL 252 >> PROVE_TAC [events_def, prob_space_def]); 253 254val PROB_INDEP = store_thm 255 ("PROB_INDEP", 256 ``!p s t u. 257 indep p s t /\ (u = s INTER t) ==> (prob p u = prob p s * prob p t)``, 258 RW_TAC std_ss [indep_def]); 259 260val PROB_PRESERVING = store_thm 261 ("PROB_PRESERVING", 262 ``!p1 p2. 263 prob_preserving p1 p2 = 264 {f | f IN measurable (p_space p1, events p1) (p_space p2, events p2) /\ 265 measure_space p1 /\ measure_space p2 /\ 266 !s. s IN events p2 ==> (prob p1 ((PREIMAGE f s)INTER(p_space p1)) = prob p2 s)}``, 267 RW_TAC std_ss [prob_preserving_def, measure_preserving_def, events_def, 268 prob_def, p_space_def]); 269 270val PROB_PRESERVING_SUBSET = store_thm 271 ("PROB_PRESERVING_SUBSET", 272 ``!p1 p2 a. 273 prob_space p1 /\ prob_space p2 /\ 274 (events p2 = subsets (sigma (p_space p2) a)) ==> 275 prob_preserving p1 (p_space p2, a, prob p2) SUBSET 276 prob_preserving p1 p2``, 277 RW_TAC std_ss [prob_space_def, prob_preserving_def, prob_def, events_def, p_space_def] 278 >> PROVE_TAC [MEASURE_PRESERVING_SUBSET]); 279 280val PROB_PRESERVING_LIFT = store_thm 281 ("PROB_PRESERVING_LIFT", 282 ``!p1 p2 a f. 283 prob_space p1 /\ prob_space p2 /\ 284 (events p2 = subsets (sigma (m_space p2) a)) /\ 285 f IN prob_preserving p1 (m_space p2, a, prob p2) ==> 286 f IN prob_preserving p1 p2``, 287 RW_TAC std_ss [prob_space_def, prob_preserving_def, prob_def, events_def, p_space_def] 288 >> PROVE_TAC [MEASURE_PRESERVING_LIFT]); 289 290val PROB_PRESERVING_UP_LIFT = store_thm 291 ("PROB_PRESERVING_UP_LIFT", 292 ``!p1 p2 f. 293 prob_space p1 /\ 294 f IN prob_preserving (p_space p1, a, prob p1) p2 /\ 295 sigma_algebra (p_space p1, events p1) /\ 296 a SUBSET events p1 ==> 297 f IN prob_preserving p1 p2``, 298 RW_TAC std_ss [prob_preserving_def, prob_def, events_def, p_space_def, prob_space_def] 299 >> PROVE_TAC [MEASURE_PRESERVING_UP_LIFT]); 300 301val PROB_PRESERVING_UP_SUBSET = store_thm 302 ("PROB_PRESERVING_UP_SUBSET", 303 ``!p1 p2. 304 prob_space p1 /\ 305 a SUBSET events p1 /\ 306 sigma_algebra (p_space p1, events p1) ==> 307 prob_preserving (p_space p1, a, prob p1) p2 SUBSET prob_preserving p1 p2``, 308 RW_TAC std_ss [prob_preserving_def, prob_def, events_def, p_space_def, prob_space_def] 309 >> PROVE_TAC [MEASURE_PRESERVING_UP_SUBSET]); 310 311val PROB_PRESERVING_UP_SIGMA = store_thm 312 ("PROB_PRESERVING_UP_SIGMA", 313 ``!p1 p2 a. 314 prob_space p1 /\ 315 (events p1 = subsets (sigma (p_space p1) a)) ==> 316 prob_preserving (p_space p1, a, prob p1) p2 SUBSET prob_preserving p1 p2``, 317 RW_TAC std_ss [prob_preserving_def, prob_def, events_def, p_space_def, prob_space_def] 318 >> PROVE_TAC [MEASURE_PRESERVING_UP_SIGMA]); 319 320val PSPACE = store_thm 321 ("PSPACE", 322 ``!a b c. p_space (a, b, c) = a``, 323 RW_TAC std_ss [p_space_def, m_space_def]); 324 325val EVENTS = store_thm 326 ("EVENTS", 327 ``!a b c. events (a, b, c) = b``, 328 RW_TAC std_ss [events_def, measurable_sets_def]); 329 330val PROB = store_thm 331 ("PROB", 332 ``!a b c. prob (a, b, c) = c``, 333 RW_TAC std_ss [prob_def, measure_def]); 334 335val EVENTS_INTER = store_thm 336 ("EVENTS_INTER", 337 ``!p s t. 338 prob_space p /\ s IN events p /\ t IN events p ==> 339 s INTER t IN events p``, 340 RW_TAC std_ss [] 341 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 342 Q.SPEC `(p_space p, events p)`) ALGEBRA_INTER 343 >> PROVE_TAC [PROB_SPACE, SIGMA_ALGEBRA_ALGEBRA]); 344 345val EVENTS_EMPTY = store_thm 346 ("EVENTS_EMPTY", 347 ``!p. prob_space p ==> {} IN events p``, 348 RW_TAC std_ss [] 349 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 350 Q.SPEC `(p_space p, events p)`) ALGEBRA_EMPTY 351 >> PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA, PROB_SPACE]); 352 353val EVENTS_SPACE = store_thm 354 ("EVENTS_SPACE", 355 ``!p. prob_space p ==> (p_space p) IN events p``, 356 RW_TAC std_ss [] 357 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 358 Q.SPEC `(p_space p, events p)`) ALGEBRA_SPACE 359 >> PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA, PROB_SPACE]); 360 361val EVENTS_UNION = store_thm 362 ("EVENTS_UNION", 363 ``!p s t. 364 prob_space p /\ s IN events p /\ t IN events p ==> 365 s UNION t IN events p``, 366 RW_TAC std_ss [] 367 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 368 Q.SPEC `(p_space p, events p)`) ALGEBRA_UNION 369 >> PROVE_TAC [PROB_SPACE, SIGMA_ALGEBRA_ALGEBRA]); 370 371val INDEP_EMPTY = store_thm 372 ("INDEP_EMPTY", 373 ``!p s. prob_space p /\ s IN events p ==> indep p {} s``, 374 RW_TAC std_ss [indep_def, EVENTS_EMPTY, PROB_EMPTY, INTER_EMPTY] 375 >> RW_TAC real_ss []); 376 377val INTER_PSPACE = store_thm 378 ("INTER_PSPACE", 379 ``!p s. prob_space p /\ s IN events p ==> 380 (p_space p INTER s = s)``, 381 RW_TAC std_ss [PROB_SPACE, SIGMA_ALGEBRA, space_def, subsets_def, subset_class_def, SUBSET_DEF] 382 >> RW_TAC std_ss [Once EXTENSION, IN_INTER] 383 >> PROVE_TAC []); 384 385val INDEP_SPACE = store_thm 386 ("INDEP_SPACE", 387 ``!p s. prob_space p /\ s IN events p ==> indep p (p_space p) s``, 388 RW_TAC std_ss [indep_def, EVENTS_SPACE, PROB_UNIV, INTER_PSPACE] 389 >> RW_TAC real_ss []); 390 391val EVENTS_DIFF = store_thm 392 ("EVENTS_DIFF", 393 ``!p s t. 394 prob_space p /\ s IN events p /\ t IN events p ==> 395 s DIFF t IN events p``, 396 RW_TAC std_ss [] 397 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 398 Q.SPEC `(p_space p, events p)`) ALGEBRA_DIFF 399 >> PROVE_TAC [PROB_SPACE, SIGMA_ALGEBRA_ALGEBRA]); 400 401val EVENTS_COMPL = store_thm 402 ("EVENTS_COMPL", 403 ``!p s. prob_space p /\ s IN events p ==> (p_space p) DIFF s IN events p``, 404 RW_TAC std_ss [] 405 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 406 Q.SPEC `(p_space p, events p)`) ALGEBRA_COMPL 407 >> PROVE_TAC [PROB_SPACE, SIGMA_ALGEBRA_ALGEBRA]); 408 409val EVENTS_COUNTABLE_UNION = store_thm 410 ("EVENTS_COUNTABLE_UNION", 411 ``!p c. 412 prob_space p /\ c SUBSET events p /\ countable c ==> 413 BIGUNION c IN events p``, 414 RW_TAC std_ss [] 415 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 416 Q.SPEC `(p_space p, events p)`) SIGMA_ALGEBRA_COUNTABLE_UNION 417 >> RW_TAC std_ss [EVENTS_SIGMA_ALGEBRA]); 418 419val PROB_ZERO_UNION = store_thm 420 ("PROB_ZERO_UNION", 421 ``!p s t. 422 prob_space p /\ s IN events p /\ t IN events p /\ (prob p t = 0) ==> 423 (prob p (s UNION t) = prob p s)``, 424 RW_TAC std_ss [] 425 >> Know `t DIFF s IN events p` 426 >- (MATCH_MP_TAC EVENTS_DIFF 427 >> RW_TAC std_ss []) 428 >> STRIP_TAC 429 >> Know `prob p (t DIFF s) = 0` 430 >- (ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 431 >> REVERSE CONJ_TAC >- PROVE_TAC [PROB_POSITIVE] 432 >> Q.PAT_ASSUM `prob p t = 0` (ONCE_REWRITE_TAC o wrap o SYM) 433 >> MATCH_MP_TAC PROB_INCREASING 434 >> RW_TAC std_ss [DIFF_SUBSET]) 435 >> STRIP_TAC 436 >> Suff `prob p (s UNION t) = prob p s + prob p (t DIFF s)` 437 >- RW_TAC real_ss [] 438 >> MATCH_MP_TAC PROB_ADDITIVE 439 >> RW_TAC std_ss [DISJOINT_DEF, DIFF_DEF, EXTENSION, IN_UNION, IN_DIFF, NOT_IN_EMPTY, IN_INTER] 440 >> PROVE_TAC []); 441 442val PROB_EQ_COMPL = store_thm 443 ("PROB_EQ_COMPL", 444 ``!p s t. 445 prob_space p /\ s IN events p /\ t IN events p /\ 446 (prob p (p_space p DIFF s) = prob p (p_space p DIFF t)) ==> 447 (prob p s = prob p t)``, 448 RW_TAC std_ss [] 449 >> Suff `1 - prob p s = 1 - prob p t` >- REAL_ARITH_TAC 450 >> POP_ASSUM MP_TAC 451 >> RW_TAC std_ss [PROB_COMPL]); 452 453val PROB_ONE_INTER = store_thm 454 ("PROB_ONE_INTER", 455 ``!p s t. 456 prob_space p /\ s IN events p /\ t IN events p /\ (prob p t = 1) ==> 457 (prob p (s INTER t) = prob p s)``, 458 RW_TAC std_ss [] 459 >> MATCH_MP_TAC PROB_EQ_COMPL 460 >> RW_TAC std_ss [EVENTS_INTER] 461 >> Know `p_space p DIFF s INTER t = (p_space p DIFF s) UNION (p_space p DIFF t)` 462 >- (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_UNION, IN_DIFF] 463 >> DECIDE_TAC) 464 >> RW_TAC std_ss [] >> POP_ASSUM (K ALL_TAC) 465 >> MATCH_MP_TAC PROB_ZERO_UNION 466 >> RW_TAC std_ss [PROB_COMPL, EVENTS_COMPL] 467 >> REAL_ARITH_TAC); 468 469val EVENTS_COUNTABLE_INTER = store_thm 470 ("EVENTS_COUNTABLE_INTER", 471 ``!p c. 472 prob_space p /\ c SUBSET events p /\ countable c /\ (~(c={})) ==> 473 BIGINTER c IN events p``, 474 RW_TAC std_ss [] 475 >> Know `BIGINTER c = p_space p DIFF (p_space p DIFF (BIGINTER c))` 476 >- (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_DIFF, LEFT_AND_OVER_OR, IN_BIGINTER] 477 >> FULL_SIMP_TAC std_ss [PROB_SPACE, SIGMA_ALGEBRA, subset_class_def, 478 subsets_def, space_def, SUBSET_DEF] 479 >> EQ_TAC 480 >- (Know `(c = {}) \/ ?x t. (c = x INSERT t) /\ ~(x IN t)` >- PROVE_TAC [SET_CASES] 481 >> RW_TAC std_ss [] 482 >> PROVE_TAC [IN_INSERT]) 483 >> PROVE_TAC []) 484 >> Rewr' 485 >> MATCH_MP_TAC EVENTS_COMPL 486 >> Know `p_space p DIFF BIGINTER c = BIGUNION (IMAGE (\s. p_space p DIFF s) c)` 487 >- (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_DIFF, IN_BIGUNION, IN_IMAGE, IN_BIGINTER] 488 >> EQ_TAC 489 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `p_space p DIFF P` 490 >> RW_TAC std_ss [IN_DIFF] >> Q.EXISTS_TAC `P` 491 >> RW_TAC std_ss []) 492 >> RW_TAC std_ss [] 493 >- FULL_SIMP_TAC std_ss [IN_DIFF] 494 >> Q.EXISTS_TAC `s'` 495 >> FULL_SIMP_TAC std_ss [IN_DIFF]) 496 >> RW_TAC std_ss [] >> POP_ASSUM (K ALL_TAC) 497 498 >> MATCH_MP_TAC EVENTS_COUNTABLE_UNION 499 >> Q.PAT_X_ASSUM `c SUBSET events p` MP_TAC 500 >> RW_TAC std_ss [image_countable, SUBSET_DEF, IN_IMAGE] 501 >> PROVE_TAC [EVENTS_COMPL]); 502 503val ABS_PROB = store_thm 504 ("ABS_PROB", 505 ``!p s. prob_space p /\ s IN events p ==> (abs (prob p s) = prob p s)``, 506 RW_TAC std_ss [abs] 507 >> PROVE_TAC [PROB_POSITIVE]); 508 509val PROB_COMPL_LE1 = store_thm 510 ("PROB_COMPL_LE1", 511 ``!p s r. 512 prob_space p /\ s IN events p ==> 513 (prob p (p_space p DIFF s) <= r = 1 - r <= prob p s)``, 514 RW_TAC std_ss [PROB_COMPL] 515 >> REAL_ARITH_TAC); 516 517val PROB_LE_1 = store_thm 518 ("PROB_LE_1", 519 ``!p s. prob_space p /\ s IN events p ==> prob p s <= 1``, 520 RW_TAC std_ss [] 521 >> Suff `0 <= 1 - prob p s` >- REAL_ARITH_TAC 522 >> RW_TAC std_ss [GSYM PROB_COMPL] 523 >> RW_TAC std_ss [EVENTS_COMPL, PROB_POSITIVE]); 524 525val PROB_EQ_BIGUNION_IMAGE = store_thm 526 ("PROB_EQ_BIGUNION_IMAGE", 527 ``!p. 528 prob_space p /\ f IN (UNIV -> events p) /\ g IN (UNIV -> events p) /\ 529 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 530 (!m n. ~(m = n) ==> DISJOINT (g m) (g n)) /\ 531 (!n : num. prob p (f n) = prob p (g n)) ==> 532 (prob p (BIGUNION (IMAGE f UNIV)) = prob p (BIGUNION (IMAGE g UNIV)))``, 533 RW_TAC std_ss [] 534 >> Know `prob p o f sums prob p (BIGUNION (IMAGE f UNIV))` 535 >- PROVE_TAC [PROB_COUNTABLY_ADDITIVE] 536 >> Know `prob p o g sums prob p (BIGUNION (IMAGE g UNIV))` 537 >- PROVE_TAC [PROB_COUNTABLY_ADDITIVE] 538 >> Suff `prob p o f = prob p o g` 539 >- (RW_TAC std_ss [] 540 >> PROVE_TAC [SUM_UNIQ]) 541 >> FUN_EQ_TAC 542 >> RW_TAC std_ss [o_THM]); 543 544val PROB_FINITELY_ADDITIVE = store_thm 545 ("PROB_FINITELY_ADDITIVE", 546 ``!p s f n. 547 prob_space p /\ f IN ((count n) -> events p) /\ 548 (!a b. a < n /\ b < n /\ ~(a = b) ==> DISJOINT (f a) (f b)) /\ 549 (s = BIGUNION (IMAGE f (count n))) ==> 550 (sum (0, n) (prob p o f) = prob p s)``, 551 RW_TAC std_ss [IN_FUNSET, IN_COUNT] 552 >> Suff 553 `(prob p o (\m. if m < n then f m else {})) sums 554 prob p (BIGUNION (IMAGE f (count n))) /\ 555 (prob p o (\m. if m < n then f m else {})) sums 556 sum (0, n) (prob p o f)` 557 >- PROVE_TAC [SUM_UNIQ] 558 >> REVERSE CONJ_TAC 559 >- (Know 560 `sum (0,n) (prob p o f) = 561 sum (0,n) (prob p o (\m. (if m < n then f m else {})))` 562 >- (MATCH_MP_TAC SUM_EQ 563 >> RW_TAC arith_ss [o_THM]) 564 >> Rewr 565 >> MATCH_MP_TAC SER_0 566 >> RW_TAC arith_ss [o_THM, PROB_EMPTY]) 567 >> Know 568 `BIGUNION (IMAGE f (count n)) = 569 BIGUNION (IMAGE (\m. (if m < n then f m else {})) UNIV)` 570 >- (SET_EQ_TAC 571 >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_COUNT, IN_UNIV] 572 >> PROVE_TAC [NOT_IN_EMPTY]) 573 >> Rewr 574 >> MATCH_MP_TAC PROB_COUNTABLY_ADDITIVE 575 >> BasicProvers.NORM_TAC std_ss 576 [IN_FUNSET, IN_UNIV, DISJOINT_EMPTY, EVENTS_EMPTY]); 577 578val ABS_1_MINUS_PROB = store_thm 579 ("ABS_1_MINUS_PROB", 580 ``!p s. 581 prob_space p /\ s IN events p /\ ~(prob p s = 0) ==> 582 abs (1 - prob p s) < 1``, 583 RW_TAC std_ss [] 584 >> Know `0 <= prob p s` >- PROVE_TAC [PROB_POSITIVE] 585 >> Know `prob p s <= 1` >- PROVE_TAC [PROB_LE_1] 586 >> RW_TAC std_ss [abs] 587 >> REPEAT (POP_ASSUM MP_TAC) 588 >> REAL_ARITH_TAC); 589 590val PROB_INCREASING_UNION = store_thm 591 ("PROB_INCREASING_UNION", 592 ``!p s f. 593 prob_space p /\ f IN (UNIV -> events p) /\ 594 (!n. f n SUBSET f (SUC n)) /\ (s = BIGUNION (IMAGE f UNIV)) ==> 595 prob p o f --> prob p s``, 596 RW_TAC std_ss [prob_space_def, events_def, prob_def, MONOTONE_CONVERGENCE]); 597 598val PROB_SUBADDITIVE = store_thm 599 ("PROB_SUBADDITIVE", 600 ``!p s t u. 601 prob_space p /\ t IN events p /\ u IN events p /\ (s = t UNION u) ==> 602 prob p s <= prob p t + prob p u``, 603 RW_TAC std_ss [] 604 >> Know `t UNION u = t UNION (u DIFF t)` 605 >- (SET_EQ_TAC 606 >> RW_TAC std_ss [IN_UNION, IN_DIFF] 607 >> PROVE_TAC []) 608 >> Rewr 609 >> Know `u DIFF t IN events p` 610 >- PROVE_TAC [EVENTS_DIFF] 611 >> STRIP_TAC 612 >> Know `prob p (t UNION (u DIFF t)) = prob p t + prob p (u DIFF t)` 613 >- (MATCH_MP_TAC PROB_ADDITIVE 614 >> RW_TAC std_ss [DISJOINT_ALT, IN_DIFF]) 615 >> Rewr 616 >> MATCH_MP_TAC REAL_LE_LADD_IMP 617 >> MATCH_MP_TAC PROB_INCREASING 618 >> RW_TAC std_ss [DIFF_DEF, SUBSET_DEF, GSPECIFICATION]); 619 620val PROB_COUNTABLY_SUBADDITIVE = store_thm 621 ("PROB_COUNTABLY_SUBADDITIVE", 622 ``!p f. 623 prob_space p /\ (IMAGE f UNIV) SUBSET events p /\ 624 summable (prob p o f) ==> 625 prob p (BIGUNION (IMAGE f UNIV)) <= suminf (prob p o f)``, 626 RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV] 627 >> Know `(prob p o f) sums suminf (prob p o f)` 628 >- PROVE_TAC [SUMMABLE_SUM] 629 >> RW_TAC std_ss [sums] 630 >> Know 631 `prob p o (\n. BIGUNION (IMAGE f (count n))) --> 632 prob p (BIGUNION (IMAGE f UNIV))` 633 >- (MATCH_MP_TAC PROB_INCREASING_UNION 634 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV] >| 635 [MATCH_MP_TAC EVENTS_COUNTABLE_UNION 636 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, image_countable, 637 COUNTABLE_COUNT] 638 >> PROVE_TAC [], 639 RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, IN_COUNT] 640 >> PROVE_TAC [LT_SUC], 641 SET_EQ_TAC 642 >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV, IN_COUNT] 643 >> REVERSE EQ_TAC >- PROVE_TAC [] 644 >> RW_TAC std_ss [] 645 >> Q.EXISTS_TAC `SUC x'` 646 >> Q.EXISTS_TAC `x'` 647 >> RW_TAC arith_ss []]) 648 >> STRIP_TAC 649 >> MATCH_MP_TAC SEQ_LE 650 >> Q.EXISTS_TAC `prob p o (\n. BIGUNION (IMAGE f (count n)))` 651 >> Q.EXISTS_TAC `(\n. sum (0,n) (prob p o f))` 652 >> RW_TAC std_ss [] 653 >> Q.EXISTS_TAC `0` 654 >> RW_TAC arith_ss [o_THM] 655 >> Induct_on `n` 656 >- RW_TAC std_ss [o_THM, COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, PROB_EMPTY, 657 sum, REAL_LE_REFL] 658 >> RW_TAC std_ss [o_THM, COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT, sum] 659 >> ONCE_REWRITE_TAC [REAL_ADD_SYM] 660 >> RW_TAC arith_ss [] 661 >> Suff 662 `prob p (f n UNION BIGUNION (IMAGE f (count n))) <= 663 prob p (f n) + prob p (BIGUNION (IMAGE f (count n)))` 664 >- (POP_ASSUM MP_TAC 665 >> REAL_ARITH_TAC) 666 >> MATCH_MP_TAC PROB_SUBADDITIVE 667 >> RW_TAC std_ss [] >- PROVE_TAC [] 668 >> MATCH_MP_TAC EVENTS_COUNTABLE_UNION 669 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT, image_countable, 670 COUNTABLE_COUNT] 671 >> PROVE_TAC []); 672 673val PROB_COUNTABLY_ZERO = store_thm 674 ("PROB_COUNTABLY_ZERO", 675 ``!p c. 676 prob_space p /\ countable c /\ c SUBSET events p /\ 677 (!x. x IN c ==> (prob p x = 0)) ==> 678 (prob p (BIGUNION c) = 0)``, 679 RW_TAC std_ss [COUNTABLE_ENUM] 680 >- RW_TAC std_ss [BIGUNION_EMPTY, PROB_EMPTY] 681 >> Know `(!n. prob p (f n) = 0) /\ (!n. f n IN events p)` 682 >- (FULL_SIMP_TAC std_ss [IN_IMAGE, IN_UNIV, SUBSET_DEF] 683 >> PROVE_TAC []) 684 >> NTAC 2 (POP_ASSUM K_TAC) 685 >> STRIP_TAC 686 >> ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 687 >> REVERSE CONJ_TAC 688 >- (MATCH_MP_TAC PROB_POSITIVE 689 >> RW_TAC std_ss [] 690 >> MATCH_MP_TAC EVENTS_COUNTABLE_UNION 691 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM, SUBSET_DEF, IN_IMAGE, IN_UNIV] 692 >> RW_TAC std_ss []) 693 >> Know `(prob p o f) sums 0` 694 >- (Know `0 = sum (0, 0) (prob p o f)` >- RW_TAC std_ss [sum] 695 >> Rewr' 696 >> MATCH_MP_TAC SER_0 697 >> RW_TAC std_ss [o_THM]) 698 >> RW_TAC std_ss [SUMS_EQ] 699 >> POP_ASSUM (REWRITE_TAC o wrap o SYM) 700 >> MATCH_MP_TAC PROB_COUNTABLY_SUBADDITIVE 701 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV] 702 >> RW_TAC std_ss []); 703 704val INDEP_SYM = store_thm 705 ("INDEP_SYM", 706 ``!p a b. prob_space p /\ indep p a b ==> indep p b a``, 707 RW_TAC std_ss [indep_def] 708 >> PROVE_TAC [REAL_MUL_SYM, INTER_COMM]); 709 710val INDEP_REFL = store_thm 711 ("INDEP_REFL", 712 ``!p a. 713 prob_space p /\ a IN events p ==> 714 (indep p a a = (prob p a = 0) \/ (prob p a = 1))``, 715 RW_TAC std_ss [indep_def, INTER_IDEMPOT] 716 >> PROVE_TAC [REAL_MUL_IDEMPOT]); 717 718 719val PROB_REAL_SUM_IMAGE = store_thm 720 ("PROB_REAL_SUM_IMAGE", 721 ``!p s. prob_space p /\ s IN events p /\ (!x. x IN s ==> {x} IN events p) /\ FINITE s ==> 722 (prob p s = SIGMA (\x. prob p {x}) s)``, 723 Suff `!s. FINITE s ==> 724 (\s. !p. prob_space p /\ s IN events p /\ (!x. x IN s ==> {x} IN events p) ==> 725 (prob p s = SIGMA (\x. prob p {x}) s)) s` 726 >- METIS_TAC [] 727 >> MATCH_MP_TAC FINITE_INDUCT 728 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, PROB_EMPTY, DELETE_NON_ELEMENT, IN_INSERT] 729 >> Q.PAT_X_ASSUM `!p. 730 prob_space p /\ s IN events p /\ 731 (!x. x IN s ==> {x} IN events p) ==> 732 (prob p s = SIGMA (\x. prob p {x}) s)` (MP_TAC o GSYM o Q.SPEC `p`) 733 >> RW_TAC std_ss [] 734 >> `s IN events p` 735 by (`s = (e INSERT s) DIFF {e}` 736 by (RW_TAC std_ss [EXTENSION, IN_INSERT, IN_DIFF, IN_SING] >> METIS_TAC [GSYM DELETE_NON_ELEMENT]) 737 >> POP_ORW 738 >> FULL_SIMP_TAC std_ss [prob_space_def, measure_space_def, sigma_algebra_def, events_def] 739 >> METIS_TAC [space_def, subsets_def, ALGEBRA_DIFF]) 740 >> ASM_SIMP_TAC std_ss [] 741 >> MATCH_MP_TAC PROB_ADDITIVE 742 >> RW_TAC std_ss [IN_DISJOINT, IN_SING, Once INSERT_SING_UNION] 743 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]); 744 745val PROB_EQUIPROBABLE_FINITE_UNIONS = store_thm 746 ("PROB_EQUIPROBABLE_FINITE_UNIONS", 747 ``!p s. prob_space p /\ s IN events p /\ (!x. x IN s ==> {x} IN events p) /\ FINITE s /\ 748 (!x y. x IN s /\ y IN s ==> (prob p {x} = prob p {y})) ==> 749 (prob p s = & (CARD s) * prob p {CHOICE s})``, 750 RW_TAC std_ss [] 751 >> Cases_on `s = {}` 752 >- RW_TAC real_ss [PROB_EMPTY, CARD_EMPTY] 753 >> `prob p s = SIGMA (\x. prob p {x}) s` 754 by METIS_TAC [PROB_REAL_SUM_IMAGE] 755 >> POP_ORW 756 >> `prob p {CHOICE s} = (\x. prob p {x}) (CHOICE s)` by RW_TAC std_ss [] 757 >> POP_ORW 758 >> (MATCH_MP_TAC o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_SAME 759 >> RW_TAC std_ss [CHOICE_DEF]); 760 761 762val PROB_REAL_SUM_IMAGE_FN = store_thm 763 ("PROB_REAL_SUM_IMAGE_FN", 764 ``!p f e s. prob_space p /\ e IN events p /\ (!x. x IN s ==> e INTER f x IN events p) /\ FINITE s /\ 765 (!x y. x IN s /\ y IN s /\ (~(x=y)) ==> DISJOINT (f x) (f y)) /\ 766 (BIGUNION (IMAGE f s) INTER p_space p = p_space p) ==> 767 (prob p e = SIGMA (\x. prob p (e INTER f x)) s)``, 768 Suff `!(s :'b -> bool). FINITE s ==> 769 (\s. !(p :('a -> bool) # (('a -> bool) -> bool) # (('a -> bool) -> real)) 770 (f :'b -> 'a -> bool) (e :'a -> bool). prob_space p /\ e IN events p /\ (!x. x IN s ==> e INTER f x IN events p) /\ 771 (!x y. x IN s /\ y IN s /\ (~(x=y)) ==> DISJOINT (f x) (f y)) /\ 772 (BIGUNION (IMAGE f s) INTER p_space p = p_space p) ==> 773 (prob p e = SIGMA (\x. prob p (e INTER f x)) s)) s` 774 >- METIS_TAC [] 775 >> MATCH_MP_TAC FINITE_INDUCT 776 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, PROB_EMPTY, DELETE_NON_ELEMENT, IN_INSERT, IMAGE_EMPTY, BIGUNION_EMPTY, INTER_EMPTY] 777 >- METIS_TAC [PROB_UNIV, PROB_EMPTY, REAL_10] 778 >> `prob p e' = 779 prob p (e' INTER f e) + 780 prob p (e' DIFF f e)` 781 by (MATCH_MP_TAC PROB_ADDITIVE 782 >> RW_TAC std_ss [] 783 >| [`e' DIFF f e = e' DIFF (e' INTER f e)` 784 by (RW_TAC std_ss [EXTENSION, IN_DIFF, IN_INTER] >> DECIDE_TAC) 785 >> POP_ORW 786 >> METIS_TAC [EVENTS_DIFF], 787 FULL_SIMP_TAC std_ss [IN_DISJOINT, IN_INTER, IN_DIFF] >> METIS_TAC [], 788 RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_UNION, IN_DIFF] >> DECIDE_TAC]) 789 >> POP_ORW 790 >> RW_TAC std_ss [REAL_EQ_LADD] 791 >> (MP_TAC o Q.ISPEC `(s :'b -> bool)`) SET_CASES 792 >> RW_TAC std_ss [] 793 >- (RW_TAC std_ss [REAL_SUM_IMAGE_THM] 794 >> `IMAGE f {e} = {f e}` 795 by RW_TAC std_ss [EXTENSION, IN_IMAGE, IN_SING] 796 >> FULL_SIMP_TAC std_ss [BIGUNION_SING, DIFF_UNIV, PROB_EMPTY] 797 >> `e' DIFF f e = {}` 798 by (RW_TAC std_ss [Once EXTENSION, NOT_IN_EMPTY, IN_DIFF] 799 >> METIS_TAC [SUBSET_DEF, MEASURABLE_SETS_SUBSET_SPACE, prob_space_def, 800 events_def, p_space_def, IN_INTER]) 801 >> RW_TAC std_ss [PROB_EMPTY]) 802 >> Q.PAT_X_ASSUM `!p f e. 803 prob_space p /\ e IN events p /\ 804 (!x. x IN s ==> e INTER f x IN events p) /\ 805 (!x y. x IN s /\ y IN s /\ ~(x = y) ==> DISJOINT (f x) (f y)) /\ 806 (BIGUNION (IMAGE f s) INTER p_space p = p_space p) ==> 807 (prob p e = SIGMA (\x. prob p (e INTER f x)) s)` 808 (MP_TAC o Q.SPECL [`p`,`(\y. if y = x then f x UNION f e else f y)`,`e' DIFF f e`]) 809 >> ASM_SIMP_TAC std_ss [] 810 >> `e' DIFF f e IN events p` 811 by (`e' DIFF f e = e' DIFF (e' INTER f e)` 812 by (RW_TAC std_ss [EXTENSION, IN_DIFF, IN_INTER] >> DECIDE_TAC) 813 >> POP_ORW 814 >> METIS_TAC [EVENTS_DIFF]) 815 >> ASM_SIMP_TAC std_ss [] 816 >> `(!x'. 817 x' IN x INSERT t ==> 818 (e' DIFF f e) INTER (if x' = x then f x UNION f e else f x') IN 819 events p)` 820 by (RW_TAC std_ss [] 821 >- (`(e' DIFF f e) INTER (f x UNION f e) = 822 e' INTER f x` 823 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_DIFF, IN_UNION] 824 >> FULL_SIMP_TAC std_ss [IN_DISJOINT, GSYM DELETE_NON_ELEMENT] 825 >> METIS_TAC []) 826 >> RW_TAC std_ss []) 827 >> `(e' DIFF f e) INTER f x' = 828 (e' INTER f x') DIFF (e' INTER f e)` 829 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_DIFF] 830 >> FULL_SIMP_TAC std_ss [IN_DISJOINT, GSYM DELETE_NON_ELEMENT] 831 >> METIS_TAC []) 832 >> METIS_TAC [EVENTS_DIFF]) 833 >> ASM_SIMP_TAC std_ss [] 834 >> `(!x' y. 835 x' IN x INSERT t /\ y IN x INSERT t /\ ~(x' = y) ==> 836 DISJOINT (if x' = x then f x UNION f e else f x') 837 (if y = x then f x UNION f e else f y))` 838 by (RW_TAC std_ss [IN_DISJOINT, IN_UNION] 839 >> FULL_SIMP_TAC std_ss [IN_DISJOINT, GSYM DELETE_NON_ELEMENT] 840 >> METIS_TAC []) 841 >> ASM_SIMP_TAC std_ss [] 842 >> `(BIGUNION 843 (IMAGE (\y. (if y = x then f x UNION f e else f y)) (x INSERT t)) INTER p_space p = p_space p)` 844 by (FULL_SIMP_TAC std_ss [IMAGE_INSERT, BIGUNION_INSERT] 845 >> `IMAGE (\y. (if y = x then f x UNION f e else f y)) t = 846 IMAGE f t` 847 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE] 848 >> EQ_TAC 849 >- (RW_TAC std_ss [] >> METIS_TAC []) 850 >> RW_TAC std_ss [] >> METIS_TAC []) 851 >> POP_ORW 852 >> METIS_TAC [UNION_COMM, UNION_ASSOC]) 853 >> ASM_SIMP_TAC std_ss [] 854 >> STRIP_TAC >> POP_ASSUM (K ALL_TAC) 855 >> FULL_SIMP_TAC std_ss [FINITE_INSERT] 856 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM] 857 >> FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT] 858 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT] 859 >> `(e' DIFF f e) INTER (f x UNION f e) = 860 e' INTER f x` 861 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_DIFF, IN_UNION] 862 >> FULL_SIMP_TAC std_ss [IN_DISJOINT, GSYM DELETE_NON_ELEMENT, IN_INSERT] 863 >> METIS_TAC []) 864 >> RW_TAC std_ss [REAL_EQ_LADD] 865 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(t :'b -> bool)`) REAL_SUM_IMAGE_IN_IF] 866 >> Suff `(\x'. 867 (if x' IN t then 868 (\x'. 869 prob p 870 ((e' DIFF f e) INTER 871 (if x' = x then f x UNION f e else f x'))) x' 872 else 873 0)) = 874 (\x. (if x IN t then (\x. prob p (e' INTER f x)) x else 0))` 875 >- RW_TAC std_ss [] 876 >> RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC std_ss [] 877 >> Suff `(e' DIFF f e) INTER f x' = e' INTER f x'` 878 >- RW_TAC std_ss [] 879 >> RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_DIFF] 880 >> FULL_SIMP_TAC std_ss [IN_DISJOINT, IN_INSERT] 881 >> METIS_TAC []); 882 883(* ************************************************************************* *) 884 885val distribution_prob_space = store_thm 886 ("distribution_prob_space", 887 ``!p X s. random_variable X p s ==> 888 prob_space (space s, subsets s, distribution p X)``, 889 RW_TAC std_ss [random_variable_def, distribution_def, prob_space_def, measure_def, PSPACE, 890 measure_space_def, m_space_def, measurable_sets_def, IN_MEASURABLE, 891 SPACE, positive_def, PREIMAGE_EMPTY, INTER_EMPTY, PROB_EMPTY, 892 PROB_POSITIVE, space_def, subsets_def, countably_additive_def] 893 >- (Q.PAT_X_ASSUM `!f. 894 f IN (UNIV -> measurable_sets p) /\ 895 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 896 BIGUNION (IMAGE f UNIV) IN measurable_sets p ==> 897 measure p o f sums measure p (BIGUNION (IMAGE f UNIV))` 898 (MP_TAC o Q.SPEC `(\x. PREIMAGE X x INTER p_space p) o f`) 899 >> RW_TAC std_ss [prob_def, o_DEF, PREIMAGE_BIGUNION, IMAGE_IMAGE] 900 >> `(BIGUNION (IMAGE (\x. PREIMAGE X (f x)) UNIV) INTER p_space p) = 901 (BIGUNION (IMAGE (\x. PREIMAGE X (f x) INTER p_space p) UNIV))` 902 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] 903 >> METIS_TAC [IN_INTER]) 904 >> POP_ORW 905 >> POP_ASSUM MATCH_MP_TAC 906 >> FULL_SIMP_TAC std_ss [o_DEF, IN_FUNSET, IN_UNIV, events_def] 907 >> CONJ_TAC 908 >- (REPEAT STRIP_TAC 909 >> Suff `DISJOINT (PREIMAGE X (f m)) (PREIMAGE X (f n))` 910 >- (RW_TAC std_ss [IN_DISJOINT, IN_INTER] >> METIS_TAC []) 911 >> RW_TAC std_ss [PREIMAGE_DISJOINT]) 912 >> Suff `BIGUNION (IMAGE (\x. PREIMAGE X (f x) INTER p_space p) UNIV) = 913 PREIMAGE X (BIGUNION (IMAGE f UNIV)) INTER p_space p` 914 >- RW_TAC std_ss [] 915 >> RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_BIGUNION, IN_IMAGE, IN_UNIV, 916 IN_PREIMAGE, IN_BIGUNION] 917 >> METIS_TAC [IN_INTER, IN_PREIMAGE]) 918 >> Suff `PREIMAGE X (space s) INTER p_space p = p_space p` 919 >- RW_TAC std_ss [prob_def] 920 >> FULL_SIMP_TAC std_ss [IN_FUNSET, EXTENSION, IN_PREIMAGE, IN_INTER] 921 >> METIS_TAC []); 922 923val distribution_lebesgue_thm1 = store_thm 924 ("distribution_lebesgue_thm1", 925 ``!X p s A. random_variable X p s /\ A IN subsets s ==> 926 (distribution p X A = integral p (indicator_fn (PREIMAGE X A INTER p_space p)))``, 927 RW_TAC std_ss [random_variable_def, prob_space_def, distribution_def, events_def, IN_MEASURABLE, p_space_def, prob_def, 928 subsets_def, space_def, GSYM integral_indicator_fn]); 929 930val distribution_lebesgue_thm2 = store_thm 931 ("distribution_lebesgue_thm2", 932 ``!X p s A. random_variable X p s /\ A IN subsets s ==> 933 (distribution p X A = integral (space s, subsets s, distribution p X) (indicator_fn A))``, 934 REPEAT STRIP_TAC 935 >> `prob_space (space s,subsets s,distribution p X)` 936 by RW_TAC std_ss [distribution_prob_space] 937 >> Q.PAT_X_ASSUM `random_variable X p s` MP_TAC 938 >> RW_TAC std_ss [random_variable_def, prob_space_def, distribution_def, events_def, IN_MEASURABLE, p_space_def, prob_def, 939 subsets_def, space_def] 940 >> `measure p (PREIMAGE X A INTER m_space p) = 941 measure (space s,subsets s,(\A. measure p (PREIMAGE X A INTER m_space p))) A` 942 by RW_TAC std_ss [measure_def] 943 >> POP_ORW 944 >> (MP_TAC o Q.SPECL [`(space s,subsets s,(\A. measure p (PREIMAGE X A INTER m_space p)))`,`A`] o INST_TYPE [``:'a``|->``:'b``]) 945 integral_indicator_fn 946 >> FULL_SIMP_TAC std_ss [measurable_sets_def, prob_space_def, distribution_def, prob_def, p_space_def]); 947 948(* ************************************************************************* *) 949 950val finite_expectation1 = store_thm 951 ("finite_expectation1", 952 ``!p X. FINITE (p_space p) /\ real_random_variable X p ==> 953 (expectation p X = 954 SIGMA (\r. r * prob p (PREIMAGE X {r} INTER p_space p)) 955 (IMAGE X (p_space p)))``, 956 RW_TAC std_ss [expectation_def, p_space_def, prob_def, prob_space_def, real_random_variable_def, events_def] 957 >> (MATCH_MP_TAC o REWRITE_RULE [finite_space_integral_def]) finite_space_integral_reduce 958 >> RW_TAC std_ss []); 959 960val finite_expectation = store_thm 961 ("finite_expectation", 962 ``!p X. FINITE (p_space p) /\ real_random_variable X p ==> 963 (expectation p X = 964 SIGMA (\r. r * distribution p X {r}) 965 (IMAGE X (p_space p)))``, 966 RW_TAC std_ss [distribution_def] 967 >> METIS_TAC [finite_expectation1]); 968 969(* ************************************************************************* *) 970 971val finite_marginal_product_space_POW = store_thm 972 ("finite_marginal_product_space_POW", 973 ``!p X Y. (POW (p_space p) = events p) /\ 974 random_variable X p (IMAGE X (p_space p), POW (IMAGE X (p_space p))) /\ 975 random_variable Y p (IMAGE Y (p_space p), POW (IMAGE Y (p_space p))) /\ 976 FINITE (p_space p) ==> 977 measure_space (((IMAGE X (p_space p)) CROSS (IMAGE Y (p_space p))), 978 POW ((IMAGE X (p_space p)) CROSS (IMAGE Y (p_space p))), 979 (\a. prob p (PREIMAGE (\x. (X x,Y x)) a INTER p_space p)))``, 980 REPEAT STRIP_TAC 981 >> `(IMAGE X (p_space p) CROSS IMAGE Y (p_space p), 982 POW (IMAGE X (p_space p) CROSS IMAGE Y (p_space p)), 983 (\a. prob p (PREIMAGE (\x. (X x,Y x)) a INTER p_space p))) = 984 (space (IMAGE X (p_space p) CROSS IMAGE Y (p_space p), 985 POW (IMAGE X (p_space p) CROSS IMAGE Y (p_space p))), 986 subsets 987 (IMAGE X (p_space p) CROSS IMAGE Y (p_space p), 988 POW (IMAGE X (p_space p) CROSS IMAGE Y (p_space p))), 989 (\a. prob p (PREIMAGE (\x. (X x,Y x)) a INTER p_space p)))` 990 by RW_TAC std_ss [space_def, subsets_def] 991 >> POP_ORW 992 >> MATCH_MP_TAC finite_additivity_sufficient_for_finite_spaces 993 >> RW_TAC std_ss [POW_SIGMA_ALGEBRA, space_def, FINITE_CROSS, subsets_def, IMAGE_FINITE] 994 >- (RW_TAC std_ss [positive_def, measure_def, measurable_sets_def, PREIMAGE_EMPTY, INTER_EMPTY] 995 >- FULL_SIMP_TAC std_ss [random_variable_def, PROB_EMPTY] 996 >> METIS_TAC [PROB_POSITIVE, SUBSET_DEF, IN_POW, IN_INTER, random_variable_def]) 997 >> RW_TAC std_ss [additive_def, measure_def, measurable_sets_def] 998 >> MATCH_MP_TAC PROB_ADDITIVE 999 >> Q.PAT_X_ASSUM `POW (p_space p) = events p` (MP_TAC o GSYM) 1000 >> FULL_SIMP_TAC std_ss [IN_POW, SUBSET_DEF, IN_PREIMAGE, IN_CROSS, IN_DISJOINT, random_variable_def, IN_INTER] 1001 >> RW_TAC std_ss [] >- METIS_TAC [SND] 1002 >> RW_TAC std_ss [Once EXTENSION, IN_UNION, IN_PREIMAGE, IN_INTER] 1003 >> METIS_TAC []); 1004 1005val finite_marginal_product_space_POW2 = store_thm 1006 ("finite_marginal_product_space_POW2", 1007 ``!p s1 s2 X Y. (POW (p_space p) = events p) /\ 1008 random_variable X p (s1, POW s1) /\ 1009 random_variable Y p (s2, POW s2) /\ 1010 FINITE (p_space p) /\ 1011 FINITE s1 /\ FINITE s2 ==> 1012 measure_space (s1 CROSS s2, POW (s1 CROSS s2), joint_distribution p X Y)``, 1013 REPEAT STRIP_TAC 1014 >> `(s1 CROSS s2, POW (s1 CROSS s2), joint_distribution p X Y) = 1015 (space (s1 CROSS s2, POW (s1 CROSS s2)), 1016 subsets 1017 (s1 CROSS s2, POW (s1 CROSS s2)), 1018 joint_distribution p X Y)` 1019 by RW_TAC std_ss [space_def, subsets_def] 1020 >> POP_ORW 1021 >> MATCH_MP_TAC finite_additivity_sufficient_for_finite_spaces 1022 >> RW_TAC std_ss [POW_SIGMA_ALGEBRA, space_def, FINITE_CROSS, subsets_def] 1023 >- (RW_TAC std_ss [positive_def, measure_def, measurable_sets_def, PREIMAGE_EMPTY, INTER_EMPTY, joint_distribution_def] 1024 >- FULL_SIMP_TAC std_ss [random_variable_def, PROB_EMPTY] 1025 >> METIS_TAC [PROB_POSITIVE, SUBSET_DEF, IN_POW, IN_INTER, random_variable_def]) 1026 >> RW_TAC std_ss [additive_def, measure_def, measurable_sets_def, joint_distribution_def] 1027 >> MATCH_MP_TAC PROB_ADDITIVE 1028 >> Q.PAT_X_ASSUM `POW (p_space p) = events p` (MP_TAC o GSYM) 1029 >> FULL_SIMP_TAC std_ss [IN_POW, SUBSET_DEF, IN_PREIMAGE, IN_CROSS, IN_DISJOINT, random_variable_def, IN_INTER] 1030 >> RW_TAC std_ss [] >- METIS_TAC [SND] 1031 >> RW_TAC std_ss [Once EXTENSION, IN_UNION, IN_PREIMAGE, IN_INTER] 1032 >> METIS_TAC []); 1033 1034val prob_x_eq_1_imp_prob_y_eq_0 = store_thm 1035 ("prob_x_eq_1_imp_prob_y_eq_0", 1036 ``!p x. prob_space p /\ 1037 {x} IN events p /\ 1038 (prob p {x} = 1) ==> 1039 (!y. {y} IN events p /\ 1040 (~(y = x)) ==> 1041 (prob p {y} = 0))``, 1042 REPEAT STRIP_TAC 1043 >> (MP_TAC o Q.SPECL [`p`, `{y}`, `{x}`]) PROB_ONE_INTER 1044 >> RW_TAC std_ss [] 1045 >> Know `{y}INTER{x} = {}` >- RW_TAC std_ss [Once EXTENSION, NOT_IN_EMPTY, IN_INTER, IN_SING] 1046 >> METIS_TAC [PROB_EMPTY]); 1047 1048val distribution_x_eq_1_imp_distribution_y_eq_0 = store_thm 1049 ("distribution_x_eq_1_imp_distribution_y_eq_0", 1050 ``!X p x. random_variable X p (IMAGE X (p_space p),POW (IMAGE X (p_space p))) /\ 1051 (distribution p X {x} = 1) ==> 1052 (!y. (~(y = x)) ==> 1053 (distribution p X {y} = 0))``, 1054 REPEAT STRIP_TAC 1055 >> (MP_TAC o Q.SPECL [`p`, `X`, `(IMAGE X (p_space p),POW (IMAGE X (p_space p)))`]) distribution_prob_space 1056 >> RW_TAC std_ss [space_def, subsets_def] 1057 >> (MP_TAC o Q.ISPECL [`(IMAGE (X :'a -> 'b) 1058 (p_space 1059 (p : 1060 ('a -> bool) # 1061 (('a -> bool) -> bool) # (('a -> bool) -> real))), 1062 POW (IMAGE X (p_space p)),distribution p X)`, 1063 `x:'b`]) prob_x_eq_1_imp_prob_y_eq_0 1064 >> SIMP_TAC std_ss [EVENTS, IN_POW, SUBSET_DEF, IN_SING, PROB] 1065 >> `x IN IMAGE X (p_space p)` 1066 by (FULL_SIMP_TAC std_ss [distribution_def, IN_IMAGE] 1067 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1068 >> `PREIMAGE X {x} INTER p_space p = {}` 1069 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_SING, IN_PREIMAGE, NOT_IN_EMPTY] 1070 >> METIS_TAC []) 1071 >> METIS_TAC [random_variable_def, PROB_EMPTY, REAL_ARITH ``~((1:real)=0)``]) 1072 >> POP_ORW 1073 >> RW_TAC std_ss [] 1074 >> Cases_on `y IN IMAGE X (p_space p)` >- ASM_SIMP_TAC std_ss [] 1075 >> FULL_SIMP_TAC std_ss [distribution_def, IN_IMAGE] 1076 >> `PREIMAGE X {y} INTER p_space p = {}` 1077 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_SING, IN_PREIMAGE, NOT_IN_EMPTY] 1078 >> METIS_TAC []) 1079 >> POP_ORW >> MATCH_MP_TAC PROB_EMPTY >> FULL_SIMP_TAC std_ss [random_variable_def]); 1080 1081val _ = export_theory (); 1082 1083