1(* interactive mode 2app load ["bossLib","realLib","transcTheory","subtypeTheory", 3 "formalizeUseful","extra_boolTheory", 4 "extra_pred_setTheory","extra_realTheory"]; 5 6 7quietdec := true; 8*) 9 10open HolKernel Parse boolLib bossLib arithmeticTheory realTheory 11 seqTheory pred_setTheory res_quanTheory listTheory 12 rich_listTheory pairTheory combinTheory realLib formalizeUseful 13 subtypeTheory extra_pred_setTheory extra_boolTheory optionTheory 14 extra_realTheory extra_numTheory; 15 16open real_sigmaTheory; 17 18(* interactive mode 19quietdec := false; 20*) 21 22val _ = new_theory "measure"; 23 24val std_ss' = std_ss ++ boolSimps.ETA_ss; 25val INTER_ASSOC = GSYM INTER_ASSOC; 26val UNION_ASSOC = GSYM UNION_ASSOC; 27 28(* ------------------------------------------------------------------------- *) 29(* Tools. *) 30(* ------------------------------------------------------------------------- *) 31 32val REVERSE = Tactical.REVERSE; 33val Strip = rpt (POP_ASSUM MP_TAC) >> rpt STRIP_TAC; 34val Simplify = RW_TAC arith_ss; 35val Suff = PARSE_TAC SUFF_TAC; 36val Know = PARSE_TAC KNOW_TAC; 37val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 38val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 39val STRONG_DISJ_TAC = CONV_TAC (REWR_CONV (GSYM IMP_DISJ_THM)) >> STRIP_TAC; 40val Cond = 41 DISCH_THEN 42 (fn mp_th => 43 let 44 val cond = fst (dest_imp (concl mp_th)) 45 in 46 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 47 end); 48 49val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 50 51(* ------------------------------------------------------------------------- *) 52(* Basic measure theory definitions. *) 53(* *) 54(* Limitations: *) 55(* *) 56(* 2. Measures must be finite, that is, lie in the range [0, +infinity). *) 57(* *) 58(* Limitation 2 is not relevant for probability measures, which must lie in *) 59(* the range [0,1] anyway. *) 60(* ------------------------------------------------------------------------- *) 61 62 63val space_def = Define 64 `space (x:'a->bool,y:('a->bool)->bool) = x`; 65 66 67val subsets_def = Define 68 `subsets (x:'a->bool,y:('a->bool)->bool) = y`; 69 70 71val SPACE = store_thm 72 ("SPACE", 73 ``!a. (space a, subsets a) = a``, 74 STRIP_TAC >> MP_TAC (Q.ISPEC `(a :('a -> bool) # (('a -> bool) -> bool))` pair_CASES) 75 >> RW_TAC std_ss [space_def, subsets_def]); 76 77val subset_class_def = Define 78 `subset_class sp sts = !x. x IN sts ==> x SUBSET sp`; 79 80 81val algebra_def = Define 82 `algebra a = 83 subset_class (space a) (subsets a) /\ 84 {} IN subsets a /\ 85 (!s. s IN subsets a ==> space a DIFF s IN subsets a) /\ 86 (!s t. s IN subsets a /\ t IN subsets a ==> s UNION t IN subsets a)`; 87 88 89val sigma_algebra_def = Define 90 `sigma_algebra a = 91 algebra a /\ 92 !c. countable c /\ c SUBSET (subsets a) ==> BIGUNION c IN (subsets a)`; 93 94 95val sigma_def = Define 96 `sigma sp st = (sp, BIGINTER {s | st SUBSET s /\ sigma_algebra (sp,s)})`; 97 98 99val m_space_def = Define 100 `m_space (sp:'a->bool, sts:('a->bool)->bool, mu:('a->bool)->real) = sp`; 101 102 103val measurable_sets_def = Define 104 `measurable_sets (sp:'a->bool, sts:('a->bool)->bool, mu:('a->bool)->real) = sts`; 105 106 107val measure_def = Define 108 `measure (sp:'a->bool, sts:('a->bool)->bool, mu:('a->bool)->real) = mu`; 109 110 111val positive_def = Define 112 `positive m = 113 (measure m {} = 0) /\ !s. s IN measurable_sets m ==> 0 <= measure m s`; 114 115 116val additive_def = Define 117 `additive m = 118 !s t. s IN measurable_sets m /\ t IN measurable_sets m /\ DISJOINT s t ==> 119 (measure m (s UNION t) = measure m s + measure m t)`; 120 121 122val countably_additive_def = Define 123 `countably_additive m = 124 !f : num -> ('a -> bool). 125 f IN (UNIV -> measurable_sets m) /\ 126 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 127 BIGUNION (IMAGE f UNIV) IN measurable_sets m ==> 128 (measure m o f) sums measure m (BIGUNION (IMAGE f UNIV))`; 129 130 131val subadditive_def = Define 132 `subadditive m = 133 !s t. 134 s IN measurable_sets m /\ t IN measurable_sets m ==> 135 measure m (s UNION t) <= measure m s + measure m t`; 136 137 138val countably_subadditive_def = Define 139 `countably_subadditive m = 140 !f : num -> ('a -> bool). 141 f IN (UNIV -> measurable_sets m) /\ 142 BIGUNION (IMAGE f UNIV) IN measurable_sets m /\ 143 summable (measure m o f) ==> 144 measure m (BIGUNION (IMAGE f UNIV)) <= suminf (measure m o f)`; 145 146 147val increasing_def = Define 148 `increasing m = 149 !s t. 150 s IN measurable_sets m /\ t IN measurable_sets m /\ s SUBSET t ==> 151 measure m s <= measure m t`; 152 153 154val measure_space_def = Define 155 `measure_space m = 156 sigma_algebra (m_space m, measurable_sets m) /\ positive m /\ countably_additive m`; 157 158 159val lambda_system_def = Define 160 `lambda_system gen (lam : ('a -> bool) -> real) = 161 {l | 162 l IN (subsets gen) /\ 163 !s. s IN (subsets gen) ==> (lam (l INTER s) + lam ((space gen DIFF l) INTER s) = lam s)}`; 164 165 166val outer_measure_space_def = Define 167 `outer_measure_space m = 168 positive m /\ increasing m /\ countably_subadditive m`; 169 170 171val inf_measure_def = Define 172 `inf_measure m s = 173 inf 174 {r | 175 ?f. 176 f IN (UNIV -> measurable_sets m) /\ 177 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 178 s SUBSET BIGUNION (IMAGE f UNIV) /\ ((measure m o f) sums r)}`; 179 180 181val closed_cdi_def = Define 182 `closed_cdi p = 183 subset_class (space p) (subsets p) /\ 184 (!s. s IN (subsets p) ==> (space p DIFF s) IN (subsets p)) /\ 185 (!f : num -> 'a -> bool. 186 f IN (UNIV -> (subsets p)) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 187 BIGUNION (IMAGE f UNIV) IN (subsets p)) /\ 188 (!f : num -> 'a -> bool. 189 f IN (UNIV -> (subsets p)) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 190 BIGUNION (IMAGE f UNIV) IN (subsets p))`; 191 192 193val smallest_closed_cdi_def = Define 194 `smallest_closed_cdi a = (space a, BIGINTER {b | (subsets a) SUBSET b /\ closed_cdi (space a, b)})`; 195 196 197val measurable_def = Define 198 `measurable a b = {f | sigma_algebra a /\ sigma_algebra b /\ 199 f IN (space a -> space b) /\ 200 !s. s IN subsets b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a}`; 201 202 203val measure_preserving_def = Define 204 `measure_preserving m1 m2 = 205 {f | 206 f IN measurable (m_space m1, measurable_sets m1) (m_space m2, measurable_sets m2) /\ 207 measure_space m1 /\ measure_space m2 /\ 208 !s. 209 s IN measurable_sets m2 ==> (measure m1 ((PREIMAGE f s)INTER(m_space m1)) = measure m2 s)}`; 210 211 212val indicator_fn_def = Define 213 `indicator_fn s = \x. if x IN s then (1:real) else (0:real)`; 214 215 216(* ------------------------------------------------------------------------- *) 217(* Basic measure theory theorems, leading to: *) 218(* 1. Caratheodory's extension theorem. *) 219(* ------------------------------------------------------------------------- *) 220 221 222val ALGEBRA_ALT_INTER = store_thm 223 ("ALGEBRA_ALT_INTER", 224 ``!a. 225 algebra a = 226 subset_class (space a) (subsets a) /\ 227 {} IN (subsets a) /\ (!s. s IN (subsets a) ==> (space a DIFF s) IN (subsets a)) /\ 228 !s t. s IN (subsets a) /\ t IN (subsets a) ==> s INTER t IN (subsets a)``, 229 RW_TAC std_ss [algebra_def, subset_class_def] 230 >> EQ_TAC >| 231 [RW_TAC std_ss [] 232 >> Know `s INTER t = space a DIFF ((space a DIFF s) UNION (space a DIFF t))` 233 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] 234 >> EQ_TAC 235 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF] >> PROVE_TAC []) 236 >> RW_TAC std_ss [] >> ASM_REWRITE_TAC []) 237 >> RW_TAC std_ss [], 238 RW_TAC std_ss [] 239 >> Know `s UNION t = space a DIFF ((space a DIFF s) INTER (space a DIFF t))` 240 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] 241 >> EQ_TAC 242 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF] >> PROVE_TAC []) 243 >> RW_TAC std_ss [] >> ASM_REWRITE_TAC []) 244 >> RW_TAC std_ss []]); 245 246 247val ALGEBRA_EMPTY = store_thm 248 ("ALGEBRA_EMPTY", 249 ``!a. algebra a ==> {} IN (subsets a)``, 250 RW_TAC std_ss [algebra_def]); 251 252 253val ALGEBRA_SPACE = store_thm 254 ("ALGEBRA_SPACE", 255 ``!a. algebra a ==> (space a) IN (subsets a)``, 256 RW_TAC std_ss [algebra_def] 257 >> PROVE_TAC [DIFF_EMPTY]); 258 259 260val ALGEBRA_COMPL = store_thm 261 ("ALGEBRA_COMPL", 262 ``!a s. algebra a /\ s IN (subsets a) ==> (space a DIFF s) IN (subsets a)``, 263 RW_TAC std_ss [algebra_def]); 264 265 266val ALGEBRA_UNION = store_thm 267 ("ALGEBRA_UNION", 268 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s UNION t IN (subsets a)``, 269 RW_TAC std_ss [algebra_def]); 270 271 272val ALGEBRA_INTER = store_thm 273 ("ALGEBRA_INTER", 274 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s INTER t IN (subsets a)``, 275 RW_TAC std_ss [ALGEBRA_ALT_INTER]); 276 277 278val ALGEBRA_DIFF = store_thm 279 ("ALGEBRA_DIFF", 280 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s DIFF t IN (subsets a)``, 281 REPEAT STRIP_TAC 282 >> Know `s DIFF t = s INTER (space a DIFF t)` 283 >- (RW_TAC std_ss [EXTENSION, IN_DIFF, IN_INTER] 284 >> FULL_SIMP_TAC std_ss [algebra_def, SUBSET_DEF, subset_class_def] 285 >> PROVE_TAC []) 286 >> RW_TAC std_ss [ALGEBRA_INTER, ALGEBRA_COMPL]); 287 288 289val ALGEBRA_FINITE_UNION = store_thm 290 ("ALGEBRA_FINITE_UNION", 291 ``!a c. algebra a /\ FINITE c /\ c SUBSET (subsets a) ==> BIGUNION c IN (subsets a)``, 292 RW_TAC std_ss [algebra_def] 293 >> NTAC 2 (POP_ASSUM MP_TAC) 294 >> Q.SPEC_TAC (`c`, `c`) 295 >> HO_MATCH_MP_TAC FINITE_INDUCT 296 >> RW_TAC std_ss [BIGUNION_EMPTY, BIGUNION_INSERT, INSERT_SUBSET]); 297 298 299val ALGEBRA_INTER_SPACE = store_thm 300 ("ALGEBRA_INTER_SPACE", 301 ``!a s. algebra a /\ s IN subsets a ==> ((space a INTER s = s) /\ (s INTER space a = s))``, 302 RW_TAC std_ss [algebra_def, SUBSET_DEF, IN_INTER, EXTENSION, subset_class_def] 303 >> PROVE_TAC []); 304 305 306val LAMBDA_SYSTEM_EMPTY = store_thm 307 ("LAMBDA_SYSTEM_EMPTY", 308 ``!g0 lam. algebra g0 /\ positive (space g0, subsets g0, lam) ==> {} IN lambda_system g0 lam``, 309 RW_TAC real_ss [lambda_system_def, GSPECIFICATION, positive_def, 310 INTER_EMPTY, DIFF_EMPTY, ALGEBRA_INTER_SPACE, measure_def] 311 >> FULL_SIMP_TAC std_ss [algebra_def]); 312 313 314val LAMBDA_SYSTEM_COMPL = store_thm 315 ("LAMBDA_SYSTEM_COMPL", 316 ``!g0 lam l. 317 algebra g0 /\ positive (space g0, subsets g0, lam) /\ l IN lambda_system g0 lam ==> 318 (space g0) DIFF l IN lambda_system g0 lam``, 319 RW_TAC real_ss [lambda_system_def, GSPECIFICATION, positive_def] 320 >- PROVE_TAC [algebra_def, subset_class_def] 321 >> Know `(space g0 DIFF (space g0 DIFF l)) = l` 322 >- (RW_TAC std_ss [Once EXTENSION, IN_DIFF, LEFT_AND_OVER_OR] >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF]) 323 >> RW_TAC std_ss [] 324 >> PROVE_TAC [REAL_ADD_SYM]); 325 326 327val LAMBDA_SYSTEM_INTER = store_thm 328 ("LAMBDA_SYSTEM_INTER", 329 ``!g0 lam l1 l2. 330 algebra g0 /\ positive (space g0, subsets g0, lam) /\ 331 l1 IN lambda_system g0 lam /\ l2 IN lambda_system g0 lam ==> 332 (l1 INTER l2) IN lambda_system g0 lam``, 333 RW_TAC real_ss [lambda_system_def, GSPECIFICATION, positive_def] 334 >- PROVE_TAC [ALGEBRA_ALT_INTER] 335 >> Know 336 `lam ((space g0 DIFF (l1 INTER l2)) INTER s) = 337 lam (l2 INTER (space g0 DIFF l1) INTER s) + lam ((space g0 DIFF l2) INTER s)` 338 >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] 339 >> Know 340 `l2 INTER (space g0 DIFF l1) INTER s = l2 INTER ((space g0 DIFF (l1 INTER l2)) INTER s)` 341 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF] 342 >> PROVE_TAC []) 343 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 344 >> Know `(space g0 DIFF l2) INTER s = (space g0 DIFF l2) INTER ((space g0 DIFF (l1 INTER l2)) INTER s)` 345 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF] 346 >> PROVE_TAC []) 347 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 348 >> Q.PAT_X_ASSUM `!g. P g` MATCH_MP_TAC 349 >> PROVE_TAC [ALGEBRA_ALT_INTER]) 350 >> Know `lam (l2 INTER s) + lam ((space g0 DIFF l2) INTER s) = lam s` 351 >- PROVE_TAC [] 352 >> Know 353 `lam (l1 INTER l2 INTER s) + lam (l2 INTER (space g0 DIFF l1) INTER s) = 354 lam (l2 INTER s)` 355 >- (Know `l2 INTER (space g0 DIFF l1) INTER s = (space g0 DIFF l1) INTER (l2 INTER s)` 356 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF] 357 >> PROVE_TAC []) 358 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 359 >> REWRITE_TAC [INTER_ASSOC] 360 >> Q.PAT_X_ASSUM `!g. P g` K_TAC 361 >> Q.PAT_X_ASSUM `!g. P g` MATCH_MP_TAC 362 >> PROVE_TAC [ALGEBRA_ALT_INTER]) 363 >> Q.SPEC_TAC (`l1 INTER l2`, `l`) 364 >> GEN_TAC 365 >> Q.SPEC_TAC (`lam (l2 INTER (space g0 DIFF l1) INTER s)`, `r1`) 366 >> Q.SPEC_TAC (`lam (l INTER s)`, `r2`) 367 >> Q.SPEC_TAC (`lam ((space g0 DIFF l2) INTER s)`, `r3`) 368 >> Q.SPEC_TAC (`lam (l2 INTER s)`, `r4`) 369 >> Q.SPEC_TAC (`lam s`, `r5`) 370 >> Q.SPEC_TAC (`lam ((space g0 DIFF l) INTER s)`, `r6`) 371 >> KILL_TAC 372 >> REAL_ARITH_TAC); 373 374 375val LAMBDA_SYSTEM_ALGEBRA = store_thm 376 ("LAMBDA_SYSTEM_ALGEBRA", 377 ``!g0 lam. 378 algebra g0 /\ positive (space g0, subsets g0, lam) ==> algebra (space g0, lambda_system g0 lam)``, 379 RW_TAC std_ss [ALGEBRA_ALT_INTER, LAMBDA_SYSTEM_EMPTY, positive_def, 380 LAMBDA_SYSTEM_COMPL, LAMBDA_SYSTEM_INTER, space_def, subsets_def, subset_class_def] 381 >> FULL_SIMP_TAC std_ss [lambda_system_def, GSPECIFICATION]); 382 383 384val LAMBDA_SYSTEM_STRONG_ADDITIVE = store_thm 385 ("LAMBDA_SYSTEM_STRONG_ADDITIVE", 386 ``!g0 lam g l1 l2. 387 algebra g0 /\ positive (space g0, subsets g0, lam) /\ g IN (subsets g0) /\ DISJOINT l1 l2 /\ 388 l1 IN lambda_system g0 lam /\ l2 IN lambda_system g0 lam ==> 389 (lam ((l1 UNION l2) INTER g) = lam (l1 INTER g) + lam (l2 INTER g))``, 390 RW_TAC std_ss [positive_def] 391 >> Know `l1 INTER g = l1 INTER ((l1 UNION l2) INTER g)` 392 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_UNION] 393 >> PROVE_TAC []) 394 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 395 >> Know `l2 INTER g = (space g0 DIFF l1) INTER ((l1 UNION l2) INTER g)` 396 >- (Q.PAT_X_ASSUM `DISJOINT x y` MP_TAC 397 >> RW_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, DISJOINT_DEF, 398 NOT_IN_EMPTY] 399 >> PROVE_TAC [algebra_def, SUBSET_DEF, subset_class_def]) 400 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 401 >> Know `(l1 UNION l2) INTER g IN (subsets g0)` 402 >- (Suff `l1 IN (subsets g0) /\ l2 IN (subsets g0)` 403 >- PROVE_TAC [algebra_def, SUBSET_DEF, ALGEBRA_ALT_INTER, subset_class_def] 404 >> rpt (POP_ASSUM MP_TAC) 405 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION]) 406 >> STRIP_TAC 407 >> Q.PAT_X_ASSUM `l1 IN x` MP_TAC 408 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION]); 409 410 411val LAMBDA_SYSTEM_ADDITIVE = store_thm 412 ("LAMBDA_SYSTEM_ADDITIVE", 413 ``!g0 lam l1 l2. 414 algebra g0 /\ positive (space g0, subsets g0, lam) ==> 415 additive (space g0, lambda_system g0 lam, lam)``, 416 RW_TAC std_ss [additive_def, measure_def, measurable_sets_def] 417 >> MP_TAC (Q.SPECL [`g0`, `lam`, `space g0`, `s`, `t`] 418 LAMBDA_SYSTEM_STRONG_ADDITIVE) 419 >> FULL_SIMP_TAC std_ss [lambda_system_def, GSPECIFICATION, ALGEBRA_INTER_SPACE, ALGEBRA_SPACE, ALGEBRA_UNION]); 420 421 422val COUNTABLY_SUBADDITIVE_SUBADDITIVE = store_thm 423 ("COUNTABLY_SUBADDITIVE_SUBADDITIVE", 424 ``!m. 425 algebra (m_space m, measurable_sets m) /\ positive m /\ countably_subadditive m ==> 426 subadditive m``, 427 RW_TAC std_ss [countably_subadditive_def, subadditive_def] 428 >> Q.PAT_X_ASSUM `!f. P f` 429 (MP_TAC o Q.SPEC `\n : num. if n = 0 then s else if n = 1 then t else {}`) 430 >> Know 431 `BIGUNION 432 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 433 UNIV) = 434 s UNION t` 435 >- (Suff 436 `IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 437 UNIV = 438 {s; t; {}}` 439 >- (RW_TAC std_ss [BIGUNION, EXTENSION, IN_INSERT, GSPECIFICATION] 440 >> RW_TAC std_ss [GSYM EXTENSION] 441 >> RW_TAC std_ss [NOT_IN_EMPTY, IN_UNION] 442 >> PROVE_TAC [NOT_IN_EMPTY]) 443 >> RW_TAC arith_ss [EXTENSION, IN_IMAGE, IN_INSERT, IN_UNIV] 444 >> RW_TAC std_ss [GSYM EXTENSION] 445 >> RW_TAC std_ss [NOT_IN_EMPTY] 446 >> KILL_TAC 447 >> EQ_TAC >- PROVE_TAC [] 448 >> Know `~(0:num = 1) /\ ~(0:num = 2) /\ ~(1:num = 2)` >- DECIDE_TAC 449 >> PROVE_TAC []) 450 >> DISCH_THEN (REWRITE_TAC o wrap) 451 >> Know 452 `(measure m o (\n. (if n = 0 then s else (if n = 1 then t else {})))) sums 453 (measure m s + measure m t)` 454 >- (Know 455 `measure m s + measure m t = 456 sum (0,2) 457 (measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))))` 458 >- (ASM_SIMP_TAC bool_ss [TWO, sum, ONE, o_DEF] 459 >> RW_TAC arith_ss [] 460 >> RW_TAC real_ss []) 461 >> DISCH_THEN (REWRITE_TAC o wrap) 462 >> MATCH_MP_TAC SER_0 463 >> RW_TAC arith_ss [o_DEF] 464 >> PROVE_TAC [positive_def]) 465 >> REWRITE_TAC [SUMS_EQ] 466 >> DISCH_THEN (REWRITE_TAC o CONJUNCTS) 467 >> DISCH_THEN MATCH_MP_TAC 468 >> CONJ_TAC 469 >- (Q.PAT_X_ASSUM `algebra a` MP_TAC 470 >> BasicProvers.NORM_TAC std_ss [IN_FUNSET, IN_UNIV, algebra_def, subsets_def, subset_class_def]) 471 >> PROVE_TAC [algebra_def, subsets_def, subset_class_def]); 472 473 474val SIGMA_ALGEBRA_ALT = store_thm 475 ("SIGMA_ALGEBRA_ALT", 476 ``!a. 477 sigma_algebra a = 478 algebra a /\ 479 (!f : num -> 'a -> bool. 480 f IN (UNIV -> (subsets a)) ==> BIGUNION (IMAGE f UNIV) IN (subsets a))``, 481 RW_TAC std_ss [sigma_algebra_def] 482 >> EQ_TAC 483 >- (RW_TAC std_ss [COUNTABLE_ALT, IN_FUNSET, IN_UNIV] 484 >> Q.PAT_X_ASSUM `!c. P c ==> Q c` MATCH_MP_TAC 485 >> REVERSE (RW_TAC std_ss [IN_IMAGE, SUBSET_DEF, IN_UNIV]) 486 >- PROVE_TAC [] 487 >> Q.EXISTS_TAC `f` 488 >> RW_TAC std_ss [] 489 >> PROVE_TAC []) 490 >> RW_TAC std_ss [COUNTABLE_ALT_BIJ] 491 >- PROVE_TAC [ALGEBRA_FINITE_UNION] 492 >> Q.PAT_X_ASSUM `!f. P f` (MP_TAC o Q.SPEC `\n. enumerate c n`) 493 >> RW_TAC std_ss' [IN_UNIV, IN_FUNSET] 494 >> Know `BIGUNION c = BIGUNION (IMAGE (enumerate c) UNIV)` 495 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_UNIV] 496 >> Suff `!s. s IN c = ?n. (enumerate c n = s)` >- PROVE_TAC [] 497 >> Q.PAT_X_ASSUM `BIJ x y z` MP_TAC 498 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV] 499 >> PROVE_TAC []) 500 >> DISCH_THEN (REWRITE_TAC o wrap) 501 >> POP_ASSUM MATCH_MP_TAC 502 >> Strip 503 >> Suff `enumerate c n IN c` >- PROVE_TAC [SUBSET_DEF] 504 >> Q.PAT_X_ASSUM `BIJ i j k` MP_TAC 505 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV]); 506 507 508val SIGMA_ALGEBRA_ALT_MONO = store_thm 509 ("SIGMA_ALGEBRA_ALT_MONO", 510 ``!a. 511 sigma_algebra a = 512 algebra a /\ 513 (!f : num -> 'a -> bool. 514 f IN (UNIV -> (subsets a)) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 515 BIGUNION (IMAGE f UNIV) IN (subsets a))``, 516 RW_TAC std_ss [SIGMA_ALGEBRA_ALT] 517 >> EQ_TAC >- PROVE_TAC [] 518 >> RW_TAC std_ss [] 519 >> Q.PAT_X_ASSUM `!f. P f` 520 (MP_TAC o Q.SPEC `\n. BIGUNION (IMAGE f (count n))`) 521 >> RW_TAC std_ss [IN_UNIV, IN_FUNSET] 522 >> Know 523 `BIGUNION (IMAGE f UNIV) = 524 BIGUNION (IMAGE (\n. BIGUNION (IMAGE f (count n))) UNIV)` 525 >- (KILL_TAC 526 >> ONCE_REWRITE_TAC [EXTENSION] 527 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV] 528 >> EQ_TAC 529 >- (RW_TAC std_ss [] 530 >> Q.EXISTS_TAC `BIGUNION (IMAGE f (count (SUC x')))` 531 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 532 >> PROVE_TAC [prim_recTheory.LESS_SUC_REFL]) 533 >> RW_TAC std_ss [] 534 >> POP_ASSUM MP_TAC 535 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 536 >> PROVE_TAC []) 537 >> DISCH_THEN (REWRITE_TAC o wrap) 538 >> POP_ASSUM MATCH_MP_TAC 539 >> REVERSE (RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_COUNT, IN_IMAGE, 540 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY]) 541 >- (Q.EXISTS_TAC `f x'` 542 >> RW_TAC std_ss [] 543 >> Q.EXISTS_TAC `x'` 544 >> DECIDE_TAC) 545 >> MATCH_MP_TAC ALGEBRA_FINITE_UNION 546 >> POP_ASSUM MP_TAC 547 >> REVERSE (RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF, IN_IMAGE]) 548 >- PROVE_TAC [] 549 >> MATCH_MP_TAC IMAGE_FINITE 550 >> RW_TAC std_ss [FINITE_COUNT]); 551 552 553val SIGMA_ALGEBRA_ALT_DISJOINT = store_thm 554 ("SIGMA_ALGEBRA_ALT_DISJOINT", 555 ``!a. 556 sigma_algebra a = 557 algebra a /\ 558 (!f. 559 f IN (UNIV -> (subsets a)) /\ 560 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 561 BIGUNION (IMAGE f UNIV) IN (subsets a))``, 562 Strip 563 >> EQ_TAC >- RW_TAC std_ss [SIGMA_ALGEBRA_ALT] 564 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALT_MONO, IN_FUNSET, IN_UNIV] 565 >> Q.PAT_X_ASSUM `!f. P f ==> Q f` (MP_TAC o Q.SPEC `\n. f (SUC n) DIFF f n`) 566 >> RW_TAC std_ss [] 567 >> Know 568 `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE (\n. f (SUC n) DIFF f n) UNIV)` 569 >- (POP_ASSUM K_TAC 570 >> ONCE_REWRITE_TAC [EXTENSION] 571 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_DIFF] 572 >> REVERSE EQ_TAC 573 >- (RW_TAC std_ss [] 574 >> POP_ASSUM MP_TAC 575 >> RW_TAC std_ss [IN_DIFF] 576 >> PROVE_TAC []) 577 >> RW_TAC std_ss [] 578 >> Induct_on `x'` >- RW_TAC std_ss [NOT_IN_EMPTY] 579 >> RW_TAC std_ss [] 580 >> Cases_on `x IN f x'` >- PROVE_TAC [] 581 >> Q.EXISTS_TAC `f (SUC x') DIFF f x'` 582 >> RW_TAC std_ss [EXTENSION, IN_DIFF] 583 >> PROVE_TAC []) 584 >> DISCH_THEN (REWRITE_TAC o wrap) 585 >> POP_ASSUM MATCH_MP_TAC 586 >> CONJ_TAC >- RW_TAC std_ss [ALGEBRA_DIFF] 587 >> HO_MATCH_MP_TAC TRANSFORM_2D_NUM 588 >> CONJ_TAC >- PROVE_TAC [DISJOINT_SYM] 589 >> RW_TAC arith_ss [] 590 >> Suff `f (SUC m) SUBSET f (m + n)` 591 >- (RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, 592 IN_INTER, IN_DIFF, SUBSET_DEF] 593 >> PROVE_TAC []) 594 >> Cases_on `n` >- PROVE_TAC [ADD_CLAUSES] 595 >> POP_ASSUM K_TAC 596 >> Know `m + SUC n' = SUC m + n'` >- DECIDE_TAC 597 >> DISCH_THEN (REWRITE_TAC o wrap) 598 >> Induct_on `n'` >- RW_TAC arith_ss [SUBSET_REFL] 599 >> MATCH_MP_TAC SUBSET_TRANS 600 >> Q.EXISTS_TAC `f (SUC m + n')` 601 >> PROVE_TAC [ADD_CLAUSES]); 602 603 604val SUBADDITIVE = store_thm 605 ("SUBADDITIVE", 606 ``!m s t u. 607 subadditive m /\ s IN measurable_sets m /\ t IN measurable_sets m /\ 608 (u = s UNION t) ==> 609 measure m u <= measure m s + measure m t``, 610 RW_TAC std_ss [subadditive_def]); 611 612 613val ADDITIVE = store_thm 614 ("ADDITIVE", 615 ``!m s t u. 616 additive m /\ s IN measurable_sets m /\ t IN measurable_sets m /\ 617 DISJOINT s t /\ (u = s UNION t) ==> 618 (measure m u = measure m s + measure m t)``, 619 RW_TAC std_ss [additive_def]); 620 621 622val COUNTABLY_SUBADDITIVE = store_thm 623 ("COUNTABLY_SUBADDITIVE", 624 ``!m f s. 625 countably_subadditive m /\ f IN (UNIV -> measurable_sets m) /\ 626 summable (measure m o f) /\ (s = BIGUNION (IMAGE f UNIV)) /\ 627 (s IN measurable_sets m) ==> 628 measure m s <= suminf (measure m o f)``, 629 PROVE_TAC [countably_subadditive_def]); 630 631 632val ADDITIVE_SUM = store_thm 633 ("ADDITIVE_SUM", 634 ``!m f n. 635 algebra (m_space m, measurable_sets m) /\ positive m /\ additive m /\ 636 f IN (UNIV -> measurable_sets m) /\ 637 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 638 (sum (0, n) (measure m o f) = 639 measure m (BIGUNION (IMAGE f (count n))))``, 640 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 641 >> Induct_on `n` 642 >- (RW_TAC std_ss [sum, COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY] 643 >> PROVE_TAC [positive_def]) 644 >> RW_TAC std_ss [sum, COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT, ADD_CLAUSES, 645 o_DEF] 646 >> MATCH_MP_TAC EQ_SYM 647 >> ONCE_REWRITE_TAC [REAL_ADD_SYM] 648 >> MATCH_MP_TAC ADDITIVE 649 >> RW_TAC std_ss [DISJOINT_COUNT] 650 >> MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_FINITE_UNION) 651 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] 652 >> PROVE_TAC [FINITE_COUNT, IMAGE_FINITE]); 653 654 655val INCREASING_ADDITIVE_SUMMABLE = store_thm 656 ("INCREASING_ADDITIVE_SUMMABLE", 657 ``!m f. 658 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m /\ 659 additive m /\ f IN (UNIV -> measurable_sets m) /\ 660 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 661 summable (measure m o f)``, 662 RW_TAC std_ss [increasing_def] 663 >> MATCH_MP_TAC POS_SUMMABLE 664 >> CONJ_TAC 665 >- FULL_SIMP_TAC std_ss [o_DEF, IN_FUNSET, IN_UNIV, positive_def] 666 >> Q.EXISTS_TAC `measure m (m_space m)` 667 >> RW_TAC std_ss [] 668 >> MP_TAC (Q.SPECL [`m`, `f`, `n`] ADDITIVE_SUM) 669 >> ASM_REWRITE_TAC [] 670 >> DISCH_THEN (REWRITE_TAC o wrap) 671 >> Q.PAT_X_ASSUM `!(s : 'a -> bool). P s` MATCH_MP_TAC 672 >> CONJ_TAC 673 >- (MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_FINITE_UNION) 674 >> Q.PAT_X_ASSUM `f IN x` MP_TAC 675 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF, IN_IMAGE] 676 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]) 677 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_SPACE, space_def, subsets_def] 678 >> Q.PAT_X_ASSUM `f IN x` MP_TAC 679 >> Q.PAT_X_ASSUM `algebra a` MP_TAC 680 >> RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, IN_COUNT, 681 IN_FUNSET, IN_UNIV, algebra_def, space_def, subsets_def, subset_class_def] 682 >> PROVE_TAC []); 683 684 685val LAMBDA_SYSTEM_POSITIVE = store_thm 686 ("LAMBDA_SYSTEM_POSITIVE", 687 ``!g0 lam. positive (space g0, subsets g0, lam) ==> positive (space g0, lambda_system g0 lam, lam)``, 688 RW_TAC std_ss [positive_def, lambda_system_def, GSPECIFICATION, 689 measure_def, measurable_sets_def]); 690 691 692val LAMBDA_SYSTEM_INCREASING = store_thm 693 ("LAMBDA_SYSTEM_INCREASING", 694 ``!g0 lam. increasing (space g0, subsets g0, lam) ==> increasing (space g0, lambda_system g0 lam, lam)``, 695 RW_TAC std_ss [increasing_def, lambda_system_def, GSPECIFICATION, 696 measure_def, measurable_sets_def]); 697 698 699val LAMBDA_SYSTEM_STRONG_SUM = store_thm 700 ("LAMBDA_SYSTEM_STRONG_SUM", 701 ``!g0 lam g f n. 702 algebra g0 /\ positive (space g0, subsets g0, lam) /\ g IN (subsets g0) /\ 703 f IN (UNIV -> lambda_system g0 lam) /\ 704 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 705 (sum (0, n) (lam o (\s. s INTER g) o f) = 706 lam (BIGUNION (IMAGE f (count n)) INTER g))``, 707 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 708 >> Induct_on `n` 709 >- (RW_TAC std_ss [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, sum, INTER_EMPTY] 710 >> PROVE_TAC [positive_def, measure_def]) 711 >> RW_TAC arith_ss [COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT, sum, o_DEF] 712 >> ONCE_REWRITE_TAC [REAL_ADD_SYM] 713 >> MATCH_MP_TAC EQ_SYM 714 >> MATCH_MP_TAC LAMBDA_SYSTEM_STRONG_ADDITIVE 715 >> Q.EXISTS_TAC `g0` 716 >> RW_TAC std_ss [DISJOINT_COUNT] 717 >> MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(space g0,lambda_system g0 lam)`) ALGEBRA_FINITE_UNION) 718 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, LAMBDA_SYSTEM_ALGEBRA] 719 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]); 720 721 722val SIGMA_ALGEBRA_ALGEBRA = store_thm 723 ("SIGMA_ALGEBRA_ALGEBRA", 724 ``!a. sigma_algebra a ==> algebra a``, 725 PROVE_TAC [sigma_algebra_def]); 726 727 728val OUTER_MEASURE_SPACE_POSITIVE = store_thm 729 ("OUTER_MEASURE_SPACE_POSITIVE", 730 ``!m. outer_measure_space m ==> positive m``, 731 PROVE_TAC [outer_measure_space_def]); 732 733 734val LAMBDA_SYSTEM_CARATHEODORY = store_thm 735 ("LAMBDA_SYSTEM_CARATHEODORY", 736 ``!gsig lam. 737 sigma_algebra gsig /\ outer_measure_space (space gsig, subsets gsig, lam) ==> 738 (!f. 739 f IN (UNIV -> lambda_system gsig lam) /\ 740 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 741 BIGUNION (IMAGE f UNIV) IN lambda_system gsig lam /\ 742 ((lam o f) sums lam (BIGUNION (IMAGE f UNIV))))``, 743 NTAC 5 STRIP_TAC 744 >> Know `summable (lam o f)` 745 >- (Suff `summable (measure (space gsig, lambda_system gsig lam, lam) o f)` 746 >- RW_TAC std_ss [measure_def] 747 >> MATCH_MP_TAC INCREASING_ADDITIVE_SUMMABLE 748 >> REWRITE_TAC [measurable_sets_def, m_space_def] 749 >> CONJ_TAC 750 >- (MATCH_MP_TAC LAMBDA_SYSTEM_ALGEBRA 751 >> CONJ_TAC >- PROVE_TAC [sigma_algebra_def] 752 >> PROVE_TAC [outer_measure_space_def]) 753 >> CONJ_TAC 754 >- PROVE_TAC [LAMBDA_SYSTEM_POSITIVE, outer_measure_space_def] 755 >> CONJ_TAC 756 >- PROVE_TAC [LAMBDA_SYSTEM_INCREASING, outer_measure_space_def] 757 >> CONJ_TAC 758 >- PROVE_TAC [LAMBDA_SYSTEM_ADDITIVE, outer_measure_space_def, 759 sigma_algebra_def] 760 >> RW_TAC std_ss []) 761 >> STRIP_TAC 762 >> Know `BIGUNION (IMAGE f UNIV) IN subsets gsig` 763 >- (Q.PAT_X_ASSUM `sigma_algebra a` MP_TAC 764 >> Q.PAT_X_ASSUM `f IN s` MP_TAC 765 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALT, IN_FUNSET, IN_UNIV] 766 >> POP_ASSUM MATCH_MP_TAC 767 >> RW_TAC std_ss [] 768 >> Q.PAT_X_ASSUM `!x. P x` MP_TAC 769 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION]) 770 >> STRIP_TAC 771 >> Suff 772 `!g l. 773 g IN subsets gsig /\ (BIGUNION (IMAGE f (UNIV : num -> bool)) = l) ==> 774 (lam (l INTER g) + lam ((space gsig DIFF l) INTER g) = lam g) /\ 775 (lam (l INTER g) = suminf (lam o (\s. s INTER g) o f))` 776 >- (RW_TAC std_ss [lambda_system_def, GSPECIFICATION, SUMS_EQ] 777 >> POP_ASSUM 778 (MP_TAC o Q.SPEC `BIGUNION (IMAGE (f : num -> 'a -> bool) UNIV)`) 779 >> RW_TAC std_ss [INTER_IDEMPOT] 780 >> Suff `(\s. s INTER BIGUNION (IMAGE f UNIV)) o f = f` 781 >- RW_TAC std_ss [] 782 >> KILL_TAC 783 >> FUN_EQ_TAC 784 >> RW_TAC std_ss [o_DEF, EXTENSION, IN_INTER, IN_BIGUNION, 785 GSPECIFICATION, IN_IMAGE, IN_UNIV] 786 >> PROVE_TAC []) 787 >> rpt GEN_TAC 788 >> STRIP_TAC 789 >> Know `summable (lam o (\s. s INTER g) o f)` 790 >- (MATCH_MP_TAC SER_COMPAR 791 >> Q.EXISTS_TAC `lam o f` 792 >> RW_TAC std_ss [] 793 >> Q.EXISTS_TAC `0` 794 >> RW_TAC arith_ss [o_DEF] 795 >> Q.PAT_X_ASSUM `outer_measure_space (space gsig,subsets gsig,lam)` MP_TAC 796 >> RW_TAC std_ss [outer_measure_space_def, increasing_def, positive_def, 797 measure_def, measurable_sets_def] 798 >> Know `f n IN subsets gsig` 799 >- (Q.PAT_X_ASSUM `f IN x` MP_TAC 800 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, lambda_system_def, 801 GSPECIFICATION]) 802 >> STRIP_TAC 803 >> Know `f n INTER g IN subsets gsig` 804 >- PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def] 805 >> STRIP_TAC 806 >> Know `0 <= lam (f n INTER g)` >- PROVE_TAC [] 807 >> RW_TAC std_ss [abs] 808 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 809 >> RW_TAC std_ss [SUBSET_DEF, IN_INTER]) 810 >> STRIP_TAC 811 >> Suff 812 `lam g <= lam (l INTER g) + lam ((space gsig DIFF l) INTER g) /\ 813 lam (l INTER g) <= suminf (lam o (\s. s INTER g) o f) /\ 814 suminf (lam o (\s. s INTER g) o f) + lam ((space gsig DIFF l) INTER g) <= lam g` 815 >- REAL_ARITH_TAC 816 >> Strip >| 817 [Know `lam = measure (space gsig,subsets gsig,lam)` >- RW_TAC std_ss [measure_def] 818 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 819 >> MATCH_MP_TAC SUBADDITIVE 820 >> REWRITE_TAC [measurable_sets_def] 821 >> CONJ_TAC 822 >- (MATCH_MP_TAC COUNTABLY_SUBADDITIVE_SUBADDITIVE 823 >> REWRITE_TAC [measurable_sets_def, m_space_def, SPACE] 824 >> PROVE_TAC [outer_measure_space_def, sigma_algebra_def]) 825 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def] 826 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def, ALGEBRA_COMPL] 827 >> RW_TAC std_ss [EXTENSION, DISJOINT_DEF, IN_INTER, NOT_IN_EMPTY, IN_DIFF, 828 IN_UNION] 829 >> FULL_SIMP_TAC std_ss [sigma_algebra_def, algebra_def, SUBSET_DEF, subset_class_def] 830 >> PROVE_TAC [], 831 Q.PAT_X_ASSUM `f IN (x -> y)` MP_TAC 832 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV] 833 >> Know `lam = measure (space gsig,subsets gsig,lam)` >- RW_TAC std_ss [measure_def] 834 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 835 >> MATCH_MP_TAC COUNTABLY_SUBADDITIVE 836 >> REWRITE_TAC [measurable_sets_def, measure_def] 837 >> CONJ_TAC >- PROVE_TAC [outer_measure_space_def] 838 >> CONJ_TAC 839 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_DEF] 840 >> POP_ASSUM (MP_TAC o Q.SPEC `x`) 841 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION] 842 >> PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def]) 843 >> CONJ_TAC >- PROVE_TAC [] 844 >> CONJ_TAC 845 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_BIGUNION, IN_IMAGE, IN_UNIV, 846 o_DEF] 847 >> REVERSE EQ_TAC >- PROVE_TAC [] 848 >> RW_TAC std_ss [GSYM EXTENSION] 849 >> Q.EXISTS_TAC `f x' INTER g` 850 >> RW_TAC std_ss [IN_INTER] 851 >> PROVE_TAC []) 852 >> PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def], 853 Suff `suminf (lam o (\s. s INTER g) o f) <= lam g - lam ((space gsig DIFF l) INTER g)` 854 >- REAL_ARITH_TAC 855 >> MATCH_MP_TAC SUMMABLE_LE 856 >> CONJ_TAC >- PROVE_TAC [] 857 >> GEN_TAC 858 >> MP_TAC (Q.SPECL [`gsig`, `lam`, `g`, `f`, `n`] LAMBDA_SYSTEM_STRONG_SUM) 859 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALGEBRA, OUTER_MEASURE_SPACE_POSITIVE] 860 >> POP_ASSUM K_TAC 861 >> Suff 862 `(lam g = lam (BIGUNION (IMAGE f (count n)) INTER g) + 863 lam ((space gsig DIFF BIGUNION (IMAGE f (count n))) INTER g)) /\ 864 lam ((space gsig DIFF BIGUNION (IMAGE f UNIV)) INTER g) <= 865 lam ((space gsig DIFF BIGUNION (IMAGE f (count n))) INTER g)` 866 >- REAL_ARITH_TAC 867 >> CONJ_TAC 868 >- (Suff `BIGUNION (IMAGE f (count n)) IN lambda_system gsig lam` 869 >- RW_TAC std_ss [lambda_system_def, GSPECIFICATION] 870 >> MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(space gsig,lambda_system gsig lam)`) ALGEBRA_FINITE_UNION) 871 >> Q.PAT_X_ASSUM `f IN (x -> y)` MP_TAC 872 >> RW_TAC std_ss [SUBSET_DEF, IN_FUNSET, IN_UNIV, IN_IMAGE] 873 >> PROVE_TAC [LAMBDA_SYSTEM_ALGEBRA, SIGMA_ALGEBRA_ALGEBRA, 874 OUTER_MEASURE_SPACE_POSITIVE, IMAGE_FINITE, FINITE_COUNT]) 875 >> Q.PAT_X_ASSUM `outer_measure_space (space gsig,subsets gsig,lam)` MP_TAC 876 >> RW_TAC std_ss [outer_measure_space_def, increasing_def, measure_def, 877 measurable_sets_def] 878 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 879 >> CONJ_TAC 880 >- PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_COMPL, ALGEBRA_INTER] 881 >> CONJ_TAC 882 >- (Know `algebra gsig` >- PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA] 883 >> STRIP_TAC 884 >> MATCH_MP_TAC ALGEBRA_INTER 885 >> RW_TAC std_ss [] 886 >> MATCH_MP_TAC ALGEBRA_COMPL 887 >> RW_TAC std_ss [] 888 >> MATCH_MP_TAC ALGEBRA_FINITE_UNION 889 >> Q.PAT_X_ASSUM `f IN x` MP_TAC 890 >> RW_TAC std_ss [SUBSET_DEF, IN_FUNSET, IN_UNIV, lambda_system_def, 891 GSPECIFICATION, IN_IMAGE] 892 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]) 893 >> RW_TAC std_ss [SUBSET_DEF, IN_INTER, IN_COMPL, IN_IMAGE, IN_BIGUNION, 894 IN_UNIV, IN_DIFF] 895 >> PROVE_TAC []]); 896 897 898val CARATHEODORY_LEMMA = store_thm 899 ("CARATHEODORY_LEMMA", 900 ``!gsig lam. 901 sigma_algebra gsig /\ outer_measure_space (space gsig, subsets gsig, lam) ==> 902 measure_space (space gsig, lambda_system gsig lam, lam)``, 903 RW_TAC std_ss [] 904 >> MP_TAC (Q.SPECL [`gsig`, `lam`] LAMBDA_SYSTEM_CARATHEODORY) 905 >> RW_TAC std_ss [measure_space_def, countably_additive_def, 906 measurable_sets_def, measure_def, m_space_def] >| 907 [RW_TAC std_ss [SIGMA_ALGEBRA_ALT_DISJOINT, subsets_def] 908 >> PROVE_TAC [LAMBDA_SYSTEM_ALGEBRA, SIGMA_ALGEBRA_ALGEBRA, 909 outer_measure_space_def], 910 PROVE_TAC [outer_measure_space_def, LAMBDA_SYSTEM_POSITIVE]]); 911 912 913val INF_MEASURE_NONEMPTY = store_thm 914 ("INF_MEASURE_NONEMPTY", 915 ``!m g s. 916 algebra (m_space m, measurable_sets m) /\ positive m /\ s IN measurable_sets m /\ 917 g SUBSET s ==> 918 measure m s IN 919 {r | 920 ?f. 921 f IN (UNIV -> measurable_sets m) /\ 922 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 923 g SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r}``, 924 RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, positive_def] 925 >> Q.EXISTS_TAC `\n. if n = 0 then s else {}` 926 >> BasicProvers.NORM_TAC std_ss 927 [SUBSET_DEF, IN_BIGUNION, DISJOINT_EMPTY, 928 IN_IMAGE, IN_UNIV, o_DEF, IN_FUNSET, ALGEBRA_EMPTY] 929 >| [PROVE_TAC [subsets_def, ALGEBRA_EMPTY], 930 PROVE_TAC [], 931 Know `measure m s = sum (0,1) (\x. measure m (if x = 0 then s else {}))` 932 >- (ASM_SIMP_TAC bool_ss [sum, ONE, REAL_ADD_LID] >> RW_TAC arith_ss []) 933 >> DISCH_THEN (REWRITE_TAC o wrap) 934 >> MATCH_MP_TAC SER_0 935 >> RW_TAC arith_ss []]); 936 937 938val INF_MEASURE_POS0 = store_thm 939 ("INF_MEASURE_POS0", 940 ``!m g x. 941 algebra (m_space m,measurable_sets m) /\ positive m /\ 942 x IN 943 {r | 944 ?f. 945 f IN (UNIV -> measurable_sets m) /\ 946 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 947 g SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r} ==> 948 0 <= x``, 949 RW_TAC std_ss [GSPECIFICATION, SUMS_EQ, IN_FUNSET, IN_UNIV, positive_def] 950 >> MATCH_MP_TAC SER_POS 951 >> RW_TAC std_ss [o_DEF]); 952 953 954val INF_MEASURE_POS = store_thm 955 ("INF_MEASURE_POS", 956 ``!m g. algebra (m_space m, measurable_sets m) /\ positive m /\ g SUBSET m_space m ==> 0 <= inf_measure m g``, 957 RW_TAC std_ss [GSPECIFICATION, inf_measure_def] 958 >> MATCH_MP_TAC LE_INF 959 >> CONJ_TAC 960 >- (Q.EXISTS_TAC `measure m (m_space m)` 961 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 962 >> PROVE_TAC [ALGEBRA_SPACE, space_def, subsets_def]) 963 >> METIS_TAC [INF_MEASURE_POS0]); 964 965 966val INCREASING = store_thm 967 ("INCREASING", 968 ``!m s t. 969 increasing m /\ s SUBSET t /\ s IN measurable_sets m /\ 970 t IN measurable_sets m ==> 971 measure m s <= measure m t``, 972 PROVE_TAC [increasing_def]); 973 974 975val ADDITIVE_INCREASING = store_thm 976 ("ADDITIVE_INCREASING", 977 ``!m. 978 algebra (m_space m, measurable_sets m) /\ positive m /\ additive m ==> 979 increasing m``, 980 RW_TAC std_ss [increasing_def, positive_def] 981 >> Suff 982 `?u. u IN measurable_sets m /\ (measure m t = measure m s + measure m u)` 983 >- (RW_TAC std_ss [] 984 >> Q.PAT_X_ASSUM `!s. P s` (MP_TAC o Q.SPEC `u`) 985 >> RW_TAC std_ss [] 986 >> NTAC 2 (POP_ASSUM MP_TAC) 987 >> REAL_ARITH_TAC) 988 >> Q.EXISTS_TAC `t DIFF s` 989 >> STRONG_CONJ_TAC >- PROVE_TAC [ALGEBRA_DIFF, subsets_def] 990 >> RW_TAC std_ss [] 991 >> MATCH_MP_TAC ADDITIVE 992 >> RW_TAC std_ss [DISJOINT_DEF, IN_DIFF, IN_UNION, EXTENSION, IN_INTER, 993 NOT_IN_EMPTY] 994 >> PROVE_TAC [SUBSET_DEF]); 995 996 997val COUNTABLY_ADDITIVE_ADDITIVE = store_thm 998 ("COUNTABLY_ADDITIVE_ADDITIVE", 999 ``!m. 1000 algebra (m_space m, measurable_sets m) /\ positive m /\ countably_additive m ==> 1001 additive m``, 1002 RW_TAC std_ss [additive_def, positive_def, countably_additive_def] 1003 >> Q.PAT_X_ASSUM `!f. P f` 1004 (MP_TAC o Q.SPEC `\n : num. if n = 0 then s else if n = 1 then t else {}`) 1005 >> Know 1006 `BIGUNION 1007 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 1008 UNIV) = 1009 s UNION t` 1010 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_UNION] 1011 >> EQ_TAC >- PROVE_TAC [NOT_IN_EMPTY] 1012 >> Know `~(1 = (0:num))` >- DECIDE_TAC 1013 >> RW_TAC std_ss [] >- PROVE_TAC [] 1014 >> Q.EXISTS_TAC `t` 1015 >> RW_TAC std_ss [] 1016 >> Q.EXISTS_TAC `1` 1017 >> RW_TAC std_ss [] 1018 >> PROVE_TAC []) 1019 >> DISCH_THEN (REWRITE_TAC o wrap) 1020 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV] 1021 >> Suff 1022 `measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))) sums 1023 (measure m s + measure m t) /\ 1024 measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))) sums 1025 measure m (s UNION t)` 1026 >- PROVE_TAC [SUM_UNIQ] 1027 >> CONJ_TAC 1028 >- (Know 1029 `measure m s + measure m t = 1030 sum (0, 2) 1031 (measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))))` 1032 >- (ASM_SIMP_TAC bool_ss [TWO, ONE, sum] 1033 >> RW_TAC std_ss [] 1034 >> RW_TAC arith_ss [REAL_ADD_LID, o_THM]) 1035 >> DISCH_THEN (REWRITE_TAC o wrap) 1036 >> MATCH_MP_TAC SER_0 1037 >> RW_TAC arith_ss [o_THM]) 1038 >> POP_ASSUM MATCH_MP_TAC 1039 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_EMPTY, space_def, subsets_def] 1040 >> RW_TAC std_ss [DISJOINT_EMPTY] 1041 >> PROVE_TAC [DISJOINT_SYM, ALGEBRA_UNION, subsets_def]); 1042 1043 1044val COUNTABLY_ADDITIVE = store_thm 1045 ("COUNTABLY_ADDITIVE", 1046 ``!m s f. 1047 countably_additive m /\ f IN (UNIV -> measurable_sets m) 1048 /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1049 (s = BIGUNION (IMAGE f UNIV)) /\ s IN measurable_sets m ==> 1050 measure m o f sums measure m s``, 1051 RW_TAC std_ss [] 1052 >> PROVE_TAC [countably_additive_def]); 1053 1054 1055val INF_MEASURE_AGREES = store_thm 1056 ("INF_MEASURE_AGREES", 1057 ``!m s. 1058 algebra (m_space m, measurable_sets m) /\ positive m /\ countably_additive m /\ 1059 s IN measurable_sets m ==> 1060 (inf_measure m s = measure m s)``, 1061 RW_TAC std_ss [inf_measure_def] 1062 >> ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 1063 >> CONJ_TAC 1064 >- (MATCH_MP_TAC INF_LE 1065 >> CONJ_TAC 1066 >- (Q.EXISTS_TAC `0` 1067 >> METIS_TAC [INF_MEASURE_POS0]) 1068 >> Q.EXISTS_TAC `measure m s` 1069 >> REVERSE CONJ_TAC >- RW_TAC std_ss [REAL_LE_REFL] 1070 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1071 >> RW_TAC std_ss [SUBSET_REFL]) 1072 >> MATCH_MP_TAC LE_INF 1073 >> CONJ_TAC 1074 >- (Q.EXISTS_TAC `measure m s` 1075 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1076 >> RW_TAC std_ss [SUBSET_REFL]) 1077 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, IN_FUNSET, IN_UNIV, 1078 IN_BIGUNION, IN_IMAGE, SUMS_EQ] 1079 >> MP_TAC (Q.SPECL [`m`] countably_additive_def) 1080 >> RW_TAC std_ss [] 1081 >> POP_ASSUM (MP_TAC o Q.SPEC `(\g. g INTER s) o f`) 1082 >> Know `BIGUNION (IMAGE ((\g. g INTER s) o f) UNIV) = s` 1083 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_INTER, o_THM] 1084 >> EQ_TAC >- PROVE_TAC [] 1085 >> RW_TAC std_ss [] 1086 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 1087 >> RW_TAC std_ss [IN_UNIV] 1088 >> Q.EXISTS_TAC `s INTER f x'` 1089 >> RW_TAC std_ss [IN_INTER] 1090 >> PROVE_TAC [EXTENSION]) 1091 >> DISCH_THEN (REWRITE_TAC o wrap) 1092 >> RW_TAC std_ss [o_THM, IN_FUNSET, IN_UNIV, IN_INTER] 1093 >> Suff `measure m o (\g. g INTER s) o f sums measure m s` 1094 >- (RW_TAC std_ss [SUMS_EQ] 1095 >> POP_ASSUM (REWRITE_TAC o wrap o GSYM) 1096 >> MATCH_MP_TAC SER_LE 1097 >> RW_TAC std_ss [o_THM] 1098 >> MATCH_MP_TAC INCREASING 1099 >> RW_TAC std_ss [ALGEBRA_INTER, INTER_SUBSET] 1100 >- (MATCH_MP_TAC ADDITIVE_INCREASING 1101 >> RW_TAC std_ss [] 1102 >> MATCH_MP_TAC COUNTABLY_ADDITIVE_ADDITIVE 1103 >> RW_TAC std_ss []) 1104 >> PROVE_TAC [ALGEBRA_INTER, subsets_def]) 1105 >> POP_ASSUM MATCH_MP_TAC 1106 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_INTER, subsets_def] 1107 >> RW_TAC std_ss [] 1108 >> Q.PAT_X_ASSUM `!m n. P m n` (MP_TAC o Q.SPECL [`m'`, `n`]) 1109 >> RW_TAC std_ss [DISJOINT_DEF, IN_INTER, NOT_IN_EMPTY, EXTENSION] 1110 >> PROVE_TAC []); 1111 1112 1113val MEASURE_DOWN = store_thm 1114 ("MEASURE_DOWN", 1115 ``!m0 m1. 1116 sigma_algebra (m_space m0,measurable_sets m0) /\ 1117 measurable_sets m0 SUBSET measurable_sets m1 /\ 1118 (measure m0 = measure m1) /\ measure_space m1 ==> 1119 measure_space m0``, 1120 RW_TAC std_ss [measure_space_def, positive_def, SUBSET_DEF, 1121 countably_additive_def, IN_FUNSET, IN_UNIV]); 1122 1123val SIGMA_ALGEBRA_SIGMA = store_thm 1124 ("SIGMA_ALGEBRA_SIGMA", 1125 ``!sp sts. subset_class sp sts ==> sigma_algebra (sigma sp sts)``, 1126 SIMP_TAC std_ss [subset_class_def] 1127 >> NTAC 3 STRIP_TAC 1128 >> RW_TAC std_ss [sigma_def, sigma_algebra_def, algebra_def, 1129 subsets_def, space_def, IN_BIGINTER, 1130 GSPECIFICATION, subset_class_def] 1131 >- (POP_ASSUM (MATCH_MP_TAC o REWRITE_RULE [IN_POW, DIFF_SUBSET, UNION_SUBSET, EMPTY_SUBSET] o 1132 Q.ISPEC `POW (sp :'a -> bool)`) 1133 >> RW_TAC std_ss [SUBSET_DEF, IN_POW, IN_BIGUNION] 1134 >> PROVE_TAC []) 1135 >> POP_ASSUM (fn th => MATCH_MP_TAC th >> ASSUME_TAC th) 1136 >> RW_TAC std_ss [SUBSET_DEF] 1137 >> Q.PAT_X_ASSUM `c SUBSET PP` MP_TAC 1138 >> CONV_TAC (LAND_CONV (SIMP_CONV (srw_ss()) [SUBSET_DEF])) 1139 >> DISCH_THEN (MP_TAC o Q.SPEC `x`) 1140 >> ASM_REWRITE_TAC [] 1141 >> DISCH_THEN MATCH_MP_TAC 1142 >> RW_TAC std_ss [] 1143 >> PROVE_TAC [SUBSET_DEF]); 1144 1145val POW_ALGEBRA = store_thm 1146 ("POW_ALGEBRA", 1147 ``algebra (sp, POW sp)``, 1148 RW_TAC std_ss [algebra_def, IN_POW, space_def, subsets_def, subset_class_def, 1149 EMPTY_SUBSET, DIFF_SUBSET, UNION_SUBSET]); 1150 1151 1152val POW_SIGMA_ALGEBRA = store_thm 1153 ("POW_SIGMA_ALGEBRA", 1154 ``sigma_algebra (sp, POW sp)``, 1155 RW_TAC std_ss [sigma_algebra_def, IN_POW, space_def, subsets_def, 1156 POW_ALGEBRA, SUBSET_DEF, IN_BIGUNION] 1157 >> PROVE_TAC []); 1158 1159 1160val UNIV_SIGMA_ALGEBRA = store_thm 1161 ("UNIV_SIGMA_ALGEBRA", 1162 ``sigma_algebra ((UNIV :'a -> bool),(UNIV :('a -> bool) -> bool))``, 1163 Know `(UNIV :('a -> bool) -> bool) = POW (UNIV :'a -> bool)` 1164 >- RW_TAC std_ss [EXTENSION, IN_POW, IN_UNIV, SUBSET_UNIV] 1165 >> RW_TAC std_ss [POW_SIGMA_ALGEBRA]); 1166 1167 1168val INF_MEASURE_EMPTY = store_thm 1169 ("INF_MEASURE_EMPTY", 1170 ``!m. algebra (m_space m, measurable_sets m) /\ positive m ==> (inf_measure m {} = 0)``, 1171 RW_TAC std_ss [] 1172 >> ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 1173 >> REVERSE CONJ_TAC >- PROVE_TAC [INF_MEASURE_POS, EMPTY_SUBSET] 1174 >> RW_TAC std_ss [inf_measure_def] 1175 >> MATCH_MP_TAC INF_LE 1176 >> CONJ_TAC >- METIS_TAC [INF_MEASURE_POS0, EMPTY_SUBSET] 1177 >> Q.EXISTS_TAC `0` 1178 >> RW_TAC std_ss [GSPECIFICATION, REAL_LE_REFL] 1179 >> Q.EXISTS_TAC `K {}` 1180 >> RW_TAC bool_ss [IN_FUNSET, IN_UNIV, ALGEBRA_EMPTY, DISJOINT_EMPTY, K_THM, 1181 SUBSET_DEF, NOT_IN_EMPTY, IN_BIGUNION, IN_IMAGE] 1182 >- PROVE_TAC [subsets_def, space_def, ALGEBRA_EMPTY] 1183 >> Know `0 = sum (0, 0) (measure m o K {})` >- RW_TAC std_ss [sum] 1184 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1185 >> MATCH_MP_TAC SER_0 1186 >> RW_TAC std_ss [K_THM, o_THM] 1187 >> PROVE_TAC [positive_def]); 1188 1189 1190val INF_MEASURE_POSITIVE = store_thm 1191 ("INF_MEASURE_POSITIVE", 1192 ``!m. 1193 algebra (m_space m, measurable_sets m) /\ positive m ==> 1194 positive (m_space m, POW (m_space m), inf_measure m)``, 1195 RW_TAC std_ss [positive_def, INF_MEASURE_EMPTY, INF_MEASURE_POS, 1196 measure_def, measurable_sets_def, IN_POW]); 1197 1198 1199val INF_MEASURE_INCREASING = store_thm 1200 ("INF_MEASURE_INCREASING", 1201 ``!m. 1202 algebra (m_space m, measurable_sets m) /\ positive m ==> 1203 increasing (m_space m, POW (m_space m), inf_measure m)``, 1204 RW_TAC std_ss [increasing_def, inf_measure_def, measurable_sets_def, IN_POW, measure_def] 1205 >> MATCH_MP_TAC LE_INF 1206 >> CONJ_TAC 1207 >- (Q.EXISTS_TAC `measure m (m_space m)` 1208 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1209 >> RW_TAC std_ss [] 1210 >> PROVE_TAC [ALGEBRA_SPACE, subsets_def, space_def, m_space_def, measurable_sets_def]) 1211 >> RW_TAC std_ss [] 1212 >> MATCH_MP_TAC INF_LE 1213 >> CONJ_TAC 1214 >- (Q.EXISTS_TAC `0` 1215 >> METIS_TAC [INF_MEASURE_POS0]) 1216 >> Q.EXISTS_TAC `x` 1217 >> POP_ASSUM MP_TAC 1218 >> RW_TAC std_ss [GSPECIFICATION, REAL_LE_REFL] 1219 >> PROVE_TAC [SUBSET_TRANS]); 1220 1221 1222val INF_MEASURE_LE = store_thm 1223 ("INF_MEASURE_LE", 1224 ``!m s x. 1225 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m /\ 1226 x IN 1227 {r | 1228 ?f. 1229 f IN (UNIV -> measurable_sets m) /\ 1230 s SUBSET BIGUNION (IMAGE f UNIV) /\ 1231 measure m o f sums r} ==> 1232 inf_measure m s <= x``, 1233 RW_TAC std_ss [GSPECIFICATION, SUMS_EQ, IN_FUNSET, IN_UNIV] 1234 >> RW_TAC std_ss [inf_measure_def] 1235 >> MATCH_MP_TAC INF_LE 1236 >> CONJ_TAC 1237 >- (Q.EXISTS_TAC `0` 1238 >> METIS_TAC [INF_MEASURE_POS0]) 1239 >> RW_TAC std_ss [GSPECIFICATION, SUMS_EQ] 1240 >> CONV_TAC (DEPTH_CONV LEFT_AND_EXISTS_CONV THENC SWAP_EXISTS_CONV) 1241 >> Q.EXISTS_TAC `\n. f n DIFF (BIGUNION (IMAGE f (count n)))` 1242 >> Q.EXISTS_TAC 1243 `suminf (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n)))))` 1244 >> REWRITE_TAC [GSYM CONJ_ASSOC, IN_FUNSET, IN_UNIV] 1245 >> BETA_TAC 1246 >> STRONG_CONJ_TAC 1247 >- (STRIP_TAC 1248 >> MATCH_MP_TAC ((REWRITE_RULE [space_def, subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_DIFF) 1249 >> RW_TAC std_ss [] 1250 >> MATCH_MP_TAC ((REWRITE_RULE [space_def, subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_FINITE_UNION) 1251 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE] 1252 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]) 1253 >> STRIP_TAC 1254 >> Know 1255 `summable (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n))))) /\ 1256 suminf (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n))))) <= 1257 suminf (measure m o f)` 1258 >- (MATCH_MP_TAC SER_POS_COMPARE 1259 >> RW_TAC std_ss [o_THM] >- PROVE_TAC [positive_def] 1260 >> MATCH_MP_TAC INCREASING 1261 >> PROVE_TAC [DIFF_SUBSET]) 1262 >> RW_TAC std_ss [] >| 1263 [RW_TAC arith_ss [DISJOINT_DEF, IN_INTER, NOT_IN_EMPTY, EXTENSION, IN_DIFF, 1264 IN_BIGUNION, IN_IMAGE, IN_COUNT] 1265 >> Know `m' < n \/ n < m'` >- DECIDE_TAC 1266 >> PROVE_TAC [], 1267 Q.PAT_X_ASSUM `s SUBSET g` MP_TAC 1268 >> RW_TAC arith_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, IN_UNIV] 1269 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 1270 >> RW_TAC std_ss [] 1271 >> Know `?n. x IN f n` >- PROVE_TAC [] 1272 >> DISCH_THEN (MP_TAC o Ho_Rewrite.REWRITE_RULE [MINIMAL_EXISTS]) 1273 >> RW_TAC std_ss [] 1274 >> Q.EXISTS_TAC 1275 `f (minimal (\n. x IN f n)) DIFF 1276 BIGUNION (IMAGE f (count (minimal (\n. x IN f n))))` 1277 >> REVERSE CONJ_TAC >- PROVE_TAC [] 1278 >> RW_TAC std_ss [IN_DIFF, IN_BIGUNION, IN_IMAGE, IN_COUNT] 1279 >> PROVE_TAC []]); 1280 1281 1282val INF_MEASURE_CLOSE = store_thm 1283 ("INF_MEASURE_CLOSE", 1284 ``!m s e. 1285 algebra (m_space m, measurable_sets m) /\ positive m /\ 0 < e /\ s SUBSET (m_space m) ==> 1286 ?f l. 1287 f IN (UNIV -> measurable_sets m) /\ s SUBSET BIGUNION (IMAGE f UNIV) /\ 1288 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1289 (measure m o f) sums l /\ l <= inf_measure m s + e``, 1290 RW_TAC std_ss [inf_measure_def] 1291 >> Suff 1292 `?l. 1293 l IN 1294 {r | 1295 ?f. 1296 f IN (UNIV -> measurable_sets m) /\ 1297 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1298 s SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r} /\ 1299 l < 1300 inf 1301 {r | 1302 ?f. 1303 f IN (UNIV -> measurable_sets m) /\ 1304 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1305 s SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r} + e` 1306 >- (RW_TAC std_ss [GSPECIFICATION] 1307 >> Q.EXISTS_TAC `f` 1308 >> Q.EXISTS_TAC `l` 1309 >> RW_TAC std_ss [] 1310 >> PROVE_TAC [REAL_LT_IMP_LE]) 1311 >> MATCH_MP_TAC INF_CLOSE 1312 >> RW_TAC std_ss [] 1313 >> Q.EXISTS_TAC `measure m (m_space m)` 1314 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1315 >> RW_TAC std_ss [] 1316 >> PROVE_TAC [ALGEBRA_SPACE, m_space_def, measurable_sets_def, subsets_def, space_def]); 1317 1318 1319val INF_MEASURE_COUNTABLY_SUBADDITIVE = store_thm 1320 ("INF_MEASURE_COUNTABLY_SUBADDITIVE", 1321 ``!m. 1322 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m ==> 1323 countably_subadditive (m_space m, POW (m_space m), inf_measure m)``, 1324 RW_TAC std_ss [countably_subadditive_def, IN_FUNSET, IN_UNIV] 1325 >> MATCH_MP_TAC REAL_LE_EPSILON 1326 >> RW_TAC std_ss [] 1327 >> MATCH_MP_TAC REAL_LE_TRANS 1328 >> Know 1329 `!n. ?g l. 1330 g IN (UNIV -> measurable_sets m) /\ 1331 f n SUBSET BIGUNION (IMAGE g UNIV) /\ 1332 (!m n. ~(m = n) ==> DISJOINT (g m) (g n)) /\ 1333 (measure m o g) sums l /\ 1334 l <= inf_measure m (f n) + e * (1 / 2) pow (n + 1)` 1335 >- (STRIP_TAC 1336 >> MATCH_MP_TAC INF_MEASURE_CLOSE 1337 >> PROVE_TAC [REAL_LT_MUL, POW_HALF_POS, measurable_sets_def, IN_POW]) 1338 >> CONV_TAC (REDEPTH_CONV (CHANGED_CONV SKOLEM_CONV)) 1339 >> RW_TAC std_ss [] 1340 >> Q.EXISTS_TAC `suminf l` 1341 >> Know `!n. 0 <= l n` 1342 >- (RW_TAC std_ss [] 1343 >> POP_ASSUM (MP_TAC o Q.SPEC `n`) 1344 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUMS_EQ] 1345 >> Q.PAT_X_ASSUM `a = b` (REWRITE_TAC o wrap o GSYM) 1346 >> MATCH_MP_TAC SUMINF_POS 1347 >> RW_TAC std_ss [o_THM] 1348 >> PROVE_TAC [positive_def]) 1349 >> STRIP_TAC 1350 >> Know 1351 `summable l /\ 1352 suminf l <= suminf (\n. inf_measure m (f n)) + e` 1353 >- (Know `(\n. e * (1 / 2) pow (n + 1)) sums (e * 1)` 1354 >- (HO_MATCH_MP_TAC SER_CMUL 1355 >> RW_TAC std_ss [POW_HALF_SER]) 1356 >> PURE_REWRITE_TAC [REAL_MUL_RID, SUMS_EQ] 1357 >> STRIP_TAC 1358 >> POP_ASSUM (ONCE_REWRITE_TAC o wrap o GSYM) 1359 >> Know 1360 `summable (\n. inf_measure m (f n) + e * (1 / 2) pow (n + 1)) /\ 1361 (suminf (\n. inf_measure m (f n)) + 1362 suminf (\n. e * (1 / 2) pow (n + 1)) = 1363 suminf (\n. inf_measure m (f n) + e * (1 / 2) pow (n + 1)))` 1364 >- (HO_MATCH_MP_TAC SUMINF_ADD 1365 >> Q.PAT_X_ASSUM `summable (a o b)` MP_TAC 1366 >> RW_TAC std_ss [o_DEF, measure_def]) 1367 >> STRIP_TAC 1368 >> POP_ASSUM (ONCE_REWRITE_TAC o wrap) 1369 >> MATCH_MP_TAC SER_POS_COMPARE 1370 >> RW_TAC std_ss []) 1371 >> RW_TAC std_ss [o_DEF, measure_def] 1372 >> MATCH_MP_TAC INF_MEASURE_LE 1373 >> RW_TAC std_ss [GSPECIFICATION] 1374 >> MP_TAC NUM_2D_BIJ_INV 1375 >> STRIP_TAC 1376 >> Q.EXISTS_TAC `UNCURRY g o f'` 1377 >> Q.PAT_X_ASSUM `!n. P n /\ Q n` MP_TAC 1378 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, SUBSET_DEF, IN_BIGUNION, 1379 IN_IMAGE] >| 1380 [Cases_on `f' x` 1381 >> RW_TAC std_ss [UNCURRY_DEF], 1382 Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `x'`) 1383 >> RW_TAC std_ss [] 1384 >> Q.PAT_X_ASSUM `!n. P n` K_TAC 1385 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 1386 >> RW_TAC std_ss [] 1387 >> Q.EXISTS_TAC `g x' x''` 1388 >> RW_TAC std_ss [] 1389 >> Q.PAT_X_ASSUM `BIJ a b c` MP_TAC 1390 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV, IN_CROSS] 1391 >> POP_ASSUM (MP_TAC o Q.SPEC `(x', x'')`) 1392 >> RW_TAC std_ss [] 1393 >> Q.EXISTS_TAC `y` 1394 >> RW_TAC std_ss [UNCURRY_DEF], 1395 Know `measure m o UNCURRY g o f' = UNCURRY (\m'. measure m o g m') o f'` 1396 >- (FUN_EQ_TAC 1397 >> RW_TAC std_ss [o_DEF] 1398 >> Cases_on `f' x` 1399 >> RW_TAC std_ss [UNCURRY_DEF]) 1400 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1401 >> MATCH_MP_TAC SUMINF_2D 1402 >> RW_TAC std_ss [o_THM] 1403 >> PROVE_TAC [positive_def]]); 1404 1405 1406val INF_MEASURE_OUTER = store_thm 1407 ("INF_MEASURE_OUTER", 1408 ``!m. 1409 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m ==> 1410 outer_measure_space (m_space m, POW(m_space m), inf_measure m)``, 1411 RW_TAC std_ss [outer_measure_space_def, INF_MEASURE_POSITIVE, 1412 INF_MEASURE_INCREASING, INF_MEASURE_COUNTABLY_SUBADDITIVE]); 1413 1414 1415val SIGMA_SUBSET = store_thm 1416 ("SIGMA_SUBSET", 1417 ``!a b. sigma_algebra b /\ a SUBSET (subsets b) ==> subsets (sigma (space b) a) SUBSET (subsets b)``, 1418 RW_TAC std_ss [sigma_def, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION, subsets_def] 1419 >> POP_ASSUM (MATCH_MP_TAC o Q.SPEC `subsets b`) 1420 >> RW_TAC std_ss [SPACE]); 1421 1422 1423val ALGEBRA_SUBSET_LAMBDA_SYSTEM = store_thm 1424 ("ALGEBRA_SUBSET_LAMBDA_SYSTEM", 1425 ``!m. 1426 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m /\ 1427 additive m ==> 1428 measurable_sets m SUBSET lambda_system (m_space m, POW (m_space m)) (inf_measure m)``, 1429 RW_TAC std_ss [SUBSET_DEF, lambda_system_def, GSPECIFICATION, 1430 IN_UNIV, GSYM REAL_LE_ANTISYM, space_def, subsets_def, IN_POW] 1431 >| [FULL_SIMP_TAC std_ss [algebra_def, subset_class_def, m_space_def, measurable_sets_def, 1432 space_def, subsets_def, SUBSET_DEF] 1433 >> PROVE_TAC [], 1434 MATCH_MP_TAC REAL_LE_EPSILON 1435 >> RW_TAC std_ss [] 1436 >> MP_TAC (Q.SPECL [`m`, `s`, `e`] INF_MEASURE_CLOSE) 1437 >> Know `s SUBSET m_space m` 1438 >- PROVE_TAC [SUBSET_DEF, algebra_def, subset_class_def, subsets_def, space_def] 1439 >> RW_TAC std_ss [SUMS_EQ, IN_FUNSET, IN_UNIV] 1440 >> MATCH_MP_TAC REAL_LE_TRANS 1441 >> Q.EXISTS_TAC `suminf (measure m o f)` 1442 >> RW_TAC std_ss [] 1443 >> POP_ASSUM K_TAC 1444 >> Know 1445 `!x. 1446 x IN measurable_sets m ==> 1447 summable (measure m o (\s. x INTER s) o f) /\ 1448 inf_measure m (x INTER s) <= suminf (measure m o (\s. x INTER s) o f)` 1449 >- (NTAC 2 STRIP_TAC 1450 >> STRONG_CONJ_TAC 1451 >- (MATCH_MP_TAC SER_COMPAR 1452 >> Q.EXISTS_TAC `measure m o f` 1453 >> RW_TAC std_ss [GREATER_EQ] 1454 >> Q.EXISTS_TAC `0` 1455 >> REVERSE (RW_TAC arith_ss [o_THM, abs]) 1456 >- PROVE_TAC [positive_def, (REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER] 1457 >> MATCH_MP_TAC INCREASING 1458 >> RW_TAC std_ss [INTER_SUBSET, (REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER]) 1459 >> RW_TAC std_ss [inf_measure_def] 1460 >> MATCH_MP_TAC INF_LE 1461 >> CONJ_TAC 1462 >- (Q.EXISTS_TAC `0` 1463 >> METIS_TAC [INF_MEASURE_POS0]) 1464 >> Q.EXISTS_TAC `suminf (measure m o (\s. x' INTER s) o f)` 1465 >> RW_TAC std_ss [REAL_LE_REFL, GSPECIFICATION] 1466 >> Q.EXISTS_TAC `(\s. x' INTER s) o f` 1467 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, 1468 (REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER, o_THM, SUMS_EQ] 1469 >- (Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPECL [`m'`, `n`]) 1470 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 1471 >> PROVE_TAC []) 1472 >> Q.PAT_X_ASSUM `s SUBSET ss` MP_TAC 1473 >> RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_INTER, IN_IMAGE, 1474 IN_UNIV, o_THM] 1475 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x''`) 1476 >> RW_TAC std_ss [] 1477 >> PROVE_TAC [IN_INTER]) 1478 >> DISCH_THEN 1479 (fn th => MP_TAC (Q.SPEC `x` th) >> MP_TAC (Q.SPEC `m_space m DIFF x` th)) 1480 >> RW_TAC std_ss [(REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_COMPL] 1481 >> MATCH_MP_TAC REAL_LE_TRANS 1482 >> Q.EXISTS_TAC 1483 `suminf (measure m o (\s. x INTER s) o f) + 1484 suminf (measure m o (\s. (m_space m DIFF x) INTER s) o f)` 1485 >> CONJ_TAC 1486 >- (Q.PAT_X_ASSUM `(a:real) <= b` MP_TAC 1487 >> Q.PAT_X_ASSUM `(a:real) <= b` MP_TAC 1488 >> REAL_ARITH_TAC) 1489 >> RW_TAC std_ss [SUMINF_ADD, o_THM] 1490 >> Know `!a b : real. (a = b) ==> a <= b` >- REAL_ARITH_TAC 1491 >> DISCH_THEN MATCH_MP_TAC 1492 >> MATCH_MP_TAC RAND_THM 1493 >> FUN_EQ_TAC 1494 >> RW_TAC std_ss [o_THM] 1495 >> MATCH_MP_TAC EQ_SYM 1496 >> MATCH_MP_TAC ADDITIVE 1497 >> RW_TAC std_ss [(REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER, 1498 (REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_COMPL, 1499 DISJOINT_DEF, IN_INTER, IN_DIFF, NOT_IN_EMPTY, EXTENSION, IN_UNION] 1500 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF, space_def, subsets_def], 1501 Know `inf_measure m = measure (m_space m, POW (m_space m), inf_measure m)` 1502 >- RW_TAC std_ss [measure_def] 1503 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1504 >> MATCH_MP_TAC SUBADDITIVE 1505 >> RW_TAC std_ss [IN_UNIV, EXTENSION, IN_INTER, IN_DIFF, IN_UNION, IN_POW, 1506 measurable_sets_def, SUBSET_DEF] 1507 >> PROVE_TAC [INF_MEASURE_COUNTABLY_SUBADDITIVE, 1508 INF_MEASURE_POSITIVE, POW_ALGEBRA, 1509 COUNTABLY_SUBADDITIVE_SUBADDITIVE, 1510 measurable_sets_def, m_space_def]]); 1511 1512 1513val CARATHEODORY = store_thm 1514 ("CARATHEODORY", 1515 ``!m0. 1516 algebra (m_space m0, measurable_sets m0) /\ positive m0 /\ countably_additive m0 ==> 1517 ?m. 1518 (!s. s IN measurable_sets m0 ==> (measure m s = measure m0 s)) /\ 1519 ((m_space m, measurable_sets m) = sigma (m_space m0) (measurable_sets m0)) /\ measure_space m``, 1520 RW_TAC std_ss [] 1521 >> Q.EXISTS_TAC `(space (sigma (m_space m0) (measurable_sets m0)), subsets (sigma (m_space m0) (measurable_sets m0)), inf_measure m0)` 1522 >> CONJ_TAC >- PROVE_TAC [INF_MEASURE_AGREES, measure_def] 1523 >> CONJ_TAC >- RW_TAC std_ss [measurable_sets_def, subsets_def, space_def, m_space_def, SPACE] 1524 >> MATCH_MP_TAC MEASURE_DOWN 1525 >> Q.EXISTS_TAC 1526 `(m_space m0, lambda_system (m_space m0, POW (m_space m0)) (inf_measure m0), inf_measure m0)` 1527 >> REWRITE_TAC [measurable_sets_def, measure_def, space_def, m_space_def, subsets_def, SPACE] 1528 >> STRONG_CONJ_TAC >- FULL_SIMP_TAC std_ss [algebra_def, SIGMA_ALGEBRA_SIGMA, space_def, subsets_def] 1529 >> STRIP_TAC 1530 >> ONCE_REWRITE_TAC [CONJ_COMM] 1531 >> STRONG_CONJ_TAC 1532 >- ((MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m0,POW (m_space m0))`) CARATHEODORY_LEMMA 1533 >> CONJ_TAC >- RW_TAC std_ss [POW_SIGMA_ALGEBRA] 1534 >> PROVE_TAC [INF_MEASURE_OUTER, COUNTABLY_ADDITIVE_ADDITIVE, 1535 ADDITIVE_INCREASING]) 1536 >> RW_TAC std_ss [] 1537 >> (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 1538 Q.SPECL [`(measurable_sets m0)`, `(m_space m0, lambda_system (m_space m0, POW (m_space m0)) (inf_measure m0))`]) SIGMA_SUBSET 1539 >> CONJ_TAC >- FULL_SIMP_TAC std_ss [measure_space_def, measurable_sets_def, m_space_def] 1540 >> PROVE_TAC [ALGEBRA_SUBSET_LAMBDA_SYSTEM, COUNTABLY_ADDITIVE_ADDITIVE, 1541 ADDITIVE_INCREASING]); 1542 1543 1544val SIGMA_SUBSET_SUBSETS = store_thm 1545 ("SIGMA_SUBSET_SUBSETS", 1546 ``!sp a. a SUBSET subsets (sigma sp a)``, 1547 RW_TAC std_ss [sigma_def, IN_BIGINTER, SUBSET_DEF, GSPECIFICATION, subsets_def]); 1548 1549 1550val IN_SIGMA = store_thm 1551 ("IN_SIGMA", 1552 ``!sp a x. x IN a ==> x IN subsets (sigma sp a)``, 1553 MP_TAC SIGMA_SUBSET_SUBSETS 1554 >> RW_TAC std_ss [SUBSET_DEF]); 1555 1556 1557val SIGMA_ALGEBRA = store_thm 1558 ("SIGMA_ALGEBRA", 1559 ``!p. 1560 sigma_algebra p = 1561 subset_class (space p) (subsets p) /\ 1562 {} IN subsets p /\ (!s. s IN subsets p ==> (space p DIFF s) IN subsets p) /\ 1563 (!c. countable c /\ c SUBSET subsets p ==> BIGUNION c IN subsets p)``, 1564 RW_TAC std_ss [sigma_algebra_def, algebra_def] 1565 >> EQ_TAC >- PROVE_TAC [] 1566 >> RW_TAC std_ss [] 1567 >> Q.PAT_X_ASSUM `!c. P c` (MP_TAC o Q.SPEC `{s; t}`) 1568 >> RW_TAC std_ss [COUNTABLE_ALT_BIJ, FINITE_INSERT, FINITE_EMPTY, SUBSET_DEF, 1569 BIGUNION_PAIR, IN_INSERT, NOT_IN_EMPTY] 1570 >> PROVE_TAC []); 1571 1572 1573val SIGMA_ALGEBRA_COUNTABLE_UNION = store_thm 1574 ("SIGMA_ALGEBRA_COUNTABLE_UNION", 1575 ``!a c. sigma_algebra a /\ countable c /\ c SUBSET subsets a ==> BIGUNION c IN subsets a``, 1576 PROVE_TAC [sigma_algebra_def]); 1577 1578 1579val SIGMA_ALGEBRA_ENUM = store_thm 1580 ("SIGMA_ALGEBRA_ENUM", 1581 ``!a (f : num -> ('a -> bool)). 1582 sigma_algebra a /\ f IN (UNIV -> subsets a) ==> BIGUNION (IMAGE f UNIV) IN subsets a``, 1583 RW_TAC std_ss [SIGMA_ALGEBRA_ALT]); 1584 1585 1586val MEASURE_COMPL = store_thm 1587 ("MEASURE_COMPL", 1588 ``!m s. 1589 measure_space m /\ s IN measurable_sets m ==> 1590 (measure m (m_space m DIFF s) = measure m (m_space m) - measure m s)``, 1591 RW_TAC std_ss [] 1592 >> Suff `measure m (m_space m) = measure m s + measure m (m_space m DIFF s)` 1593 >- REAL_ARITH_TAC 1594 >> MATCH_MP_TAC ADDITIVE 1595 >> Q.PAT_X_ASSUM `measure_space m` MP_TAC 1596 >> RW_TAC std_ss [measure_space_def, sigma_algebra_def, DISJOINT_DEF, 1597 EXTENSION, IN_DIFF, IN_UNIV, IN_UNION, IN_INTER, 1598 NOT_IN_EMPTY] 1599 >> PROVE_TAC [COUNTABLY_ADDITIVE_ADDITIVE, ALGEBRA_COMPL, subsets_def, space_def, 1600 algebra_def, subset_class_def, SUBSET_DEF]); 1601 1602 1603val SIGMA_PROPERTY = store_thm 1604 ("SIGMA_PROPERTY", 1605 ``!sp p a. 1606 subset_class sp p /\ {} IN p /\ a SUBSET p /\ (!s. s IN (p INTER subsets (sigma sp a)) ==> (sp DIFF s) IN p) /\ 1607 (!c. countable c /\ c SUBSET (p INTER subsets (sigma sp a)) ==> BIGUNION c IN p) ==> 1608 subsets (sigma sp a) SUBSET p``, 1609 RW_TAC std_ss [] 1610 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 1611 >- SIMP_TAC std_ss [SUBSET_INTER] 1612 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp,b)}` 1613 >- (KILL_TAC 1614 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def]) 1615 >> RW_TAC std_ss [GSPECIFICATION] 1616 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 1617 >> Know `subset_class sp a` >- PROVE_TAC [subset_class_def, SUBSET_DEF] 1618 >> STRIP_TAC 1619 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, SIGMA_ALGEBRA_SIGMA] 1620 >> STRIP_TAC 1621 >> RW_TAC std_ss [SIGMA_ALGEBRA, IN_INTER, space_def, subsets_def, SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY] 1622 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 1623 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 1624 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1625 FULL_SIMP_TAC std_ss [sigma_algebra_def] 1626 >> Q.PAT_X_ASSUM `!c. P c ==> BIGUNION c IN subsets (sigma sp a)` MATCH_MP_TAC 1627 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_INTER]]); 1628 1629 1630val MEASURE_EMPTY = store_thm 1631 ("MEASURE_EMPTY", 1632 ``!m. measure_space m ==> (measure m {} = 0)``, 1633 RW_TAC std_ss [measure_space_def, positive_def]); 1634 1635 1636val SIGMA_SUBSET_MEASURABLE_SETS = store_thm 1637 ("SIGMA_SUBSET_MEASURABLE_SETS", 1638 ``!a m. 1639 measure_space m /\ a SUBSET measurable_sets m ==> 1640 subsets (sigma (m_space m) a) SUBSET measurable_sets m``, 1641 RW_TAC std_ss [measure_space_def] 1642 >> MATCH_MP_TAC SIGMA_PROPERTY 1643 >> RW_TAC std_ss [IN_INTER, SUBSET_INTER] 1644 >> PROVE_TAC [SIGMA_ALGEBRA, space_def, subsets_def]); 1645 1646 1647val SIGMA_ALGEBRA_FN = store_thm 1648 ("SIGMA_ALGEBRA_FN", 1649 ``!a. 1650 sigma_algebra a = 1651 subset_class (space a) (subsets a) /\ 1652 {} IN subsets a /\ (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 1653 (!f : num -> 'a -> bool. 1654 f IN (UNIV -> subsets a) ==> BIGUNION (IMAGE f UNIV) IN subsets a)``, 1655 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_UNIV, SUBSET_DEF] 1656 >> EQ_TAC 1657 >- (RW_TAC std_ss [] 1658 >> Q.PAT_X_ASSUM `!c. P c ==> Q c` MATCH_MP_TAC 1659 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM, IN_IMAGE] 1660 >> PROVE_TAC []) 1661 >> RW_TAC std_ss [COUNTABLE_ENUM] 1662 >- RW_TAC std_ss [BIGUNION_EMPTY] 1663 >> Q.PAT_X_ASSUM `!f. (!x. P x f) ==> Q f` MATCH_MP_TAC 1664 >> POP_ASSUM MP_TAC 1665 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1666 >> PROVE_TAC []); 1667 1668 1669val SIGMA_ALGEBRA_FN_DISJOINT = store_thm 1670 ("SIGMA_ALGEBRA_FN_DISJOINT", 1671 ``!a. 1672 sigma_algebra a = 1673 subset_class (space a) (subsets a) /\ 1674 {} IN subsets a /\ (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 1675 (!s t. s IN subsets a /\ t IN subsets a ==> s UNION t IN subsets a) /\ 1676 (!f : num -> 'a -> bool. 1677 f IN (UNIV -> subsets a) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 1678 BIGUNION (IMAGE f UNIV) IN subsets a)``, 1679 RW_TAC std_ss [SIGMA_ALGEBRA_ALT_DISJOINT, algebra_def] 1680 >> EQ_TAC 1681 >> RW_TAC std_ss []); 1682 1683val SIGMA_PROPERTY_ALT = store_thm 1684 ("SIGMA_PROPERTY_ALT", 1685 ``!sp p a. 1686 subset_class sp p /\ 1687 {} IN p /\ a SUBSET p /\ (!s. s IN (p INTER subsets (sigma sp a)) ==> sp DIFF s IN p) /\ 1688 (!(f : num -> 'a -> bool). 1689 f IN (UNIV -> (p INTER subsets (sigma sp a))) ==> BIGUNION (IMAGE f UNIV) IN p) ==> 1690 subsets (sigma sp a) SUBSET p``, 1691 RW_TAC std_ss [] 1692 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 1693 >- SIMP_TAC std_ss [SUBSET_INTER] 1694 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp, b)}` 1695 >- (KILL_TAC 1696 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def]) 1697 >> RW_TAC std_ss [GSPECIFICATION] 1698 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 1699 >> POP_ASSUM MP_TAC 1700 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, 1701 SIGMA_ALGEBRA_SIGMA] 1702 >> STRIP_TAC 1703 >> RW_TAC std_ss [SIGMA_ALGEBRA_FN, IN_INTER, FUNSET_INTER, subsets_def, space_def, 1704 SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY] 1705 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 1706 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 1707 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 1708 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1709 FULL_SIMP_TAC std_ss [(Q.SPEC `(sigma sp a)`) SIGMA_ALGEBRA_FN]]); 1710 1711val SIGMA_PROPERTY_DISJOINT_WEAK = store_thm 1712 ("SIGMA_PROPERTY_DISJOINT_WEAK", 1713 ``!sp p a. 1714 subset_class sp p /\ 1715 {} IN p /\ a SUBSET p /\ (!s. s IN (p INTER subsets (sigma sp a)) ==> (sp DIFF s) IN p) /\ 1716 (!s t. s IN p /\ t IN p ==> s UNION t IN p) /\ 1717 (!f : num -> 'a -> bool. 1718 f IN (UNIV -> (p INTER subsets (sigma sp a))) /\ 1719 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 1720 BIGUNION (IMAGE f UNIV) IN p) ==> 1721 subsets (sigma sp a) SUBSET p``, 1722 RW_TAC std_ss [] 1723 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 1724 >- SIMP_TAC std_ss [SUBSET_INTER] 1725 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp, b)}` 1726 >- (KILL_TAC 1727 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def, space_def]) 1728 >> RW_TAC std_ss [GSPECIFICATION] 1729 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 1730 >> POP_ASSUM MP_TAC 1731 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, SIGMA_ALGEBRA_SIGMA] 1732 >> STRIP_TAC 1733 >> RW_TAC std_ss [SIGMA_ALGEBRA_FN_DISJOINT, IN_INTER, FUNSET_INTER, subsets_def, space_def, SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY] 1734 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 1735 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 1736 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1737 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_UNION 1738 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1739 FULL_SIMP_TAC std_ss [(Q.SPEC `(sigma sp a)`) SIGMA_ALGEBRA_FN_DISJOINT]]); 1740 1741 1742val SPACE_SMALLEST_CLOSED_CDI = store_thm 1743 ("SPACE_SMALLEST_CLOSED_CDI", 1744 ``!a. space (smallest_closed_cdi a) = space a``, 1745 RW_TAC std_ss [smallest_closed_cdi_def, space_def]); 1746 1747 1748val SMALLEST_CLOSED_CDI = store_thm 1749 ("SMALLEST_CLOSED_CDI", 1750 ``!a. algebra a ==> subsets a SUBSET subsets (smallest_closed_cdi a) /\ closed_cdi (smallest_closed_cdi a) /\ 1751 subset_class (space a) (subsets (smallest_closed_cdi a))``, 1752 Know `!a. algebra a ==> subsets a SUBSET subsets (smallest_closed_cdi a) /\ closed_cdi (smallest_closed_cdi a)` 1753 >- (RW_TAC std_ss [smallest_closed_cdi_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, 1754 subset_class_def, algebra_def, subsets_def] 1755 >> RW_TAC std_ss [closed_cdi_def, GSPECIFICATION, IN_BIGINTER, IN_FUNSET, 1756 IN_UNIV, subsets_def, space_def, subset_class_def] 1757 >> POP_ASSUM (MP_TAC o Q.SPEC `{x | x SUBSET space a}`) 1758 >> RW_TAC std_ss [GSPECIFICATION] 1759 >> POP_ASSUM MATCH_MP_TAC 1760 >> RW_TAC std_ss [SUBSET_DEF] 1761 >> PROVE_TAC [IN_DIFF, IN_BIGUNION, IN_IMAGE, IN_UNIV]) 1762 >> SIMP_TAC std_ss [] 1763 >> RW_TAC std_ss [closed_cdi_def, SPACE_SMALLEST_CLOSED_CDI]); 1764 1765 1766val CLOSED_CDI_DUNION = store_thm 1767 ("CLOSED_CDI_DUNION", 1768 ``!p s t. 1769 {} IN subsets p /\ closed_cdi p /\ s IN subsets p /\ t IN subsets p /\ DISJOINT s t ==> 1770 s UNION t IN subsets p``, 1771 RW_TAC std_ss [closed_cdi_def] 1772 >> Q.PAT_X_ASSUM `!f. P f` 1773 (MP_TAC o Q.SPEC `\n. if n = 0 then s else if n = 1 then t else {}`) 1774 >> Know 1775 `BIGUNION 1776 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 1777 UNIV) = 1778 BIGUNION 1779 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 1780 (count 2))` 1781 >- (MATCH_MP_TAC BIGUNION_IMAGE_UNIV 1782 >> RW_TAC arith_ss []) 1783 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1784 >> RW_TAC bool_ss [COUNT_SUC, IMAGE_INSERT, TWO, ONE, BIGUNION_INSERT, 1785 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] 1786 >> ONCE_REWRITE_TAC [UNION_COMM] 1787 >> POP_ASSUM MATCH_MP_TAC 1788 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, DISJOINT_EMPTY] 1789 >> PROVE_TAC [DISJOINT_SYM]); 1790 1791 1792val CLOSED_CDI_COMPL = store_thm 1793 ("CLOSED_CDI_COMPL", 1794 ``!p s. closed_cdi p /\ s IN subsets p ==> space p DIFF s IN subsets p``, 1795 RW_TAC std_ss [closed_cdi_def]); 1796 1797 1798val CLOSED_CDI_DISJOINT = store_thm 1799 ("CLOSED_CDI_DISJOINT", 1800 ``!p f. 1801 closed_cdi p /\ f IN (UNIV -> subsets p) /\ 1802 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 1803 BIGUNION (IMAGE f UNIV) IN subsets p``, 1804 RW_TAC std_ss [closed_cdi_def]); 1805 1806 1807val CLOSED_CDI_INCREASING = store_thm 1808 ("CLOSED_CDI_INCREASING", 1809 ``!p f. 1810 closed_cdi p /\ f IN (UNIV -> subsets p) /\ (f 0 = {}) /\ 1811 (!n. f n SUBSET f (SUC n)) ==> 1812 BIGUNION (IMAGE f UNIV) IN subsets p``, 1813 RW_TAC std_ss [closed_cdi_def]); 1814 1815val SIGMA_PROPERTY_DISJOINT_LEMMA1 = store_thm 1816 ("SIGMA_PROPERTY_DISJOINT_LEMMA1", 1817 ``!a. 1818 algebra a ==> 1819 (!s t. 1820 s IN subsets a /\ t IN subsets (smallest_closed_cdi a) ==> 1821 s INTER t IN subsets (smallest_closed_cdi a))``, 1822 RW_TAC std_ss [IN_BIGINTER, GSPECIFICATION, smallest_closed_cdi_def, subsets_def] 1823 >> Suff 1824 `t IN 1825 {b | b IN subsets (smallest_closed_cdi a) /\ s INTER b IN subsets (smallest_closed_cdi a)}` 1826 >- RW_TAC std_ss [GSPECIFICATION, IN_BIGINTER, smallest_closed_cdi_def, subsets_def] 1827 >> first_x_assum MATCH_MP_TAC 1828 >> STRONG_CONJ_TAC 1829 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_BIGINTER, 1830 smallest_closed_cdi_def, subsets_def] 1831 >> PROVE_TAC [ALGEBRA_INTER]) 1832 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, closed_cdi_def, space_def, subsets_def] >| 1833 [(MP_TAC o UNDISCH o Q.SPEC `a`) SMALLEST_CLOSED_CDI 1834 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, GSPECIFICATION] 1835 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF], 1836 PROVE_TAC [closed_cdi_def, SMALLEST_CLOSED_CDI, SPACE_SMALLEST_CLOSED_CDI], 1837 Know `s INTER (space a DIFF s') = 1838 space (smallest_closed_cdi a) DIFF 1839 (space (smallest_closed_cdi a) DIFF s UNION (s INTER s'))` 1840 >- (RW_TAC std_ss [EXTENSION, INTER_DEF, COMPL_DEF, UNION_DEF, GSPECIFICATION, IN_UNIV, 1841 IN_DIFF] 1842 >> PROVE_TAC [SPACE_SMALLEST_CLOSED_CDI]) 1843 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1844 >> MATCH_MP_TAC CLOSED_CDI_COMPL 1845 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1846 >> MATCH_MP_TAC CLOSED_CDI_DUNION 1847 >> CONJ_TAC 1848 >- PROVE_TAC [ALGEBRA_EMPTY, SMALLEST_CLOSED_CDI, SUBSET_DEF] 1849 >> CONJ_TAC >- RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1850 >> CONJ_TAC 1851 >- (MATCH_MP_TAC CLOSED_CDI_COMPL 1852 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI]) 1853 >> CONJ_TAC >- PROVE_TAC [SMALLEST_CLOSED_CDI, SUBSET_DEF] 1854 >> RW_TAC std_ss [DISJOINT_DEF, COMPL_DEF, INTER_DEF, IN_DIFF, IN_UNIV, GSPECIFICATION, 1855 EXTENSION, NOT_IN_EMPTY] 1856 >> DECIDE_TAC, 1857 Q.PAT_X_ASSUM `f IN x` MP_TAC 1858 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1859 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1860 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF], 1861 Know 1862 `s INTER BIGUNION (IMAGE f UNIV) = 1863 BIGUNION (IMAGE (\m. case m of 0 => {} | SUC n => s INTER f n) UNIV)` 1864 >- (KILL_TAC 1865 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1866 IN_INTER] 1867 >> (EQ_TAC >> RW_TAC std_ss [NOT_IN_EMPTY]) >| 1868 [Q.EXISTS_TAC `s INTER f x'` 1869 >> RW_TAC std_ss [IN_INTER] 1870 >> Q.EXISTS_TAC `SUC x'` 1871 >> RW_TAC arith_ss [IN_INTER, num_case_def], 1872 POP_ASSUM (MP_TAC) 1873 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1874 >> RW_TAC arith_ss [num_case_def, IN_INTER], 1875 POP_ASSUM (MP_TAC) 1876 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1877 >> RW_TAC arith_ss [num_case_def, IN_INTER] 1878 >> Q.EXISTS_TAC `f n` 1879 >> RW_TAC std_ss [] 1880 >> PROVE_TAC []]) 1881 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1882 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1883 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1884 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1885 >- (REVERSE (Cases_on `m`) >- RW_TAC arith_ss [] 1886 >> RW_TAC arith_ss [] 1887 >> PROVE_TAC [SMALLEST_CLOSED_CDI, ALGEBRA_EMPTY, SUBSET_DEF]) 1888 >> Cases_on `n` >- RW_TAC arith_ss [num_case_def, EMPTY_SUBSET] 1889 >> RW_TAC arith_ss [num_case_def, SUBSET_DEF, IN_INTER], 1890 Q.PAT_X_ASSUM `f IN x` MP_TAC 1891 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1892 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 1893 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF], 1894 Know 1895 `s INTER BIGUNION (IMAGE f UNIV) = 1896 BIGUNION (IMAGE (\n. s INTER f n) UNIV)` 1897 >- (KILL_TAC 1898 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1899 IN_INTER] 1900 >> (EQ_TAC >> RW_TAC std_ss []) >| 1901 [Q.EXISTS_TAC `s INTER f x'` 1902 >> RW_TAC std_ss [IN_INTER] 1903 >> Q.EXISTS_TAC `x'` 1904 >> RW_TAC arith_ss [IN_INTER], 1905 POP_ASSUM (MP_TAC) 1906 >> RW_TAC arith_ss [IN_INTER], 1907 POP_ASSUM (MP_TAC) 1908 >> RW_TAC arith_ss [IN_INTER] 1909 >> Q.EXISTS_TAC `f n` 1910 >> RW_TAC std_ss [] 1911 >> PROVE_TAC []]) 1912 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1913 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 1914 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1915 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1916 >> Q.PAT_X_ASSUM `!m n. PP m n` (MP_TAC o Q.SPECL [`m`, `n`]) 1917 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 1918 >> PROVE_TAC []]); 1919 1920val SIGMA_PROPERTY_DISJOINT_LEMMA2 = store_thm 1921 ("SIGMA_PROPERTY_DISJOINT_LEMMA2", 1922 ``!a. 1923 algebra a ==> 1924 (!s t. 1925 s IN subsets (smallest_closed_cdi a) /\ t IN subsets (smallest_closed_cdi a) ==> 1926 s INTER t IN subsets (smallest_closed_cdi a))``, 1927 RW_TAC std_ss [] 1928 >> POP_ASSUM MP_TAC 1929 >> SIMP_TAC std_ss [smallest_closed_cdi_def, IN_BIGINTER, GSPECIFICATION, subsets_def] 1930 >> STRIP_TAC >> Q.X_GEN_TAC `P` 1931 >> Suff 1932 `t IN 1933 {b | b IN subsets (smallest_closed_cdi a) /\ s INTER b IN subsets (smallest_closed_cdi a)}` 1934 >- RW_TAC std_ss [GSPECIFICATION, IN_BIGINTER, smallest_closed_cdi_def, subsets_def] 1935 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 1936 >> STRONG_CONJ_TAC 1937 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION] >| 1938 [PROVE_TAC [SMALLEST_CLOSED_CDI, SUBSET_DEF], 1939 PROVE_TAC [SIGMA_PROPERTY_DISJOINT_LEMMA1, INTER_COMM]]) 1940 >> SIMP_TAC std_ss [GSPECIFICATION, SUBSET_DEF, closed_cdi_def, space_def, subsets_def] 1941 >> STRIP_TAC >> REPEAT CONJ_TAC >| 1942 [(MP_TAC o UNDISCH o Q.SPEC `a`) SMALLEST_CLOSED_CDI 1943 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, GSPECIFICATION] 1944 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF], 1945 Q.X_GEN_TAC `s'` 1946 >> REPEAT STRIP_TAC 1947 >- PROVE_TAC [closed_cdi_def, SMALLEST_CLOSED_CDI, 1948 SPACE_SMALLEST_CLOSED_CDI] 1949 >> Know `s INTER (space a DIFF s') = 1950 space (smallest_closed_cdi a) DIFF 1951 (space (smallest_closed_cdi a) DIFF s UNION (s INTER s'))` 1952 >- (RW_TAC std_ss [EXTENSION, INTER_DEF, COMPL_DEF, UNION_DEF, GSPECIFICATION, IN_UNIV, 1953 IN_DIFF, SPACE_SMALLEST_CLOSED_CDI] 1954 >> DECIDE_TAC) 1955 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1956 >> MATCH_MP_TAC CLOSED_CDI_COMPL 1957 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1958 >> MATCH_MP_TAC CLOSED_CDI_DUNION 1959 >> CONJ_TAC 1960 >- PROVE_TAC [ALGEBRA_EMPTY, SMALLEST_CLOSED_CDI, SUBSET_DEF] 1961 >> CONJ_TAC >- RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1962 >> CONJ_TAC 1963 >- (MATCH_MP_TAC CLOSED_CDI_COMPL 1964 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI]) 1965 >> CONJ_TAC >- PROVE_TAC [SMALLEST_CLOSED_CDI, SUBSET_DEF] 1966 >> RW_TAC std_ss [DISJOINT_DEF, COMPL_DEF, INTER_DEF, IN_DIFF, IN_UNIV, GSPECIFICATION, 1967 EXTENSION, NOT_IN_EMPTY] 1968 >> DECIDE_TAC, 1969 Q.X_GEN_TAC `f` >> REPEAT STRIP_TAC 1970 >- (Q.PAT_X_ASSUM `f IN x` MP_TAC 1971 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1972 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1973 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF]) 1974 >> Know 1975 `s INTER BIGUNION (IMAGE f UNIV) = 1976 BIGUNION (IMAGE (\m. case m of 0 => {} | SUC n => s INTER f n) UNIV)` 1977 >- (KILL_TAC 1978 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1979 IN_INTER] 1980 >> (EQ_TAC >> RW_TAC std_ss [NOT_IN_EMPTY]) >| 1981 [Q.EXISTS_TAC `s INTER f x'` 1982 >> RW_TAC std_ss [IN_INTER] 1983 >> Q.EXISTS_TAC `SUC x'` 1984 >> RW_TAC arith_ss [IN_INTER, num_case_def], 1985 POP_ASSUM (MP_TAC) 1986 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1987 >> RW_TAC arith_ss [num_case_def, IN_INTER], 1988 POP_ASSUM (MP_TAC) 1989 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1990 >> RW_TAC arith_ss [num_case_def, IN_INTER] 1991 >> Q.EXISTS_TAC `f n` 1992 >> RW_TAC std_ss [] 1993 >> PROVE_TAC []]) 1994 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1995 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1996 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1997 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1998 >- (REVERSE (Cases_on `m`) >- RW_TAC arith_ss [] 1999 >> RW_TAC arith_ss [] 2000 >> PROVE_TAC [SMALLEST_CLOSED_CDI, ALGEBRA_EMPTY, SUBSET_DEF]) 2001 >> Cases_on `n` >- RW_TAC arith_ss [num_case_def, EMPTY_SUBSET] 2002 >> RW_TAC arith_ss [num_case_def, SUBSET_DEF, IN_INTER], 2003 Q.X_GEN_TAC `f` >> REPEAT STRIP_TAC 2004 >- (Q.PAT_X_ASSUM `f IN x` MP_TAC 2005 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 2006 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 2007 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF]) 2008 >> Know 2009 `s INTER BIGUNION (IMAGE f UNIV) = 2010 BIGUNION (IMAGE (\n. s INTER f n) UNIV)` 2011 >- (KILL_TAC 2012 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 2013 IN_INTER] 2014 >> (EQ_TAC >> RW_TAC std_ss []) >| 2015 [Q.EXISTS_TAC `s INTER f x'` 2016 >> RW_TAC std_ss [IN_INTER] 2017 >> Q.EXISTS_TAC `x'` 2018 >> RW_TAC arith_ss [IN_INTER], 2019 POP_ASSUM (MP_TAC) 2020 >> RW_TAC arith_ss [IN_INTER], 2021 POP_ASSUM (MP_TAC) 2022 >> RW_TAC arith_ss [IN_INTER] 2023 >> Q.EXISTS_TAC `f n` 2024 >> RW_TAC std_ss [] 2025 >> PROVE_TAC []]) 2026 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2027 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 2028 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 2029 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 2030 >> Q.PAT_X_ASSUM `!m n. PP m n` (MP_TAC o Q.SPECL [`m`, `n`]) 2031 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 2032 >> PROVE_TAC []]); 2033 2034val SIGMA_PROPERTY_DISJOINT_LEMMA = store_thm 2035 ("SIGMA_PROPERTY_DISJOINT_LEMMA", 2036 ``!sp a p. algebra (sp, a) /\ a SUBSET p /\ closed_cdi (sp, p) ==> subsets (sigma sp a) SUBSET p``, 2037 RW_TAC std_ss [] 2038 >> MATCH_MP_TAC SUBSET_TRANS 2039 >> Q.EXISTS_TAC `subsets (smallest_closed_cdi (sp, a))` 2040 >> REVERSE CONJ_TAC 2041 >- (RW_TAC std_ss [SUBSET_DEF, smallest_closed_cdi_def, IN_BIGINTER, 2042 GSPECIFICATION, subsets_def, space_def] 2043 >> PROVE_TAC [SUBSET_DEF]) 2044 >> NTAC 2 (POP_ASSUM K_TAC) 2045 >> Suff `subsets (smallest_closed_cdi (sp, a)) IN {b | a SUBSET b /\ sigma_algebra (sp,b)}` 2046 >- (KILL_TAC 2047 >> RW_TAC std_ss [sigma_def, BIGINTER, SUBSET_DEF, GSPECIFICATION, subsets_def]) 2048 >> RW_TAC std_ss [GSPECIFICATION, SIGMA_ALGEBRA_ALT_DISJOINT, 2049 ALGEBRA_ALT_INTER, space_def, subsets_def] >| 2050 [PROVE_TAC [SMALLEST_CLOSED_CDI, subsets_def], 2051 PROVE_TAC [SMALLEST_CLOSED_CDI, space_def], 2052 PROVE_TAC [ALGEBRA_EMPTY, SUBSET_DEF, SMALLEST_CLOSED_CDI, space_def], 2053 PROVE_TAC [SMALLEST_CLOSED_CDI, CLOSED_CDI_COMPL, space_def, SPACE_SMALLEST_CLOSED_CDI], 2054 PROVE_TAC [SIGMA_PROPERTY_DISJOINT_LEMMA2], 2055 PROVE_TAC [SMALLEST_CLOSED_CDI, CLOSED_CDI_DISJOINT]]); 2056 2057 2058val SIGMA_PROPERTY_DISJOINT_WEAK = store_thm 2059 ("SIGMA_PROPERTY_DISJOINT_WEAK", 2060 ``!sp p a. 2061 algebra (sp, a) /\ a SUBSET p /\ 2062 subset_class sp p /\ 2063 (!s. s IN p ==> sp DIFF s IN p) /\ 2064 (!f : num -> 'a -> bool. 2065 f IN (UNIV -> p) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 2066 BIGUNION (IMAGE f UNIV) IN p) /\ 2067 (!f : num -> 'a -> bool. 2068 f IN (UNIV -> p) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 2069 BIGUNION (IMAGE f UNIV) IN p) ==> 2070 subsets (sigma sp a) SUBSET p``, 2071 RW_TAC std_ss [] 2072 >> MATCH_MP_TAC (Q.SPECL [`sp`, `a`, `p`] SIGMA_PROPERTY_DISJOINT_LEMMA) 2073 >> RW_TAC std_ss [closed_cdi_def, space_def, subsets_def]); 2074 2075 2076val SIGMA_PROPERTY_DISJOINT = store_thm 2077 ("SIGMA_PROPERTY_DISJOINT", 2078 ``!sp p a. 2079 algebra (sp,a) /\ a SUBSET p /\ 2080 (!s. s IN (p INTER subsets (sigma sp a)) ==> sp DIFF s IN p) /\ 2081 (!f : num -> 'a -> bool. 2082 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ (f 0 = {}) /\ 2083 (!n. f n SUBSET f (SUC n)) ==> 2084 BIGUNION (IMAGE f UNIV) IN p) /\ 2085 (!f : num -> 'a -> bool. 2086 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ 2087 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 2088 BIGUNION (IMAGE f UNIV) IN p) ==> 2089 subsets (sigma sp a) SUBSET p``, 2090 RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_INTER] 2091 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 2092 >- (KILL_TAC 2093 >> SIMP_TAC std_ss [SUBSET_INTER]) 2094 >> MATCH_MP_TAC 2095 (Q.SPECL [`sp`, `p INTER subsets (sigma sp a)`, `a`] SIGMA_PROPERTY_DISJOINT_WEAK) 2096 >> RW_TAC std_ss [SUBSET_INTER, IN_INTER, IN_FUNSET, IN_UNIV] >| 2097 [PROVE_TAC [SUBSET_DEF, IN_SIGMA], 2098 (MP_TAC o Q.SPECL [`sp`,`a`]) SIGMA_ALGEBRA_SIGMA 2099 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2100 >> RW_TAC std_ss [algebra_def, space_def, subsets_def] 2101 >> POP_ASSUM MP_TAC 2102 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 2103 >> RW_TAC std_ss [sigma_algebra_def, algebra_def, space_def, subsets_def] 2104 >> NTAC 4 (POP_ASSUM (K ALL_TAC)) 2105 >> POP_ASSUM MP_TAC 2106 >> Know `space (sigma sp a) = sp` >- RW_TAC std_ss [sigma_def, space_def] 2107 >> RW_TAC std_ss [subset_class_def, IN_INTER], 2108 (MP_TAC o Q.SPECL [`sp`,`a`]) SIGMA_ALGEBRA_SIGMA 2109 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2110 >> RW_TAC std_ss [algebra_def, space_def, subsets_def] 2111 >> POP_ASSUM MP_TAC 2112 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 2113 >> Know `space (sigma sp a) = sp` >- RW_TAC std_ss [sigma_def, space_def] 2114 >> RW_TAC std_ss [SIGMA_ALGEBRA, algebra_def, subsets_def, space_def], 2115 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION 2116 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2117 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, COUNTABLE_IMAGE_NUM, SUBSET_DEF, 2118 IN_IMAGE, IN_UNIV, algebra_def, subsets_def, space_def] 2119 >> PROVE_TAC [], 2120 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION 2121 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2122 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, COUNTABLE_IMAGE_NUM, SUBSET_DEF, 2123 IN_IMAGE, IN_UNIV, algebra_def, subsets_def, space_def] 2124 >> PROVE_TAC []]); 2125 2126 2127val MEASURE_COUNTABLY_ADDITIVE = store_thm 2128 ("MEASURE_COUNTABLY_ADDITIVE", 2129 ``!m s f. 2130 measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 2131 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 2132 (s = BIGUNION (IMAGE f UNIV)) ==> 2133 measure m o f sums measure m s``, 2134 RW_TAC std_ss [] 2135 >> MATCH_MP_TAC COUNTABLY_ADDITIVE 2136 >> RW_TAC std_ss [] 2137 >- PROVE_TAC [measure_space_def] 2138 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 2139 Q.SPEC `(m_space m, measurable_sets m)`) SIGMA_ALGEBRA_COUNTABLE_UNION 2140 >> CONJ_TAC >- PROVE_TAC [measure_space_def] 2141 >> Q.PAT_X_ASSUM `f IN P` MP_TAC 2142 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM, SUBSET_DEF, IN_IMAGE, IN_UNIV, 2143 IN_FUNSET] 2144 >> PROVE_TAC []); 2145 2146 2147val MEASURE_SPACE_ADDITIVE = store_thm 2148 ("MEASURE_SPACE_ADDITIVE", 2149 ``!m. measure_space m ==> additive m``, 2150 RW_TAC std_ss [] 2151 >> MATCH_MP_TAC COUNTABLY_ADDITIVE_ADDITIVE 2152 >> PROVE_TAC [measure_space_def, SIGMA_ALGEBRA_ALGEBRA]); 2153 2154 2155val MEASURE_ADDITIVE = store_thm 2156 ("MEASURE_ADDITIVE", 2157 ``!m s t u. 2158 measure_space m /\ s IN measurable_sets m /\ t IN measurable_sets m /\ 2159 DISJOINT s t /\ (u = s UNION t) ==> 2160 (measure m u = measure m s + measure m t)``, 2161 RW_TAC std_ss [] 2162 >> MATCH_MP_TAC ADDITIVE 2163 >> RW_TAC std_ss [MEASURE_SPACE_ADDITIVE]); 2164 2165 2166val MEASURE_COUNTABLE_INCREASING = store_thm 2167 ("MEASURE_COUNTABLE_INCREASING", 2168 ``!m s f. 2169 measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 2170 (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) /\ 2171 (s = BIGUNION (IMAGE f UNIV)) ==> 2172 measure m o f --> measure m s``, 2173 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 2174 >> Know 2175 `measure m o f = (\n. sum (0, n) (measure m o (\m. f (SUC m) DIFF f m)))` 2176 >- (FUN_EQ_TAC 2177 >> Induct >- RW_TAC std_ss [o_THM, sum, MEASURE_EMPTY] 2178 >> POP_ASSUM (MP_TAC o SYM) 2179 >> RW_TAC arith_ss [o_THM, sum] 2180 >> MATCH_MP_TAC MEASURE_ADDITIVE 2181 >> FULL_SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_DIFF, DISJOINT_DEF, NOT_IN_EMPTY, IN_INTER, SUBSET_DEF] 2182 >> Know `algebra (m_space m, measurable_sets m)` 2183 >- FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, space_def, subsets_def] 2184 >> STRIP_TAC 2185 >> (MP_TAC o REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m, measurable_sets m)`) ALGEBRA_DIFF 2186 >> PROVE_TAC []) 2187 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2188 >> RW_TAC std_ss [GSYM sums] 2189 >> MATCH_MP_TAC COUNTABLY_ADDITIVE 2190 >> CONJ_TAC >- PROVE_TAC [measure_space_def] 2191 >> CONJ_TAC 2192 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV] 2193 >> Know `algebra (m_space m, measurable_sets m)` 2194 >- FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, space_def, subsets_def] 2195 >> STRIP_TAC 2196 >> (MP_TAC o REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m, measurable_sets m)`) ALGEBRA_DIFF 2197 >> PROVE_TAC []) 2198 >> CONJ_TAC 2199 >- (REPEAT STRIP_TAC 2200 >> MATCH_MP_TAC DISJOINT_DIFFS 2201 >> Q.EXISTS_TAC `f` 2202 >> RW_TAC std_ss []) 2203 >> CONJ_TAC 2204 >- (FULL_SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_DIFF, DISJOINT_DEF, NOT_IN_EMPTY, IN_INTER, 2205 SUBSET_DEF, IN_BIGUNION, IN_IMAGE, IN_UNIV, DIFF_DEF] 2206 >> STRIP_TAC 2207 >> REVERSE (EQ_TAC >> RW_TAC std_ss []) 2208 >- PROVE_TAC [] 2209 >> Know `x IN f x'` >- PROVE_TAC [] 2210 >> NTAC 2 (POP_ASSUM K_TAC) 2211 >> Induct_on `x'` >- RW_TAC std_ss [] 2212 >> POP_ASSUM MP_TAC 2213 >> Cases_on `x IN f x'` >- RW_TAC std_ss [] 2214 >> RW_TAC std_ss [] 2215 >> Q.EXISTS_TAC `f (SUC x') DIFF f x'` 2216 >> RW_TAC std_ss [EXTENSION, DIFF_DEF, GSPECIFICATION] 2217 >> PROVE_TAC []) 2218 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 2219 Q.SPEC `(m_space m, measurable_sets m)`) SIGMA_ALGEBRA_COUNTABLE_UNION 2220 >> CONJ_TAC >- PROVE_TAC [measure_space_def] 2221 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM] 2222 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV] 2223 >> PROVE_TAC []); 2224 2225 2226val MEASURE_SPACE_REDUCE = store_thm 2227 ("MEASURE_SPACE_REDUCE", 2228 ``!m. (m_space m, measurable_sets m, measure m) = m``, 2229 Cases 2230 >> Q.SPEC_TAC (`r`, `r`) 2231 >> Cases 2232 >> RW_TAC std_ss [m_space_def, measurable_sets_def, measure_def]); 2233 2234 2235val SPACE_SIGMA = store_thm 2236 ("SPACE_SIGMA", 2237 ``!sp a. space (sigma sp a) = sp``, 2238 RW_TAC std_ss [sigma_def, space_def]); 2239 2240val MONOTONE_CONVERGENCE = store_thm 2241 ("MONOTONE_CONVERGENCE", 2242 ``!m s f. 2243 measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 2244 (!n. f n SUBSET f (SUC n)) /\ 2245 (s = BIGUNION (IMAGE f UNIV)) ==> 2246 measure m o f --> measure m s``, 2247 RW_TAC std_ss [measure_space_def, IN_FUNSET, IN_UNIV] 2248 >> (MP_TAC o 2249 INST_TYPE [beta |-> ``:num``] o 2250 Q.SPECL [`m`, `BIGUNION (IMAGE f UNIV)`, `\x. num_CASE x {} f`]) 2251 MEASURE_COUNTABLE_INCREASING 2252 >> Cond 2253 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV, num_case_def, measure_space_def] >| 2254 [Cases_on `x` >| 2255 [RW_TAC std_ss [num_case_def] 2256 >> PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY, subsets_def], 2257 RW_TAC std_ss [num_case_def]], 2258 Cases_on `n` 2259 >> RW_TAC std_ss [num_case_def, EMPTY_SUBSET], 2260 RW_TAC std_ss [EXTENSION,GSPECIFICATION] 2261 >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV] 2262 >> EQ_TAC >| 2263 [RW_TAC std_ss [] 2264 >> Q.EXISTS_TAC `SUC x'` 2265 >> RW_TAC std_ss [num_case_def], 2266 RW_TAC std_ss [] 2267 >> POP_ASSUM MP_TAC 2268 >> Cases_on `x'` >- RW_TAC std_ss [NOT_IN_EMPTY, num_case_def] 2269 >> RW_TAC std_ss [num_case_def] 2270 >> PROVE_TAC []]]) 2271 >> RW_TAC std_ss [] 2272 >> Know `measure m o f = (\n. (measure m o (\x. num_CASE x {} f)) (SUC n))` 2273 >- (RW_TAC std_ss [FUN_EQ_THM] 2274 >> RW_TAC std_ss [num_case_def, o_THM]) 2275 >> Rewr 2276 >> Ho_Rewrite.REWRITE_TAC [GSYM SEQ_SUC] 2277 >> RW_TAC std_ss' []); 2278 2279val SIGMA_REDUCE = store_thm 2280 ("SIGMA_REDUCE", 2281 ``!sp a. (sp, subsets (sigma sp a)) = sigma sp a``, 2282 PROVE_TAC [SPACE_SIGMA, SPACE]); 2283 2284 2285val MEASURABLE_SETS_SUBSET_SPACE = store_thm 2286 ("MEASURABLE_SETS_SUBSET_SPACE", 2287 ``!m s. measure_space m /\ s IN measurable_sets m ==> 2288 s SUBSET m_space m``, 2289 RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, subsets_def, space_def, subset_class_def]); 2290 2291 2292val MEASURABLE_DIFF_PROPERTY = store_thm 2293 ("MEASURABLE_DIFF_PROPERTY", 2294 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2295 f IN (space a -> space b) /\ 2296 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2297 (!s. s IN subsets b ==> 2298 (PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s))``, 2299 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def, GSPECIFICATION, 2300 PREIMAGE_DIFF, IN_IMAGE] 2301 >> MATCH_MP_TAC SUBSET_ANTISYM 2302 >> RW_TAC std_ss [SUBSET_DEF, IN_DIFF, IN_PREIMAGE] 2303 >> Q.PAT_X_ASSUM `!s. s IN subsets b ==> PREIMAGE f s IN subsets a` (MP_TAC o Q.SPEC `space b DIFF s`) 2304 >> Know `x IN PREIMAGE f (space b DIFF s)` 2305 >- RW_TAC std_ss [IN_PREIMAGE, IN_DIFF] 2306 >> PROVE_TAC [subset_class_def, SUBSET_DEF]); 2307 2308 2309val MEASURABLE_BIGUNION_PROPERTY = store_thm 2310 ("MEASURABLE_BIGUNION_PROPERTY", 2311 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2312 f IN (space a -> space b) /\ 2313 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2314 (!c. c SUBSET subsets b ==> 2315 (PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c)))``, 2316 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def, GSPECIFICATION, 2317 PREIMAGE_BIGUNION, IN_IMAGE]); 2318 2319 2320val MEASUBABLE_BIGUNION_LEMMA = store_thm 2321 ("MEASUBABLE_BIGUNION_LEMMA", 2322 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2323 f IN (space a -> space b) /\ 2324 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2325 (!c. countable c /\ c SUBSET (IMAGE (PREIMAGE f) (subsets b)) ==> 2326 BIGUNION c IN IMAGE (PREIMAGE f) (subsets b))``, 2327 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_IMAGE] 2328 >> Q.EXISTS_TAC `BIGUNION (IMAGE (\x. @x'. x' IN subsets b /\ (PREIMAGE f x' = x)) c)` 2329 >> REVERSE CONJ_TAC 2330 >- (Q.PAT_X_ASSUM `!c. countable c /\ c SUBSET subsets b ==> BIGUNION c IN subsets b` MATCH_MP_TAC 2331 >> RW_TAC std_ss [image_countable, SUBSET_DEF, IN_IMAGE] 2332 >> Suff `(\x''. x'' IN subsets b) (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = x'))` 2333 >- RW_TAC std_ss [] 2334 >> MATCH_MP_TAC SELECT_ELIM_THM 2335 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2336 >> PROVE_TAC []) 2337 >> RW_TAC std_ss [PREIMAGE_BIGUNION, IMAGE_IMAGE] 2338 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_IMAGE] 2339 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2340 >> EQ_TAC 2341 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `s` >> ASM_REWRITE_TAC [] 2342 >> Q.PAT_X_ASSUM `!x. x IN c ==> ?x'. (x = PREIMAGE f x') /\ x' IN subsets b` (MP_TAC o Q.SPEC `s`) 2343 >> RW_TAC std_ss [] 2344 >> Q.EXISTS_TAC `PREIMAGE f x'` >> ASM_REWRITE_TAC [] 2345 >> Suff `(\x''. PREIMAGE f x' = PREIMAGE f x'') 2346 (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = PREIMAGE f x'))` 2347 >- METIS_TAC [] 2348 >> MATCH_MP_TAC SELECT_ELIM_THM 2349 >> PROVE_TAC []) 2350 >> RW_TAC std_ss [] 2351 >> Q.EXISTS_TAC `x'` 2352 >> ASM_REWRITE_TAC [] 2353 >> Know `(\x''. x IN PREIMAGE f x'' ==> x IN x') (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = x'))` 2354 >- (MATCH_MP_TAC SELECT_ELIM_THM 2355 >> RW_TAC std_ss [] 2356 >> PROVE_TAC []) 2357 >> RW_TAC std_ss []); 2358 2359 2360val MEASURABLE_SIGMA_PREIMAGES = store_thm 2361 ("MEASURABLE_SIGMA_PREIMAGES", 2362 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2363 f IN (space a -> space b) /\ 2364 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2365 sigma_algebra (space a, IMAGE (PREIMAGE f) (subsets b))``, 2366 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def] 2367 >| [FULL_SIMP_TAC std_ss [subset_class_def, GSPECIFICATION, IN_IMAGE] 2368 >> PROVE_TAC [], 2369 RW_TAC std_ss [IN_IMAGE] 2370 >> Q.EXISTS_TAC `{}` 2371 >> RW_TAC std_ss [PREIMAGE_EMPTY], 2372 RW_TAC std_ss [IN_IMAGE, PREIMAGE_DIFF] 2373 >> FULL_SIMP_TAC std_ss [IN_IMAGE] 2374 >> Q.EXISTS_TAC `space b DIFF x` 2375 >> RW_TAC std_ss [PREIMAGE_DIFF] 2376 >> MATCH_MP_TAC SUBSET_ANTISYM 2377 >> RW_TAC std_ss [SUBSET_DEF, IN_DIFF, IN_PREIMAGE] 2378 >> Q.PAT_X_ASSUM `!s. s IN subsets b ==> PREIMAGE f s IN subsets a` (MP_TAC o Q.SPEC `space b DIFF x`) 2379 >> Know `x' IN PREIMAGE f (space b DIFF x)` 2380 >- RW_TAC std_ss [IN_PREIMAGE, IN_DIFF] 2381 >> PROVE_TAC [subset_class_def, SUBSET_DEF], 2382 (MP_TAC o REWRITE_RULE [IN_FUNSET, SIGMA_ALGEBRA] o Q.SPECL [`a`, `b`, `f`]) MEASUBABLE_BIGUNION_LEMMA 2383 >> RW_TAC std_ss []]); 2384 2385 2386val IN_MEASURABLE = store_thm 2387 ("IN_MEASURABLE", 2388 ``!a b f. f IN measurable a b = 2389 sigma_algebra a /\ 2390 sigma_algebra b /\ 2391 f IN (space a -> space b) /\ 2392 (!s. s IN subsets b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a)``, 2393 RW_TAC std_ss [measurable_def, GSPECIFICATION]); 2394 2395 2396val MEASURABLE_SIGMA = store_thm 2397 ("MEASURABLE_SIGMA", 2398 ``!f a b sp. 2399 sigma_algebra a /\ 2400 subset_class sp b /\ 2401 f IN (space a -> sp) /\ 2402 (!s. s IN b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a) 2403 ==> 2404 f IN measurable a (sigma sp b)``, 2405 RW_TAC std_ss [] 2406 >> REWRITE_TAC [IN_MEASURABLE] 2407 >> CONJ_TAC >- FULL_SIMP_TAC std_ss [sigma_def, space_def] 2408 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, SPACE_SIGMA, subsets_def, GSPECIFICATION] 2409 >> Know `subsets (sigma sp b) SUBSET {x' | ((PREIMAGE f x')INTER(space a)) IN subsets a /\ x' SUBSET sp}` 2410 >- (MATCH_MP_TAC SIGMA_PROPERTY 2411 >> RW_TAC std_ss [subset_class_def, GSPECIFICATION, IN_INTER, EMPTY_SUBSET, 2412 PREIMAGE_EMPTY, PREIMAGE_DIFF, SUBSET_INTER, SIGMA_ALGEBRA, 2413 DIFF_SUBSET, SUBSET_DEF, NOT_IN_EMPTY, IN_DIFF, 2414 PREIMAGE_BIGUNION, IN_BIGUNION] 2415 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, INTER_EMPTY], 2416 PROVE_TAC [subset_class_def, SUBSET_DEF], 2417 Know `(PREIMAGE f sp DIFF PREIMAGE f s') INTER space a = 2418 (PREIMAGE f sp INTER space a) DIFF (PREIMAGE f s' INTER space a)` 2419 >- (RW_TAC std_ss [Once EXTENSION, IN_DIFF, IN_INTER, IN_PREIMAGE] >> DECIDE_TAC) 2420 >> RW_TAC std_ss [] 2421 >> Know `PREIMAGE f sp INTER space a = space a` 2422 >- (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] >> METIS_TAC [IN_FUNSET]) 2423 >> FULL_SIMP_TAC std_ss [sigma_algebra_def, ALGEBRA_COMPL], 2424 FULL_SIMP_TAC std_ss [sigma_algebra_def] 2425 >> `BIGUNION (IMAGE (PREIMAGE f) c) INTER space a = BIGUNION (IMAGE (\x. (PREIMAGE f x) INTER (space a)) c)` 2426 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE] 2427 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 2428 >> EQ_TAC 2429 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `PREIMAGE f x' INTER space a` >> ASM_REWRITE_TAC [IN_INTER] 2430 >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 2431 >> RW_TAC std_ss [] >> METIS_TAC [IN_INTER, IN_PREIMAGE]) 2432 >> RW_TAC std_ss [] 2433 >> Q.PAT_X_ASSUM `!c. countable c /\ c SUBSET subsets a ==> BIGUNION c IN subsets a` MATCH_MP_TAC 2434 >> RW_TAC std_ss [image_countable, SUBSET_DEF, IN_IMAGE] 2435 >> PROVE_TAC [], 2436 PROVE_TAC []]) 2437 >> RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION]); 2438 2439 2440val MEASURABLE_SUBSET = store_thm 2441 ("MEASURABLE_SUBSET", 2442 ``!a b. measurable a b SUBSET measurable a (sigma (space b) (subsets b))``, 2443 RW_TAC std_ss [SUBSET_DEF] 2444 >> MATCH_MP_TAC MEASURABLE_SIGMA 2445 >> FULL_SIMP_TAC std_ss [IN_MEASURABLE, SIGMA_ALGEBRA, space_def, subsets_def]); 2446 2447 2448val MEASURABLE_LIFT = store_thm 2449 ("MEASURABLE_LIFT", 2450 ``!f a b. 2451 f IN measurable a b ==> f IN measurable a (sigma (space b) (subsets b))``, 2452 PROVE_TAC [MEASURABLE_SUBSET, SUBSET_DEF]); 2453 2454 2455val IN_MEASURE_PRESERVING = store_thm 2456 ("IN_MEASURE_PRESERVING", 2457 ``!m1 m2 f. 2458 f IN measure_preserving m1 m2 = 2459 f IN measurable (m_space m1, measurable_sets m1) (m_space m2, measurable_sets m2) /\ 2460 measure_space m1 /\ measure_space m2 /\ 2461 !s. 2462 s IN measurable_sets m2 ==> 2463 (measure m1 ((PREIMAGE f s)INTER(m_space m1)) = measure m2 s)``, 2464 RW_TAC std_ss [measure_preserving_def, GSPECIFICATION]); 2465 2466 2467val MEASURE_PRESERVING_LIFT = store_thm 2468 ("MEASURE_PRESERVING_LIFT", 2469 ``!m1 m2 a f. 2470 measure_space m1 /\ measure_space m2 /\ 2471 (measurable_sets m2 = subsets (sigma (m_space m2) a)) /\ 2472 f IN measure_preserving m1 (m_space m2, a, measure m2) ==> 2473 f IN measure_preserving m1 m2``, 2474 RW_TAC std_ss [] 2475 >> REVERSE (Cases_on `algebra (m_space m2, a)`) 2476 >- FULL_SIMP_TAC std_ss [IN_MEASURE_PRESERVING, IN_MEASURABLE, m_space_def, measurable_sets_def, sigma_algebra_def] 2477 >> Suff `f IN measure_preserving m1 (m_space m2, measurable_sets m2, measure m2)` 2478 >- RW_TAC std_ss [MEASURE_SPACE_REDUCE] 2479 >> ASM_REWRITE_TAC [] 2480 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 2481 >> REWRITE_TAC [IN_MEASURE_PRESERVING, measurable_sets_def, measure_def, m_space_def] 2482 >> STRIP_TAC 2483 >> STRONG_CONJ_TAC 2484 >- (Know `(m_space m2,subsets (sigma (m_space m2) a)) = sigma (m_space m2) a` 2485 >- (Q.ABBREV_TAC `Q = (m_space m2,subsets (sigma (m_space m2) a))` 2486 >> Know `sigma (m_space m2) a = (space (sigma (m_space m2) a), subsets (sigma (m_space m2) a))` 2487 >- RW_TAC std_ss [SPACE] 2488 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2489 >> Q.UNABBREV_TAC `Q` 2490 >> RW_TAC std_ss [PAIR_EQ, sigma_def, space_def]) 2491 >> RW_TAC std_ss [] 2492 >> POP_ASSUM (K ALL_TAC) 2493 >> Know `(sigma (m_space m2) a) = sigma (space (m_space m2, a)) (subsets (m_space m2, a))` 2494 >- RW_TAC std_ss [space_def, subsets_def] 2495 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2496 >> MATCH_MP_TAC MEASURABLE_LIFT 2497 >> ASM_REWRITE_TAC []) 2498 >> Q.PAT_X_ASSUM `f IN X` K_TAC 2499 >> REWRITE_TAC [IN_MEASURABLE, space_def, subsets_def] 2500 >> STRIP_TAC 2501 >> ASM_REWRITE_TAC [] 2502 >> CONJ_TAC 2503 >- (Q.PAT_X_ASSUM `measurable_sets m2 = subsets (sigma (m_space m2) a)` (MP_TAC o GSYM) 2504 >> RW_TAC std_ss [MEASURE_SPACE_REDUCE]) 2505 >> Suff `subsets (sigma (m_space m2) a) SUBSET {s | measure m1 ((PREIMAGE f s)INTER (m_space m1)) = measure m2 s}` 2506 >- RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION] 2507 >> MATCH_MP_TAC SIGMA_PROPERTY_DISJOINT 2508 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, IN_INTER, IN_FUNSET, 2509 IN_UNIV, PREIMAGE_COMPL, PREIMAGE_BIGUNION, IMAGE_IMAGE, 2510 MEASURE_COMPL] >| 2511 [Q.PAT_X_ASSUM `measure m1 (PREIMAGE f s INTER m_space m1) = measure m2 s` (fn thm => ONCE_REWRITE_TAC [GSYM thm]) 2512 >> Know `m_space m2 IN a` >- PROVE_TAC [ALGEBRA_SPACE, subsets_def, space_def] 2513 >> STRIP_TAC 2514 >> Q.PAT_X_ASSUM `!s. s IN a ==> (measure m1 (PREIMAGE f s INTER m_space m1) = measure m2 s)` 2515 ((fn thm => ONCE_REWRITE_TAC [GSYM thm]) o UNDISCH o Q.SPEC `m_space m2`) 2516 >> Know `PREIMAGE f (m_space m2) INTER m_space m1 = m_space m1` 2517 >- (FULL_SIMP_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, IN_FUNSET] >> METIS_TAC []) 2518 >> RW_TAC std_ss [PREIMAGE_DIFF] 2519 >> `((PREIMAGE f (m_space m2) DIFF PREIMAGE f s) INTER m_space m1) = 2520 ((PREIMAGE f (m_space m2) INTER m_space m1) DIFF (PREIMAGE f s INTER m_space m1))` 2521 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_DIFF, IN_PREIMAGE] >> DECIDE_TAC) 2522 >> RW_TAC std_ss [MEASURE_COMPL], 2523 `BIGUNION (IMAGE (PREIMAGE f o f') UNIV) INTER m_space m1 = 2524 BIGUNION (IMAGE (\x:num. (PREIMAGE f o f') x INTER m_space m1) UNIV)` 2525 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] 2526 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 2527 >> EQ_TAC 2528 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `PREIMAGE f (f' x') INTER m_space m1` 2529 >> ASM_REWRITE_TAC [IN_INTER] >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 2530 >> RW_TAC std_ss [] >> METIS_TAC [IN_PREIMAGE, IN_INTER]) 2531 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2532 >> Suff 2533 `(measure m2 o f') --> measure m2 (BIGUNION (IMAGE f' UNIV)) /\ 2534 (measure m2 o f') --> 2535 measure m1 (BIGUNION (IMAGE (\x. (PREIMAGE f o f') x INTER m_space m1) UNIV))` 2536 >- PROVE_TAC [SEQ_UNIQ] 2537 >> CONJ_TAC 2538 >- (MATCH_MP_TAC MEASURE_COUNTABLE_INCREASING 2539 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF]) 2540 >> Know `measure m2 o f' = measure m1 o (\x. (PREIMAGE f o f') x INTER m_space m1)` 2541 >- (FUN_EQ_TAC 2542 >> RW_TAC std_ss [o_THM]) 2543 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2544 >> MATCH_MP_TAC MEASURE_COUNTABLE_INCREASING 2545 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, PREIMAGE_EMPTY, INTER_EMPTY] 2546 >> Suff `PREIMAGE f (f' n) SUBSET PREIMAGE f (f' (SUC n))` 2547 >- RW_TAC std_ss [SUBSET_DEF, IN_INTER] 2548 >> MATCH_MP_TAC PREIMAGE_SUBSET 2549 >> RW_TAC std_ss [SUBSET_DEF], 2550 `BIGUNION (IMAGE (PREIMAGE f o f') UNIV) INTER m_space m1 = 2551 BIGUNION (IMAGE (\x:num. (PREIMAGE f o f') x INTER m_space m1) UNIV)` 2552 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] 2553 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 2554 >> EQ_TAC 2555 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `PREIMAGE f (f' x') INTER m_space m1` 2556 >> ASM_REWRITE_TAC [IN_INTER] >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 2557 >> RW_TAC std_ss [] >> METIS_TAC [IN_PREIMAGE, IN_INTER]) 2558 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2559 >> Suff 2560 `(measure m2 o f') sums measure m2 (BIGUNION (IMAGE f' UNIV)) /\ 2561 (measure m2 o f') sums 2562 measure m1 (BIGUNION (IMAGE (\x. (PREIMAGE f o f') x INTER m_space m1) UNIV))` 2563 >- PROVE_TAC [SUM_UNIQ] 2564 >> CONJ_TAC 2565 >- (MATCH_MP_TAC MEASURE_COUNTABLY_ADDITIVE 2566 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV]) 2567 >> Know `measure m2 o f' = measure m1 o (\x. (PREIMAGE f o f') x INTER m_space m1)` 2568 >- (FUN_EQ_TAC 2569 >> RW_TAC std_ss [o_THM]) 2570 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2571 >> MATCH_MP_TAC MEASURE_COUNTABLY_ADDITIVE 2572 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, IN_DISJOINT, PREIMAGE_DISJOINT, IN_INTER] 2573 >> METIS_TAC [IN_DISJOINT, PREIMAGE_DISJOINT]]); 2574 2575 2576val MEASURE_PRESERVING_SUBSET = store_thm 2577 ("MEASURE_PRESERVING_SUBSET", 2578 ``!m1 m2 a. 2579 measure_space m1 /\ measure_space m2 /\ 2580 (measurable_sets m2 = subsets (sigma (m_space m2) a)) ==> 2581 measure_preserving m1 (m_space m2, a, measure m2) SUBSET 2582 measure_preserving m1 m2``, 2583 RW_TAC std_ss [SUBSET_DEF] 2584 >> MATCH_MP_TAC MEASURE_PRESERVING_LIFT 2585 >> PROVE_TAC []); 2586 2587 2588val MEASURABLE_I = store_thm 2589 ("MEASURABLE_I", 2590 ``!a. sigma_algebra a ==> I IN measurable a a``, 2591 RW_TAC std_ss [IN_MEASURABLE, I_THM, PREIMAGE_I, IN_FUNSET, GSPEC_ID, SPACE, SUBSET_REFL] 2592 >> Know `s INTER space a = s` 2593 >- (FULL_SIMP_TAC std_ss [Once EXTENSION, sigma_algebra_def, algebra_def, IN_INTER, subset_class_def, SUBSET_DEF] 2594 >> METIS_TAC []) 2595 >> RW_TAC std_ss []); 2596 2597 2598val MEASURABLE_COMP = store_thm 2599 ("MEASURABLE_COMP", 2600 ``!f g a b c. 2601 f IN measurable a b /\ g IN measurable b c ==> 2602 (g o f) IN measurable a c``, 2603 RW_TAC std_ss [IN_MEASURABLE, GSYM PREIMAGE_COMP, IN_FUNSET, SIGMA_ALGEBRA, space_def, subsets_def, GSPECIFICATION] 2604 >> `PREIMAGE f (PREIMAGE g s) INTER space a = 2605 PREIMAGE f (PREIMAGE g s INTER space b) INTER space a` 2606 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] >> METIS_TAC []) 2607 >> METIS_TAC []); 2608 2609 2610val MEASURABLE_COMP_STRONG = store_thm 2611 ("MEASURABLE_COMP_STRONG", 2612 ``!f g a b c. 2613 f IN measurable a b /\ 2614 sigma_algebra c /\ 2615 g IN (space b -> space c) /\ 2616 (!x. x IN (subsets c) ==> PREIMAGE g x INTER (IMAGE f (space a)) IN subsets b) ==> 2617 (g o f) IN measurable a c``, 2618 RW_TAC bool_ss [IN_MEASURABLE] 2619 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET] >> PROVE_TAC [], 2620 RW_TAC std_ss [PREIMAGE_ALT] 2621 >> ONCE_REWRITE_TAC [o_ASSOC] 2622 >> ONCE_REWRITE_TAC [GSYM PREIMAGE_ALT] 2623 >> Know `PREIMAGE f (s o g) INTER space a = PREIMAGE f (s o g INTER (IMAGE f (space a))) INTER space a` 2624 >- (RW_TAC std_ss [GSYM PREIMAGE_ALT] 2625 >> RW_TAC std_ss [Once EXTENSION, IN_PREIMAGE, IN_INTER, IN_IMAGE] 2626 >> EQ_TAC 2627 >> RW_TAC std_ss [] 2628 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE] 2629 >> Q.EXISTS_TAC `x` 2630 >> Know `g (f x) IN space c` 2631 >- (FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF] >> PROVE_TAC []) 2632 >> PROVE_TAC []) 2633 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2634 >> FULL_SIMP_TAC std_ss [PREIMAGE_ALT]]); 2635 2636 2637val MEASURABLE_COMP_STRONGER = store_thm 2638 ("MEASURABLE_COMP_STRONGER", 2639 ``!f g a b c t. 2640 f IN measurable a b /\ 2641 sigma_algebra c /\ 2642 g IN (space b -> space c) /\ 2643 (IMAGE f (space a)) SUBSET t /\ 2644 (!s. s IN subsets c ==> (PREIMAGE g s INTER t) IN subsets b) ==> 2645 (g o f) IN measurable a c``, 2646 RW_TAC bool_ss [IN_MEASURABLE] 2647 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET] >> PROVE_TAC [], 2648 RW_TAC std_ss [PREIMAGE_ALT] 2649 >> ONCE_REWRITE_TAC [o_ASSOC] 2650 >> ONCE_REWRITE_TAC [GSYM PREIMAGE_ALT] 2651 >> Know `(PREIMAGE (f:'a->'b) (((s : 'c -> bool) o (g :'b -> 'c)) INTER 2652 (t :'b -> bool)) INTER space a = PREIMAGE f (s o g) INTER space a)` 2653 >- (RW_TAC std_ss [GSYM PREIMAGE_ALT] 2654 >> RW_TAC std_ss [Once EXTENSION, IN_PREIMAGE, IN_INTER, IN_IMAGE] 2655 >> EQ_TAC 2656 >> RW_TAC std_ss [] 2657 >> Know `g (f x) IN space c` 2658 >- (FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF] >> PROVE_TAC []) 2659 >> STRIP_TAC 2660 >> Know `(f x) IN space b` 2661 >- FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE, IN_FUNSET] 2662 >> STRIP_TAC 2663 >> Know `x IN space a` 2664 >- FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE] 2665 >> STRIP_TAC 2666 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2667 >> Q.PAT_X_ASSUM `!x. (?x'. (x = f x') /\ x' IN space a) ==> x IN t` MATCH_MP_TAC 2668 >> Q.EXISTS_TAC `x` 2669 >> ASM_REWRITE_TAC []) 2670 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap o GSYM) 2671 >> RW_TAC std_ss [PREIMAGE_ALT] 2672 >> RW_TAC std_ss [GSYM PREIMAGE_ALT, GSYM PREIMAGE_COMP]]); 2673 2674 2675val MEASURABLE_UP_LIFT = store_thm 2676 ("MEASURABLE_UP_LIFT", 2677 ``!sp a b c f. f IN measurable (sp, a) c /\ 2678 sigma_algebra (sp, b) /\ a SUBSET b ==> f IN measurable (sp,b) c``, 2679 RW_TAC std_ss [IN_MEASURABLE, GSPECIFICATION, SUBSET_DEF, IN_FUNSET, space_def, subsets_def]); 2680 2681 2682val MEASURABLE_UP_SUBSET = store_thm 2683 ("MEASURABLE_UP_SUBSET", 2684 ``!sp a b c. a SUBSET b /\ sigma_algebra (sp, b) 2685 ==> measurable (sp, a) c SUBSET measurable (sp, b) c``, 2686 RW_TAC std_ss [MEASURABLE_UP_LIFT, SUBSET_DEF] 2687 >> MATCH_MP_TAC MEASURABLE_UP_LIFT 2688 >> Q.EXISTS_TAC `a` 2689 >> ASM_REWRITE_TAC [SUBSET_DEF]); 2690 2691 2692val MEASURABLE_UP_SIGMA = store_thm 2693 ("MEASURABLE_UP_SIGMA", 2694 ``!a b. measurable a b SUBSET measurable (sigma (space a) (subsets a)) b``, 2695 RW_TAC std_ss [SUBSET_DEF, IN_MEASURABLE, space_def, subsets_def, SPACE_SIGMA] 2696 >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA]) 2697 >> PROVE_TAC [SIGMA_SUBSET_SUBSETS, SUBSET_DEF]); 2698 2699val MEASURE_PRESERVING_UP_LIFT = store_thm 2700 ("MEASURE_PRESERVING_UP_LIFT", 2701 ``!m1 m2 f. 2702 measure_space m1 /\ 2703 f IN measure_preserving (m_space m1, a, measure m1) m2 /\ 2704 sigma_algebra (m_space m1, measurable_sets m1) /\ 2705 a SUBSET measurable_sets m1 ==> 2706 f IN measure_preserving m1 m2``, 2707 RW_TAC std_ss [measure_preserving_def, GSPECIFICATION, SUBSET_DEF, 2708 measure_def, measurable_sets_def, m_space_def, SPACE] 2709 >> MATCH_MP_TAC MEASURABLE_UP_LIFT 2710 >> Q.EXISTS_TAC `a` 2711 >> RW_TAC std_ss [SUBSET_DEF]); 2712 2713val MEASURE_PRESERVING_UP_SUBSET = store_thm 2714 ("MEASURE_PRESERVING_UP_SUBSET", 2715 ``!m1 m2. 2716 measure_space m1 /\ 2717 a SUBSET measurable_sets m1 /\ 2718 sigma_algebra (m_space m1, measurable_sets m1) ==> 2719 measure_preserving (m_space m1, a, measure m1) m2 SUBSET measure_preserving m1 m2``, 2720 RW_TAC std_ss [MEASURE_PRESERVING_UP_LIFT, SUBSET_DEF] 2721 >> MATCH_MP_TAC MEASURE_PRESERVING_UP_LIFT 2722 >> PROVE_TAC [SUBSET_DEF]); 2723 2724val MEASURE_PRESERVING_UP_SIGMA = store_thm 2725 ("MEASURE_PRESERVING_UP_SIGMA", 2726 ``!m1 m2 a. 2727 measure_space m1 /\ 2728 (measurable_sets m1 = subsets (sigma (m_space m1) a)) ==> 2729 measure_preserving (m_space m1, a, measure m1) m2 SUBSET measure_preserving m1 m2``, 2730 RW_TAC std_ss [MEASURE_PRESERVING_UP_LIFT, SUBSET_DEF] 2731 >> MATCH_MP_TAC MEASURE_PRESERVING_UP_LIFT 2732 >> ASM_REWRITE_TAC [SIGMA_SUBSET_SUBSETS, SIGMA_REDUCE] 2733 >> FULL_SIMP_TAC std_ss [IN_MEASURE_PRESERVING, IN_MEASURABLE, m_space_def, measurable_sets_def] 2734 >> MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA 2735 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, space_def, subsets_def]); 2736 2737 2738 2739(* ****************** *) 2740 2741 2742 2743 2744val MEASURABLE_PROD_SIGMA = store_thm 2745 ("MEASURABLE_PROD_SIGMA", 2746 ``!a a1 a2 f. 2747 sigma_algebra a /\ 2748 (FST o f) IN measurable a a1 /\ 2749 (SND o f) IN measurable a a2 ==> 2750 f IN measurable a (sigma ((space a1) CROSS (space a2)) (prod_sets (subsets a1) (subsets a2)))``, 2751 REPEAT STRIP_TAC 2752 >> MATCH_MP_TAC MEASURABLE_SIGMA 2753 >> FULL_SIMP_TAC std_ss [IN_MEASURABLE] 2754 >> CONJ_TAC 2755 >- (RW_TAC std_ss [subset_class_def, subsets_def, space_def, IN_PROD_SETS] 2756 >> PROVE_TAC [SIGMA_ALGEBRA, CROSS_SUBSET, SUBSET_DEF, subset_class_def, subsets_def, space_def]) 2757 >> CONJ_TAC 2758 >- (RW_TAC std_ss [IN_FUNSET, SPACE_SIGMA, IN_CROSS] 2759 >> FULL_SIMP_TAC std_ss [IN_FUNSET, o_DEF]) 2760 >> RW_TAC std_ss [IN_PROD_SETS] 2761 >> RW_TAC std_ss [PREIMAGE_CROSS] 2762 >> `PREIMAGE (FST o f) t INTER PREIMAGE (SND o f) u INTER space a = 2763 (PREIMAGE (FST o f) t INTER space a) INTER (PREIMAGE (SND o f) u INTER space a)` 2764 by (RW_TAC std_ss [Once EXTENSION, IN_INTER] >> DECIDE_TAC) 2765 >> PROVE_TAC [sigma_algebra_def, ALGEBRA_INTER]); 2766 2767 2768val MEASURABLE_RANGE_REDUCE = store_thm 2769 ("MEASURABLE_RANGE_REDUCE", 2770 ``!m f s. measure_space m /\ 2771 f IN measurable (m_space m, measurable_sets m) (s, POW s) /\ 2772 (~(s = {})) ==> 2773 f IN measurable (m_space m, measurable_sets m) 2774 (s INTER (IMAGE f (m_space m)), POW (s INTER (IMAGE f (m_space m))))``, 2775 RW_TAC std_ss [IN_MEASURABLE, POW_SIGMA_ALGEBRA, subsets_def, space_def, IN_FUNSET, 2776 IN_INTER, IN_IMAGE, IN_POW, SUBSET_INTER, 2777 MEASURABLE_SETS_SUBSET_SPACE, INTER_SUBSET] 2778 >> METIS_TAC []); 2779 2780val MEASURABLE_POW_TO_POW = store_thm 2781 ("MEASURABLE_POW_TO_POW", 2782 ``!m f. 2783 measure_space m /\ 2784 (measurable_sets m = POW (m_space m)) ==> 2785 f IN measurable (m_space m, measurable_sets m) (UNIV, POW(UNIV))``, 2786 RW_TAC std_ss [IN_MEASURABLE, IN_POW, IN_UNIV, POW_SIGMA_ALGEBRA, subsets_def, space_def, IN_FUNSET, 2787 PREIMAGE_UNIV, SUBSET_UNIV, measure_space_def, SUBSET_DEF, IN_INTER]); 2788 2789val MEASURABLE_POW_TO_POW_IMAGE = store_thm 2790 ("MEASURABLE_POW_TO_POW_IMAGE", 2791 ``!m f. 2792 measure_space m /\ 2793 (measurable_sets m = POW (m_space m)) ==> 2794 f IN measurable (m_space m, measurable_sets m) (IMAGE f (m_space m), POW(IMAGE f (m_space m)))``, 2795 REPEAT STRIP_TAC 2796 >> (MP_TAC o Q.SPECL [`m`,`f`,`UNIV`]) MEASURABLE_RANGE_REDUCE 2797 >> ASM_SIMP_TAC std_ss [UNIV_NEQ_EMPTY, INTER_UNIV, MEASURABLE_POW_TO_POW]); 2798 2799 2800val MEASURE_SPACE_SUBSET = store_thm 2801 ("MEASURE_SPACE_SUBSET", 2802 ``!s s' m. s' SUBSET s /\ measure_space (s,POW s, m) ==> 2803 measure_space (s',POW s', m)``, 2804 RW_TAC std_ss [measure_space_def, m_space_def, measurable_sets_def, POW_SIGMA_ALGEBRA, 2805 positive_def, measure_def, IN_POW, countably_additive_def, IN_FUNSET, IN_POW] 2806 >> METIS_TAC [SUBSET_TRANS, SUBSET_REFL]); 2807 2808 2809val STRONG_MEASURE_SPACE_SUBSET = store_thm 2810 ("STRONG_MEASURE_SPACE_SUBSET", 2811 ``!s s'. s' SUBSET m_space s /\ measure_space s /\ POW s' SUBSET measurable_sets s ==> 2812 measure_space (s',POW s', measure s)``, 2813 REPEAT STRIP_TAC >> MATCH_MP_TAC MEASURE_DOWN 2814 >> Q.EXISTS_TAC `s` 2815 >> RW_TAC std_ss [measure_def, m_space_def, measurable_sets_def, POW_SIGMA_ALGEBRA]); 2816 2817 2818val MEASURE_REAL_SUM_IMAGE = store_thm 2819 ("MEASURE_REAL_SUM_IMAGE", 2820 ``!m s. measure_space m /\ s IN measurable_sets m /\ (!x. x IN s ==> {x} IN measurable_sets m) /\ FINITE s ==> 2821 (measure m s = SIGMA (\x. measure m {x}) s)``, 2822 Suff `!s. FINITE s ==> 2823 (\s. !m. measure_space m /\ s IN measurable_sets m /\ (!x. x IN s ==> {x} IN measurable_sets m) ==> 2824 (measure m s = SIGMA (\x. measure m {x}) s)) s` 2825 >- METIS_TAC [] 2826 >> MATCH_MP_TAC FINITE_INDUCT 2827 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, MEASURE_EMPTY, DELETE_NON_ELEMENT, IN_INSERT] 2828 >> Q.PAT_X_ASSUM `!p. 2829 measure_space m /\ s IN measurable_set m /\ 2830 (!x. x IN s ==> {x} IN measurable_sets m) ==> 2831 (measure m s = SIGMA (\x. measure m {x}) s)` (MP_TAC o GSYM o Q.SPEC `m`) 2832 >> RW_TAC std_ss [] 2833 >> `s IN measurable_sets m` 2834 by (`s = (e INSERT s) DIFF {e}` 2835 by (RW_TAC std_ss [EXTENSION, IN_INSERT, IN_DIFF, IN_SING] >> METIS_TAC [GSYM DELETE_NON_ELEMENT]) 2836 >> POP_ORW 2837 >> FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def] 2838 >> METIS_TAC [space_def, subsets_def, ALGEBRA_DIFF]) 2839 >> ASM_SIMP_TAC std_ss [] 2840 >> MATCH_MP_TAC MEASURE_ADDITIVE 2841 >> RW_TAC std_ss [IN_DISJOINT, IN_SING, Once INSERT_SING_UNION] 2842 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]); 2843 2844val SIGMA_POW = store_thm 2845 ("SIGMA_POW", 2846 ``!s. sigma s (POW s) = (s,POW s)``, 2847 RW_TAC std_ss [sigma_def, PAIR_EQ, EXTENSION, IN_BIGINTER, IN_POW, GSPECIFICATION] 2848 >> EQ_TAC 2849 >- (RW_TAC std_ss [] >> POP_ASSUM (MP_TAC o Q.SPEC `POW s`) 2850 >> METIS_TAC [IN_POW, POW_SIGMA_ALGEBRA, SUBSET_REFL]) 2851 >> RW_TAC std_ss [SUBSET_DEF, IN_POW] >> METIS_TAC []); 2852 2853val finite_additivity_sufficient_for_finite_spaces = store_thm 2854 ("finite_additivity_sufficient_for_finite_spaces", 2855 ``!s m. sigma_algebra s /\ FINITE (space s) /\ 2856 positive (space s, subsets s, m) /\ 2857 additive (space s, subsets s, m) ==> 2858 measure_space (space s, subsets s, m)``, 2859 RW_TAC std_ss [countably_additive_def, additive_def, measurable_sets_def, measure_def, 2860 IN_FUNSET, IN_UNIV, measure_space_def, m_space_def, SPACE] 2861 >> `FINITE (subsets s)` 2862 by (Suff `subsets s SUBSET (POW (space s))` 2863 >- METIS_TAC [SUBSET_FINITE, FINITE_POW] 2864 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF, IN_POW] 2865 >> METIS_TAC []) 2866 >> `?N. !n. n >= N ==> (f n = {})` 2867 by METIS_TAC [finite_enumeration_of_sets_has_max_non_empty] 2868 >> FULL_SIMP_TAC std_ss [GREATER_EQ] 2869 >> `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE f (count N))` 2870 by METIS_TAC [BIGUNION_IMAGE_UNIV] 2871 >> RW_TAC std_ss [sums, SEQ] 2872 >> Q.EXISTS_TAC `N` 2873 >> RW_TAC std_ss [GREATER_EQ] 2874 >> Suff `!n. N <= n ==> (sum (0,n) (m o f) = m(BIGUNION (IMAGE f (count N))))` 2875 >- RW_TAC real_ss [LESS_EQ_REFL] 2876 >> Induct 2877 >- (RW_TAC std_ss [sum] >> `count 0 = {}` by RW_TAC real_ss [EXTENSION, IN_COUNT, NOT_IN_EMPTY] 2878 >> FULL_SIMP_TAC std_ss [IMAGE_EMPTY, BIGUNION_EMPTY, positive_def, measure_def]) 2879 >> STRIP_TAC 2880 >> Cases_on `SUC n' = N` 2881 >- (POP_ORW 2882 >> `m = measure (space s, subsets s,m)` by RW_TAC std_ss [measure_def] 2883 >> POP_ORW 2884 >> MATCH_MP_TAC ADDITIVE_SUM 2885 >> RW_TAC std_ss [m_space_def, measurable_sets_def, IN_FUNSET, IN_UNIV, additive_def, 2886 measure_def, SIGMA_ALGEBRA_ALGEBRA, SPACE]) 2887 >> `N <= n'` 2888 by (NTAC 2 (POP_ASSUM MP_TAC) >> DECIDE_TAC) 2889 >> FULL_SIMP_TAC std_ss [] 2890 >> RW_TAC std_ss [sum] 2891 >> FULL_SIMP_TAC real_ss [positive_def, measure_def]); 2892 2893 2894val finite_additivity_sufficient_for_finite_spaces2 = store_thm 2895 ("finite_additivity_sufficient_for_finite_spaces2", 2896 ``!m. sigma_algebra (m_space m, measurable_sets m) /\ FINITE (m_space m) /\ 2897 positive m /\ 2898 additive m ==> 2899 measure_space m``, 2900 REPEAT STRIP_TAC 2901 >> Suff `measure_space (space (m_space m, measurable_sets m), subsets (m_space m, measurable_sets m), measure m)` 2902 >- RW_TAC std_ss [space_def, subsets_def, MEASURE_SPACE_REDUCE] 2903 >> MATCH_MP_TAC finite_additivity_sufficient_for_finite_spaces 2904 >> RW_TAC std_ss [space_def, subsets_def, MEASURE_SPACE_REDUCE]); 2905 2906 2907val _ = export_theory (); 2908