1(* ------------------------------------------------------------------------- *) 2(* Measure Theory defined on the extended reals and includes Borel spaces *) 3(* Authors: Tarek Mhamdi, Osman Hasan, Sofiene Tahar *) 4(* HVG Group, Concordia University, Montreal *) 5(* ------------------------------------------------------------------------- *) 6(* Based on the work of Aaron Coble, Cambridge University *) 7(* ------------------------------------------------------------------------- *) 8 9(* interactive mode 10app load ["arithmeticTheory", "realTheory", "seqTheory", "pred_setTheory","res_quanTheory", 11 "res_quanTools", "listTheory", "transcTheory", "rich_listTheory", "pairTheory", 12 "combinTheory", "realLib", "optionTheory", "real_sigmaTheory", 13 "util_probTheory", "extrealTheory"]; 14quietdec := true; 15*) 16 17open HolKernel Parse boolLib bossLib arithmeticTheory realTheory 18 seqTheory pred_setTheory res_quanTheory res_quanTools listTheory transcTheory 19 rich_listTheory pairTheory combinTheory realLib optionTheory 20 real_sigmaTheory util_probTheory extrealTheory; 21 22val _ = new_theory "measure"; 23 24val REVERSE = Tactical.REVERSE; 25 26val S_TAC = rpt (POP_ASSUM MP_TAC) >> rpt RESQ_STRIP_TAC; 27val Strip = S_TAC; 28 29fun K_TAC _ = ALL_TAC; 30val KILL_TAC = POP_ASSUM_LIST K_TAC; 31val Know = Q_TAC KNOW_TAC; 32val Suff = Q_TAC SUFF_TAC; 33val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 34 35val Cond = 36 MATCH_MP_TAC (PROVE [] ``!a b c. a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 37 >> CONJ_TAC; 38 39local 40 val th = prove (``!a b. a /\ (a ==> b) ==> a /\ b``, PROVE_TAC []) 41in 42 val STRONG_CONJ_TAC :tactic = MATCH_MP_TAC th >> CONJ_TAC 43end; 44 45fun wrap a = [a]; 46val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 47val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 48val std_ss' = std_ss ++ boolSimps.ETA_ss; 49 50(* 51 interactive mode 52quietdec := false; 53*) 54 55(* ------------------------------------------------------------------------- *) 56(* Basic measure theory definitions. *) 57(* ------------------------------------------------------------------------- *) 58 59val space_def = Define 60 `space (x:'a->bool,y:('a->bool)->bool) = x`; 61 62 63val subsets_def = Define 64 `subsets (x:'a->bool,y:('a->bool)->bool) = y`; 65 66 67val subset_class_def = Define 68 `subset_class sp sts = !x. x IN sts ==> x SUBSET sp`; 69 70 71val algebra_def = Define 72 `algebra a = 73 subset_class (space a) (subsets a) /\ 74 {} IN subsets a /\ 75 (!s. s IN subsets a ==> space a DIFF s IN subsets a) /\ 76 (!s t. s IN subsets a /\ t IN subsets a ==> s UNION t IN subsets a)`; 77 78 79val sigma_algebra_def = Define 80 `sigma_algebra a = 81 algebra a /\ 82 !c. countable c /\ c SUBSET (subsets a) ==> BIGUNION c IN (subsets a)`; 83 84 85val sigma_def = Define 86 `sigma sp st = (sp, BIGINTER {s | st SUBSET s /\ sigma_algebra (sp,s)})`; 87 88 89val m_space_def = Define 90 `m_space (sp:'a->bool, sts:('a->bool)->bool, mu:('a->bool)->real) = sp`; 91 92 93val measurable_sets_def = Define 94 `measurable_sets (sp:'a->bool, sts:('a->bool)->bool, mu:('a->bool)->real) = sts`; 95 96 97val measure_def = Define 98 `measure (sp:'a->bool, sts:('a->bool)->bool, mu:('a->bool)->real) = mu`; 99 100 101val positive_def = Define 102 `positive m = 103 (measure m {} = 0) /\ !s. s IN measurable_sets m ==> 0 <= measure m s`; 104 105 106val additive_def = Define 107 `additive m = 108 !s t. s IN measurable_sets m /\ t IN measurable_sets m /\ DISJOINT s t ==> 109 (measure m (s UNION t) = measure m s + measure m t)`; 110 111 112val countably_additive_def = Define 113 `countably_additive m = 114 !f : num -> ('a -> bool). 115 f IN (UNIV -> measurable_sets m) /\ 116 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 117 BIGUNION (IMAGE f UNIV) IN measurable_sets m ==> 118 (measure m o f) sums measure m (BIGUNION (IMAGE f UNIV))`; 119 120 121val subadditive_def = Define 122 `subadditive m = 123 !s t. 124 s IN measurable_sets m /\ t IN measurable_sets m ==> 125 measure m (s UNION t) <= measure m s + measure m t`; 126 127 128val countably_subadditive_def = Define 129 `countably_subadditive m = 130 !f : num -> ('a -> bool). 131 f IN (UNIV -> measurable_sets m) /\ 132 BIGUNION (IMAGE f UNIV) IN measurable_sets m /\ 133 summable (measure m o f) ==> 134 measure m (BIGUNION (IMAGE f UNIV)) <= suminf (measure m o f)`; 135 136 137val increasing_def = Define 138 `increasing m = 139 !s t. 140 s IN measurable_sets m /\ t IN measurable_sets m /\ s SUBSET t ==> 141 measure m s <= measure m t`; 142 143 144val measure_space_def = Define 145 `measure_space m = 146 sigma_algebra (m_space m, measurable_sets m) /\ positive m /\ countably_additive m`; 147 148 149val lambda_system_def = Define 150 `lambda_system gen (lam : ('a -> bool) -> real) = 151 {l | 152 l IN (subsets gen) /\ 153 !s. s IN (subsets gen) ==> (lam (l INTER s) + lam ((space gen DIFF l) INTER s) = lam s)}`; 154 155 156val outer_measure_space_def = Define 157 `outer_measure_space m = 158 positive m /\ increasing m /\ countably_subadditive m`; 159 160 161val inf_measure_def = Define 162 `inf_measure m s = 163 inf 164 {r | 165 ?f. 166 f IN (UNIV -> measurable_sets m) /\ 167 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 168 s SUBSET BIGUNION (IMAGE f UNIV) /\ ((measure m o f) sums r)}`; 169 170 171val closed_cdi_def = Define 172 `closed_cdi p = 173 subset_class (space p) (subsets p) /\ 174 (!s. s IN (subsets p) ==> (space p DIFF s) IN (subsets p)) /\ 175 (!f : num -> 'a -> bool. 176 f IN (UNIV -> (subsets p)) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 177 BIGUNION (IMAGE f UNIV) IN (subsets p)) /\ 178 (!f : num -> 'a -> bool. 179 f IN (UNIV -> (subsets p)) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 180 BIGUNION (IMAGE f UNIV) IN (subsets p))`; 181 182 183val smallest_closed_cdi_def = Define 184 `smallest_closed_cdi a = (space a, BIGINTER {b | (subsets a) SUBSET b /\ 185 closed_cdi (space a, b)})`; 186 187 188val measurable_def = Define 189 `measurable a b = {f | sigma_algebra a /\ sigma_algebra b /\ 190 f IN (space a -> space b) /\ 191 !s. s IN subsets b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a}`; 192 193 194val measure_preserving_def = Define 195 `measure_preserving m1 m2 = 196 {f | 197 f IN measurable (m_space m1, measurable_sets m1) (m_space m2, measurable_sets m2) /\ 198 measure_space m1 /\ measure_space m2 /\ 199 !s. 200 s IN measurable_sets m2 ==> 201 (measure m1 ((PREIMAGE f s)INTER(m_space m1)) = measure m2 s)}`; 202 203val indicator_fn_def = Define 204 `indicator_fn s = \x. if x IN s then (1:extreal) else (0:extreal)`; 205 206val pos_simple_fn_def = Define 207 `pos_simple_fn m f (s:num->bool) a x = 208 (!t. 0 <= f t) /\ 209 (!t. t IN m_space m ==> (f t = SIGMA (\i. Normal (x i) * (indicator_fn (a i) t)) s)) /\ 210 (!i. i IN s ==> a i IN measurable_sets m) /\ 211 FINITE s /\ (!i. i IN s ==> 0 <= x i) /\ 212 (!i j. i IN s /\ j IN s /\ (~(i=j)) ==> DISJOINT (a i) (a j)) /\ 213 (BIGUNION (IMAGE a s) = m_space m)`; 214 215val null_set_def = Define `null_set m s = s IN measurable_sets m /\ (measure m s = 0)`; 216 217(* ------------------------------------------------------------------------- *) 218(* Basic measure theory theorems *) 219(* ------------------------------------------------------------------------- *) 220 221val SPACE = store_thm 222 ("SPACE", 223 ``!a. (space a, subsets a) = a``, 224 STRIP_TAC >> MP_TAC (Q.ISPEC `(a :('a -> bool) # (('a -> bool) -> bool))` pair_CASES) 225 >> RW_TAC std_ss [space_def, subsets_def]); 226 227val ALGEBRA_ALT_INTER = store_thm 228 ("ALGEBRA_ALT_INTER", 229 ``!a. 230 algebra a = 231 subset_class (space a) (subsets a) /\ 232 {} IN (subsets a) /\ (!s. s IN (subsets a) ==> (space a DIFF s) IN (subsets a)) /\ 233 !s t. s IN (subsets a) /\ t IN (subsets a) ==> s INTER t IN (subsets a)``, 234 RW_TAC std_ss [algebra_def, subset_class_def] 235 >> EQ_TAC >| 236 [RW_TAC std_ss [] 237 >> Know `s INTER t = space a DIFF ((space a DIFF s) UNION (space a DIFF t))` 238 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] 239 >> EQ_TAC 240 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF] >> PROVE_TAC []) 241 >> RW_TAC std_ss [] >> ASM_REWRITE_TAC []) 242 >> RW_TAC std_ss [], 243 RW_TAC std_ss [] 244 >> Know `s UNION t = space a DIFF ((space a DIFF s) INTER (space a DIFF t))` 245 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] 246 >> EQ_TAC 247 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF] >> PROVE_TAC []) 248 >> RW_TAC std_ss [] >> ASM_REWRITE_TAC []) 249 >> RW_TAC std_ss []]); 250 251 252val ALGEBRA_EMPTY = store_thm 253 ("ALGEBRA_EMPTY", 254 ``!a. algebra a ==> {} IN (subsets a)``, 255 RW_TAC std_ss [algebra_def]); 256 257 258val ALGEBRA_SPACE = store_thm 259 ("ALGEBRA_SPACE", 260 ``!a. algebra a ==> (space a) IN (subsets a)``, 261 RW_TAC std_ss [algebra_def] 262 >> PROVE_TAC [DIFF_EMPTY]); 263 264 265val ALGEBRA_COMPL = store_thm 266 ("ALGEBRA_COMPL", 267 ``!a s. algebra a /\ s IN (subsets a) ==> (space a DIFF s) IN (subsets a)``, 268 RW_TAC std_ss [algebra_def]); 269 270 271val ALGEBRA_UNION = store_thm 272 ("ALGEBRA_UNION", 273 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s UNION t IN (subsets a)``, 274 RW_TAC std_ss [algebra_def]); 275 276 277val ALGEBRA_INTER = store_thm 278 ("ALGEBRA_INTER", 279 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s INTER t IN (subsets a)``, 280 RW_TAC std_ss [ALGEBRA_ALT_INTER]); 281 282 283val ALGEBRA_DIFF = store_thm 284 ("ALGEBRA_DIFF", 285 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s DIFF t IN (subsets a)``, 286 REPEAT STRIP_TAC 287 >> Know `s DIFF t = s INTER (space a DIFF t)` 288 >- (RW_TAC std_ss [EXTENSION, IN_DIFF, IN_INTER] 289 >> FULL_SIMP_TAC std_ss [algebra_def, SUBSET_DEF, subset_class_def] 290 >> PROVE_TAC []) 291 >> RW_TAC std_ss [ALGEBRA_INTER, ALGEBRA_COMPL]); 292 293 294val ALGEBRA_FINITE_UNION = store_thm 295 ("ALGEBRA_FINITE_UNION", 296 ``!a c. algebra a /\ FINITE c /\ c SUBSET (subsets a) ==> BIGUNION c IN (subsets a)``, 297 RW_TAC std_ss [algebra_def] 298 >> NTAC 2 (POP_ASSUM MP_TAC) 299 >> Q.SPEC_TAC (`c`, `c`) 300 >> HO_MATCH_MP_TAC FINITE_INDUCT 301 >> RW_TAC std_ss [BIGUNION_EMPTY, BIGUNION_INSERT, INSERT_SUBSET]); 302 303 304val ALGEBRA_INTER_SPACE = store_thm 305 ("ALGEBRA_INTER_SPACE", 306 ``!a s. algebra a /\ s IN subsets a ==> ((space a INTER s = s) /\ (s INTER space a = s))``, 307 RW_TAC std_ss [algebra_def, SUBSET_DEF, IN_INTER, EXTENSION, subset_class_def] 308 >> PROVE_TAC []); 309 310val LAMBDA_SYSTEM_EMPTY = store_thm 311 ("LAMBDA_SYSTEM_EMPTY", 312 ``!g0 lam. algebra g0 /\ positive (space g0, subsets g0, lam) ==> {} IN lambda_system g0 lam``, 313 RW_TAC real_ss [lambda_system_def, GSPECIFICATION, positive_def, 314 INTER_EMPTY, DIFF_EMPTY, ALGEBRA_INTER_SPACE, measure_def] 315 >> FULL_SIMP_TAC std_ss [algebra_def]); 316 317 318val LAMBDA_SYSTEM_COMPL = store_thm 319 ("LAMBDA_SYSTEM_COMPL", 320 ``!g0 lam l. 321 algebra g0 /\ positive (space g0, subsets g0, lam) /\ l IN lambda_system g0 lam ==> 322 (space g0) DIFF l IN lambda_system g0 lam``, 323 RW_TAC real_ss [lambda_system_def, GSPECIFICATION, positive_def] 324 >- PROVE_TAC [algebra_def, subset_class_def] 325 >> Know `(space g0 DIFF (space g0 DIFF l)) = l` 326 >- (RW_TAC std_ss [Once EXTENSION, IN_DIFF, LEFT_AND_OVER_OR] >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF]) 327 >> RW_TAC std_ss [] 328 >> PROVE_TAC [REAL_ADD_SYM]); 329 330val LAMBDA_SYSTEM_INTER = store_thm 331 ("LAMBDA_SYSTEM_INTER", 332 ``!g0 lam l1 l2. 333 algebra g0 /\ positive (space g0, subsets g0, lam) /\ 334 l1 IN lambda_system g0 lam /\ l2 IN lambda_system g0 lam ==> 335 (l1 INTER l2) IN lambda_system g0 lam``, 336 RW_TAC real_ss [lambda_system_def, GSPECIFICATION, positive_def] 337 >- PROVE_TAC [ALGEBRA_ALT_INTER] 338 >> Know 339 `lam ((space g0 DIFF (l1 INTER l2)) INTER s) = 340 lam (l2 INTER (space g0 DIFF l1) INTER s) + lam ((space g0 DIFF l2) INTER s)` 341 >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] 342 >> Know 343 `l2 INTER (space g0 DIFF l1) INTER s = l2 INTER ((space g0 DIFF (l1 INTER l2)) INTER s)` 344 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF] 345 >> PROVE_TAC []) 346 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 347 >> Know `(space g0 DIFF l2) INTER s = (space g0 DIFF l2) INTER ((space g0 DIFF (l1 INTER l2)) INTER s)` 348 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF] 349 >> PROVE_TAC []) 350 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 351 >> Q.PAT_X_ASSUM `!g. P g` MATCH_MP_TAC 352 >> PROVE_TAC [ALGEBRA_ALT_INTER]) 353 >> Know `lam (l2 INTER s) + lam ((space g0 DIFF l2) INTER s) = lam s` 354 >- PROVE_TAC [] 355 >> Know 356 `lam (l1 INTER l2 INTER s) + lam (l2 INTER (space g0 DIFF l1) INTER s) = 357 lam (l2 INTER s)` 358 >- (Know `l2 INTER (space g0 DIFF l1) INTER s = (space g0 DIFF l1) INTER (l2 INTER s)` 359 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF] 360 >> PROVE_TAC []) 361 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 362 >> REWRITE_TAC [GSYM INTER_ASSOC] 363 >> Q.PAT_X_ASSUM `!g. P g` K_TAC 364 >> Q.PAT_X_ASSUM `!g. P g` MATCH_MP_TAC 365 >> PROVE_TAC [ALGEBRA_ALT_INTER]) 366 >> Q.SPEC_TAC (`l1 INTER l2`, `l`) 367 >> GEN_TAC 368 >> Q.SPEC_TAC (`lam (l2 INTER (space g0 DIFF l1) INTER s)`, `r1`) 369 >> Q.SPEC_TAC (`lam (l INTER s)`, `r2`) 370 >> Q.SPEC_TAC (`lam ((space g0 DIFF l2) INTER s)`, `r3`) 371 >> Q.SPEC_TAC (`lam (l2 INTER s)`, `r4`) 372 >> Q.SPEC_TAC (`lam s`, `r5`) 373 >> Q.SPEC_TAC (`lam ((space g0 DIFF l) INTER s)`, `r6`) 374 >> KILL_TAC 375 >> REAL_ARITH_TAC); 376 377val LAMBDA_SYSTEM_ALGEBRA = store_thm 378 ("LAMBDA_SYSTEM_ALGEBRA", 379 ``!g0 lam. 380 algebra g0 /\ positive (space g0, subsets g0, lam) 381 ==> algebra (space g0, lambda_system g0 lam)``, 382 RW_TAC std_ss [ALGEBRA_ALT_INTER, LAMBDA_SYSTEM_EMPTY, positive_def, 383 LAMBDA_SYSTEM_COMPL, LAMBDA_SYSTEM_INTER, space_def, 384 subsets_def, subset_class_def] 385 >> FULL_SIMP_TAC std_ss [lambda_system_def, GSPECIFICATION]); 386 387val LAMBDA_SYSTEM_STRONG_ADDITIVE = store_thm 388 ("LAMBDA_SYSTEM_STRONG_ADDITIVE", 389 ``!g0 lam g l1 l2. 390 algebra g0 /\ positive (space g0, subsets g0, lam) /\ g IN (subsets g0) /\ DISJOINT l1 l2 /\ 391 l1 IN lambda_system g0 lam /\ l2 IN lambda_system g0 lam ==> 392 (lam ((l1 UNION l2) INTER g) = lam (l1 INTER g) + lam (l2 INTER g))``, 393 RW_TAC std_ss [positive_def] 394 >> Know `l1 INTER g = l1 INTER ((l1 UNION l2) INTER g)` 395 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_UNION] 396 >> PROVE_TAC []) 397 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 398 >> Know `l2 INTER g = (space g0 DIFF l1) INTER ((l1 UNION l2) INTER g)` 399 >- (Q.PAT_X_ASSUM `DISJOINT x y` MP_TAC 400 >> RW_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, DISJOINT_DEF, 401 NOT_IN_EMPTY] 402 >> PROVE_TAC [algebra_def, SUBSET_DEF, subset_class_def]) 403 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 404 >> Know `(l1 UNION l2) INTER g IN (subsets g0)` 405 >- (Suff `l1 IN (subsets g0) /\ l2 IN (subsets g0)` 406 >- PROVE_TAC [algebra_def, SUBSET_DEF, ALGEBRA_ALT_INTER, subset_class_def] 407 >> rpt (POP_ASSUM MP_TAC) 408 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION]) 409 >> STRIP_TAC 410 >> Q.PAT_X_ASSUM `l1 IN x` MP_TAC 411 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION]); 412 413val LAMBDA_SYSTEM_ADDITIVE = store_thm 414 ("LAMBDA_SYSTEM_ADDITIVE", 415 ``!g0 lam l1 l2. 416 algebra g0 /\ positive (space g0, subsets g0, lam) ==> 417 additive (space g0, lambda_system g0 lam, lam)``, 418 RW_TAC std_ss [additive_def, measure_def, measurable_sets_def] 419 >> MP_TAC (Q.SPECL [`g0`, `lam`, `space g0`, `s`, `t`] 420 LAMBDA_SYSTEM_STRONG_ADDITIVE) 421 >> FULL_SIMP_TAC std_ss [lambda_system_def, GSPECIFICATION, ALGEBRA_INTER_SPACE, 422 ALGEBRA_SPACE, ALGEBRA_UNION]); 423 424val COUNTABLY_SUBADDITIVE_SUBADDITIVE = store_thm 425 ("COUNTABLY_SUBADDITIVE_SUBADDITIVE", 426 ``!m. 427 algebra (m_space m, measurable_sets m) /\ positive m /\ countably_subadditive m ==> 428 subadditive m``, 429 RW_TAC std_ss [countably_subadditive_def, subadditive_def] 430 >> Q.PAT_X_ASSUM `!f. P f` 431 (MP_TAC o Q.SPEC `\n : num. if n = 0 then s else if n = 1 then t else {}`) 432 >> Know 433 `BIGUNION 434 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 435 UNIV) = 436 s UNION t` 437 >- (Suff 438 `IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 439 UNIV = 440 {s; t; {}}` 441 >- (RW_TAC std_ss [BIGUNION, EXTENSION, IN_INSERT, GSPECIFICATION] 442 >> RW_TAC std_ss [GSYM EXTENSION] 443 >> RW_TAC std_ss [NOT_IN_EMPTY, IN_UNION] 444 >> PROVE_TAC [NOT_IN_EMPTY]) 445 >> RW_TAC arith_ss [EXTENSION, IN_IMAGE, IN_INSERT, IN_UNIV] 446 >> RW_TAC std_ss [GSYM EXTENSION] 447 >> RW_TAC std_ss [NOT_IN_EMPTY] 448 >> KILL_TAC 449 >> EQ_TAC >- PROVE_TAC [] 450 >> Know `~(0:num = 1) /\ ~(0:num = 2) /\ ~(1:num = 2)` >- DECIDE_TAC 451 >> PROVE_TAC []) 452 >> DISCH_THEN (REWRITE_TAC o wrap) 453 >> Know 454 `(measure m o (\n. (if n = 0 then s else (if n = 1 then t else {})))) sums 455 (measure m s + measure m t)` 456 >- (Know 457 `measure m s + measure m t = 458 sum (0,2) 459 (measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))))` 460 >- (ASM_SIMP_TAC bool_ss [TWO, sum, ONE, o_DEF] 461 >> RW_TAC arith_ss [] 462 >> RW_TAC real_ss []) 463 >> DISCH_THEN (REWRITE_TAC o wrap) 464 >> MATCH_MP_TAC SER_0 465 >> RW_TAC arith_ss [o_DEF] 466 >> PROVE_TAC [positive_def]) 467 >> REWRITE_TAC [SUMS_EQ] 468 >> DISCH_THEN (REWRITE_TAC o CONJUNCTS) 469 >> DISCH_THEN MATCH_MP_TAC 470 >> CONJ_TAC 471 >- (Q.PAT_X_ASSUM `algebra a` MP_TAC 472 >> BasicProvers.NORM_TAC std_ss [IN_FUNSET, IN_UNIV, algebra_def, subsets_def, subset_class_def]) 473 >> PROVE_TAC [algebra_def, subsets_def, subset_class_def]); 474 475 476val SIGMA_ALGEBRA_ALT = store_thm 477 ("SIGMA_ALGEBRA_ALT", 478 ``!a. 479 sigma_algebra a = 480 algebra a /\ 481 (!f : num -> 'a -> bool. 482 f IN (UNIV -> (subsets a)) ==> BIGUNION (IMAGE f UNIV) IN (subsets a))``, 483 RW_TAC std_ss [sigma_algebra_def] 484 >> EQ_TAC 485 >- (RW_TAC std_ss [COUNTABLE_ALT, IN_FUNSET, IN_UNIV] 486 >> Q.PAT_X_ASSUM `!c. P c ==> Q c` MATCH_MP_TAC 487 >> REVERSE (RW_TAC std_ss [IN_IMAGE, SUBSET_DEF, IN_UNIV]) 488 >- PROVE_TAC [] 489 >> Q.EXISTS_TAC `f` 490 >> RW_TAC std_ss [] 491 >> PROVE_TAC []) 492 >> RW_TAC std_ss [COUNTABLE_ALT_BIJ] 493 >- PROVE_TAC [ALGEBRA_FINITE_UNION] 494 >> Q.PAT_X_ASSUM `!f. P f` (MP_TAC o Q.SPEC `\n. enumerate c n`) 495 >> RW_TAC std_ss' [IN_UNIV, IN_FUNSET] 496 >> Know `BIGUNION c = BIGUNION (IMAGE (enumerate c) UNIV)` 497 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_UNIV] 498 >> Suff `!s. s IN c = ?n. (enumerate c n = s)` >- PROVE_TAC [] 499 >> Q.PAT_X_ASSUM `BIJ x y z` MP_TAC 500 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV] 501 >> PROVE_TAC []) 502 >> DISCH_THEN (REWRITE_TAC o wrap) 503 >> POP_ASSUM MATCH_MP_TAC 504 >> Strip 505 >> Suff `enumerate c n IN c` >- PROVE_TAC [SUBSET_DEF] 506 >> Q.PAT_X_ASSUM `BIJ i j k` MP_TAC 507 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV]); 508 509 510val SIGMA_ALGEBRA_ALT_MONO = store_thm 511 ("SIGMA_ALGEBRA_ALT_MONO", 512 ``!a. 513 sigma_algebra a = 514 algebra a /\ 515 (!f : num -> 'a -> bool. 516 f IN (UNIV -> (subsets a)) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 517 BIGUNION (IMAGE f UNIV) IN (subsets a))``, 518 RW_TAC std_ss [SIGMA_ALGEBRA_ALT] 519 >> EQ_TAC >- PROVE_TAC [] 520 >> RW_TAC std_ss [] 521 >> Q.PAT_X_ASSUM `!f. P f` 522 (MP_TAC o Q.SPEC `\n. BIGUNION (IMAGE f (count n))`) 523 >> RW_TAC std_ss [IN_UNIV, IN_FUNSET] 524 >> Know 525 `BIGUNION (IMAGE f UNIV) = 526 BIGUNION (IMAGE (\n. BIGUNION (IMAGE f (count n))) UNIV)` 527 >- (KILL_TAC 528 >> ONCE_REWRITE_TAC [EXTENSION] 529 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV] 530 >> EQ_TAC 531 >- (RW_TAC std_ss [] 532 >> Q.EXISTS_TAC `BIGUNION (IMAGE f (count (SUC x')))` 533 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 534 >> PROVE_TAC [prim_recTheory.LESS_SUC_REFL]) 535 >> RW_TAC std_ss [] 536 >> POP_ASSUM MP_TAC 537 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 538 >> PROVE_TAC []) 539 >> DISCH_THEN (REWRITE_TAC o wrap) 540 >> POP_ASSUM MATCH_MP_TAC 541 >> REVERSE (RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_COUNT, IN_IMAGE, 542 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY]) 543 >- (Q.EXISTS_TAC `f x'` 544 >> RW_TAC std_ss [] 545 >> Q.EXISTS_TAC `x'` 546 >> DECIDE_TAC) 547 >> MATCH_MP_TAC ALGEBRA_FINITE_UNION 548 >> POP_ASSUM MP_TAC 549 >> REVERSE (RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF, IN_IMAGE]) 550 >- PROVE_TAC [] 551 >> MATCH_MP_TAC IMAGE_FINITE 552 >> RW_TAC std_ss [FINITE_COUNT]); 553 554 555val SIGMA_ALGEBRA_ALT_DISJOINT = store_thm 556 ("SIGMA_ALGEBRA_ALT_DISJOINT", 557 ``!a. 558 sigma_algebra a = 559 algebra a /\ 560 (!f. 561 f IN (UNIV -> (subsets a)) /\ 562 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 563 BIGUNION (IMAGE f UNIV) IN (subsets a))``, 564 Strip 565 >> EQ_TAC >- RW_TAC std_ss [SIGMA_ALGEBRA_ALT] 566 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALT_MONO, IN_FUNSET, IN_UNIV] 567 >> Q.PAT_X_ASSUM `!f. P f ==> Q f` (MP_TAC o Q.SPEC `\n. f (SUC n) DIFF f n`) 568 >> RW_TAC std_ss [] 569 >> Know 570 `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE (\n. f (SUC n) DIFF f n) UNIV)` 571 >- (POP_ASSUM K_TAC 572 >> ONCE_REWRITE_TAC [EXTENSION] 573 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_DIFF] 574 >> REVERSE EQ_TAC 575 >- (RW_TAC std_ss [] 576 >> POP_ASSUM MP_TAC 577 >> RW_TAC std_ss [IN_DIFF] 578 >> PROVE_TAC []) 579 >> RW_TAC std_ss [] 580 >> Induct_on `x'` >- RW_TAC std_ss [NOT_IN_EMPTY] 581 >> RW_TAC std_ss [] 582 >> Cases_on `x IN f x'` >- PROVE_TAC [] 583 >> Q.EXISTS_TAC `f (SUC x') DIFF f x'` 584 >> RW_TAC std_ss [EXTENSION, IN_DIFF] 585 >> PROVE_TAC []) 586 >> DISCH_THEN (REWRITE_TAC o wrap) 587 >> POP_ASSUM MATCH_MP_TAC 588 >> CONJ_TAC >- RW_TAC std_ss [ALGEBRA_DIFF] 589 >> HO_MATCH_MP_TAC TRANSFORM_2D_NUM 590 >> CONJ_TAC >- PROVE_TAC [DISJOINT_SYM] 591 >> RW_TAC arith_ss [] 592 >> Suff `f (SUC m) SUBSET f (m + n)` 593 >- (RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, 594 IN_INTER, IN_DIFF, SUBSET_DEF] 595 >> PROVE_TAC []) 596 >> Cases_on `n` >- PROVE_TAC [ADD_CLAUSES] 597 >> POP_ASSUM K_TAC 598 >> Know `m + SUC n' = SUC m + n'` >- DECIDE_TAC 599 >> DISCH_THEN (REWRITE_TAC o wrap) 600 >> Induct_on `n'` >- RW_TAC arith_ss [SUBSET_REFL] 601 >> MATCH_MP_TAC SUBSET_TRANS 602 >> Q.EXISTS_TAC `f (SUC m + n')` 603 >> PROVE_TAC [ADD_CLAUSES]); 604 605 606val SUBADDITIVE = store_thm 607 ("SUBADDITIVE", 608 ``!m s t u. 609 subadditive m /\ s IN measurable_sets m /\ t IN measurable_sets m /\ 610 (u = s UNION t) ==> 611 measure m u <= measure m s + measure m t``, 612 RW_TAC std_ss [subadditive_def]); 613 614 615val ADDITIVE = store_thm 616 ("ADDITIVE", 617 ``!m s t u. 618 additive m /\ s IN measurable_sets m /\ t IN measurable_sets m /\ 619 DISJOINT s t /\ (u = s UNION t) ==> 620 (measure m u = measure m s + measure m t)``, 621 RW_TAC std_ss [additive_def]); 622 623 624val COUNTABLY_SUBADDITIVE = store_thm 625 ("COUNTABLY_SUBADDITIVE", 626 ``!m f s. 627 countably_subadditive m /\ f IN (UNIV -> measurable_sets m) /\ 628 summable (measure m o f) /\ (s = BIGUNION (IMAGE f UNIV)) /\ 629 (s IN measurable_sets m) ==> 630 measure m s <= suminf (measure m o f)``, 631 PROVE_TAC [countably_subadditive_def]); 632 633 634val ADDITIVE_SUM = store_thm 635 ("ADDITIVE_SUM", 636 ``!m f n. 637 algebra (m_space m, measurable_sets m) /\ positive m /\ additive m /\ 638 f IN (UNIV -> measurable_sets m) /\ 639 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 640 (sum (0, n) (measure m o f) = 641 measure m (BIGUNION (IMAGE f (count n))))``, 642 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 643 >> Induct_on `n` 644 >- (RW_TAC std_ss [sum, COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY] 645 >> PROVE_TAC [positive_def]) 646 >> RW_TAC std_ss [sum, COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT, ADD_CLAUSES, 647 o_DEF] 648 >> MATCH_MP_TAC EQ_SYM 649 >> ONCE_REWRITE_TAC [REAL_ADD_SYM] 650 >> MATCH_MP_TAC ADDITIVE 651 >> RW_TAC std_ss [DISJOINT_COUNT] 652 >> MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_FINITE_UNION) 653 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] 654 >> PROVE_TAC [FINITE_COUNT, IMAGE_FINITE]); 655 656val INCREASING_ADDITIVE_SUMMABLE = store_thm 657 ("INCREASING_ADDITIVE_SUMMABLE", 658 ``!m f. 659 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m /\ 660 additive m /\ f IN (UNIV -> measurable_sets m) /\ 661 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 662 summable (measure m o f)``, 663 RW_TAC std_ss [increasing_def] 664 >> MATCH_MP_TAC POS_SUMMABLE 665 >> CONJ_TAC 666 >- FULL_SIMP_TAC std_ss [o_DEF, IN_FUNSET, IN_UNIV, positive_def] 667 >> Q.EXISTS_TAC `measure m (m_space m)` 668 >> RW_TAC std_ss [] 669 >> MP_TAC (Q.SPECL [`m`, `f`, `n`] ADDITIVE_SUM) 670 >> ASM_REWRITE_TAC [] 671 >> DISCH_THEN (REWRITE_TAC o wrap) 672 >> Q.PAT_X_ASSUM `!(s : 'a -> bool). P s` MATCH_MP_TAC 673 >> CONJ_TAC 674 >- (MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_FINITE_UNION) 675 >> Q.PAT_X_ASSUM `f IN x` MP_TAC 676 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF, IN_IMAGE] 677 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]) 678 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_SPACE, space_def, subsets_def] 679 >> Q.PAT_X_ASSUM `f IN x` MP_TAC 680 >> Q.PAT_X_ASSUM `algebra a` MP_TAC 681 >> RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, IN_COUNT, 682 IN_FUNSET, IN_UNIV, algebra_def, space_def, subsets_def, subset_class_def] 683 >> PROVE_TAC []); 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 691val LAMBDA_SYSTEM_INCREASING = store_thm 692 ("LAMBDA_SYSTEM_INCREASING", 693 ``!g0 lam. increasing (space g0, subsets g0, lam) ==> increasing (space g0, lambda_system g0 lam, lam)``, 694 RW_TAC std_ss [increasing_def, lambda_system_def, GSPECIFICATION, 695 measure_def, measurable_sets_def]); 696 697val LAMBDA_SYSTEM_STRONG_SUM = store_thm 698 ("LAMBDA_SYSTEM_STRONG_SUM", 699 ``!g0 lam g f n. 700 algebra g0 /\ positive (space g0, subsets g0, lam) /\ g IN (subsets g0) /\ 701 f IN (UNIV -> lambda_system g0 lam) /\ 702 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 703 (sum (0, n) (lam o (\s. s INTER g) o f) = 704 lam (BIGUNION (IMAGE f (count n)) INTER g))``, 705 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 706 >> Induct_on `n` 707 >- (RW_TAC std_ss [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, sum, INTER_EMPTY] 708 >> PROVE_TAC [positive_def, measure_def]) 709 >> RW_TAC arith_ss [COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT, sum, o_DEF] 710 >> ONCE_REWRITE_TAC [REAL_ADD_SYM] 711 >> MATCH_MP_TAC EQ_SYM 712 >> MATCH_MP_TAC LAMBDA_SYSTEM_STRONG_ADDITIVE 713 >> Q.EXISTS_TAC `g0` 714 >> RW_TAC std_ss [DISJOINT_COUNT] 715 >> MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(space g0,lambda_system g0 lam)`) ALGEBRA_FINITE_UNION) 716 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, LAMBDA_SYSTEM_ALGEBRA] 717 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]); 718 719val SIGMA_ALGEBRA_ALGEBRA = store_thm 720 ("SIGMA_ALGEBRA_ALGEBRA", 721 ``!a. sigma_algebra a ==> algebra a``, 722 PROVE_TAC [sigma_algebra_def]); 723 724val OUTER_MEASURE_SPACE_POSITIVE = store_thm 725 ("OUTER_MEASURE_SPACE_POSITIVE", 726 ``!m. outer_measure_space m ==> positive m``, 727 PROVE_TAC [outer_measure_space_def]); 728 729val LAMBDA_SYSTEM_CARATHEODORY = store_thm 730 ("LAMBDA_SYSTEM_CARATHEODORY", 731 ``!gsig lam. 732 sigma_algebra gsig /\ outer_measure_space (space gsig, subsets gsig, lam) ==> 733 (!f. 734 f IN (UNIV -> lambda_system gsig lam) /\ 735 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 736 BIGUNION (IMAGE f UNIV) IN lambda_system gsig lam /\ 737 ((lam o f) sums lam (BIGUNION (IMAGE f UNIV))))``, 738 NTAC 5 STRIP_TAC 739 >> Know `summable (lam o f)` 740 >- (Suff `summable (measure (space gsig, lambda_system gsig lam, lam) o f)` 741 >- RW_TAC std_ss [measure_def] 742 >> MATCH_MP_TAC INCREASING_ADDITIVE_SUMMABLE 743 >> REWRITE_TAC [measurable_sets_def, m_space_def] 744 >> CONJ_TAC 745 >- (MATCH_MP_TAC LAMBDA_SYSTEM_ALGEBRA 746 >> CONJ_TAC >- PROVE_TAC [sigma_algebra_def] 747 >> PROVE_TAC [outer_measure_space_def]) 748 >> CONJ_TAC 749 >- PROVE_TAC [LAMBDA_SYSTEM_POSITIVE, outer_measure_space_def] 750 >> CONJ_TAC 751 >- PROVE_TAC [LAMBDA_SYSTEM_INCREASING, outer_measure_space_def] 752 >> CONJ_TAC 753 >- PROVE_TAC [LAMBDA_SYSTEM_ADDITIVE, outer_measure_space_def, 754 sigma_algebra_def] 755 >> RW_TAC std_ss []) 756 >> STRIP_TAC 757 >> Know `BIGUNION (IMAGE f UNIV) IN subsets gsig` 758 >- (Q.PAT_X_ASSUM `sigma_algebra a` MP_TAC 759 >> Q.PAT_X_ASSUM `f IN s` MP_TAC 760 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALT, IN_FUNSET, IN_UNIV] 761 >> POP_ASSUM MATCH_MP_TAC 762 >> RW_TAC std_ss [] 763 >> Q.PAT_X_ASSUM `!x. P x` MP_TAC 764 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION]) 765 >> STRIP_TAC 766 >> Suff 767 `!g l. 768 g IN subsets gsig /\ (BIGUNION (IMAGE f (UNIV : num -> bool)) = l) ==> 769 (lam (l INTER g) + lam ((space gsig DIFF l) INTER g) = lam g) /\ 770 (lam (l INTER g) = suminf (lam o (\s. s INTER g) o f))` 771 >- (RW_TAC std_ss [lambda_system_def, GSPECIFICATION, SUMS_EQ] 772 >> POP_ASSUM 773 (MP_TAC o Q.SPEC `BIGUNION (IMAGE (f : num -> 'a -> bool) UNIV)`) 774 >> RW_TAC std_ss [INTER_IDEMPOT] 775 >> Suff `(\s. s INTER BIGUNION (IMAGE f UNIV)) o f = f` 776 >- RW_TAC std_ss [] 777 >> KILL_TAC 778 >> RW_TAC std_ss [FUN_EQ_THM] 779 >> RW_TAC std_ss [o_DEF, EXTENSION, IN_INTER, IN_BIGUNION, 780 GSPECIFICATION, IN_IMAGE, IN_UNIV] 781 >> METIS_TAC [IN_INTER,SPECIFICATION,IN_BIGUNION_IMAGE,IN_UNIV]) 782 >> rpt GEN_TAC 783 >> STRIP_TAC 784 >> Know `summable (lam o (\s. s INTER g) o f)` 785 >- (MATCH_MP_TAC SER_COMPAR 786 >> Q.EXISTS_TAC `lam o f` 787 >> RW_TAC std_ss [] 788 >> Q.EXISTS_TAC `0` 789 >> RW_TAC arith_ss [o_DEF] 790 >> Q.PAT_X_ASSUM `outer_measure_space (space gsig,subsets gsig,lam)` MP_TAC 791 >> RW_TAC std_ss [outer_measure_space_def, increasing_def, positive_def, 792 measure_def, measurable_sets_def] 793 >> Know `f n IN subsets gsig` 794 >- (Q.PAT_X_ASSUM `f IN x` MP_TAC 795 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, lambda_system_def, 796 GSPECIFICATION]) 797 >> STRIP_TAC 798 >> Know `f n INTER g IN subsets gsig` 799 >- PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def] 800 >> STRIP_TAC 801 >> Know `0 <= lam (f n INTER g)` >- PROVE_TAC [] 802 >> RW_TAC std_ss [abs] 803 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 804 >> RW_TAC std_ss [SUBSET_DEF, IN_INTER]) 805 >> STRIP_TAC 806 >> Suff 807 `lam g <= lam (l INTER g) + lam ((space gsig DIFF l) INTER g) /\ 808 lam (l INTER g) <= suminf (lam o (\s. s INTER g) o f) /\ 809 suminf (lam o (\s. s INTER g) o f) + lam ((space gsig DIFF l) INTER g) <= lam g` 810 >- REAL_ARITH_TAC 811 >> Strip >| 812 [Know `lam = measure (space gsig,subsets gsig,lam)` >- RW_TAC std_ss [measure_def] 813 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 814 >> MATCH_MP_TAC SUBADDITIVE 815 >> REWRITE_TAC [measurable_sets_def] 816 >> CONJ_TAC 817 >- (MATCH_MP_TAC COUNTABLY_SUBADDITIVE_SUBADDITIVE 818 >> REWRITE_TAC [measurable_sets_def, m_space_def, SPACE] 819 >> PROVE_TAC [outer_measure_space_def, sigma_algebra_def]) 820 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def] 821 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def, ALGEBRA_COMPL] 822 >> RW_TAC std_ss [EXTENSION, DISJOINT_DEF, IN_INTER, NOT_IN_EMPTY, IN_DIFF, 823 IN_UNION] 824 >> FULL_SIMP_TAC std_ss [sigma_algebra_def, algebra_def, SUBSET_DEF, subset_class_def] 825 >> PROVE_TAC [], 826 Q.PAT_X_ASSUM `f IN (x -> y)` MP_TAC 827 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV] 828 >> Know `lam = measure (space gsig,subsets gsig,lam)` >- RW_TAC std_ss [measure_def] 829 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 830 >> MATCH_MP_TAC COUNTABLY_SUBADDITIVE 831 >> REWRITE_TAC [measurable_sets_def, measure_def] 832 >> CONJ_TAC >- PROVE_TAC [outer_measure_space_def] 833 >> CONJ_TAC 834 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_DEF] 835 >> POP_ASSUM (MP_TAC o Q.SPEC `x`) 836 >> RW_TAC std_ss [lambda_system_def, GSPECIFICATION] 837 >> PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def]) 838 >> CONJ_TAC >- PROVE_TAC [] 839 >> CONJ_TAC 840 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_BIGUNION, IN_IMAGE, IN_UNIV, 841 o_DEF] 842 >> REVERSE EQ_TAC >- PROVE_TAC [] 843 >> RW_TAC std_ss [GSYM EXTENSION] 844 >> Q.EXISTS_TAC `f x' INTER g` 845 >> RW_TAC std_ss [IN_INTER] 846 >> PROVE_TAC []) 847 >> PROVE_TAC [ALGEBRA_INTER, sigma_algebra_def], 848 Suff `suminf (lam o (\s. s INTER g) o f) <= lam g - lam ((space gsig DIFF l) INTER g)` 849 >- REAL_ARITH_TAC 850 >> MATCH_MP_TAC SUMMABLE_LE 851 >> CONJ_TAC >- PROVE_TAC [] 852 >> GEN_TAC 853 >> MP_TAC (Q.SPECL [`gsig`, `lam`, `g`, `f`, `n`] LAMBDA_SYSTEM_STRONG_SUM) 854 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALGEBRA, OUTER_MEASURE_SPACE_POSITIVE] 855 >> POP_ASSUM K_TAC 856 >> Suff 857 `(lam g = lam (BIGUNION (IMAGE f (count n)) INTER g) + 858 lam ((space gsig DIFF BIGUNION (IMAGE f (count n))) INTER g)) /\ 859 lam ((space gsig DIFF BIGUNION (IMAGE f UNIV)) INTER g) <= 860 lam ((space gsig DIFF BIGUNION (IMAGE f (count n))) INTER g)` 861 >- REAL_ARITH_TAC 862 >> CONJ_TAC 863 >- (Suff `BIGUNION (IMAGE f (count n)) IN lambda_system gsig lam` 864 >- RW_TAC std_ss [lambda_system_def, GSPECIFICATION] 865 >> MATCH_MP_TAC ((REWRITE_RULE [subsets_def] o Q.SPEC `(space gsig,lambda_system gsig lam)`) ALGEBRA_FINITE_UNION) 866 >> Q.PAT_X_ASSUM `f IN (x -> y)` MP_TAC 867 >> RW_TAC std_ss [SUBSET_DEF, IN_FUNSET, IN_UNIV, IN_IMAGE] 868 >> PROVE_TAC [LAMBDA_SYSTEM_ALGEBRA, SIGMA_ALGEBRA_ALGEBRA, 869 OUTER_MEASURE_SPACE_POSITIVE, IMAGE_FINITE, FINITE_COUNT]) 870 >> Q.PAT_X_ASSUM `outer_measure_space (space gsig,subsets gsig,lam)` MP_TAC 871 >> RW_TAC std_ss [outer_measure_space_def, increasing_def, measure_def, 872 measurable_sets_def] 873 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 874 >> CONJ_TAC 875 >- PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_COMPL, ALGEBRA_INTER] 876 >> CONJ_TAC 877 >- (Know `algebra gsig` >- PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA] 878 >> STRIP_TAC 879 >> MATCH_MP_TAC ALGEBRA_INTER 880 >> RW_TAC std_ss [] 881 >> MATCH_MP_TAC ALGEBRA_COMPL 882 >> RW_TAC std_ss [] 883 >> MATCH_MP_TAC ALGEBRA_FINITE_UNION 884 >> Q.PAT_X_ASSUM `f IN x` MP_TAC 885 >> RW_TAC std_ss [SUBSET_DEF, IN_FUNSET, IN_UNIV, lambda_system_def, 886 GSPECIFICATION, IN_IMAGE] 887 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]) 888 >> RW_TAC std_ss [SUBSET_DEF, IN_INTER, IN_COMPL, IN_IMAGE, IN_BIGUNION, 889 IN_UNIV, IN_DIFF] 890 >> PROVE_TAC []]); 891 892val CARATHEODORY_LEMMA = store_thm 893 ("CARATHEODORY_LEMMA", 894 ``!gsig lam. 895 sigma_algebra gsig /\ outer_measure_space (space gsig, subsets gsig, lam) ==> 896 measure_space (space gsig, lambda_system gsig lam, lam)``, 897 RW_TAC std_ss [] 898 >> MP_TAC (Q.SPECL [`gsig`, `lam`] LAMBDA_SYSTEM_CARATHEODORY) 899 >> RW_TAC std_ss [measure_space_def, countably_additive_def, 900 measurable_sets_def, measure_def, m_space_def] >| 901 [RW_TAC std_ss [SIGMA_ALGEBRA_ALT_DISJOINT, subsets_def] 902 >> PROVE_TAC [LAMBDA_SYSTEM_ALGEBRA, SIGMA_ALGEBRA_ALGEBRA, 903 outer_measure_space_def], 904 PROVE_TAC [outer_measure_space_def, LAMBDA_SYSTEM_POSITIVE]]); 905 906val INF_MEASURE_NONEMPTY = store_thm 907 ("INF_MEASURE_NONEMPTY", 908 ``!m g s. 909 algebra (m_space m, measurable_sets m) /\ positive m /\ s IN measurable_sets m /\ 910 g SUBSET s ==> 911 measure m s IN 912 {r | 913 ?f. 914 f IN (UNIV -> measurable_sets m) /\ 915 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 916 g SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r}``, 917 RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, positive_def] 918 >> Q.EXISTS_TAC `\n. if n = 0 then s else {}` 919 >> BasicProvers.NORM_TAC std_ss 920 [SUBSET_DEF, IN_BIGUNION, DISJOINT_EMPTY, 921 IN_IMAGE, IN_UNIV, o_DEF, IN_FUNSET, ALGEBRA_EMPTY] 922 >| [PROVE_TAC [subsets_def, ALGEBRA_EMPTY], 923 PROVE_TAC [], 924 Know `measure m s = sum (0,1) (\x. measure m (if x = 0 then s else {}))` 925 >- (ASM_SIMP_TAC bool_ss [sum, ONE, REAL_ADD_LID] >> RW_TAC arith_ss []) 926 >> DISCH_THEN (REWRITE_TAC o wrap) 927 >> MATCH_MP_TAC SER_0 928 >> RW_TAC arith_ss []]); 929 930val INF_MEASURE_POS0 = store_thm 931 ("INF_MEASURE_POS0", 932 ``!m g x. 933 algebra (m_space m,measurable_sets m) /\ positive m /\ 934 x IN 935 {r | 936 ?f. 937 f IN (UNIV -> measurable_sets m) /\ 938 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 939 g SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r} ==> 940 0 <= x``, 941 RW_TAC std_ss [GSPECIFICATION, SUMS_EQ, IN_FUNSET, IN_UNIV, positive_def] 942 >> MATCH_MP_TAC SER_POS 943 >> RW_TAC std_ss [o_DEF]); 944 945val INF_MEASURE_POS = store_thm 946 ("INF_MEASURE_POS", 947 ``!m g. algebra (m_space m, measurable_sets m) /\ positive m /\ g SUBSET m_space m ==> 0 <= inf_measure m g``, 948 RW_TAC std_ss [GSPECIFICATION, inf_measure_def] 949 >> MATCH_MP_TAC LE_INF 950 >> CONJ_TAC 951 >- (Q.EXISTS_TAC `measure m (m_space m)` 952 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 953 >> PROVE_TAC [ALGEBRA_SPACE, space_def, subsets_def]) 954 >> METIS_TAC [INF_MEASURE_POS0]); 955 956val INCREASING = store_thm 957 ("INCREASING", 958 ``!m s t. 959 increasing m /\ s SUBSET t /\ s IN measurable_sets m /\ 960 t IN measurable_sets m ==> 961 measure m s <= measure m t``, 962 PROVE_TAC [increasing_def]); 963 964val ADDITIVE_INCREASING = store_thm 965 ("ADDITIVE_INCREASING", 966 ``!m. 967 algebra (m_space m, measurable_sets m) /\ positive m /\ additive m ==> 968 increasing m``, 969 RW_TAC std_ss [increasing_def, positive_def] 970 >> Suff 971 `?u. u IN measurable_sets m /\ (measure m t = measure m s + measure m u)` 972 >- (RW_TAC std_ss [] 973 >> Q.PAT_X_ASSUM `!s. P s` (MP_TAC o Q.SPEC `u`) 974 >> RW_TAC std_ss [] 975 >> NTAC 2 (POP_ASSUM MP_TAC) 976 >> REAL_ARITH_TAC) 977 >> Q.EXISTS_TAC `t DIFF s` 978 >> STRONG_CONJ_TAC >- PROVE_TAC [ALGEBRA_DIFF, subsets_def] 979 >> RW_TAC std_ss [] 980 >> MATCH_MP_TAC ADDITIVE 981 >> RW_TAC std_ss [DISJOINT_DEF, IN_DIFF, IN_UNION, EXTENSION, IN_INTER, 982 NOT_IN_EMPTY] 983 >> PROVE_TAC [SUBSET_DEF]); 984 985val COUNTABLY_ADDITIVE_ADDITIVE = store_thm 986 ("COUNTABLY_ADDITIVE_ADDITIVE", 987 ``!m. 988 algebra (m_space m, measurable_sets m) /\ positive m /\ countably_additive m ==> 989 additive m``, 990 RW_TAC std_ss [additive_def, positive_def, countably_additive_def] 991 >> Q.PAT_X_ASSUM `!f. P f` 992 (MP_TAC o Q.SPEC `\n : num. if n = 0 then s else if n = 1 then t else {}`) 993 >> Know 994 `BIGUNION 995 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 996 UNIV) = 997 s UNION t` 998 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_UNION] 999 >> EQ_TAC >- PROVE_TAC [NOT_IN_EMPTY] 1000 >> Know `~(1 = (0:num))` >- DECIDE_TAC 1001 >> RW_TAC std_ss [] >- PROVE_TAC [] 1002 >> Q.EXISTS_TAC `t` 1003 >> RW_TAC std_ss [] 1004 >> Q.EXISTS_TAC `1` 1005 >> RW_TAC std_ss [] 1006 >> PROVE_TAC []) 1007 >> DISCH_THEN (REWRITE_TAC o wrap) 1008 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV] 1009 >> Suff 1010 `measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))) sums 1011 (measure m s + measure m t) /\ 1012 measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))) sums 1013 measure m (s UNION t)` 1014 >- PROVE_TAC [SUM_UNIQ] 1015 >> CONJ_TAC 1016 >- (Know 1017 `measure m s + measure m t = 1018 sum (0, 2) 1019 (measure m o (\n. (if n = 0 then s else (if n = 1 then t else {}))))` 1020 >- (ASM_SIMP_TAC bool_ss [TWO, ONE, sum] 1021 >> RW_TAC std_ss [] 1022 >> RW_TAC arith_ss [REAL_ADD_LID, o_THM]) 1023 >> DISCH_THEN (REWRITE_TAC o wrap) 1024 >> MATCH_MP_TAC SER_0 1025 >> RW_TAC arith_ss [o_THM]) 1026 >> POP_ASSUM MATCH_MP_TAC 1027 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_EMPTY, space_def, subsets_def] 1028 >> RW_TAC std_ss [DISJOINT_EMPTY] 1029 >> PROVE_TAC [DISJOINT_SYM, ALGEBRA_UNION, subsets_def]); 1030 1031val COUNTABLY_ADDITIVE = store_thm 1032 ("COUNTABLY_ADDITIVE", 1033 ``!m s f. 1034 countably_additive m /\ f IN (UNIV -> measurable_sets m) 1035 /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1036 (s = BIGUNION (IMAGE f UNIV)) /\ s IN measurable_sets m ==> 1037 measure m o f sums measure m s``, 1038 RW_TAC std_ss [] 1039 >> PROVE_TAC [countably_additive_def]); 1040 1041val INF_MEASURE_AGREES = store_thm 1042 ("INF_MEASURE_AGREES", 1043 ``!m s. 1044 algebra (m_space m, measurable_sets m) /\ positive m /\ countably_additive m /\ 1045 s IN measurable_sets m ==> 1046 (inf_measure m s = measure m s)``, 1047 RW_TAC std_ss [inf_measure_def] 1048 >> ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 1049 >> CONJ_TAC 1050 >- (MATCH_MP_TAC INF_LE 1051 >> CONJ_TAC 1052 >- (Q.EXISTS_TAC `0` 1053 >> METIS_TAC [INF_MEASURE_POS0]) 1054 >> Q.EXISTS_TAC `measure m s` 1055 >> REVERSE CONJ_TAC >- RW_TAC std_ss [REAL_LE_REFL] 1056 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1057 >> RW_TAC std_ss [SUBSET_REFL]) 1058 >> MATCH_MP_TAC LE_INF 1059 >> CONJ_TAC 1060 >- (Q.EXISTS_TAC `measure m s` 1061 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1062 >> RW_TAC std_ss [SUBSET_REFL]) 1063 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, IN_FUNSET, IN_UNIV, 1064 IN_BIGUNION, IN_IMAGE, SUMS_EQ] 1065 >> MP_TAC (Q.SPECL [`m`] countably_additive_def) 1066 >> RW_TAC std_ss [] 1067 >> POP_ASSUM (MP_TAC o Q.SPEC `(\g. g INTER s) o f`) 1068 >> Know `BIGUNION (IMAGE ((\g. g INTER s) o f) UNIV) = s` 1069 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_INTER, o_THM] 1070 >> EQ_TAC >- PROVE_TAC [] 1071 >> RW_TAC std_ss [] 1072 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 1073 >> RW_TAC std_ss [IN_UNIV] 1074 >> Q.EXISTS_TAC `s INTER f x'` 1075 >> RW_TAC std_ss [IN_INTER] 1076 >> PROVE_TAC [EXTENSION]) 1077 >> DISCH_THEN (REWRITE_TAC o wrap) 1078 >> RW_TAC std_ss [o_THM, IN_FUNSET, IN_UNIV, IN_INTER] 1079 >> Suff `measure m o (\g. g INTER s) o f sums measure m s` 1080 >- (RW_TAC std_ss [SUMS_EQ] 1081 >> POP_ASSUM (REWRITE_TAC o wrap o GSYM) 1082 >> MATCH_MP_TAC SER_LE 1083 >> RW_TAC std_ss [o_THM] 1084 >> MATCH_MP_TAC INCREASING 1085 >> RW_TAC std_ss [ALGEBRA_INTER, INTER_SUBSET] 1086 >- (MATCH_MP_TAC ADDITIVE_INCREASING 1087 >> RW_TAC std_ss [] 1088 >> MATCH_MP_TAC COUNTABLY_ADDITIVE_ADDITIVE 1089 >> RW_TAC std_ss []) 1090 >> PROVE_TAC [ALGEBRA_INTER, subsets_def]) 1091 >> POP_ASSUM MATCH_MP_TAC 1092 >> CONJ_TAC >- PROVE_TAC [ALGEBRA_INTER, subsets_def] 1093 >> RW_TAC std_ss [] 1094 >> Q.PAT_X_ASSUM `!m n. P m n` (MP_TAC o Q.SPECL [`m'`, `n`]) 1095 >> RW_TAC std_ss [DISJOINT_DEF, IN_INTER, NOT_IN_EMPTY, EXTENSION] 1096 >> PROVE_TAC []); 1097 1098val MEASURE_DOWN = store_thm 1099 ("MEASURE_DOWN", 1100 ``!m0 m1. 1101 sigma_algebra (m_space m0,measurable_sets m0) /\ 1102 measurable_sets m0 SUBSET measurable_sets m1 /\ 1103 (measure m0 = measure m1) /\ measure_space m1 ==> 1104 measure_space m0``, 1105 RW_TAC std_ss [measure_space_def, positive_def, SUBSET_DEF, 1106 countably_additive_def, IN_FUNSET, IN_UNIV]); 1107 1108val SIGMA_ALGEBRA_SIGMA = store_thm 1109 ("SIGMA_ALGEBRA_SIGMA", 1110 ``!sp sts. subset_class sp sts ==> sigma_algebra (sigma sp sts)``, 1111 SIMP_TAC std_ss [subset_class_def] 1112 >> NTAC 3 STRIP_TAC 1113 >> RW_TAC std_ss [sigma_def, sigma_algebra_def, algebra_def, 1114 subsets_def, space_def, IN_BIGINTER, 1115 GSPECIFICATION, subset_class_def] 1116 >- (POP_ASSUM (MATCH_MP_TAC o REWRITE_RULE [IN_POW, DIFF_SUBSET, UNION_SUBSET, EMPTY_SUBSET] o 1117 Q.ISPEC `POW (sp :'a -> bool)`) 1118 >> RW_TAC std_ss [SUBSET_DEF, IN_POW, IN_BIGUNION] 1119 >> PROVE_TAC []) 1120 >> POP_ASSUM (fn th => MATCH_MP_TAC th >> ASSUME_TAC th) 1121 >> RW_TAC std_ss [SUBSET_DEF] 1122 >> Q.PAT_X_ASSUM `c SUBSET PP` MP_TAC 1123 >> CONV_TAC (LAND_CONV (SIMP_CONV (srw_ss()) [SUBSET_DEF])) 1124 >> DISCH_THEN (MP_TAC o Q.SPEC `x`) 1125 >> ASM_REWRITE_TAC [] 1126 >> DISCH_THEN MATCH_MP_TAC 1127 >> RW_TAC std_ss [] 1128 >> PROVE_TAC [SUBSET_DEF]); 1129 1130val POW_ALGEBRA = store_thm 1131 ("POW_ALGEBRA", 1132 ``algebra (sp, POW sp)``, 1133 RW_TAC std_ss [algebra_def, IN_POW, space_def, subsets_def, subset_class_def, 1134 EMPTY_SUBSET, DIFF_SUBSET, UNION_SUBSET]); 1135 1136val POW_SIGMA_ALGEBRA = store_thm 1137 ("POW_SIGMA_ALGEBRA", 1138 ``sigma_algebra (sp, POW sp)``, 1139 RW_TAC std_ss [sigma_algebra_def, IN_POW, space_def, subsets_def, 1140 POW_ALGEBRA, SUBSET_DEF, IN_BIGUNION] 1141 >> PROVE_TAC []); 1142 1143val UNIV_SIGMA_ALGEBRA = store_thm 1144 ("UNIV_SIGMA_ALGEBRA", 1145 ``sigma_algebra ((UNIV :'a -> bool),(UNIV :('a -> bool) -> bool))``, 1146 Know `(UNIV :('a -> bool) -> bool) = POW (UNIV :'a -> bool)` 1147 >- RW_TAC std_ss [EXTENSION, IN_POW, IN_UNIV, SUBSET_UNIV] 1148 >> RW_TAC std_ss [POW_SIGMA_ALGEBRA]); 1149 1150val INF_MEASURE_EMPTY = store_thm 1151 ("INF_MEASURE_EMPTY", 1152 ``!m. algebra (m_space m, measurable_sets m) /\ positive m ==> (inf_measure m {} = 0)``, 1153 RW_TAC std_ss [] 1154 >> ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 1155 >> REVERSE CONJ_TAC >- PROVE_TAC [INF_MEASURE_POS, EMPTY_SUBSET] 1156 >> RW_TAC std_ss [inf_measure_def] 1157 >> MATCH_MP_TAC INF_LE 1158 >> CONJ_TAC >- METIS_TAC [INF_MEASURE_POS0, EMPTY_SUBSET] 1159 >> Q.EXISTS_TAC `0` 1160 >> RW_TAC std_ss [GSPECIFICATION, REAL_LE_REFL] 1161 >> Q.EXISTS_TAC `K {}` 1162 >> RW_TAC bool_ss [IN_FUNSET, IN_UNIV, ALGEBRA_EMPTY, DISJOINT_EMPTY, K_THM, 1163 SUBSET_DEF, NOT_IN_EMPTY, IN_BIGUNION, IN_IMAGE] 1164 >- PROVE_TAC [subsets_def, space_def, ALGEBRA_EMPTY] 1165 >> Know `0 = sum (0, 0) (measure m o K {})` >- RW_TAC std_ss [sum] 1166 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1167 >> MATCH_MP_TAC SER_0 1168 >> RW_TAC std_ss [K_THM, o_THM] 1169 >> PROVE_TAC [positive_def]); 1170 1171val INF_MEASURE_POSITIVE = store_thm 1172 ("INF_MEASURE_POSITIVE", 1173 ``!m. 1174 algebra (m_space m, measurable_sets m) /\ positive m ==> 1175 positive (m_space m, POW (m_space m), inf_measure m)``, 1176 RW_TAC std_ss [positive_def, INF_MEASURE_EMPTY, INF_MEASURE_POS, 1177 measure_def, measurable_sets_def, IN_POW]); 1178 1179val INF_MEASURE_INCREASING = store_thm 1180 ("INF_MEASURE_INCREASING", 1181 ``!m. 1182 algebra (m_space m, measurable_sets m) /\ positive m ==> 1183 increasing (m_space m, POW (m_space m), inf_measure m)``, 1184 RW_TAC std_ss [increasing_def, inf_measure_def, measurable_sets_def, IN_POW, measure_def] 1185 >> MATCH_MP_TAC LE_INF 1186 >> CONJ_TAC 1187 >- (Q.EXISTS_TAC `measure m (m_space m)` 1188 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1189 >> RW_TAC std_ss [] 1190 >> PROVE_TAC [ALGEBRA_SPACE, subsets_def, space_def, m_space_def, measurable_sets_def]) 1191 >> RW_TAC std_ss [] 1192 >> MATCH_MP_TAC INF_LE 1193 >> CONJ_TAC 1194 >- (Q.EXISTS_TAC `0` 1195 >> METIS_TAC [INF_MEASURE_POS0]) 1196 >> Q.EXISTS_TAC `x` 1197 >> POP_ASSUM MP_TAC 1198 >> RW_TAC std_ss [GSPECIFICATION, REAL_LE_REFL] 1199 >> PROVE_TAC [SUBSET_TRANS]); 1200 1201val INF_MEASURE_LE = store_thm 1202 ("INF_MEASURE_LE", 1203 ``!m s x. 1204 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m /\ 1205 x IN 1206 {r | ?f. 1207 f IN (UNIV -> measurable_sets m) /\ 1208 s SUBSET BIGUNION (IMAGE f UNIV) /\ 1209 measure m o f sums r} ==> 1210 inf_measure m s <= x``, 1211 RW_TAC std_ss [GSPECIFICATION, SUMS_EQ, IN_FUNSET, IN_UNIV] 1212 >> RW_TAC std_ss [inf_measure_def] 1213 >> MATCH_MP_TAC INF_LE 1214 >> CONJ_TAC 1215 >- (Q.EXISTS_TAC `0` 1216 >> METIS_TAC [INF_MEASURE_POS0]) 1217 >> RW_TAC std_ss [GSPECIFICATION, SUMS_EQ] 1218 >> CONV_TAC (DEPTH_CONV LEFT_AND_EXISTS_CONV THENC SWAP_EXISTS_CONV) 1219 >> Q.EXISTS_TAC `\n. f n DIFF (BIGUNION (IMAGE f (count n)))` 1220 >> Q.EXISTS_TAC 1221 `suminf (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n)))))` 1222 >> REWRITE_TAC [GSYM CONJ_ASSOC, IN_FUNSET, IN_UNIV] 1223 >> BETA_TAC 1224 >> STRONG_CONJ_TAC 1225 >- (STRIP_TAC 1226 >> MATCH_MP_TAC ((REWRITE_RULE [space_def, subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_DIFF) 1227 >> RW_TAC std_ss [] 1228 >> MATCH_MP_TAC ((REWRITE_RULE [space_def, subsets_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_FINITE_UNION) 1229 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE] 1230 >> PROVE_TAC [IMAGE_FINITE, FINITE_COUNT]) 1231 >> STRIP_TAC 1232 >> Know 1233 `summable (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n))))) /\ 1234 suminf (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n))))) <= 1235 suminf (measure m o f)` 1236 >- (MATCH_MP_TAC SER_POS_COMPARE 1237 >> RW_TAC std_ss [o_THM] >- PROVE_TAC [positive_def] 1238 >> MATCH_MP_TAC INCREASING 1239 >> PROVE_TAC [DIFF_SUBSET]) 1240 >> RW_TAC std_ss [] >| 1241 [RW_TAC arith_ss [DISJOINT_DEF, IN_INTER, NOT_IN_EMPTY, EXTENSION, IN_DIFF, 1242 IN_BIGUNION, IN_IMAGE, IN_COUNT] 1243 >> Know `m' < n \/ n < m'` >- DECIDE_TAC 1244 >> PROVE_TAC [], 1245 Q.PAT_X_ASSUM `s SUBSET g` MP_TAC 1246 >> RW_TAC arith_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, IN_UNIV] 1247 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 1248 >> RW_TAC std_ss [] 1249 >> Know `?n. x IN f n` >- PROVE_TAC [] 1250 >> DISCH_THEN (MP_TAC o Ho_Rewrite.REWRITE_RULE [MINIMAL_EXISTS]) 1251 >> RW_TAC std_ss [] 1252 >> Q.EXISTS_TAC 1253 `f (minimal (\n. x IN f n)) DIFF 1254 BIGUNION (IMAGE f (count (minimal (\n. x IN f n))))` 1255 >> REVERSE CONJ_TAC >- PROVE_TAC [] 1256 >> RW_TAC std_ss [IN_DIFF, IN_BIGUNION, IN_IMAGE, IN_COUNT] 1257 >> PROVE_TAC []]); 1258 1259val INF_MEASURE_CLOSE = store_thm 1260 ("INF_MEASURE_CLOSE", 1261 ``!m s e. 1262 algebra (m_space m, measurable_sets m) /\ positive m /\ 0 < e /\ s SUBSET (m_space m) ==> 1263 ?f l. 1264 f IN (UNIV -> measurable_sets m) /\ s SUBSET BIGUNION (IMAGE f UNIV) /\ 1265 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1266 (measure m o f) sums l /\ l <= inf_measure m s + e``, 1267 RW_TAC std_ss [inf_measure_def] 1268 >> Suff 1269 `?l. 1270 l IN {r | ?f. 1271 f IN (UNIV -> measurable_sets m) /\ 1272 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1273 s SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r} /\ 1274 l < inf {r | ?f. 1275 f IN (UNIV -> measurable_sets m) /\ 1276 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1277 s SUBSET BIGUNION (IMAGE f UNIV) /\ measure m o f sums r} + e` 1278 >- (RW_TAC std_ss [GSPECIFICATION] 1279 >> Q.EXISTS_TAC `f` 1280 >> Q.EXISTS_TAC `l` 1281 >> RW_TAC std_ss [] 1282 >> PROVE_TAC [REAL_LT_IMP_LE]) 1283 >> MATCH_MP_TAC INF_CLOSE 1284 >> RW_TAC std_ss [] 1285 >> Q.EXISTS_TAC `measure m (m_space m)` 1286 >> MATCH_MP_TAC INF_MEASURE_NONEMPTY 1287 >> RW_TAC std_ss [] 1288 >> PROVE_TAC [ALGEBRA_SPACE, m_space_def, measurable_sets_def, subsets_def, space_def]); 1289 1290val INF_MEASURE_COUNTABLY_SUBADDITIVE = store_thm 1291 ("INF_MEASURE_COUNTABLY_SUBADDITIVE", 1292 ``!m. 1293 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m ==> 1294 countably_subadditive (m_space m, POW (m_space m), inf_measure m)``, 1295 RW_TAC std_ss [countably_subadditive_def, IN_FUNSET, IN_UNIV] 1296 >> MATCH_MP_TAC REAL_LE_EPSILON 1297 >> RW_TAC std_ss [] 1298 >> MATCH_MP_TAC REAL_LE_TRANS 1299 >> Know 1300 `!n. ?g l. 1301 g IN (UNIV -> measurable_sets m) /\ 1302 f n SUBSET BIGUNION (IMAGE g UNIV) /\ 1303 (!m n. ~(m = n) ==> DISJOINT (g m) (g n)) /\ 1304 (measure m o g) sums l /\ 1305 l <= inf_measure m (f n) + e * (1 / 2) pow (n + 1)` 1306 >- (STRIP_TAC 1307 >> MATCH_MP_TAC INF_MEASURE_CLOSE 1308 >> PROVE_TAC [REAL_LT_MUL, POW_HALF_POS, measurable_sets_def, IN_POW]) 1309 >> CONV_TAC (REDEPTH_CONV (CHANGED_CONV SKOLEM_CONV)) 1310 >> RW_TAC std_ss [] 1311 >> Q.EXISTS_TAC `suminf l` 1312 >> Know `!n. 0 <= l n` 1313 >- (RW_TAC std_ss [] 1314 >> POP_ASSUM (MP_TAC o Q.SPEC `n`) 1315 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUMS_EQ] 1316 >> Q.PAT_X_ASSUM `a = b` (REWRITE_TAC o wrap o GSYM) 1317 >> MATCH_MP_TAC SUMINF_POS 1318 >> RW_TAC std_ss [o_THM] 1319 >> PROVE_TAC [positive_def]) 1320 >> STRIP_TAC 1321 >> Know 1322 `summable l /\ 1323 suminf l <= suminf (\n. inf_measure m (f n)) + e` 1324 >- (Know `(\n. e * (1 / 2) pow (n + 1)) sums (e * 1)` 1325 >- (HO_MATCH_MP_TAC SER_CMUL 1326 >> RW_TAC std_ss [POW_HALF_SER]) 1327 >> PURE_REWRITE_TAC [REAL_MUL_RID, SUMS_EQ] 1328 >> STRIP_TAC 1329 >> POP_ASSUM (ONCE_REWRITE_TAC o wrap o GSYM) 1330 >> Know 1331 `summable (\n. inf_measure m (f n) + e * (1 / 2) pow (n + 1)) /\ 1332 (suminf (\n. inf_measure m (f n)) + 1333 suminf (\n. e * (1 / 2) pow (n + 1)) = 1334 suminf (\n. inf_measure m (f n) + e * (1 / 2) pow (n + 1)))` 1335 >- (HO_MATCH_MP_TAC SUMINF_ADD 1336 >> Q.PAT_X_ASSUM `summable (a o b)` MP_TAC 1337 >> RW_TAC std_ss [o_DEF, measure_def]) 1338 >> STRIP_TAC 1339 >> POP_ASSUM (ONCE_REWRITE_TAC o wrap) 1340 >> MATCH_MP_TAC SER_POS_COMPARE 1341 >> RW_TAC std_ss []) 1342 >> RW_TAC std_ss [o_DEF, measure_def] 1343 >> MATCH_MP_TAC INF_MEASURE_LE 1344 >> RW_TAC std_ss [GSPECIFICATION] 1345 >> MP_TAC NUM_2D_BIJ_INV 1346 >> STRIP_TAC 1347 >> Q.EXISTS_TAC `UNCURRY g o f'` 1348 >> Q.PAT_X_ASSUM `!n. P n /\ Q n` MP_TAC 1349 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, SUBSET_DEF, IN_BIGUNION, 1350 IN_IMAGE] >| 1351 [Cases_on `f' x` 1352 >> RW_TAC std_ss [UNCURRY_DEF], 1353 Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `x'`) 1354 >> RW_TAC std_ss [] 1355 >> Q.PAT_X_ASSUM `!n. P n` K_TAC 1356 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 1357 >> RW_TAC std_ss [] 1358 >> Q.EXISTS_TAC `g x' x''` 1359 >> RW_TAC std_ss [] 1360 >> Q.PAT_X_ASSUM `BIJ a b c` MP_TAC 1361 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV, IN_CROSS] 1362 >> POP_ASSUM (MP_TAC o Q.SPEC `(x', x'')`) 1363 >> RW_TAC std_ss [] 1364 >> Q.EXISTS_TAC `y` 1365 >> RW_TAC std_ss [UNCURRY_DEF], 1366 Know `measure m o UNCURRY g o f' = UNCURRY (\m'. measure m o g m') o f'` 1367 >- (RW_TAC std_ss [FUN_EQ_THM] 1368 >> RW_TAC std_ss [o_DEF] 1369 >> Cases_on `f' x` 1370 >> RW_TAC std_ss [UNCURRY_DEF]) 1371 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1372 >> MATCH_MP_TAC SUMINF_2D 1373 >> RW_TAC std_ss [o_THM] 1374 >> PROVE_TAC [positive_def]]); 1375 1376val INF_MEASURE_OUTER = store_thm 1377 ("INF_MEASURE_OUTER", 1378 ``!m. 1379 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m ==> 1380 outer_measure_space (m_space m, POW(m_space m), inf_measure m)``, 1381 RW_TAC std_ss [outer_measure_space_def, INF_MEASURE_POSITIVE, 1382 INF_MEASURE_INCREASING, INF_MEASURE_COUNTABLY_SUBADDITIVE]); 1383 1384val SIGMA_SUBSET = store_thm 1385 ("SIGMA_SUBSET", 1386 ``!a b. sigma_algebra b /\ a SUBSET (subsets b) ==> subsets (sigma (space b) a) SUBSET (subsets b)``, 1387 RW_TAC std_ss [sigma_def, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION, subsets_def] 1388 >> POP_ASSUM (MATCH_MP_TAC o Q.SPEC `subsets b`) 1389 >> RW_TAC std_ss [SPACE]); 1390 1391val ALGEBRA_SUBSET_LAMBDA_SYSTEM = store_thm 1392 ("ALGEBRA_SUBSET_LAMBDA_SYSTEM", 1393 ``!m. 1394 algebra (m_space m, measurable_sets m) /\ positive m /\ increasing m /\ 1395 additive m ==> 1396 measurable_sets m SUBSET lambda_system (m_space m, POW (m_space m)) (inf_measure m)``, 1397 RW_TAC std_ss [SUBSET_DEF, lambda_system_def, GSPECIFICATION, 1398 IN_UNIV, GSYM REAL_LE_ANTISYM, space_def, subsets_def, IN_POW] 1399 >| [FULL_SIMP_TAC std_ss [algebra_def, subset_class_def, m_space_def, measurable_sets_def, 1400 space_def, subsets_def, SUBSET_DEF] 1401 >> PROVE_TAC [], 1402 MATCH_MP_TAC REAL_LE_EPSILON 1403 >> RW_TAC std_ss [] 1404 >> MP_TAC (Q.SPECL [`m`, `s`, `e`] INF_MEASURE_CLOSE) 1405 >> Know `s SUBSET m_space m` 1406 >- PROVE_TAC [SUBSET_DEF, algebra_def, subset_class_def, subsets_def, space_def] 1407 >> RW_TAC std_ss [SUMS_EQ, IN_FUNSET, IN_UNIV] 1408 >> MATCH_MP_TAC REAL_LE_TRANS 1409 >> Q.EXISTS_TAC `suminf (measure m o f)` 1410 >> RW_TAC std_ss [] 1411 >> POP_ASSUM K_TAC 1412 >> Know 1413 `!x. 1414 x IN measurable_sets m ==> 1415 summable (measure m o (\s. x INTER s) o f) /\ 1416 inf_measure m (x INTER s) <= suminf (measure m o (\s. x INTER s) o f)` 1417 >- (NTAC 2 STRIP_TAC 1418 >> STRONG_CONJ_TAC 1419 >- (MATCH_MP_TAC SER_COMPAR 1420 >> Q.EXISTS_TAC `measure m o f` 1421 >> RW_TAC std_ss [GREATER_EQ] 1422 >> Q.EXISTS_TAC `0` 1423 >> REVERSE (RW_TAC arith_ss [o_THM, abs]) 1424 >- PROVE_TAC [positive_def, (REWRITE_RULE [subsets_def, space_def] o 1425 Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER] 1426 >> MATCH_MP_TAC INCREASING 1427 >> RW_TAC std_ss [INTER_SUBSET, (REWRITE_RULE [subsets_def, space_def] o 1428 Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER]) 1429 >> RW_TAC std_ss [inf_measure_def] 1430 >> MATCH_MP_TAC INF_LE 1431 >> CONJ_TAC 1432 >- (Q.EXISTS_TAC `0` 1433 >> METIS_TAC [INF_MEASURE_POS0]) 1434 >> Q.EXISTS_TAC `suminf (measure m o (\s. x' INTER s) o f)` 1435 >> RW_TAC std_ss [REAL_LE_REFL, GSPECIFICATION] 1436 >> Q.EXISTS_TAC `(\s. x' INTER s) o f` 1437 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, 1438 (REWRITE_RULE [subsets_def, space_def] o Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER, o_THM, SUMS_EQ] 1439 >- (Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPECL [`m'`, `n`]) 1440 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 1441 >> PROVE_TAC []) 1442 >> Q.PAT_X_ASSUM `s SUBSET ss` MP_TAC 1443 >> RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_INTER, IN_IMAGE, 1444 IN_UNIV, o_THM] 1445 >> Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x''`) 1446 >> RW_TAC std_ss [] 1447 >> PROVE_TAC [IN_INTER]) 1448 >> DISCH_THEN 1449 (fn th => MP_TAC (Q.SPEC `x` th) >> MP_TAC (Q.SPEC `m_space m DIFF x` th)) 1450 >> RW_TAC std_ss [(REWRITE_RULE [subsets_def, space_def] o 1451 Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_COMPL] 1452 >> MATCH_MP_TAC REAL_LE_TRANS 1453 >> Q.EXISTS_TAC 1454 `suminf (measure m o (\s. x INTER s) o f) + 1455 suminf (measure m o (\s. (m_space m DIFF x) INTER s) o f)` 1456 >> CONJ_TAC 1457 >- (Q.PAT_X_ASSUM `(a:real) <= b` MP_TAC 1458 >> Q.PAT_X_ASSUM `(a:real) <= b` MP_TAC 1459 >> REAL_ARITH_TAC) 1460 >> RW_TAC std_ss [SUMINF_ADD, o_THM] 1461 >> Know `!a b : real. (a = b) ==> a <= b` >- REAL_ARITH_TAC 1462 >> DISCH_THEN MATCH_MP_TAC 1463 >> AP_TERM_TAC 1464 >> RW_TAC std_ss [FUN_EQ_THM] 1465 >> RW_TAC std_ss [o_THM] 1466 >> MATCH_MP_TAC EQ_SYM 1467 >> MATCH_MP_TAC ADDITIVE 1468 >> RW_TAC std_ss [(REWRITE_RULE [subsets_def, space_def] o 1469 Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_INTER, 1470 (REWRITE_RULE [subsets_def, space_def] o 1471 Q.SPEC `(m_space m,measurable_sets m)`) ALGEBRA_COMPL, 1472 DISJOINT_DEF, IN_INTER, IN_DIFF, NOT_IN_EMPTY, EXTENSION, IN_UNION] 1473 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF, space_def, subsets_def], 1474 Know `inf_measure m = measure (m_space m, POW (m_space m), inf_measure m)` 1475 >- RW_TAC std_ss [measure_def] 1476 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1477 >> MATCH_MP_TAC SUBADDITIVE 1478 >> RW_TAC std_ss [IN_UNIV, EXTENSION, IN_INTER, IN_DIFF, IN_UNION, IN_POW, 1479 measurable_sets_def, SUBSET_DEF] 1480 >> PROVE_TAC [INF_MEASURE_COUNTABLY_SUBADDITIVE, 1481 INF_MEASURE_POSITIVE, POW_ALGEBRA, 1482 COUNTABLY_SUBADDITIVE_SUBADDITIVE, 1483 measurable_sets_def, m_space_def]]); 1484 1485val CARATHEODORY = store_thm 1486 ("CARATHEODORY", 1487 ``!m0. 1488 algebra (m_space m0, measurable_sets m0) /\ positive m0 /\ countably_additive m0 ==> 1489 ?m. 1490 (!s. s IN measurable_sets m0 ==> (measure m s = measure m0 s)) /\ 1491 ((m_space m, measurable_sets m) = 1492 sigma (m_space m0) (measurable_sets m0)) /\ measure_space m``, 1493 RW_TAC std_ss [] 1494 >> Q.EXISTS_TAC `(space (sigma (m_space m0) (measurable_sets m0)), 1495 subsets (sigma (m_space m0) (measurable_sets m0)), 1496 inf_measure m0)` 1497 >> CONJ_TAC >- PROVE_TAC [INF_MEASURE_AGREES, measure_def] 1498 >> CONJ_TAC >- RW_TAC std_ss [measurable_sets_def, subsets_def, space_def, m_space_def, SPACE] 1499 >> MATCH_MP_TAC MEASURE_DOWN 1500 >> Q.EXISTS_TAC 1501 `(m_space m0, 1502 lambda_system (m_space m0, POW (m_space m0)) (inf_measure m0), 1503 inf_measure m0)` 1504 >> REWRITE_TAC [measurable_sets_def, measure_def, space_def, m_space_def, subsets_def, SPACE] 1505 >> STRONG_CONJ_TAC >- FULL_SIMP_TAC std_ss [algebra_def, SIGMA_ALGEBRA_SIGMA, 1506 space_def, subsets_def] 1507 >> STRIP_TAC 1508 >> ONCE_REWRITE_TAC [CONJ_COMM] 1509 >> STRONG_CONJ_TAC 1510 >- ((MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 1511 Q.SPEC `(m_space m0,POW (m_space m0))`) CARATHEODORY_LEMMA 1512 >> CONJ_TAC >- RW_TAC std_ss [POW_SIGMA_ALGEBRA] 1513 >> PROVE_TAC [INF_MEASURE_OUTER, COUNTABLY_ADDITIVE_ADDITIVE, 1514 ADDITIVE_INCREASING]) 1515 >> RW_TAC std_ss [] 1516 >> (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 1517 Q.SPECL [`(measurable_sets m0)`, `(m_space m0, 1518 lambda_system (m_space m0, POW (m_space m0)) 1519 (inf_measure m0))`]) SIGMA_SUBSET 1520 >> CONJ_TAC >- FULL_SIMP_TAC std_ss [measure_space_def, measurable_sets_def, m_space_def] 1521 >> PROVE_TAC [ALGEBRA_SUBSET_LAMBDA_SYSTEM, COUNTABLY_ADDITIVE_ADDITIVE, 1522 ADDITIVE_INCREASING]); 1523 1524val SIGMA_SUBSET_SUBSETS = store_thm 1525 ("SIGMA_SUBSET_SUBSETS", 1526 ``!sp a. a SUBSET subsets (sigma sp a)``, 1527 RW_TAC std_ss [sigma_def, IN_BIGINTER, SUBSET_DEF, GSPECIFICATION, subsets_def]); 1528 1529val IN_SIGMA = store_thm 1530 ("IN_SIGMA", 1531 ``!sp a x. x IN a ==> x IN subsets (sigma sp a)``, 1532 MP_TAC SIGMA_SUBSET_SUBSETS 1533 >> RW_TAC std_ss [SUBSET_DEF]); 1534 1535val SIGMA_ALGEBRA = store_thm 1536 ("SIGMA_ALGEBRA", 1537 ``!p. 1538 sigma_algebra p = 1539 subset_class (space p) (subsets p) /\ 1540 {} IN subsets p /\ (!s. s IN subsets p ==> (space p DIFF s) IN subsets p) /\ 1541 (!c. countable c /\ c SUBSET subsets p ==> BIGUNION c IN subsets p)``, 1542 RW_TAC std_ss [sigma_algebra_def, algebra_def] 1543 >> EQ_TAC >- PROVE_TAC [] 1544 >> RW_TAC std_ss [] 1545 >> Q.PAT_X_ASSUM `!c. P c` (MP_TAC o Q.SPEC `{s; t}`) 1546 >> RW_TAC std_ss [COUNTABLE_ALT_BIJ, FINITE_INSERT, FINITE_EMPTY, SUBSET_DEF, 1547 BIGUNION_PAIR, IN_INSERT, NOT_IN_EMPTY] 1548 >> PROVE_TAC []); 1549 1550val SIGMA_ALGEBRA_COUNTABLE_UNION = store_thm 1551 ("SIGMA_ALGEBRA_COUNTABLE_UNION", 1552 ``!a c. sigma_algebra a /\ countable c /\ c SUBSET subsets a ==> BIGUNION c IN subsets a``, 1553 PROVE_TAC [sigma_algebra_def]); 1554 1555val SIGMA_ALGEBRA_ENUM = store_thm 1556 ("SIGMA_ALGEBRA_ENUM", 1557 ``!a (f : num -> ('a -> bool)). 1558 sigma_algebra a /\ f IN (UNIV -> subsets a) ==> BIGUNION (IMAGE f UNIV) IN subsets a``, 1559 RW_TAC std_ss [SIGMA_ALGEBRA_ALT]); 1560 1561val MEASURE_COMPL = store_thm 1562 ("MEASURE_COMPL", 1563 ``!m s. 1564 measure_space m /\ s IN measurable_sets m ==> 1565 (measure m (m_space m DIFF s) = measure m (m_space m) - measure m s)``, 1566 RW_TAC std_ss [] 1567 >> Suff `measure m (m_space m) = measure m s + measure m (m_space m DIFF s)` 1568 >- REAL_ARITH_TAC 1569 >> MATCH_MP_TAC ADDITIVE 1570 >> Q.PAT_X_ASSUM `measure_space m` MP_TAC 1571 >> RW_TAC std_ss [measure_space_def, sigma_algebra_def, DISJOINT_DEF, 1572 EXTENSION, IN_DIFF, IN_UNIV, IN_UNION, IN_INTER, 1573 NOT_IN_EMPTY] 1574 >> PROVE_TAC [COUNTABLY_ADDITIVE_ADDITIVE, ALGEBRA_COMPL, subsets_def, space_def, 1575 algebra_def, subset_class_def, SUBSET_DEF]); 1576 1577val SIGMA_PROPERTY = store_thm 1578 ("SIGMA_PROPERTY", 1579 ``!sp p a. 1580 subset_class sp p /\ {} IN p /\ a SUBSET p /\ 1581 (!s. s IN (p INTER subsets (sigma sp a)) ==> (sp DIFF s) IN p) /\ 1582 (!c. countable c /\ c SUBSET (p INTER subsets (sigma sp a)) ==> 1583 BIGUNION c IN p) ==> 1584 subsets (sigma sp a) SUBSET p``, 1585 RW_TAC std_ss [] 1586 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 1587 >- SIMP_TAC std_ss [SUBSET_INTER] 1588 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp,b)}` 1589 >- (KILL_TAC 1590 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def]) 1591 >> RW_TAC std_ss [GSPECIFICATION] 1592 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 1593 >> Know `subset_class sp a` >- PROVE_TAC [subset_class_def, SUBSET_DEF] 1594 >> STRIP_TAC 1595 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, 1596 SIGMA_ALGEBRA_SIGMA] 1597 >> STRIP_TAC 1598 >> RW_TAC std_ss [SIGMA_ALGEBRA, IN_INTER, space_def, subsets_def, SIGMA_ALGEBRA_ALGEBRA, 1599 ALGEBRA_EMPTY] 1600 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 1601 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 1602 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 1603 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1604 FULL_SIMP_TAC std_ss [sigma_algebra_def] 1605 >> Q.PAT_X_ASSUM `!c. P c ==> BIGUNION c IN subsets (sigma sp a)` MATCH_MP_TAC 1606 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_INTER]]); 1607 1608val MEASURE_EMPTY = store_thm 1609 ("MEASURE_EMPTY", 1610 ``!m. measure_space m ==> (measure m {} = 0)``, 1611 RW_TAC std_ss [measure_space_def, positive_def]); 1612 1613val SIGMA_SUBSET_MEASURABLE_SETS = store_thm 1614 ("SIGMA_SUBSET_MEASURABLE_SETS", 1615 ``!a m. 1616 measure_space m /\ a SUBSET measurable_sets m ==> 1617 subsets (sigma (m_space m) a) SUBSET measurable_sets m``, 1618 RW_TAC std_ss [measure_space_def] 1619 >> MATCH_MP_TAC SIGMA_PROPERTY 1620 >> RW_TAC std_ss [IN_INTER, SUBSET_INTER] 1621 >> PROVE_TAC [SIGMA_ALGEBRA, space_def, subsets_def]); 1622 1623val SIGMA_ALGEBRA_FN = store_thm 1624 ("SIGMA_ALGEBRA_FN", 1625 ``!a. 1626 sigma_algebra a = 1627 subset_class (space a) (subsets a) /\ 1628 {} IN subsets a /\ (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 1629 (!f : num -> 'a -> bool. 1630 f IN (UNIV -> subsets a) ==> BIGUNION (IMAGE f UNIV) IN subsets a)``, 1631 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_UNIV, SUBSET_DEF] 1632 >> EQ_TAC 1633 >- (RW_TAC std_ss [] 1634 >> Q.PAT_X_ASSUM `!c. P c ==> Q c` MATCH_MP_TAC 1635 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM, IN_IMAGE] 1636 >> PROVE_TAC []) 1637 >> RW_TAC std_ss [COUNTABLE_ENUM] 1638 >- RW_TAC std_ss [BIGUNION_EMPTY] 1639 >> Q.PAT_X_ASSUM `!f. (!x. P x f) ==> Q f` MATCH_MP_TAC 1640 >> POP_ASSUM MP_TAC 1641 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1642 >> PROVE_TAC []); 1643 1644val SIGMA_ALGEBRA_FN_DISJOINT = store_thm 1645 ("SIGMA_ALGEBRA_FN_DISJOINT", 1646 ``!a. 1647 sigma_algebra a = 1648 subset_class (space a) (subsets a) /\ 1649 {} IN subsets a /\ (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 1650 (!s t. s IN subsets a /\ t IN subsets a ==> s UNION t IN subsets a) /\ 1651 (!f : num -> 'a -> bool. 1652 f IN (UNIV -> subsets a) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 1653 BIGUNION (IMAGE f UNIV) IN subsets a)``, 1654 RW_TAC std_ss [SIGMA_ALGEBRA_ALT_DISJOINT, algebra_def] 1655 >> EQ_TAC 1656 >> RW_TAC std_ss []); 1657 1658val SIGMA_PROPERTY_ALT = store_thm 1659 ("SIGMA_PROPERTY_ALT", 1660 ``!sp p a. 1661 subset_class sp p /\ 1662 {} IN p /\ a SUBSET p /\ (!s. s IN (p INTER subsets (sigma sp a)) ==> sp DIFF s IN p) /\ 1663 (!f : num -> 'a -> bool. 1664 f IN (UNIV -> p INTER subsets (sigma sp a)) ==> BIGUNION (IMAGE f UNIV) IN p) ==> 1665 subsets (sigma sp a) SUBSET p``, 1666 RW_TAC std_ss [] 1667 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 1668 >- SIMP_TAC std_ss [SUBSET_INTER] 1669 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp, b)}` 1670 >- (KILL_TAC 1671 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def]) 1672 >> RW_TAC std_ss [GSPECIFICATION] 1673 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 1674 >> POP_ASSUM MP_TAC 1675 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, 1676 SIGMA_ALGEBRA_SIGMA] 1677 >> STRIP_TAC 1678 >> RW_TAC std_ss [SIGMA_ALGEBRA_FN, IN_INTER, FUNSET_INTER, subsets_def, space_def, 1679 SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY] 1680 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 1681 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 1682 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 1683 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1684 FULL_SIMP_TAC std_ss [(Q.SPEC `(sigma sp a)`) SIGMA_ALGEBRA_FN]]); 1685 1686val SIGMA_PROPERTY_DISJOINT_WEAK = store_thm 1687 ("SIGMA_PROPERTY_DISJOINT_WEAK", 1688 ``!sp p a. 1689 subset_class sp p /\ 1690 {} IN p /\ a SUBSET p /\ (!s. s IN (p INTER subsets (sigma sp a)) ==> (sp DIFF s) IN p) /\ 1691 (!s t. s IN p /\ t IN p ==> s UNION t IN p) /\ 1692 (!f : num -> 'a -> bool. 1693 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ 1694 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 1695 BIGUNION (IMAGE f UNIV) IN p) ==> 1696 subsets (sigma sp a) SUBSET p``, 1697 RW_TAC std_ss [] 1698 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 1699 >- SIMP_TAC std_ss [SUBSET_INTER] 1700 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp, b)}` 1701 >- (KILL_TAC 1702 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def, space_def]) 1703 >> RW_TAC std_ss [GSPECIFICATION] 1704 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 1705 >> POP_ASSUM MP_TAC 1706 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, 1707 SIGMA_ALGEBRA_SIGMA] 1708 >> STRIP_TAC 1709 >> RW_TAC std_ss [SIGMA_ALGEBRA_FN_DISJOINT, IN_INTER, FUNSET_INTER, subsets_def, space_def, 1710 SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY] 1711 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 1712 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 1713 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 1714 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1715 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 1716 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_UNION 1717 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 1718 FULL_SIMP_TAC std_ss [(Q.SPEC `(sigma sp a)`) SIGMA_ALGEBRA_FN_DISJOINT]]); 1719 1720val SPACE_SMALLEST_CLOSED_CDI = store_thm 1721 ("SPACE_SMALLEST_CLOSED_CDI", 1722 ``!a. space (smallest_closed_cdi a) = space a``, 1723 RW_TAC std_ss [smallest_closed_cdi_def, space_def]); 1724 1725val SMALLEST_CLOSED_CDI = store_thm 1726 ("SMALLEST_CLOSED_CDI", 1727 ``!a. algebra a ==> subsets a SUBSET subsets (smallest_closed_cdi a) /\ 1728 closed_cdi (smallest_closed_cdi a) /\ 1729 subset_class (space a) (subsets (smallest_closed_cdi a))``, 1730 Know `!a. algebra a ==> subsets a SUBSET subsets (smallest_closed_cdi a) /\ 1731 closed_cdi (smallest_closed_cdi a)` 1732 >- (RW_TAC std_ss [smallest_closed_cdi_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, 1733 subset_class_def, algebra_def, subsets_def] 1734 >> RW_TAC std_ss [closed_cdi_def, GSPECIFICATION, IN_BIGINTER, IN_FUNSET, 1735 IN_UNIV, subsets_def, space_def, subset_class_def] 1736 >> POP_ASSUM (MP_TAC o Q.SPEC `{x | x SUBSET space a}`) 1737 >> RW_TAC std_ss [GSPECIFICATION] 1738 >> POP_ASSUM MATCH_MP_TAC 1739 >> RW_TAC std_ss [SUBSET_DEF] 1740 >> PROVE_TAC [IN_DIFF, IN_BIGUNION, IN_IMAGE, IN_UNIV]) 1741 >> SIMP_TAC std_ss [] 1742 >> RW_TAC std_ss [closed_cdi_def, SPACE_SMALLEST_CLOSED_CDI]); 1743 1744val CLOSED_CDI_DUNION = store_thm 1745 ("CLOSED_CDI_DUNION", 1746 ``!p s t. 1747 {} IN subsets p /\ closed_cdi p /\ s IN subsets p /\ t IN subsets p /\ DISJOINT s t ==> 1748 s UNION t IN subsets p``, 1749 RW_TAC std_ss [closed_cdi_def] 1750 >> Q.PAT_X_ASSUM `!f. P f` 1751 (MP_TAC o Q.SPEC `\n. if n = 0 then s else if n = 1 then t else {}`) 1752 >> Know 1753 `BIGUNION 1754 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 1755 UNIV) = 1756 BIGUNION 1757 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 1758 (count 2))` 1759 >- (MATCH_MP_TAC BIGUNION_IMAGE_UNIV 1760 >> RW_TAC arith_ss []) 1761 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1762 >> RW_TAC bool_ss [COUNT_SUC, IMAGE_INSERT, TWO, ONE, BIGUNION_INSERT, 1763 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] 1764 >> ONCE_REWRITE_TAC [UNION_COMM] 1765 >> POP_ASSUM MATCH_MP_TAC 1766 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, DISJOINT_EMPTY] 1767 >> PROVE_TAC [DISJOINT_SYM]); 1768 1769val CLOSED_CDI_COMPL = store_thm 1770 ("CLOSED_CDI_COMPL", 1771 ``!p s. closed_cdi p /\ s IN subsets p ==> space p DIFF s IN subsets p``, 1772 RW_TAC std_ss [closed_cdi_def]); 1773 1774val CLOSED_CDI_DISJOINT = store_thm 1775 ("CLOSED_CDI_DISJOINT", 1776 ``!p f. 1777 closed_cdi p /\ f IN (UNIV -> subsets p) /\ 1778 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 1779 BIGUNION (IMAGE f UNIV) IN subsets p``, 1780 RW_TAC std_ss [closed_cdi_def]); 1781 1782val CLOSED_CDI_INCREASING = store_thm 1783 ("CLOSED_CDI_INCREASING", 1784 ``!p f. 1785 closed_cdi p /\ f IN (UNIV -> subsets p) /\ (f 0 = {}) /\ 1786 (!n. f n SUBSET f (SUC n)) ==> 1787 BIGUNION (IMAGE f UNIV) IN subsets p``, 1788 RW_TAC std_ss [closed_cdi_def]); 1789 1790val SIGMA_PROPERTY_DISJOINT_LEMMA1 = store_thm 1791 ("SIGMA_PROPERTY_DISJOINT_LEMMA1", 1792 ``!a. 1793 algebra a ==> 1794 (!s t. 1795 s IN subsets a /\ t IN subsets (smallest_closed_cdi a) ==> 1796 s INTER t IN subsets (smallest_closed_cdi a))``, 1797 RW_TAC std_ss [IN_BIGINTER, GSPECIFICATION, smallest_closed_cdi_def, subsets_def] 1798 >> Suff 1799 `t IN 1800 {b | b IN subsets (smallest_closed_cdi a) /\ s INTER b IN subsets (smallest_closed_cdi a)}` 1801 >- RW_TAC std_ss [GSPECIFICATION, IN_BIGINTER, smallest_closed_cdi_def, subsets_def] 1802 >> first_x_assum MATCH_MP_TAC 1803 >> STRONG_CONJ_TAC 1804 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_BIGINTER, 1805 smallest_closed_cdi_def, subsets_def] 1806 >> PROVE_TAC [ALGEBRA_INTER]) 1807 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, closed_cdi_def, space_def, subsets_def] >| 1808 [(MP_TAC o UNDISCH o Q.SPEC `a`) SMALLEST_CLOSED_CDI 1809 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, GSPECIFICATION] 1810 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF], 1811 PROVE_TAC [closed_cdi_def, SMALLEST_CLOSED_CDI, SPACE_SMALLEST_CLOSED_CDI], 1812 Know `s INTER (space a DIFF s') = 1813 space (smallest_closed_cdi a) DIFF 1814 (space (smallest_closed_cdi a) DIFF s UNION (s INTER s'))` 1815 >- (RW_TAC std_ss [EXTENSION, INTER_DEF, COMPL_DEF, UNION_DEF, GSPECIFICATION, IN_UNIV, 1816 IN_DIFF] 1817 >> PROVE_TAC [SPACE_SMALLEST_CLOSED_CDI]) 1818 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1819 >> MATCH_MP_TAC CLOSED_CDI_COMPL 1820 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1821 >> MATCH_MP_TAC CLOSED_CDI_DUNION 1822 >> CONJ_TAC 1823 >- PROVE_TAC [ALGEBRA_EMPTY, SMALLEST_CLOSED_CDI, SUBSET_DEF] 1824 >> CONJ_TAC >- RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1825 >> CONJ_TAC 1826 >- (MATCH_MP_TAC CLOSED_CDI_COMPL 1827 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI]) 1828 >> CONJ_TAC >- PROVE_TAC [SMALLEST_CLOSED_CDI, SUBSET_DEF] 1829 >> RW_TAC std_ss [DISJOINT_DEF, COMPL_DEF, INTER_DEF, IN_DIFF, IN_UNIV, GSPECIFICATION, 1830 EXTENSION, NOT_IN_EMPTY] 1831 >> DECIDE_TAC, 1832 Q.PAT_X_ASSUM `f IN x` MP_TAC 1833 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1834 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1835 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF], 1836 Know 1837 `s INTER BIGUNION (IMAGE f UNIV) = 1838 BIGUNION (IMAGE (\m. case m of 0 => {} | SUC n => s INTER f n) UNIV)` 1839 >- (KILL_TAC 1840 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1841 IN_INTER] 1842 >> (EQ_TAC >> RW_TAC std_ss [NOT_IN_EMPTY]) >| 1843 [Q.EXISTS_TAC `s INTER f x'` 1844 >> RW_TAC std_ss [IN_INTER] 1845 >> Q.EXISTS_TAC `SUC x'` 1846 >> RW_TAC arith_ss [IN_INTER, num_case_def], 1847 POP_ASSUM (MP_TAC) 1848 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1849 >> RW_TAC arith_ss [num_case_def, IN_INTER], 1850 POP_ASSUM (MP_TAC) 1851 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1852 >> RW_TAC arith_ss [num_case_def, IN_INTER] 1853 >> Q.EXISTS_TAC `f n` 1854 >> RW_TAC std_ss [] 1855 >> PROVE_TAC []]) 1856 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1857 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1858 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1859 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1860 >- (REVERSE (Cases_on `m`) >- RW_TAC arith_ss [] 1861 >> RW_TAC arith_ss [] 1862 >> PROVE_TAC [SMALLEST_CLOSED_CDI, ALGEBRA_EMPTY, SUBSET_DEF]) 1863 >> Cases_on `n` >- RW_TAC arith_ss [num_case_def, EMPTY_SUBSET] 1864 >> RW_TAC arith_ss [num_case_def, SUBSET_DEF, IN_INTER], 1865 Q.PAT_X_ASSUM `f IN x` MP_TAC 1866 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1867 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 1868 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF], 1869 Know 1870 `s INTER BIGUNION (IMAGE f UNIV) = 1871 BIGUNION (IMAGE (\n. s INTER f n) UNIV)` 1872 >- (KILL_TAC 1873 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1874 IN_INTER] 1875 >> (EQ_TAC >> RW_TAC std_ss []) >| 1876 [Q.EXISTS_TAC `s INTER f x'` 1877 >> RW_TAC std_ss [IN_INTER] 1878 >> Q.EXISTS_TAC `x'` 1879 >> RW_TAC arith_ss [IN_INTER], 1880 POP_ASSUM (MP_TAC) 1881 >> RW_TAC arith_ss [IN_INTER], 1882 POP_ASSUM (MP_TAC) 1883 >> RW_TAC arith_ss [IN_INTER] 1884 >> Q.EXISTS_TAC `f n` 1885 >> RW_TAC std_ss [] 1886 >> PROVE_TAC []]) 1887 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1888 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 1889 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1890 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1891 >> Q.PAT_X_ASSUM `!m n. PP m n` (MP_TAC o Q.SPECL [`m`, `n`]) 1892 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 1893 >> PROVE_TAC []]); 1894 1895val SIGMA_PROPERTY_DISJOINT_LEMMA2 = store_thm 1896 ("SIGMA_PROPERTY_DISJOINT_LEMMA2", 1897 ``!a. 1898 algebra a ==> 1899 (!s t. 1900 s IN subsets (smallest_closed_cdi a) /\ t IN subsets (smallest_closed_cdi a) ==> 1901 s INTER t IN subsets (smallest_closed_cdi a))``, 1902 RW_TAC std_ss [] 1903 >> POP_ASSUM MP_TAC 1904 >> SIMP_TAC std_ss [smallest_closed_cdi_def, IN_BIGINTER, GSPECIFICATION, subsets_def] 1905 >> STRIP_TAC >> Q.X_GEN_TAC `P` 1906 >> Suff 1907 `t IN 1908 {b | b IN subsets (smallest_closed_cdi a) /\ s INTER b IN subsets (smallest_closed_cdi a)}` 1909 >- RW_TAC std_ss [GSPECIFICATION, IN_BIGINTER, smallest_closed_cdi_def, subsets_def] 1910 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 1911 >> STRONG_CONJ_TAC 1912 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION] >| 1913 [PROVE_TAC [SMALLEST_CLOSED_CDI, SUBSET_DEF], 1914 PROVE_TAC [SIGMA_PROPERTY_DISJOINT_LEMMA1, INTER_COMM]]) 1915 >> SIMP_TAC std_ss [GSPECIFICATION, SUBSET_DEF, closed_cdi_def, space_def, subsets_def] 1916 >> STRIP_TAC >> REPEAT CONJ_TAC >| 1917 [(MP_TAC o UNDISCH o Q.SPEC `a`) SMALLEST_CLOSED_CDI 1918 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, GSPECIFICATION] 1919 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF], 1920 Q.X_GEN_TAC `s'` 1921 >> REPEAT STRIP_TAC 1922 >- PROVE_TAC [closed_cdi_def, SMALLEST_CLOSED_CDI, 1923 SPACE_SMALLEST_CLOSED_CDI] 1924 >> Know `s INTER (space a DIFF s') = 1925 space (smallest_closed_cdi a) DIFF 1926 (space (smallest_closed_cdi a) DIFF s UNION (s INTER s'))` 1927 >- (RW_TAC std_ss [EXTENSION, INTER_DEF, COMPL_DEF, UNION_DEF, GSPECIFICATION, IN_UNIV, 1928 IN_DIFF, SPACE_SMALLEST_CLOSED_CDI] 1929 >> DECIDE_TAC) 1930 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1931 >> MATCH_MP_TAC CLOSED_CDI_COMPL 1932 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1933 >> MATCH_MP_TAC CLOSED_CDI_DUNION 1934 >> CONJ_TAC 1935 >- PROVE_TAC [ALGEBRA_EMPTY, SMALLEST_CLOSED_CDI, SUBSET_DEF] 1936 >> CONJ_TAC >- RW_TAC std_ss [SMALLEST_CLOSED_CDI] 1937 >> CONJ_TAC 1938 >- (MATCH_MP_TAC CLOSED_CDI_COMPL 1939 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI]) 1940 >> CONJ_TAC >- PROVE_TAC [SMALLEST_CLOSED_CDI, SUBSET_DEF] 1941 >> RW_TAC std_ss [DISJOINT_DEF, COMPL_DEF, INTER_DEF, IN_DIFF, IN_UNIV, GSPECIFICATION, 1942 EXTENSION, NOT_IN_EMPTY] 1943 >> DECIDE_TAC, 1944 Q.X_GEN_TAC `f` >> REPEAT STRIP_TAC 1945 >- (Q.PAT_X_ASSUM `f IN x` MP_TAC 1946 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1947 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1948 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF]) 1949 >> Know 1950 `s INTER BIGUNION (IMAGE f UNIV) = 1951 BIGUNION (IMAGE (\m. case m of 0 => {} | SUC n => s INTER f n) UNIV)` 1952 >- (KILL_TAC 1953 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1954 IN_INTER] 1955 >> (EQ_TAC >> RW_TAC std_ss [NOT_IN_EMPTY]) >| 1956 [Q.EXISTS_TAC `s INTER f x'` 1957 >> RW_TAC std_ss [IN_INTER] 1958 >> Q.EXISTS_TAC `SUC x'` 1959 >> RW_TAC arith_ss [IN_INTER, num_case_def], 1960 POP_ASSUM (MP_TAC) 1961 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1962 >> RW_TAC arith_ss [num_case_def, IN_INTER], 1963 POP_ASSUM (MP_TAC) 1964 >> Cases_on `m` >- RW_TAC arith_ss [num_case_def, NOT_IN_EMPTY] 1965 >> RW_TAC arith_ss [num_case_def, IN_INTER] 1966 >> Q.EXISTS_TAC `f n` 1967 >> RW_TAC std_ss [] 1968 >> PROVE_TAC []]) 1969 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1970 >> MATCH_MP_TAC CLOSED_CDI_INCREASING 1971 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1972 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1973 >- (REVERSE (Cases_on `m`) >- RW_TAC arith_ss [] 1974 >> RW_TAC arith_ss [] 1975 >> PROVE_TAC [SMALLEST_CLOSED_CDI, ALGEBRA_EMPTY, SUBSET_DEF]) 1976 >> Cases_on `n` >- RW_TAC arith_ss [num_case_def, EMPTY_SUBSET] 1977 >> RW_TAC arith_ss [num_case_def, SUBSET_DEF, IN_INTER], 1978 Q.X_GEN_TAC `f` >> REPEAT STRIP_TAC 1979 >- (Q.PAT_X_ASSUM `f IN x` MP_TAC 1980 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1981 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 1982 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF]) 1983 >> Know 1984 `s INTER BIGUNION (IMAGE f UNIV) = 1985 BIGUNION (IMAGE (\n. s INTER f n) UNIV)` 1986 >- (KILL_TAC 1987 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1988 IN_INTER] 1989 >> (EQ_TAC >> RW_TAC std_ss []) >| 1990 [Q.EXISTS_TAC `s INTER f x'` 1991 >> RW_TAC std_ss [IN_INTER] 1992 >> Q.EXISTS_TAC `x'` 1993 >> RW_TAC arith_ss [IN_INTER], 1994 POP_ASSUM (MP_TAC) 1995 >> RW_TAC arith_ss [IN_INTER], 1996 POP_ASSUM (MP_TAC) 1997 >> RW_TAC arith_ss [IN_INTER] 1998 >> Q.EXISTS_TAC `f n` 1999 >> RW_TAC std_ss [] 2000 >> PROVE_TAC []]) 2001 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2002 >> MATCH_MP_TAC CLOSED_CDI_DISJOINT 2003 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 2004 >> RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, IN_UNIV, GSPECIFICATION] 2005 >> Q.PAT_X_ASSUM `!m n. PP m n` (MP_TAC o Q.SPECL [`m`, `n`]) 2006 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 2007 >> PROVE_TAC []]); 2008 2009val SIGMA_PROPERTY_DISJOINT_LEMMA = store_thm 2010 ("SIGMA_PROPERTY_DISJOINT_LEMMA", 2011 ``!sp a p. algebra (sp, a) /\ a SUBSET p /\ closed_cdi (sp, p) 2012 ==> subsets (sigma sp a) SUBSET p``, 2013 RW_TAC std_ss [] 2014 >> MATCH_MP_TAC SUBSET_TRANS 2015 >> Q.EXISTS_TAC `subsets (smallest_closed_cdi (sp, a))` 2016 >> REVERSE CONJ_TAC 2017 >- (RW_TAC std_ss [SUBSET_DEF, smallest_closed_cdi_def, IN_BIGINTER, 2018 GSPECIFICATION, subsets_def, space_def] 2019 >> PROVE_TAC [SUBSET_DEF]) 2020 >> NTAC 2 (POP_ASSUM K_TAC) 2021 >> Suff `subsets (smallest_closed_cdi (sp, a)) IN {b | a SUBSET b /\ sigma_algebra (sp,b)}` 2022 >- (KILL_TAC 2023 >> RW_TAC std_ss [sigma_def, BIGINTER, SUBSET_DEF, GSPECIFICATION,subsets_def]) 2024 >> RW_TAC std_ss [GSPECIFICATION, SIGMA_ALGEBRA_ALT_DISJOINT, 2025 ALGEBRA_ALT_INTER, space_def, subsets_def] >| 2026 [PROVE_TAC [SMALLEST_CLOSED_CDI, subsets_def], 2027 PROVE_TAC [SMALLEST_CLOSED_CDI, space_def], 2028 PROVE_TAC [ALGEBRA_EMPTY, SUBSET_DEF, SMALLEST_CLOSED_CDI, space_def], 2029 PROVE_TAC [SMALLEST_CLOSED_CDI, CLOSED_CDI_COMPL, space_def, SPACE_SMALLEST_CLOSED_CDI], 2030 PROVE_TAC [SIGMA_PROPERTY_DISJOINT_LEMMA2], 2031 PROVE_TAC [SMALLEST_CLOSED_CDI, CLOSED_CDI_DISJOINT]]); 2032 2033val SIGMA_PROPERTY_DISJOINT_WEAK = store_thm 2034 ("SIGMA_PROPERTY_DISJOINT_WEAK", 2035 ``!sp p a. 2036 algebra (sp, a) /\ a SUBSET p /\ 2037 subset_class sp p /\ 2038 (!s. s IN p ==> sp DIFF s IN p) /\ 2039 (!f : num -> 'a -> bool. 2040 f IN (UNIV -> p) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 2041 BIGUNION (IMAGE f UNIV) IN p) /\ 2042 (!f : num -> 'a -> bool. 2043 f IN (UNIV -> p) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 2044 BIGUNION (IMAGE f UNIV) IN p) ==> 2045 subsets (sigma sp a) SUBSET p``, 2046 RW_TAC std_ss [] 2047 >> MATCH_MP_TAC (Q.SPECL [`sp`, `a`, `p`] SIGMA_PROPERTY_DISJOINT_LEMMA) 2048 >> RW_TAC std_ss [closed_cdi_def, space_def, subsets_def]); 2049 2050val SIGMA_PROPERTY_DISJOINT = store_thm 2051 ("SIGMA_PROPERTY_DISJOINT", 2052 ``!sp p a. 2053 algebra (sp,a) /\ a SUBSET p /\ 2054 (!s. s IN (p INTER subsets (sigma sp a)) ==> sp DIFF s IN p) /\ 2055 (!f : num -> 'a -> bool. 2056 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ (f 0 = {}) /\ 2057 (!n. f n SUBSET f (SUC n)) ==> 2058 BIGUNION (IMAGE f UNIV) IN p) /\ 2059 (!f : num -> 'a -> bool. 2060 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ 2061 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 2062 BIGUNION (IMAGE f UNIV) IN p) ==> 2063 subsets (sigma sp a) SUBSET p``, 2064 RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_INTER] 2065 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 2066 >- (KILL_TAC 2067 >> SIMP_TAC std_ss [SUBSET_INTER]) 2068 >> MATCH_MP_TAC 2069 (Q.SPECL [`sp`, `p INTER subsets (sigma sp a)`, `a`] SIGMA_PROPERTY_DISJOINT_WEAK) 2070 >> RW_TAC std_ss [SUBSET_INTER, IN_INTER, IN_FUNSET, IN_UNIV] >| 2071 [PROVE_TAC [SUBSET_DEF, IN_SIGMA], 2072 (MP_TAC o Q.SPECL [`sp`,`a`]) SIGMA_ALGEBRA_SIGMA 2073 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2074 >> RW_TAC std_ss [algebra_def, space_def, subsets_def] 2075 >> POP_ASSUM MP_TAC 2076 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 2077 >> RW_TAC std_ss [sigma_algebra_def, algebra_def, space_def, subsets_def] 2078 >> NTAC 4 (POP_ASSUM (K ALL_TAC)) 2079 >> POP_ASSUM MP_TAC 2080 >> Know `space (sigma sp a) = sp` >- RW_TAC std_ss [sigma_def, space_def] 2081 >> RW_TAC std_ss [subset_class_def, IN_INTER], 2082 (MP_TAC o Q.SPECL [`sp`,`a`]) SIGMA_ALGEBRA_SIGMA 2083 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2084 >> RW_TAC std_ss [algebra_def, space_def, subsets_def] 2085 >> POP_ASSUM MP_TAC 2086 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 2087 >> Know `space (sigma sp a) = sp` >- RW_TAC std_ss [sigma_def, space_def] 2088 >> RW_TAC std_ss [SIGMA_ALGEBRA, algebra_def, subsets_def, space_def], 2089 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION 2090 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2091 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, COUNTABLE_IMAGE_NUM, SUBSET_DEF, 2092 IN_IMAGE, IN_UNIV, algebra_def, subsets_def, space_def] 2093 >> PROVE_TAC [], 2094 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION 2095 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 2096 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, COUNTABLE_IMAGE_NUM, SUBSET_DEF, 2097 IN_IMAGE, IN_UNIV, algebra_def, subsets_def, space_def] 2098 >> PROVE_TAC []]); 2099 2100val MEASURE_COUNTABLY_ADDITIVE = store_thm 2101 ("MEASURE_COUNTABLY_ADDITIVE", 2102 ``!m s f. 2103 measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 2104 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 2105 (s = BIGUNION (IMAGE f UNIV)) ==> 2106 measure m o f sums measure m s``, 2107 RW_TAC std_ss [] 2108 >> MATCH_MP_TAC COUNTABLY_ADDITIVE 2109 >> RW_TAC std_ss [] 2110 >- PROVE_TAC [measure_space_def] 2111 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 2112 Q.SPEC `(m_space m, measurable_sets m)`) SIGMA_ALGEBRA_COUNTABLE_UNION 2113 >> CONJ_TAC >- PROVE_TAC [measure_space_def] 2114 >> Q.PAT_X_ASSUM `f IN P` MP_TAC 2115 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM, SUBSET_DEF, IN_IMAGE, IN_UNIV, 2116 IN_FUNSET] 2117 >> PROVE_TAC []); 2118 2119val MEASURE_SPACE_ADDITIVE = store_thm 2120 ("MEASURE_SPACE_ADDITIVE", 2121 ``!m. measure_space m ==> additive m``, 2122 RW_TAC std_ss [] 2123 >> MATCH_MP_TAC COUNTABLY_ADDITIVE_ADDITIVE 2124 >> PROVE_TAC [measure_space_def, SIGMA_ALGEBRA_ALGEBRA]); 2125 2126val MEASURE_ADDITIVE = store_thm 2127 ("MEASURE_ADDITIVE", 2128 ``!m s t u. 2129 measure_space m /\ s IN measurable_sets m /\ t IN measurable_sets m /\ 2130 DISJOINT s t /\ (u = s UNION t) ==> 2131 (measure m u = measure m s + measure m t)``, 2132 RW_TAC std_ss [] 2133 >> MATCH_MP_TAC ADDITIVE 2134 >> RW_TAC std_ss [MEASURE_SPACE_ADDITIVE]); 2135 2136val MEASURE_COUNTABLE_INCREASING = store_thm 2137 ("MEASURE_COUNTABLE_INCREASING", 2138 ``!m s f. 2139 measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 2140 (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) /\ 2141 (s = BIGUNION (IMAGE f UNIV)) ==> 2142 measure m o f --> measure m s``, 2143 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 2144 >> Know 2145 `measure m o f = (\n. sum (0, n) (measure m o (\m. f (SUC m) DIFF f m)))` 2146 >- (RW_TAC std_ss [FUN_EQ_THM] 2147 >> Induct_on `n` >- RW_TAC std_ss [o_THM, sum, MEASURE_EMPTY] 2148 >> POP_ASSUM (MP_TAC o SYM) 2149 >> RW_TAC arith_ss [o_THM, sum] 2150 >> MATCH_MP_TAC MEASURE_ADDITIVE 2151 >> FULL_SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_DIFF, DISJOINT_DEF, NOT_IN_EMPTY, 2152 IN_INTER, SUBSET_DEF] 2153 >> Know `algebra (m_space m, measurable_sets m)` 2154 >- FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, 2155 space_def, subsets_def] 2156 >> STRIP_TAC 2157 >> (MP_TAC o REWRITE_RULE [subsets_def, space_def] o 2158 Q.SPEC `(m_space m, measurable_sets m)`) ALGEBRA_DIFF 2159 >> PROVE_TAC []) 2160 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2161 >> RW_TAC std_ss [GSYM sums] 2162 >> MATCH_MP_TAC COUNTABLY_ADDITIVE 2163 >> CONJ_TAC >- PROVE_TAC [measure_space_def] 2164 >> CONJ_TAC 2165 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV] 2166 >> Know `algebra (m_space m, measurable_sets m)` 2167 >- FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, 2168 space_def, subsets_def] 2169 >> STRIP_TAC 2170 >> (MP_TAC o REWRITE_RULE [subsets_def, space_def] o 2171 Q.SPEC `(m_space m, measurable_sets m)`) ALGEBRA_DIFF 2172 >> PROVE_TAC []) 2173 >> CONJ_TAC 2174 >- (REPEAT STRIP_TAC 2175 >> MATCH_MP_TAC DISJOINT_DIFFS 2176 >> Q.EXISTS_TAC `f` 2177 >> RW_TAC std_ss []) 2178 >> CONJ_TAC 2179 >- (FULL_SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_DIFF, DISJOINT_DEF, NOT_IN_EMPTY, IN_INTER, 2180 SUBSET_DEF, IN_BIGUNION, IN_IMAGE, IN_UNIV, DIFF_DEF] 2181 >> STRIP_TAC 2182 >> REVERSE (EQ_TAC >> RW_TAC std_ss []) 2183 >- PROVE_TAC [] 2184 >> Know `x IN f x'` >- PROVE_TAC [] 2185 >> NTAC 2 (POP_ASSUM K_TAC) 2186 >> Induct_on `x'` >- RW_TAC std_ss [] 2187 >> POP_ASSUM MP_TAC 2188 >> Cases_on `x IN f x'` >- RW_TAC std_ss [] 2189 >> RW_TAC std_ss [] 2190 >> Q.EXISTS_TAC `f (SUC x') DIFF f x'` 2191 >> RW_TAC std_ss [EXTENSION, DIFF_DEF, GSPECIFICATION] 2192 >> PROVE_TAC []) 2193 >> (MATCH_MP_TAC o REWRITE_RULE [subsets_def, space_def] o 2194 Q.SPEC `(m_space m, measurable_sets m)`) SIGMA_ALGEBRA_COUNTABLE_UNION 2195 >> CONJ_TAC >- PROVE_TAC [measure_space_def] 2196 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM] 2197 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV] 2198 >> PROVE_TAC []); 2199 2200val MEASURE_SPACE_REDUCE = store_thm 2201 ("MEASURE_SPACE_REDUCE", 2202 ``!m. (m_space m, measurable_sets m, measure m) = m``, 2203 Cases 2204 >> Q.SPEC_TAC (`r`, `r`) 2205 >> Cases 2206 >> RW_TAC std_ss [m_space_def, measurable_sets_def, measure_def]); 2207 2208val SPACE_SIGMA = store_thm 2209 ("SPACE_SIGMA", 2210 ``!sp a. space (sigma sp a) = sp``, 2211 RW_TAC std_ss [sigma_def, space_def]); 2212 2213val MONOTONE_CONVERGENCE = store_thm 2214 ("MONOTONE_CONVERGENCE", 2215 ``!m s f. 2216 measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 2217 (!n. f n SUBSET f (SUC n)) /\ 2218 (s = BIGUNION (IMAGE f UNIV)) ==> 2219 measure m o f --> measure m s``, 2220 RW_TAC std_ss [measure_space_def, IN_FUNSET, IN_UNIV] 2221 >> (MP_TAC o 2222 INST_TYPE [beta |-> ``:num``] o 2223 Q.SPECL [`m`, `BIGUNION (IMAGE f UNIV)`, `\x. num_CASE x {} f`]) 2224 MEASURE_COUNTABLE_INCREASING 2225 >> Cond 2226 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV, num_case_def, measure_space_def] >| 2227 [Cases_on `x` >| 2228 [RW_TAC std_ss [num_case_def] 2229 >> PROVE_TAC [SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY, subsets_def], 2230 RW_TAC std_ss [num_case_def]], 2231 Cases_on `n` 2232 >> RW_TAC std_ss [num_case_def, EMPTY_SUBSET], 2233 RW_TAC std_ss [EXTENSION,GSPECIFICATION] 2234 >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV] 2235 >> EQ_TAC >| 2236 [RW_TAC std_ss [] 2237 >> Q.EXISTS_TAC `SUC x'` 2238 >> RW_TAC std_ss [num_case_def], 2239 RW_TAC std_ss [] 2240 >> POP_ASSUM MP_TAC 2241 >> Cases_on `x'` >- RW_TAC std_ss [NOT_IN_EMPTY, num_case_def] 2242 >> RW_TAC std_ss [num_case_def] 2243 >> PROVE_TAC []]]) 2244 >> RW_TAC std_ss [] 2245 >> Know `measure m o f = (\n. (measure m o (\x. num_CASE x {} f)) (SUC n))` 2246 >- (RW_TAC std_ss [FUN_EQ_THM] 2247 >> RW_TAC std_ss [num_case_def, o_THM]) 2248 >> Rewr 2249 >> Ho_Rewrite.REWRITE_TAC [GSYM SEQ_SUC] 2250 >> RW_TAC std_ss' []); 2251 2252val SIGMA_REDUCE = store_thm 2253 ("SIGMA_REDUCE", 2254 ``!sp a. (sp, subsets (sigma sp a)) = sigma sp a``, 2255 PROVE_TAC [SPACE_SIGMA, SPACE]); 2256 2257val MEASURABLE_SETS_SUBSET_SPACE = store_thm 2258 ("MEASURABLE_SETS_SUBSET_SPACE", 2259 ``!m s. measure_space m /\ s IN measurable_sets m ==> 2260 s SUBSET m_space m``, 2261 RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, subsets_def, space_def, 2262 subset_class_def]); 2263 2264val MEASURABLE_DIFF_PROPERTY = store_thm 2265 ("MEASURABLE_DIFF_PROPERTY", 2266 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2267 f IN (space a -> space b) /\ 2268 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2269 (!s. s IN subsets b ==> 2270 (PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s))``, 2271 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def, GSPECIFICATION, 2272 PREIMAGE_DIFF, IN_IMAGE] 2273 >> MATCH_MP_TAC SUBSET_ANTISYM 2274 >> RW_TAC std_ss [SUBSET_DEF, IN_DIFF, IN_PREIMAGE] 2275 >> Q.PAT_X_ASSUM `!s. s IN subsets b ==> PREIMAGE f s IN subsets a` 2276 (MP_TAC o Q.SPEC `space b DIFF s`) 2277 >> Know `x IN PREIMAGE f (space b DIFF s)` 2278 >- RW_TAC std_ss [IN_PREIMAGE, IN_DIFF] 2279 >> PROVE_TAC [subset_class_def, SUBSET_DEF]); 2280 2281val MEASURABLE_BIGUNION_PROPERTY = store_thm 2282 ("MEASURABLE_BIGUNION_PROPERTY", 2283 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2284 f IN (space a -> space b) /\ 2285 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2286 (!c. c SUBSET subsets b ==> 2287 (PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c)))``, 2288 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def, GSPECIFICATION, 2289 PREIMAGE_BIGUNION, IN_IMAGE]); 2290 2291val MEASUBABLE_BIGUNION_LEMMA = store_thm 2292 ("MEASUBABLE_BIGUNION_LEMMA", 2293 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2294 f IN (space a -> space b) /\ 2295 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2296 (!c. countable c /\ c SUBSET (IMAGE (PREIMAGE f) (subsets b)) ==> 2297 BIGUNION c IN IMAGE (PREIMAGE f) (subsets b))``, 2298 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_IMAGE] 2299 >> Q.EXISTS_TAC `BIGUNION (IMAGE (\x. @x'. x' IN subsets b /\ (PREIMAGE f x' = x)) c)` 2300 >> REVERSE CONJ_TAC 2301 >- (Q.PAT_X_ASSUM `!c. countable c /\ c SUBSET subsets b ==> BIGUNION c IN subsets b` 2302 MATCH_MP_TAC 2303 >> RW_TAC std_ss [image_countable, SUBSET_DEF, IN_IMAGE] 2304 >> Suff `(\x''. x'' IN subsets b) (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = x'))` 2305 >- RW_TAC std_ss [] 2306 >> MATCH_MP_TAC SELECT_ELIM_THM 2307 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2308 >> PROVE_TAC []) 2309 >> RW_TAC std_ss [PREIMAGE_BIGUNION, IMAGE_IMAGE] 2310 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_IMAGE] 2311 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2312 >> EQ_TAC 2313 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `s` >> ASM_REWRITE_TAC [] 2314 >> Q.PAT_X_ASSUM `!x. x IN c ==> ?x'. (x = PREIMAGE f x') /\ x' IN subsets b` 2315 (MP_TAC o Q.SPEC `s`) 2316 >> RW_TAC std_ss [] 2317 >> Q.EXISTS_TAC `PREIMAGE f x'` >> ASM_REWRITE_TAC [] 2318 >> Suff `(\x''. PREIMAGE f x' = PREIMAGE f x'') 2319 (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = PREIMAGE f x'))` 2320 >- METIS_TAC [] 2321 >> MATCH_MP_TAC SELECT_ELIM_THM 2322 >> PROVE_TAC []) 2323 >> RW_TAC std_ss [] 2324 >> Q.EXISTS_TAC `x'` 2325 >> ASM_REWRITE_TAC [] 2326 >> Know `(\x''. x IN PREIMAGE f x'' ==> x IN x') 2327 (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = x'))` 2328 >- (MATCH_MP_TAC SELECT_ELIM_THM 2329 >> RW_TAC std_ss [] 2330 >> PROVE_TAC []) 2331 >> RW_TAC std_ss []); 2332 2333val MEASURABLE_SIGMA_PREIMAGES = store_thm 2334 ("MEASURABLE_SIGMA_PREIMAGES", 2335 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2336 f IN (space a -> space b) /\ 2337 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2338 sigma_algebra (space a, IMAGE (PREIMAGE f) (subsets b))``, 2339 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def] 2340 >| [FULL_SIMP_TAC std_ss [subset_class_def, GSPECIFICATION, IN_IMAGE] 2341 >> PROVE_TAC [], 2342 RW_TAC std_ss [IN_IMAGE] 2343 >> Q.EXISTS_TAC `{}` 2344 >> RW_TAC std_ss [PREIMAGE_EMPTY], 2345 RW_TAC std_ss [IN_IMAGE, PREIMAGE_DIFF] 2346 >> FULL_SIMP_TAC std_ss [IN_IMAGE] 2347 >> Q.EXISTS_TAC `space b DIFF x` 2348 >> RW_TAC std_ss [PREIMAGE_DIFF] 2349 >> MATCH_MP_TAC SUBSET_ANTISYM 2350 >> RW_TAC std_ss [SUBSET_DEF, IN_DIFF, IN_PREIMAGE] 2351 >> Q.PAT_X_ASSUM `!s. s IN subsets b ==> PREIMAGE f s IN subsets a` 2352 (MP_TAC o Q.SPEC `space b DIFF x`) 2353 >> Know `x' IN PREIMAGE f (space b DIFF x)` 2354 >- RW_TAC std_ss [IN_PREIMAGE, IN_DIFF] 2355 >> PROVE_TAC [subset_class_def, SUBSET_DEF], 2356 (MP_TAC o REWRITE_RULE [IN_FUNSET, SIGMA_ALGEBRA] o Q.SPECL [`a`, `b`, `f`]) 2357 MEASUBABLE_BIGUNION_LEMMA 2358 >> RW_TAC std_ss []]); 2359 2360val IN_MEASURABLE = store_thm 2361 ("IN_MEASURABLE", 2362 ``!a b f. f IN measurable a b = 2363 sigma_algebra a /\ 2364 sigma_algebra b /\ 2365 f IN (space a -> space b) /\ 2366 (!s. s IN subsets b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a)``, 2367 RW_TAC std_ss [measurable_def, GSPECIFICATION]); 2368 2369val MEASURABLE_SIGMA = store_thm 2370 ("MEASURABLE_SIGMA", 2371 ``!f a b sp. 2372 sigma_algebra a /\ 2373 subset_class sp b /\ 2374 f IN (space a -> sp) /\ 2375 (!s. s IN b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a) 2376 ==> 2377 f IN measurable a (sigma sp b)``, 2378 RW_TAC std_ss [] 2379 >> REWRITE_TAC [IN_MEASURABLE] 2380 >> CONJ_TAC >- FULL_SIMP_TAC std_ss [sigma_def, space_def] 2381 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, SPACE_SIGMA, subsets_def, GSPECIFICATION] 2382 >> Know `subsets (sigma sp b) SUBSET {x' | ((PREIMAGE f x')INTER(space a)) IN subsets a /\ 2383 x' SUBSET sp}` 2384 >- (MATCH_MP_TAC SIGMA_PROPERTY 2385 >> RW_TAC std_ss [subset_class_def, GSPECIFICATION, IN_INTER, EMPTY_SUBSET, 2386 PREIMAGE_EMPTY, PREIMAGE_DIFF, SUBSET_INTER, SIGMA_ALGEBRA, 2387 DIFF_SUBSET, SUBSET_DEF, NOT_IN_EMPTY, IN_DIFF, 2388 PREIMAGE_BIGUNION, IN_BIGUNION] 2389 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, INTER_EMPTY], 2390 PROVE_TAC [subset_class_def, SUBSET_DEF], 2391 Know `(PREIMAGE f sp DIFF PREIMAGE f s') INTER space a = 2392 (PREIMAGE f sp INTER space a) DIFF (PREIMAGE f s' INTER space a)` 2393 >- (RW_TAC std_ss [Once EXTENSION, IN_DIFF, IN_INTER, IN_PREIMAGE] >> DECIDE_TAC) 2394 >> RW_TAC std_ss [] 2395 >> Know `PREIMAGE f sp INTER space a = space a` 2396 >- (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] >> METIS_TAC [IN_FUNSET]) 2397 >> FULL_SIMP_TAC std_ss [sigma_algebra_def, ALGEBRA_COMPL], 2398 FULL_SIMP_TAC std_ss [sigma_algebra_def] 2399 >> `BIGUNION (IMAGE (PREIMAGE f) c) INTER space a = 2400 BIGUNION (IMAGE (\x. (PREIMAGE f x) INTER (space a)) c)` 2401 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE] 2402 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 2403 >> EQ_TAC 2404 >- (RW_TAC std_ss [] 2405 >> Q.EXISTS_TAC `PREIMAGE f x' INTER space a` 2406 >> ASM_REWRITE_TAC [IN_INTER] 2407 >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 2408 >> RW_TAC std_ss [] >> METIS_TAC [IN_INTER, IN_PREIMAGE]) 2409 >> RW_TAC std_ss [] 2410 >> Q.PAT_X_ASSUM `!c. countable c /\ c SUBSET subsets a ==> 2411 BIGUNION c IN subsets a` MATCH_MP_TAC 2412 >> RW_TAC std_ss [image_countable, SUBSET_DEF, IN_IMAGE] 2413 >> PROVE_TAC [], 2414 PROVE_TAC []]) 2415 >> RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION]); 2416 2417val MEASURABLE_SUBSET = store_thm 2418 ("MEASURABLE_SUBSET", 2419 ``!a b. measurable a b SUBSET measurable a (sigma (space b) (subsets b))``, 2420 RW_TAC std_ss [SUBSET_DEF] 2421 >> MATCH_MP_TAC MEASURABLE_SIGMA 2422 >> FULL_SIMP_TAC std_ss [IN_MEASURABLE, SIGMA_ALGEBRA, space_def, subsets_def]); 2423 2424val MEASURABLE_LIFT = store_thm 2425 ("MEASURABLE_LIFT", 2426 ``!f a b. 2427 f IN measurable a b ==> f IN measurable a (sigma (space b) (subsets b))``, 2428 PROVE_TAC [MEASURABLE_SUBSET, SUBSET_DEF]); 2429 2430val IN_MEASURE_PRESERVING = store_thm 2431 ("IN_MEASURE_PRESERVING", 2432 ``!m1 m2 f. 2433 f IN measure_preserving m1 m2 = 2434 f IN measurable (m_space m1, measurable_sets m1) (m_space m2, measurable_sets m2) /\ 2435 measure_space m1 /\ measure_space m2 /\ 2436 !s. 2437 s IN measurable_sets m2 ==> 2438 (measure m1 ((PREIMAGE f s)INTER(m_space m1)) = measure m2 s)``, 2439 RW_TAC std_ss [measure_preserving_def, GSPECIFICATION]); 2440 2441val MEASURE_PRESERVING_LIFT = store_thm 2442 ("MEASURE_PRESERVING_LIFT", 2443 ``!m1 m2 a f. 2444 measure_space m1 /\ measure_space m2 /\ 2445 (measurable_sets m2 = subsets (sigma (m_space m2) a)) /\ 2446 f IN measure_preserving m1 (m_space m2, a, measure m2) ==> 2447 f IN measure_preserving m1 m2``, 2448 RW_TAC std_ss [] 2449 >> REVERSE (Cases_on `algebra (m_space m2, a)`) 2450 >- FULL_SIMP_TAC std_ss [IN_MEASURE_PRESERVING, IN_MEASURABLE, m_space_def, 2451 measurable_sets_def, sigma_algebra_def] 2452 >> Suff `f IN measure_preserving m1 (m_space m2, measurable_sets m2, measure m2)` 2453 >- RW_TAC std_ss [MEASURE_SPACE_REDUCE] 2454 >> ASM_REWRITE_TAC [] 2455 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 2456 >> REWRITE_TAC [IN_MEASURE_PRESERVING, measurable_sets_def, measure_def, m_space_def] 2457 >> STRIP_TAC 2458 >> STRONG_CONJ_TAC 2459 >- (Know `(m_space m2,subsets (sigma (m_space m2) a)) = sigma (m_space m2) a` 2460 >- (Q.ABBREV_TAC `Q = (m_space m2,subsets (sigma (m_space m2) a))` 2461 >> Know `sigma (m_space m2) a = (space (sigma (m_space m2) a), 2462 subsets (sigma (m_space m2) a))` 2463 >- RW_TAC std_ss [SPACE] 2464 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2465 >> Q.UNABBREV_TAC `Q` 2466 >> RW_TAC std_ss [PAIR_EQ, sigma_def, space_def]) 2467 >> RW_TAC std_ss [] 2468 >> POP_ASSUM (K ALL_TAC) 2469 >> Know `(sigma (m_space m2) a) = sigma (space (m_space m2, a)) (subsets (m_space m2, a))` 2470 >- RW_TAC std_ss [space_def, subsets_def] 2471 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2472 >> MATCH_MP_TAC MEASURABLE_LIFT 2473 >> ASM_REWRITE_TAC []) 2474 >> Q.PAT_X_ASSUM `f IN X` K_TAC 2475 >> REWRITE_TAC [IN_MEASURABLE, space_def, subsets_def] 2476 >> STRIP_TAC 2477 >> ASM_REWRITE_TAC [] 2478 >> CONJ_TAC 2479 >- (Q.PAT_X_ASSUM `measurable_sets m2 = subsets (sigma (m_space m2) a)` (MP_TAC o GSYM) 2480 >> RW_TAC std_ss [MEASURE_SPACE_REDUCE]) 2481 >> Suff `subsets (sigma (m_space m2) a) SUBSET 2482 {s | measure m1 ((PREIMAGE f s) INTER (m_space m1)) = measure m2 s}` 2483 >- RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION] 2484 >> MATCH_MP_TAC SIGMA_PROPERTY_DISJOINT 2485 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, IN_INTER, IN_FUNSET, 2486 IN_UNIV, PREIMAGE_COMPL, PREIMAGE_BIGUNION, IMAGE_IMAGE, 2487 MEASURE_COMPL] >| 2488 [Q.PAT_X_ASSUM `measure m1 (PREIMAGE f s INTER m_space m1) = measure m2 s` 2489 (fn thm => ONCE_REWRITE_TAC [GSYM thm]) 2490 >> Know `m_space m2 IN a` >- PROVE_TAC [ALGEBRA_SPACE, subsets_def, space_def] 2491 >> STRIP_TAC 2492 >> Q.PAT_X_ASSUM `!s. s IN a ==> (measure m1 (PREIMAGE f s INTER m_space m1) = measure m2 s)` 2493 ((fn thm => ONCE_REWRITE_TAC [GSYM thm]) o UNDISCH o Q.SPEC `m_space m2`) 2494 >> Know `PREIMAGE f (m_space m2) INTER m_space m1 = m_space m1` 2495 >- (FULL_SIMP_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, IN_FUNSET] >> METIS_TAC []) 2496 >> RW_TAC std_ss [PREIMAGE_DIFF] 2497 >> `((PREIMAGE f (m_space m2) DIFF PREIMAGE f s) INTER m_space m1) = 2498 ((PREIMAGE f (m_space m2) INTER m_space m1) DIFF (PREIMAGE f s INTER m_space m1))` 2499 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_DIFF, IN_PREIMAGE] >> DECIDE_TAC) 2500 >> RW_TAC std_ss [MEASURE_COMPL], 2501 `BIGUNION (IMAGE (PREIMAGE f o f') UNIV) INTER m_space m1 = 2502 BIGUNION (IMAGE (\x:num. (PREIMAGE f o f') x INTER m_space m1) UNIV)` 2503 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] 2504 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 2505 >> EQ_TAC 2506 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `PREIMAGE f (f' x') INTER m_space m1` 2507 >> ASM_REWRITE_TAC [IN_INTER] >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 2508 >> RW_TAC std_ss [] >> METIS_TAC [IN_PREIMAGE, IN_INTER]) 2509 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2510 >> Suff 2511 `(measure m2 o f') --> measure m2 (BIGUNION (IMAGE f' UNIV)) /\ 2512 (measure m2 o f') --> 2513 measure m1 (BIGUNION (IMAGE (\x. (PREIMAGE f o f') x INTER m_space m1) UNIV))` 2514 >- PROVE_TAC [SEQ_UNIQ] 2515 >> CONJ_TAC 2516 >- (MATCH_MP_TAC MEASURE_COUNTABLE_INCREASING 2517 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF]) 2518 >> Know `measure m2 o f' = measure m1 o (\x. (PREIMAGE f o f') x INTER m_space m1)` 2519 >- (RW_TAC std_ss [FUN_EQ_THM] 2520 >> RW_TAC std_ss [o_THM]) 2521 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2522 >> MATCH_MP_TAC MEASURE_COUNTABLE_INCREASING 2523 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, PREIMAGE_EMPTY, INTER_EMPTY] 2524 >> Suff `PREIMAGE f (f' n) SUBSET PREIMAGE f (f' (SUC n))` 2525 >- RW_TAC std_ss [SUBSET_DEF, IN_INTER] 2526 >> MATCH_MP_TAC PREIMAGE_SUBSET 2527 >> RW_TAC std_ss [SUBSET_DEF], 2528 `BIGUNION (IMAGE (PREIMAGE f o f') UNIV) INTER m_space m1 = 2529 BIGUNION (IMAGE (\x:num. (PREIMAGE f o f') x INTER m_space m1) UNIV)` 2530 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] 2531 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 2532 >> EQ_TAC 2533 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `PREIMAGE f (f' x') INTER m_space m1` 2534 >> ASM_REWRITE_TAC [IN_INTER] >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 2535 >> RW_TAC std_ss [] >> METIS_TAC [IN_PREIMAGE, IN_INTER]) 2536 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2537 >> Suff 2538 `(measure m2 o f') sums measure m2 (BIGUNION (IMAGE f' UNIV)) /\ 2539 (measure m2 o f') sums 2540 measure m1 (BIGUNION (IMAGE (\x. (PREIMAGE f o f') x INTER m_space m1) UNIV))` 2541 >- PROVE_TAC [SUM_UNIQ] 2542 >> CONJ_TAC 2543 >- (MATCH_MP_TAC MEASURE_COUNTABLY_ADDITIVE 2544 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV]) 2545 >> Know `measure m2 o f' = measure m1 o (\x. (PREIMAGE f o f') x INTER m_space m1)` 2546 >- (RW_TAC std_ss [FUN_EQ_THM] 2547 >> RW_TAC std_ss [o_THM]) 2548 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2549 >> MATCH_MP_TAC MEASURE_COUNTABLY_ADDITIVE 2550 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, IN_DISJOINT, PREIMAGE_DISJOINT, IN_INTER] 2551 >> METIS_TAC [IN_DISJOINT, PREIMAGE_DISJOINT]]); 2552 2553val MEASURE_PRESERVING_SUBSET = store_thm 2554 ("MEASURE_PRESERVING_SUBSET", 2555 ``!m1 m2 a. 2556 measure_space m1 /\ measure_space m2 /\ 2557 (measurable_sets m2 = subsets (sigma (m_space m2) a)) ==> 2558 measure_preserving m1 (m_space m2, a, measure m2) SUBSET 2559 measure_preserving m1 m2``, 2560 RW_TAC std_ss [SUBSET_DEF] 2561 >> MATCH_MP_TAC MEASURE_PRESERVING_LIFT 2562 >> PROVE_TAC []); 2563 2564val MEASURABLE_I = store_thm 2565 ("MEASURABLE_I", 2566 ``!a. sigma_algebra a ==> I IN measurable a a``, 2567 RW_TAC std_ss [IN_MEASURABLE, I_THM, PREIMAGE_I, IN_FUNSET, GSPEC_ID, SPACE, SUBSET_REFL] 2568 >> Know `s INTER space a = s` 2569 >- (FULL_SIMP_TAC std_ss [Once EXTENSION, sigma_algebra_def, algebra_def, IN_INTER, 2570 subset_class_def, SUBSET_DEF] 2571 >> METIS_TAC []) 2572 >> RW_TAC std_ss []); 2573 2574val MEASURABLE_COMP = store_thm 2575 ("MEASURABLE_COMP", 2576 ``!f g a b c. 2577 f IN measurable a b /\ g IN measurable b c ==> 2578 (g o f) IN measurable a c``, 2579 RW_TAC std_ss [IN_MEASURABLE, GSYM PREIMAGE_COMP, IN_FUNSET, SIGMA_ALGEBRA, space_def, 2580 subsets_def, GSPECIFICATION] 2581 >> `PREIMAGE f (PREIMAGE g s) INTER space a = 2582 PREIMAGE f (PREIMAGE g s INTER space b) INTER space a` 2583 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] >> METIS_TAC []) 2584 >> METIS_TAC []); 2585 2586val MEASURABLE_COMP_STRONG = store_thm 2587 ("MEASURABLE_COMP_STRONG", 2588 ``!f g a b c. 2589 f IN measurable a b /\ 2590 sigma_algebra c /\ 2591 g IN (space b -> space c) /\ 2592 (!x. x IN (subsets c) ==> PREIMAGE g x INTER (IMAGE f (space a)) IN subsets b) ==> 2593 (g o f) IN measurable a c``, 2594 RW_TAC bool_ss [IN_MEASURABLE] 2595 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET] >> PROVE_TAC [], 2596 RW_TAC std_ss [PREIMAGE_ALT] 2597 >> ONCE_REWRITE_TAC [o_ASSOC] 2598 >> ONCE_REWRITE_TAC [GSYM PREIMAGE_ALT] 2599 >> Know `PREIMAGE f (s o g) INTER space a = 2600 PREIMAGE f (s o g INTER (IMAGE f (space a))) INTER space a` 2601 >- (RW_TAC std_ss [GSYM PREIMAGE_ALT] 2602 >> RW_TAC std_ss [Once EXTENSION, IN_PREIMAGE, IN_INTER, IN_IMAGE] 2603 >> EQ_TAC 2604 >> RW_TAC std_ss [] 2605 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE] 2606 >> Q.EXISTS_TAC `x` 2607 >> Know `g (f x) IN space c` 2608 >- (FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF] >> PROVE_TAC []) 2609 >> PROVE_TAC []) 2610 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2611 >> FULL_SIMP_TAC std_ss [PREIMAGE_ALT]]); 2612 2613val MEASURABLE_COMP_STRONGER = store_thm 2614 ("MEASURABLE_COMP_STRONGER", 2615 ``!f g a b c t. 2616 f IN measurable a b /\ 2617 sigma_algebra c /\ 2618 g IN (space b -> space c) /\ 2619 (IMAGE f (space a)) SUBSET t /\ 2620 (!s. s IN subsets c ==> (PREIMAGE g s INTER t) IN subsets b) ==> 2621 (g o f) IN measurable a c``, 2622 RW_TAC bool_ss [IN_MEASURABLE] 2623 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET] >> PROVE_TAC [], 2624 RW_TAC std_ss [PREIMAGE_ALT] 2625 >> ONCE_REWRITE_TAC [o_ASSOC] 2626 >> ONCE_REWRITE_TAC [GSYM PREIMAGE_ALT] 2627 >> Know `(PREIMAGE (f:'a->'b) (((s : 'c -> bool) o (g :'b -> 'c)) INTER 2628 (t :'b -> bool)) INTER space a = PREIMAGE f (s o g) INTER space a)` 2629 >- (RW_TAC std_ss [GSYM PREIMAGE_ALT] 2630 >> RW_TAC std_ss [Once EXTENSION, IN_PREIMAGE, IN_INTER, IN_IMAGE] 2631 >> EQ_TAC 2632 >> RW_TAC std_ss [] 2633 >> Know `g (f x) IN space c` 2634 >- (FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF] >> PROVE_TAC []) 2635 >> STRIP_TAC 2636 >> Know `(f x) IN space b` 2637 >- FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE, IN_FUNSET] 2638 >> STRIP_TAC 2639 >> Know `x IN space a` 2640 >- FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE] 2641 >> STRIP_TAC 2642 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2643 >> Q.PAT_X_ASSUM `!x. (?x'. (x = f x') /\ x' IN space a) ==> x IN t` MATCH_MP_TAC 2644 >> Q.EXISTS_TAC `x` 2645 >> ASM_REWRITE_TAC []) 2646 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap o GSYM) 2647 >> RW_TAC std_ss [PREIMAGE_ALT] 2648 >> RW_TAC std_ss [GSYM PREIMAGE_ALT, GSYM PREIMAGE_COMP]]); 2649 2650val MEASURABLE_UP_LIFT = store_thm 2651 ("MEASURABLE_UP_LIFT", 2652 ``!sp a b c f. f IN measurable (sp, a) c /\ 2653 sigma_algebra (sp, b) /\ a SUBSET b ==> f IN measurable (sp,b) c``, 2654 RW_TAC std_ss [IN_MEASURABLE, GSPECIFICATION, SUBSET_DEF, IN_FUNSET, space_def, subsets_def]); 2655 2656val MEASURABLE_UP_SUBSET = store_thm 2657 ("MEASURABLE_UP_SUBSET", 2658 ``!sp a b c. a SUBSET b /\ sigma_algebra (sp, b) 2659 ==> measurable (sp, a) c SUBSET measurable (sp, b) c``, 2660 RW_TAC std_ss [MEASURABLE_UP_LIFT, SUBSET_DEF] 2661 >> MATCH_MP_TAC MEASURABLE_UP_LIFT 2662 >> Q.EXISTS_TAC `a` 2663 >> ASM_REWRITE_TAC [SUBSET_DEF]); 2664 2665val MEASURABLE_UP_SIGMA = store_thm 2666 ("MEASURABLE_UP_SIGMA", 2667 ``!a b. measurable a b SUBSET measurable (sigma (space a) (subsets a)) b``, 2668 RW_TAC std_ss [SUBSET_DEF, IN_MEASURABLE, space_def, subsets_def, SPACE_SIGMA] 2669 >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA]) 2670 >> PROVE_TAC [SIGMA_SUBSET_SUBSETS, SUBSET_DEF]); 2671 2672val MEASURE_PRESERVING_UP_LIFT = store_thm 2673 ("MEASURE_PRESERVING_UP_LIFT", 2674 ``!m1 m2 f. 2675 measure_space m1 /\ 2676 f IN measure_preserving (m_space m1, a, measure m1) m2 /\ 2677 sigma_algebra (m_space m1, measurable_sets m1) /\ 2678 a SUBSET measurable_sets m1 ==> 2679 f IN measure_preserving m1 m2``, 2680 RW_TAC std_ss [measure_preserving_def, GSPECIFICATION, SUBSET_DEF, 2681 measure_def, measurable_sets_def, m_space_def, SPACE] 2682 >> MATCH_MP_TAC MEASURABLE_UP_LIFT 2683 >> Q.EXISTS_TAC `a` 2684 >> RW_TAC std_ss [SUBSET_DEF]); 2685 2686val MEASURE_PRESERVING_UP_SUBSET = store_thm 2687 ("MEASURE_PRESERVING_UP_SUBSET", 2688 ``!m1 m2. 2689 measure_space m1 /\ 2690 a SUBSET measurable_sets m1 /\ 2691 sigma_algebra (m_space m1, measurable_sets m1) ==> 2692 measure_preserving (m_space m1, a, measure m1) m2 SUBSET measure_preserving m1 m2``, 2693 RW_TAC std_ss [MEASURE_PRESERVING_UP_LIFT, SUBSET_DEF] 2694 >> MATCH_MP_TAC MEASURE_PRESERVING_UP_LIFT 2695 >> PROVE_TAC [SUBSET_DEF]); 2696 2697val MEASURE_PRESERVING_UP_SIGMA = store_thm 2698 ("MEASURE_PRESERVING_UP_SIGMA", 2699 ``!m1 m2 a. 2700 measure_space m1 /\ 2701 (measurable_sets m1 = subsets (sigma (m_space m1) a)) ==> 2702 measure_preserving (m_space m1, a, measure m1) m2 SUBSET measure_preserving m1 m2``, 2703 RW_TAC std_ss [MEASURE_PRESERVING_UP_LIFT, SUBSET_DEF] 2704 >> MATCH_MP_TAC MEASURE_PRESERVING_UP_LIFT 2705 >> ASM_REWRITE_TAC [SIGMA_SUBSET_SUBSETS, SIGMA_REDUCE] 2706 >> FULL_SIMP_TAC std_ss [IN_MEASURE_PRESERVING, IN_MEASURABLE, m_space_def, 2707 measurable_sets_def] 2708 >> MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA 2709 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, space_def, subsets_def]); 2710 2711(* ****************** *) 2712 2713val MEASURABLE_PROD_SIGMA = store_thm 2714 ("MEASURABLE_PROD_SIGMA", 2715 ``!a a1 a2 f. 2716 sigma_algebra a /\ 2717 (FST o f) IN measurable a a1 /\ 2718 (SND o f) IN measurable a a2 ==> 2719 f IN measurable a (sigma ((space a1) CROSS (space a2)) 2720 (prod_sets (subsets a1) (subsets a2)))``, 2721 REPEAT STRIP_TAC 2722 >> MATCH_MP_TAC MEASURABLE_SIGMA 2723 >> FULL_SIMP_TAC std_ss [IN_MEASURABLE] 2724 >> CONJ_TAC 2725 >- (RW_TAC std_ss [subset_class_def, subsets_def, space_def, IN_PROD_SETS] 2726 >> PROVE_TAC [SIGMA_ALGEBRA, CROSS_SUBSET, SUBSET_DEF, subset_class_def, subsets_def, 2727 space_def]) 2728 >> CONJ_TAC 2729 >- (RW_TAC std_ss [IN_FUNSET, SPACE_SIGMA, IN_CROSS] 2730 >> FULL_SIMP_TAC std_ss [IN_FUNSET, o_DEF]) 2731 >> RW_TAC std_ss [IN_PROD_SETS] 2732 >> RW_TAC std_ss [PREIMAGE_CROSS] 2733 >> `PREIMAGE (FST o f) t INTER PREIMAGE (SND o f) u INTER space a = 2734 (PREIMAGE (FST o f) t INTER space a) INTER (PREIMAGE (SND o f) u INTER space a)` 2735 by (RW_TAC std_ss [Once EXTENSION, IN_INTER] >> DECIDE_TAC) 2736 >> PROVE_TAC [sigma_algebra_def, ALGEBRA_INTER]); 2737 2738val MEASURABLE_RANGE_REDUCE = store_thm 2739 ("MEASURABLE_RANGE_REDUCE", 2740 ``!m f s. measure_space m /\ 2741 f IN measurable (m_space m, measurable_sets m) (s, POW s) /\ 2742 (~(s = {})) ==> 2743 f IN measurable (m_space m, measurable_sets m) 2744 (s INTER (IMAGE f (m_space m)), POW (s INTER (IMAGE f (m_space m))))``, 2745 RW_TAC std_ss [IN_MEASURABLE, POW_SIGMA_ALGEBRA, subsets_def, space_def, IN_FUNSET, 2746 IN_INTER, IN_IMAGE, IN_POW, SUBSET_INTER, 2747 MEASURABLE_SETS_SUBSET_SPACE, INTER_SUBSET] 2748 >> METIS_TAC []); 2749 2750val MEASURABLE_POW_TO_POW = store_thm 2751 ("MEASURABLE_POW_TO_POW", 2752 ``!m f. 2753 measure_space m /\ 2754 (measurable_sets m = POW (m_space m)) ==> 2755 f IN measurable (m_space m, measurable_sets m) (UNIV, POW(UNIV))``, 2756 RW_TAC std_ss [IN_MEASURABLE, IN_POW, IN_UNIV, POW_SIGMA_ALGEBRA, subsets_def, space_def, 2757 IN_FUNSET, PREIMAGE_UNIV, SUBSET_UNIV, measure_space_def, SUBSET_DEF, 2758 IN_INTER]); 2759 2760val MEASURABLE_POW_TO_POW_IMAGE = store_thm 2761 ("MEASURABLE_POW_TO_POW_IMAGE", 2762 ``!m f. 2763 measure_space m /\ 2764 (measurable_sets m = POW (m_space m)) ==> 2765 f IN measurable (m_space m, measurable_sets m) 2766 (IMAGE f (m_space m), POW(IMAGE f (m_space m)))``, 2767 REPEAT STRIP_TAC 2768 >> (MP_TAC o Q.SPECL [`m`,`f`,`UNIV`]) MEASURABLE_RANGE_REDUCE 2769 >> ASM_SIMP_TAC std_ss [UNIV_NOT_EMPTY, INTER_UNIV, MEASURABLE_POW_TO_POW]); 2770 2771val MEASURE_SPACE_SUBSET = store_thm 2772 ("MEASURE_SPACE_SUBSET", 2773 ``!s s' m. s' SUBSET s /\ measure_space (s,POW s, m) ==> 2774 measure_space (s',POW s', m)``, 2775 RW_TAC std_ss [measure_space_def, m_space_def, measurable_sets_def, POW_SIGMA_ALGEBRA, 2776 positive_def, measure_def, IN_POW, countably_additive_def, IN_FUNSET, IN_POW] 2777 >> METIS_TAC [SUBSET_TRANS, SUBSET_REFL]); 2778 2779val STRONG_MEASURE_SPACE_SUBSET = store_thm 2780 ("STRONG_MEASURE_SPACE_SUBSET", 2781 ``!s s'. s' SUBSET m_space s /\ measure_space s /\ POW s' SUBSET measurable_sets s ==> 2782 measure_space (s',POW s', measure s)``, 2783 REPEAT STRIP_TAC >> MATCH_MP_TAC MEASURE_DOWN 2784 >> Q.EXISTS_TAC `s` 2785 >> RW_TAC std_ss [measure_def, m_space_def, measurable_sets_def, POW_SIGMA_ALGEBRA]); 2786 2787val MEASURE_REAL_SUM_IMAGE = store_thm 2788 ("MEASURE_REAL_SUM_IMAGE", 2789 ``!m s. measure_space m /\ s IN measurable_sets m /\ 2790 (!x. x IN s ==> {x} IN measurable_sets m) /\ FINITE s ==> 2791 (measure m s = SIGMA (\x. measure m {x}) s)``, 2792 Suff `!s. FINITE s ==> 2793 (\s. !m. measure_space m /\ s IN measurable_sets m /\ 2794 (!x. x IN s ==> {x} IN measurable_sets m) ==> 2795 (measure m s = SIGMA (\x. measure m {x}) s)) s` 2796 >- METIS_TAC [] 2797 >> MATCH_MP_TAC FINITE_INDUCT 2798 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, MEASURE_EMPTY, DELETE_NON_ELEMENT, IN_INSERT] 2799 >> Q.PAT_X_ASSUM `!p. 2800 measure_space m /\ s IN measurable_set m /\ 2801 (!x. x IN s ==> {x} IN measurable_sets m) ==> 2802 (measure m s = SIGMA (\x. measure m {x}) s)` (MP_TAC o GSYM o Q.SPEC `m`) 2803 >> RW_TAC std_ss [] 2804 >> `s IN measurable_sets m` 2805 by (`s = (e INSERT s) DIFF {e}` 2806 by (RW_TAC std_ss [EXTENSION, IN_INSERT, IN_DIFF, IN_SING] 2807 >> METIS_TAC [GSYM DELETE_NON_ELEMENT]) 2808 >> POP_ORW 2809 >> FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def] 2810 >> METIS_TAC [space_def, subsets_def, ALGEBRA_DIFF]) 2811 >> ASM_SIMP_TAC std_ss [] 2812 >> MATCH_MP_TAC MEASURE_ADDITIVE 2813 >> RW_TAC std_ss [IN_DISJOINT, IN_SING, Once INSERT_SING_UNION] 2814 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]); 2815 2816val SIGMA_POW = store_thm 2817 ("SIGMA_POW", 2818 ``!s. sigma s (POW s) = (s,POW s)``, 2819 RW_TAC std_ss [sigma_def, PAIR_EQ, EXTENSION, IN_BIGINTER, IN_POW, GSPECIFICATION] 2820 >> EQ_TAC 2821 >- (RW_TAC std_ss [] >> POP_ASSUM (MP_TAC o Q.SPEC `POW s`) 2822 >> METIS_TAC [IN_POW, POW_SIGMA_ALGEBRA, SUBSET_REFL]) 2823 >> RW_TAC std_ss [SUBSET_DEF, IN_POW] >> METIS_TAC []); 2824 2825val finite_additivity_sufficient_for_finite_spaces = store_thm 2826 ("finite_additivity_sufficient_for_finite_spaces", 2827 ``!s m. sigma_algebra s /\ FINITE (space s) /\ 2828 positive (space s, subsets s, m) /\ 2829 additive (space s, subsets s, m) ==> 2830 measure_space (space s, subsets s, m)``, 2831 RW_TAC std_ss [countably_additive_def, additive_def, measurable_sets_def, measure_def, 2832 IN_FUNSET, IN_UNIV, measure_space_def, m_space_def, SPACE] 2833 >> `FINITE (subsets s)` 2834 by (Suff `subsets s SUBSET (POW (space s))` 2835 >- METIS_TAC [SUBSET_FINITE, FINITE_POW] 2836 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF, IN_POW] 2837 >> METIS_TAC []) 2838 >> `?N. !n. n >= N ==> (f n = {})` 2839 by METIS_TAC [finite_enumeration_of_sets_has_max_non_empty] 2840 >> FULL_SIMP_TAC std_ss [GREATER_EQ] 2841 >> `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE f (count N))` 2842 by METIS_TAC [BIGUNION_IMAGE_UNIV] 2843 >> RW_TAC std_ss [sums, SEQ] 2844 >> Q.EXISTS_TAC `N` 2845 >> RW_TAC std_ss [GREATER_EQ] 2846 >> Suff `!n. N <= n ==> (sum (0,n) (m o f) = m(BIGUNION (IMAGE f (count N))))` 2847 >- RW_TAC real_ss [LESS_EQ_REFL] 2848 >> Induct 2849 >- (RW_TAC std_ss [sum] >> `count 0 = {}` by RW_TAC real_ss [EXTENSION, IN_COUNT, NOT_IN_EMPTY] 2850 >> FULL_SIMP_TAC std_ss [IMAGE_EMPTY, BIGUNION_EMPTY, positive_def, measure_def]) 2851 >> STRIP_TAC 2852 >> Cases_on `SUC n' = N` 2853 >- (POP_ORW 2854 >> `m = measure (space s, subsets s,m)` by RW_TAC std_ss [measure_def] 2855 >> POP_ORW 2856 >> MATCH_MP_TAC ADDITIVE_SUM 2857 >> RW_TAC std_ss [m_space_def, measurable_sets_def, IN_FUNSET, IN_UNIV, additive_def, 2858 measure_def, SIGMA_ALGEBRA_ALGEBRA, SPACE]) 2859 >> `N <= n'` 2860 by (NTAC 2 (POP_ASSUM MP_TAC) >> DECIDE_TAC) 2861 >> FULL_SIMP_TAC std_ss [] 2862 >> RW_TAC std_ss [sum] 2863 >> FULL_SIMP_TAC real_ss [positive_def, measure_def]); 2864 2865val finite_additivity_sufficient_for_finite_spaces2 = store_thm 2866 ("finite_additivity_sufficient_for_finite_spaces2", 2867 ``!m. sigma_algebra (m_space m, measurable_sets m) /\ FINITE (m_space m) /\ 2868 positive m /\ 2869 additive m ==> 2870 measure_space m``, 2871 REPEAT STRIP_TAC 2872 >> Suff `measure_space (space (m_space m, measurable_sets m), 2873 subsets (m_space m, measurable_sets m), measure m)` 2874 >- RW_TAC std_ss [space_def, subsets_def, MEASURE_SPACE_REDUCE] 2875 >> MATCH_MP_TAC finite_additivity_sufficient_for_finite_spaces 2876 >> RW_TAC std_ss [space_def, subsets_def, MEASURE_SPACE_REDUCE]); 2877 2878val IMAGE_SING = store_thm 2879 ("IMAGE_SING", ``!f x. IMAGE f {x} = {f x}``, 2880 RW_TAC std_ss [EXTENSION,IN_SING,IN_IMAGE] >> METIS_TAC []); 2881 2882val SUBSET_BIGINTER = store_thm 2883("SUBSET_BIGINTER", ``!X P. X SUBSET BIGINTER P <=> !Y. Y IN P ==> X SUBSET Y``, 2884 RW_TAC std_ss [SUBSET_DEF,IN_BIGINTER] 2885 >> METIS_TAC []); 2886 2887val MEASURE_SPACE_INCREASING = store_thm 2888 ("MEASURE_SPACE_INCREASING",``!m. measure_space m ==> increasing m``, 2889 RW_TAC real_ss [] >> `additive m` by RW_TAC real_ss [MEASURE_SPACE_ADDITIVE] 2890 >> FULL_SIMP_TAC real_ss [measure_space_def,sigma_algebra_def,ADDITIVE_INCREASING]); 2891 2892val MEASURE_SPACE_POSITIVE = store_thm 2893 ("MEASURE_SPACE_POSITIVE",``!m. measure_space m ==> positive m``, 2894 PROVE_TAC [measure_space_def]); 2895 2896val MEASURE_SPACE_INTER = store_thm 2897 ("MEASURE_SPACE_INTER",``!m s t. (measure_space m) /\ (s IN measurable_sets m) /\ 2898 (t IN measurable_sets m) ==> (s INTER t IN measurable_sets m)``, 2899 METIS_TAC [measure_space_def,sigma_algebra_def,subsets_def, 2900 (REWRITE_RULE [subsets_def] (Q.SPEC `(m_space m,measurable_sets m)` ALGEBRA_INTER))]); 2901 2902val MEASURE_SPACE_UNION = store_thm 2903 ("MEASURE_SPACE_UNION",``!m s t. (measure_space m) /\ (s IN measurable_sets m) /\ 2904 (t IN measurable_sets m) ==> (s UNION t IN measurable_sets m)``, 2905 METIS_TAC [measure_space_def,sigma_algebra_def,subsets_def, 2906 (REWRITE_RULE [subsets_def] (Q.SPEC `(m_space m,measurable_sets m)` 2907 ALGEBRA_UNION))]); 2908 2909val MEASURE_SPACE_DIFF = store_thm 2910 ("MEASURE_SPACE_DIFF",``!m s t. (measure_space m) /\ (s IN measurable_sets m) /\ 2911 (t IN measurable_sets m) ==> (s DIFF t IN measurable_sets m)``, 2912 METIS_TAC [measure_space_def,sigma_algebra_def,subsets_def, 2913 (REWRITE_RULE [subsets_def] (Q.SPEC `(m_space m,measurable_sets m)` ALGEBRA_DIFF))]); 2914 2915val MEASURE_COMPL_SUBSET = store_thm 2916 ("MEASURE_COMPL_SUBSET", 2917 ``!m s. 2918 measure_space m /\ s IN measurable_sets m /\ t IN measurable_sets m /\ (t SUBSET s) ==> 2919 (measure m (s DIFF t) = measure m s - measure m t)``, 2920 RW_TAC std_ss [] 2921 >> Suff `measure m s = measure m t + measure m (s DIFF t)` 2922 >- REAL_ARITH_TAC 2923 >> MATCH_MP_TAC ADDITIVE 2924 >> Q.PAT_X_ASSUM `measure_space m` MP_TAC 2925 >> RW_TAC std_ss [measure_space_def, sigma_algebra_def, DISJOINT_DEF, 2926 EXTENSION, IN_DIFF, IN_UNIV, IN_UNION, IN_INTER, 2927 NOT_IN_EMPTY] 2928 >> METIS_TAC [COUNTABLY_ADDITIVE_ADDITIVE,MEASURE_SPACE_DIFF,measure_space_def, 2929 sigma_algebra_def,SUBSET_DEF]); 2930 2931val MEASURE_SPACE_BIGUNION = store_thm 2932 ("MEASURE_SPACE_BIGUNION",``!m s. measure_space m /\ (!n:num. s n IN measurable_sets m) 2933 ==> (BIGUNION (IMAGE s UNIV) IN measurable_sets m)``, 2934 RW_TAC std_ss [] 2935 >> (MP_TAC o REWRITE_RULE [subsets_def,space_def,IN_UNIV,IN_FUNSET] o 2936 Q.SPEC `(m_space m,measurable_sets m)`) SIGMA_ALGEBRA_FN 2937 >> METIS_TAC [measure_space_def]); 2938 2939val MEASURE_SPACE_IN_MSPACE = store_thm 2940 ("MEASURE_SPACE_IN_MSPACE",``!m A. measure_space m /\ A IN measurable_sets m 2941 ==> (!x. x IN A ==> x IN m_space m)``, 2942 METIS_TAC [measure_space_def,sigma_algebra_def,algebra_def,measurable_sets_def,space_def, 2943 subset_class_def,subsets_def,SUBSET_DEF]); 2944 2945val MEASURE_SPACE_SUBSET_MSPACE = store_thm 2946 ("MEASURE_SPACE_SUBSET_MSPACE", ``!A m. measure_space m /\ A IN measurable_sets m 2947 ==> A SUBSET m_space m``, 2948 RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def,subset_class_def, 2949 subsets_def, space_def]); 2950 2951val MEASURE_SPACE_EMPTY_MEASURABLE = store_thm 2952 ("MEASURE_SPACE_EMPTY_MEASURABLE",``!m. measure_space m 2953 ==> {} IN measurable_sets m``, 2954 RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def,subsets_def, space_def]); 2955 2956val MEASURE_SPACE_MSPACE_MEASURABLE = store_thm 2957 ("MEASURE_SPACE_MSPACE_MEASURABLE",``!m. measure_space m ==> (m_space m) IN measurable_sets m``, 2958 RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, subsets_def, space_def] 2959 >> METIS_TAC [DIFF_EMPTY]); 2960 2961val SIGMA_ALGEBRA_FN_BIGINTER = store_thm 2962 ("SIGMA_ALGEBRA_FN_BIGINTER", 2963 ``!a. 2964 sigma_algebra a ==> subset_class (space a) (subsets a) /\ {} IN subsets a /\ 2965 (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 2966 (!f : num -> 'a -> bool. f IN (UNIV -> subsets a) 2967 ==> BIGINTER (IMAGE f UNIV) IN subsets a)``, 2968 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_UNIV, SUBSET_DEF] 2969 >> ASSUME_TAC (Q.SPECL [`space a`,`(IMAGE (f:num -> 'a -> bool) UNIV)`] DIFF_BIGINTER) 2970 >> `!t. t IN IMAGE f UNIV ==> t SUBSET space a` 2971 by (FULL_SIMP_TAC std_ss [IN_IMAGE,sigma_algebra_def,algebra_def,subsets_def, 2972 space_def,subset_class_def,IN_UNIV] 2973 >> RW_TAC std_ss [] 2974 >> METIS_TAC []) 2975 >> `IMAGE f UNIV <> {}` by RW_TAC std_ss [IMAGE_EQ_EMPTY,UNIV_NOT_EMPTY] 2976 >> FULL_SIMP_TAC std_ss [] 2977 >> `BIGUNION (IMAGE (\u. space a DIFF u) (IMAGE f UNIV)) IN subsets a` 2978 by (Q.PAT_X_ASSUM `!c. M ==> BIGUNION c IN subsets a` (MATCH_MP_TAC) 2979 >> RW_TAC std_ss [] 2980 >- (MATCH_MP_TAC image_countable 2981 >> RW_TAC std_ss [COUNTABLE_ENUM] 2982 >> Q.EXISTS_TAC `f` 2983 >> RW_TAC std_ss []) 2984 >> FULL_SIMP_TAC std_ss [IN_IMAGE]) 2985 >> METIS_TAC []); 2986 2987val MEASURE_SPACE_BIGINTER = store_thm 2988 ("MEASURE_SPACE_BIGINTER",``!m s. measure_space m /\ (!n:num. s n IN measurable_sets m) 2989 ==> (BIGINTER (IMAGE s UNIV) IN measurable_sets m)``, 2990 RW_TAC std_ss [] 2991 >> (MP_TAC o REWRITE_RULE [subsets_def,space_def,IN_UNIV,IN_FUNSET] o 2992 Q.SPEC `(m_space m,measurable_sets m)`) SIGMA_ALGEBRA_FN_BIGINTER 2993 >> METIS_TAC [measure_space_def]); 2994 2995val MONOTONE_CONVERGENCE2 = store_thm 2996 ("MONOTONE_CONVERGENCE2", ``!m f. measure_space m /\ 2997 f IN (UNIV -> measurable_sets m) /\ (!n. f n SUBSET f (SUC n)) ==> 2998 (measure m o f --> measure m (BIGUNION (IMAGE f UNIV)))``, 2999 METIS_TAC [MONOTONE_CONVERGENCE]); 3000 3001val MONOTONE_CONVERGENCE_BIGINTER = store_thm 3002 ("MONOTONE_CONVERGENCE_BIGINTER", 3003 ``!m s f. 3004 measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 3005 (!n. f (SUC n) SUBSET f n) /\ (s = BIGINTER (IMAGE f UNIV)) ==> 3006 measure m o f --> measure m s``, 3007 RW_TAC std_ss [IN_FUNSET, IN_UNIV] 3008 >> `BIGINTER (IMAGE f UNIV) IN measurable_sets m` by METIS_TAC [MEASURE_SPACE_BIGINTER] 3009 >> `!n. f n SUBSET f 0` 3010 by (Induct_on `n` >- RW_TAC std_ss [SUBSET_REFL] 3011 >> METIS_TAC [SUBSET_TRANS]) 3012 >> `BIGINTER (IMAGE f UNIV) SUBSET (f 0)` 3013 by (MATCH_MP_TAC BIGINTER_SUBSET 3014 >> METIS_TAC [IMAGE_EQ_EMPTY,UNIV_NOT_EMPTY,IN_IMAGE,IN_UNIV]) 3015 >> Q.ABBREV_TAC `g = (\n. (f 0) DIFF (f n))` 3016 >> FULL_SIMP_TAC std_ss [o_DEF] 3017 >> `!n. measure m (f 0) - measure m (f n) = measure m (g n)` by METIS_TAC [MEASURE_COMPL_SUBSET] 3018 >> `(\x. measure m (f x)) = (\x. (\x. measure m (f 0)) x - (\x. measure m (g x)) x)` 3019 by (RW_TAC std_ss [FUN_EQ_THM] 3020 >> METIS_TAC [REAL_EQ_SUB_LADD,REAL_EQ_SUB_RADD,real_sub,REAL_ADD_COMM]) 3021 >> POP_ORW 3022 >> `BIGINTER (IMAGE f UNIV) = (f 0) DIFF BIGUNION (IMAGE (\u. (f 0) DIFF u) (IMAGE f UNIV))` 3023 by (MATCH_MP_TAC DIFF_BIGINTER 3024 >> METIS_TAC [IN_IMAGE,IN_UNIV,IMAGE_EQ_EMPTY,UNIV_NOT_EMPTY]) 3025 >> POP_ORW 3026 >> `BIGUNION (IMAGE (\u. f 0 DIFF u) (IMAGE f UNIV)) = BIGUNION (IMAGE (\n. f 0 DIFF f n) UNIV)` 3027 by (RW_TAC std_ss [EXTENSION,IN_BIGUNION_IMAGE,IN_UNIV,IN_IMAGE] 3028 >> METIS_TAC [SUBSET_DEF,IN_DIFF]) 3029 >> POP_ORW 3030 >> RW_TAC std_ss [] 3031 >> `(\n. measure m (g n)) --> measure m (BIGUNION (IMAGE g UNIV))` 3032 by ((MATCH_MP_TAC o REWRITE_RULE [o_DEF]) MONOTONE_CONVERGENCE2 3033 >> RW_TAC std_ss [IN_FUNSET,IN_UNIV] 3034 >- METIS_TAC [MEASURE_SPACE_DIFF] 3035 >> Q.UNABBREV_TAC `g` 3036 >> RW_TAC std_ss [SUBSET_DEF,IN_DIFF,GSPECIFICATION] 3037 >> METIS_TAC [SUBSET_DEF]) 3038 >> Suff `measure m (f 0 DIFF BIGUNION (IMAGE (\n. f 0 DIFF f n) UNIV)) = 3039 measure m (f 0) - measure m (BIGUNION (IMAGE (\n. f 0 DIFF f n) UNIV))` 3040 >- (RW_TAC std_ss [] 3041 >> `(\x. measure m (f 0) - measure m (g x)) = 3042 (\x. (\x. measure m (f 0)) x - (\x. measure m (g x)) x)` 3043 by RW_TAC std_ss [FUN_EQ_THM] 3044 >> POP_ORW 3045 >> MATCH_MP_TAC SEQ_SUB 3046 >> METIS_TAC [SEQ_CONST]) 3047 >> MATCH_MP_TAC MEASURE_COMPL_SUBSET 3048 >> RW_TAC std_ss [] 3049 >- (MATCH_MP_TAC MEASURE_SPACE_BIGUNION 3050 >> METIS_TAC [MEASURE_SPACE_DIFF]) 3051 >> RW_TAC std_ss [BIGUNION_SUBSET,IN_IMAGE,IN_UNIV] 3052 >> METIS_TAC [DIFF_SUBSET]); 3053 3054val MONOTONE_CONVERGENCE_BIGINTER2 = store_thm 3055 ("MONOTONE_CONVERGENCE_BIGINTER2", 3056 ``!m f. measure_space m /\ f IN (UNIV -> measurable_sets m) /\ 3057 (!n. f (SUC n) SUBSET f n) ==> 3058 measure m o f --> measure m (BIGINTER (IMAGE f UNIV))``, 3059 METIS_TAC [MONOTONE_CONVERGENCE_BIGINTER]); 3060 3061val MEASURE_SPACE_RESTRICTED = store_thm 3062("MEASURE_SPACE_RESTRICTED", ``!m s. measure_space m /\ s IN measurable_sets m ==> 3063 measure_space (s, IMAGE (\t. s INTER t) (measurable_sets m), measure m)``, 3064 RW_TAC std_ss [] 3065 >> `positive (s,IMAGE (\t. s INTER t) (measurable_sets m),measure m)` 3066 by (RW_TAC std_ss [positive_def,measure_def,measurable_sets_def,IN_IMAGE] 3067 >> METIS_TAC [MEASURE_SPACE_POSITIVE,MEASURE_SPACE_INTER,positive_def]) 3068 >> `countably_additive (s,IMAGE (\t. s INTER t) (measurable_sets m),measure m)` 3069 by (RW_TAC std_ss [countably_additive_def,measure_def,measurable_sets_def, 3070 IN_IMAGE,IN_FUNSET,IN_UNIV] 3071 >> `!x. f x IN measurable_sets m` by METIS_TAC [MEASURE_SPACE_INTER] 3072 >> `BIGUNION (IMAGE f univ(:num)) IN measurable_sets m` 3073 by METIS_TAC [MEASURE_SPACE_INTER] 3074 >> `countably_additive m` by METIS_TAC [measure_space_def] 3075 >> FULL_SIMP_TAC std_ss [countably_additive_def,IN_FUNSET,IN_UNIV]) 3076 >> RW_TAC std_ss [measure_space_def,sigma_algebra_def,measurable_sets_def,subsets_def, 3077 m_space_def,IN_IMAGE] 3078 >- (RW_TAC std_ss [algebra_def,space_def,subsets_def,subset_class_def,IN_IMAGE] 3079 >| [RW_TAC std_ss [INTER_SUBSET], 3080 METIS_TAC [INTER_EMPTY,MEASURE_SPACE_EMPTY_MEASURABLE], 3081 Q.EXISTS_TAC `m_space m DIFF t` 3082 >> RW_TAC std_ss [MEASURE_SPACE_DIFF,MEASURE_SPACE_MSPACE_MEASURABLE,EXTENSION, 3083 IN_DIFF,IN_INTER] 3084 >> METIS_TAC [MEASURE_SPACE_SUBSET_MSPACE,SUBSET_DEF], 3085 Q.EXISTS_TAC `t' UNION t''` 3086 >> RW_TAC std_ss [MEASURE_SPACE_UNION,UNION_OVER_INTER]]) 3087 >> `BIGUNION c SUBSET s` 3088 by (RW_TAC std_ss [SUBSET_DEF,IN_BIGUNION] 3089 >> FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_IMAGE] 3090 >> `?t. (s' = s INTER t) /\ t IN measurable_sets m` by METIS_TAC [] 3091 >> METIS_TAC [IN_INTER]) 3092 >> Q.EXISTS_TAC `BIGUNION c` 3093 >> RW_TAC std_ss [SUBSET_INTER2] 3094 >> Suff `BIGUNION c IN subsets (m_space m, measurable_sets m)` 3095 >- RW_TAC std_ss [subsets_def] 3096 >> MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION 3097 >> RW_TAC std_ss [subsets_def] 3098 >- FULL_SIMP_TAC std_ss [measure_space_def] 3099 >> FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_IMAGE] 3100 >> METIS_TAC [MEASURE_SPACE_INTER]); 3101 3102val MEASURE_SPACE_CMUL = store_thm 3103 ("MEASURE_SPACE_CMUL", ``!m c. measure_space m /\ 0 <= c ==> 3104 measure_space (m_space m, measurable_sets m, (\a. c * measure m a))``, 3105 RW_TAC real_ss [measure_space_def,m_space_def,measurable_sets_def,measure_def,positive_def] 3106 >- METIS_TAC [REAL_LE_MUL] 3107 >> RW_TAC std_ss [countably_additive_def,measure_def,measurable_sets_def,o_DEF] 3108 >> METIS_TAC [SER_CMUL,countably_additive_def]); 3109 3110val BIGUNION_IMAGE_Q = store_thm 3111 ("BIGUNION_IMAGE_Q", 3112 ``!a f: extreal -> 'a -> bool. sigma_algebra a /\ f IN (Q_set -> subsets a) 3113 ==> BIGUNION (IMAGE f Q_set) IN subsets a``, 3114 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_UNIV, SUBSET_DEF] 3115 >> Q.PAT_X_ASSUM `!c. countable c /\ P c ==> Q c` MATCH_MP_TAC 3116 >> RW_TAC std_ss [image_countable, IN_IMAGE, Q_COUNTABLE] 3117 >> METIS_TAC []); 3118 3119 3120(* ******************************************* *) 3121(* ------------------------------------ *) 3122(* Borel Space and Measurable functions *) 3123(* ------------------------------------ *) 3124(* ******************************************* *) 3125 3126val Borel_def = Define 3127 `Borel = sigma (UNIV:extreal->bool) (IMAGE (\a. {x | x < a}) UNIV)`; 3128 3129val SIGMA_ALGEBRA_BOREL = store_thm 3130 ("SIGMA_ALGEBRA_BOREL",``sigma_algebra Borel``, 3131 RW_TAC std_ss [Borel_def] 3132 >> MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA 3133 >> RW_TAC std_ss [subset_class_def,SUBSET_UNIV]); 3134 3135val MEASURABLE_BOREL = store_thm 3136 ("MEASURABLE_BOREL",``!f a. (f IN measurable a Borel) = (sigma_algebra a) /\ 3137 (f IN (space a -> UNIV)) /\ 3138 (!c. ((PREIMAGE f {x| x < c}) INTER (space a)) IN subsets a)``, 3139 RW_TAC std_ss [] 3140 >> `sigma_algebra Borel` by RW_TAC std_ss [SIGMA_ALGEBRA_BOREL] 3141 >> `space Borel = UNIV` by RW_TAC std_ss [Borel_def,space_def,SPACE_SIGMA] 3142 >> EQ_TAC 3143 >- (RW_TAC std_ss [Borel_def,IN_MEASURABLE,IN_FUNSET,IN_UNIV,subsets_def,GSPECIFICATION] 3144 >> POP_ASSUM MATCH_MP_TAC 3145 >> MATCH_MP_TAC IN_SIGMA 3146 >> RW_TAC std_ss [IN_IMAGE,IN_UNIV] 3147 >> METIS_TAC []) 3148 >> RW_TAC std_ss [Borel_def] 3149 >> MATCH_MP_TAC MEASURABLE_SIGMA 3150 >> RW_TAC std_ss [subset_class_def,SUBSET_UNIV,IN_IMAGE,IN_UNIV] 3151 >> METIS_TAC []); 3152 3153val IN_MEASURABLE_BOREL = store_thm 3154 ("IN_MEASURABLE_BOREL", ``!f a. f IN measurable a Borel = 3155 ( sigma_algebra a /\ f IN (space a -> UNIV) /\ 3156 !c. ({x | f x < c} INTER space a) IN subsets a)``, 3157 RW_TAC std_ss [] 3158 >> `!c. {x | f x < c} = PREIMAGE f {x| x < c}` 3159 by RW_TAC std_ss [EXTENSION,IN_PREIMAGE,GSPECIFICATION] 3160 >> RW_TAC std_ss [MEASURABLE_BOREL]); 3161 3162val IN_MEASURABLE_BOREL_NEGINF = store_thm 3163 ("IN_MEASURABLE_BOREL_NEGINF", ``!f a. f IN measurable a Borel ==> 3164 ({x | f x = NegInf} INTER space a IN subsets a )``, 3165 RW_TAC std_ss [IN_MEASURABLE_BOREL,GSPECIFICATION,IN_FUNSET,IN_UNIV] 3166 >> `{x | f x = NegInf} INTER space a = 3167 BIGINTER (IMAGE (\n. {x | f x < -(&n)} INTER space a) UNIV)` 3168 by (RW_TAC std_ss [EXTENSION,IN_BIGINTER_IMAGE,IN_UNIV,GSPECIFICATION,IN_INTER] 3169 >> EQ_TAC >- METIS_TAC [num_not_infty,lt_infty,extreal_ainv_def,extreal_of_num_def] 3170 >> RW_TAC std_ss [] 3171 >> SPOSE_NOT_THEN ASSUME_TAC 3172 >> METIS_TAC [SIMP_EXTREAL_ARCH,extreal_lt_def,extreal_ainv_def,neg_neg,lt_neg]) 3173 >> RW_TAC std_ss [] 3174 >> RW_TAC std_ss [IN_FUNSET,IN_UNIV,SIGMA_ALGEBRA_FN_BIGINTER]); 3175 3176val IN_MEASURABLE_BOREL_ALT1 = store_thm 3177 ("IN_MEASURABLE_BOREL_ALT1", ``!f a. f IN measurable a Borel = 3178 ( sigma_algebra a /\ f IN (space a -> UNIV) /\ 3179 !c. ({x | c <= f x} INTER space a) IN subsets a )``, 3180 RW_TAC std_ss [IN_MEASURABLE_BOREL,GSPECIFICATION,IN_FUNSET,IN_UNIV] 3181 >> EQ_TAC 3182 >- (RW_TAC std_ss [] 3183 >> `{x | c <= f x} = PREIMAGE f {x | c <= x}` by RW_TAC std_ss[PREIMAGE_def, GSPECIFICATION] 3184 >> `!c. {x | f x < c} = PREIMAGE f {x | x < c}` 3185 by RW_TAC std_ss[PREIMAGE_def, GSPECIFICATION] 3186 >> `!c. space a DIFF ((PREIMAGE f {x | x < c}) INTER space a) IN subsets a` 3187 by METIS_TAC [sigma_algebra_def,algebra_def] 3188 >> `!c. space a DIFF (PREIMAGE f {x | x < c}) IN subsets a` 3189 by METIS_TAC [DIFF_INTER2] 3190 >> `!c. (PREIMAGE f (COMPL {x | x < c}) INTER space a) IN subsets a` 3191 by METIS_TAC [GSYM PREIMAGE_COMPL_INTER] 3192 >> `!c. COMPL {x | x < c} = {x | c <= x}` 3193 by RW_TAC std_ss [EXTENSION, IN_COMPL, IN_UNIV, IN_DIFF, GSPECIFICATION, extreal_lt_def] 3194 >> FULL_SIMP_TAC std_ss []) 3195 >> RW_TAC std_ss [] 3196 >> `{x | f x < c} = PREIMAGE f {x | x < c}` 3197 by RW_TAC std_ss[PREIMAGE_def,GSPECIFICATION] 3198 >> `!c. {x | c <= f x} = PREIMAGE f {x | c <= x}` 3199 by RW_TAC std_ss[PREIMAGE_def,GSPECIFICATION] 3200 >> `!c. space a DIFF ((PREIMAGE f {x | c <= x}) INTER space a) IN subsets a` 3201 by METIS_TAC [sigma_algebra_def,algebra_def] 3202 >> `!c. space a DIFF (PREIMAGE f {x | c <= x}) IN subsets a` 3203 by METIS_TAC [DIFF_INTER2] 3204 >> `!c. (PREIMAGE f (COMPL {x | c <= x}) INTER space a) IN subsets a` 3205 by METIS_TAC [GSYM PREIMAGE_COMPL_INTER] 3206 >> `!c. COMPL {x | c <= x} = {x | x < c}` 3207 by RW_TAC std_ss [EXTENSION, IN_COMPL, IN_UNIV, IN_DIFF, GSPECIFICATION, extreal_lt_def] 3208 >> METIS_TAC []); 3209 3210val IN_MEASURABLE_BOREL_ALT2 = store_thm 3211("IN_MEASURABLE_BOREL_ALT2", ``!f a. f IN measurable a Borel = 3212 (sigma_algebra a /\ f IN (space a -> UNIV) /\ 3213 !c. ({x | f x <= c } INTER space a) IN subsets a)``, 3214 RW_TAC std_ss [] 3215 >> EQ_TAC 3216 >- (RW_TAC std_ss [IN_MEASURABLE_BOREL] 3217 >> Cases_on `c = NegInf` 3218 >- (RW_TAC std_ss [le_infty] >> METIS_TAC [IN_MEASURABLE_BOREL, IN_MEASURABLE_BOREL_NEGINF]) 3219 >> Cases_on `c = PosInf` 3220 >- (RW_TAC std_ss [le_infty,GSPEC_T,INTER_UNIV] 3221 >> FULL_SIMP_TAC std_ss [ALGEBRA_SPACE,sigma_algebra_def]) 3222 >> `?r. c = Normal r` by METIS_TAC [extreal_cases] 3223 >> RW_TAC std_ss [] 3224 >> `{x | f x <= Normal r} INTER (space a) = 3225 BIGINTER (IMAGE (\n:num. {x | f x < Normal (r + (1 / 2) pow n)} INTER space a) UNIV)` 3226 by (RW_TAC std_ss [EXTENSION, IN_BIGINTER_IMAGE, IN_UNIV,IN_INTER] 3227 >> EQ_TAC 3228 >- (RW_TAC std_ss [GSPECIFICATION,GSYM extreal_add_def] 3229 >> `0:real < (1 / 2) pow n` by RW_TAC real_ss [REAL_POW_LT] 3230 >> `0 < Normal ((1 / 2) pow n)` by METIS_TAC [extreal_of_num_def, extreal_lt_eq] 3231 >> Cases_on `f x = NegInf` >- METIS_TAC [lt_infty,extreal_add_def] 3232 >> METIS_TAC [let_add2,extreal_of_num_def,extreal_not_infty, add_rzero, le_infty]) 3233 >> RW_TAC std_ss [GSPECIFICATION] 3234 >> `!n. f x < Normal (r + (1 / 2) pow n)` by METIS_TAC [] 3235 >> `(\n. r + (1 / 2) pow n) = (\n. (\n. r) n + (\n. (1 / 2) pow n) n) ` 3236 by RW_TAC real_ss [FUN_EQ_THM] 3237 >> `(\n. r) --> r` by RW_TAC std_ss [SEQ_CONST] 3238 >> `(\n. (1 / 2) pow n) --> 0` by RW_TAC real_ss [SEQ_POWER] 3239 >> `(\n. r + (1 / 2) pow n) --> r` 3240 by METIS_TAC [Q.SPECL [`(\n. r)`,`r`,`(\n. (1/2) pow n)`,`0`] SEQ_ADD, 3241 REAL_ADD_RID] 3242 >> Cases_on `f x = NegInf` >- METIS_TAC [le_infty] 3243 >> `f x <> PosInf` by METIS_TAC [lt_infty] 3244 >> `?r. f x = Normal r` by METIS_TAC [extreal_cases] 3245 >> FULL_SIMP_TAC std_ss [extreal_lt_eq,extreal_le_def] 3246 >> METIS_TAC [REAL_LT_IMP_LE, 3247 Q.SPECL [`r'`,`r`,`(\n. r + (1 / 2) pow n)`] LE_SEQ_IMP_LE_LIM]) 3248 >> `BIGINTER (IMAGE (\n:num. {x | f x < Normal (r + (1 / 2) pow n)} INTER space a) UNIV) 3249 IN subsets a` 3250 by (RW_TAC std_ss [] 3251 >> (MP_TAC o Q.SPEC `a`) SIGMA_ALGEBRA_FN_BIGINTER 3252 >> RW_TAC std_ss [] 3253 >> `(\n. {x | f x < Normal (r + (1/2) pow n)} INTER space a) IN (UNIV -> subsets a)` by (RW_TAC std_ss [IN_FUNSET]) 3254 >> METIS_TAC []) 3255 >> METIS_TAC []) 3256 >> RW_TAC std_ss [IN_MEASURABLE_BOREL] 3257 >> `!c. {x | c < f x} INTER space a IN subsets a` 3258 by (RW_TAC std_ss [] 3259 >> `{x | c < f x} INTER space a = (space a) DIFF ({x | f x <= c} INTER space a)` 3260 by (RW_TAC std_ss [EXTENSION,IN_INTER,GSPECIFICATION,IN_DIFF] 3261 >> METIS_TAC [extreal_lt_def]) 3262 >> METIS_TAC [sigma_algebra_def,algebra_def]) 3263 >> `{x | f x = PosInf} INTER space a = BIGINTER (IMAGE (\n. {x | &n < f x} INTER space a) UNIV)` 3264 by (RW_TAC std_ss [EXTENSION,IN_BIGINTER_IMAGE,IN_UNIV,GSPECIFICATION,IN_INTER] 3265 >> EQ_TAC >- METIS_TAC [num_not_infty,lt_infty] 3266 >> RW_TAC std_ss [] 3267 >> SPOSE_NOT_THEN ASSUME_TAC 3268 >> METIS_TAC [SIMP_EXTREAL_ARCH,extreal_lt_def]) 3269 >> `{x | f x = PosInf} INTER space a IN subsets a` 3270 by RW_TAC std_ss [IN_FUNSET,IN_UNIV,SIGMA_ALGEBRA_FN_BIGINTER] 3271 >> `{x | f x <> PosInf} INTER space a = (space a) DIFF ({x | f x = PosInf} INTER (space a))` 3272 by (RW_TAC std_ss [IN_INTER, EXTENSION, GSPECIFICATION, IN_SING, IN_DIFF] >> METIS_TAC []) 3273 >> Cases_on `c = PosInf` 3274 >- (RW_TAC std_ss [GSYM lt_infty] >> METIS_TAC [sigma_algebra_def, algebra_def, lt_infty]) 3275 >> Cases_on `c = NegInf` 3276 >- (RW_TAC std_ss [lt_infty,GSPEC_F,INTER_EMPTY] 3277 >> FULL_SIMP_TAC std_ss [sigma_algebra_def, algebra_def]) 3278 >> `?r. c = Normal r` by METIS_TAC [extreal_cases] 3279 >> RW_TAC std_ss [] 3280 >> `{x | f x < Normal r} INTER (space a) = 3281 BIGUNION (IMAGE (\n:num. {x | f x <= Normal (r - (1/2) pow n)} INTER space a) UNIV)` 3282 by (RW_TAC std_ss [EXTENSION, IN_BIGUNION_IMAGE, IN_UNIV, IN_INTER, GSPECIFICATION] 3283 >> `(\n. r - (1 / 2) pow n) = (\n. (\n. r) n - (\n. (1 / 2) pow n) n)` 3284 by RW_TAC real_ss [FUN_EQ_THM] 3285 >> `(\n. r) --> r` by RW_TAC std_ss [SEQ_CONST] 3286 >> `(\n. (1 / 2) pow n) --> 0` by RW_TAC real_ss [SEQ_POWER] 3287 >> `(\n. r - (1 / 2) pow n) --> r` 3288 by METIS_TAC [Q.SPECL [`(\n. r)`,`r`,`(\n. (1/2) pow n)`,`0`] SEQ_SUB, 3289 REAL_SUB_RZERO] 3290 >> EQ_TAC 3291 >- (RW_TAC std_ss [] 3292 >> Cases_on `f x = NegInf` >- METIS_TAC [le_infty] 3293 >> `f x <> PosInf` by METIS_TAC [lt_infty] 3294 >> `?r. f x = Normal r` by METIS_TAC [extreal_cases] 3295 >> FULL_SIMP_TAC std_ss [extreal_lt_eq,extreal_le_def] 3296 >> `!e:real. 0 < e ==> ?N. !n. n >= N ==> abs ((1 / 2) pow n) < e` 3297 by FULL_SIMP_TAC real_ss [Q.SPECL [`(\n. (1/2) pow n)`,`0`] SEQ, REAL_SUB_RZERO] 3298 >> `!n. abs ((1 / 2) pow n):real = (1 / 2) pow n` 3299 by FULL_SIMP_TAC real_ss [POW_POS,ABS_REFL] 3300 >> `!e:real. 0 < e ==> ?N. !n. n >= N ==> (1 / 2) pow n < e` by METIS_TAC [] 3301 >> `?N. !n. n >= N ==> (1 / 2) pow n < r - r'` by METIS_TAC [REAL_SUB_LT] 3302 >> Q.EXISTS_TAC `N` 3303 >> `(1 / 2) pow N < r - r'` by FULL_SIMP_TAC real_ss [] 3304 >> FULL_SIMP_TAC real_ss [GSYM REAL_LT_ADD_SUB, REAL_ADD_COMM, REAL_LT_IMP_LE]) 3305 >> RW_TAC std_ss [] 3306 >- (`!n. - ((1 / 2) pow n) < 0:real` 3307 by METIS_TAC [REAL_POW_LT, REAL_NEG_0, REAL_LT_NEG, EVAL ``0:real < 1/2``] 3308 >> `!n. r - (1 / 2) pow n < r` by METIS_TAC [REAL_LT_IADD, REAL_ADD_RID, real_sub] 3309 >> Cases_on `f x = NegInf` >- METIS_TAC [lt_infty] 3310 >> `f x <> PosInf` by METIS_TAC [le_infty, extreal_not_infty] 3311 >> `?r. f x = Normal r` by METIS_TAC [extreal_cases] 3312 >> FULL_SIMP_TAC std_ss [extreal_lt_eq, extreal_le_def] 3313 >> METIS_TAC [REAL_LET_TRANS]) 3314 >> METIS_TAC []) 3315 >> FULL_SIMP_TAC std_ss [] 3316 >> MATCH_MP_TAC SIGMA_ALGEBRA_ENUM 3317 >> RW_TAC std_ss [IN_FUNSET]); 3318 3319val IN_MEASURABLE_BOREL_ALT3 = store_thm 3320("IN_MEASURABLE_BOREL_ALT3", ``!f a. f IN measurable a Borel = 3321 sigma_algebra a /\ f IN (space a -> UNIV) /\ 3322 !c. ({x | c < f x } INTER space a) IN subsets a``, 3323 RW_TAC std_ss [IN_MEASURABLE_BOREL_ALT2,GSPECIFICATION] 3324 >> EQ_TAC 3325 >- (RW_TAC std_ss [] 3326 >> `{x| c < f x} = PREIMAGE f {x | c < x}` by RW_TAC std_ss[PREIMAGE_def, GSPECIFICATION] 3327 >> `!c. {x | f x <= c} = PREIMAGE f {x | x <= c}` 3328 by RW_TAC std_ss[PREIMAGE_def, GSPECIFICATION] 3329 >> `!c. space a DIFF ((PREIMAGE f {x | x <= c}) INTER space a) IN subsets a` 3330 by METIS_TAC [sigma_algebra_def, algebra_def] 3331 >> `!c. space a DIFF (PREIMAGE f {x | x <= c}) IN subsets a` 3332 by METIS_TAC [DIFF_INTER2] 3333 >> `!c. (PREIMAGE f (COMPL {x | x <= c}) INTER space a) IN subsets a` 3334 by METIS_TAC [GSYM PREIMAGE_COMPL_INTER] 3335 >> `COMPL {x | x <= c} = {x | c < x}` 3336 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_COMPL, extreal_lt_def] 3337 >> METIS_TAC []) 3338 >> RW_TAC std_ss [] 3339 >> `{x | f x <= c} = PREIMAGE f {x | x <= c}` by RW_TAC std_ss[PREIMAGE_def, GSPECIFICATION] 3340 >> `!c. { x | c < f x } = PREIMAGE f { x | c < x }` 3341 by RW_TAC std_ss[PREIMAGE_def, GSPECIFICATION] 3342 >> `!c. space a DIFF ((PREIMAGE f {x | c < x}) INTER space a) IN subsets a` 3343 by METIS_TAC [sigma_algebra_def, algebra_def] 3344 >> `!c. space a DIFF (PREIMAGE f {x | c < x}) IN subsets a` by METIS_TAC [DIFF_INTER2] 3345 >> `!c. (PREIMAGE f (COMPL {x | c < x}) INTER space a) IN subsets a` 3346 by METIS_TAC [GSYM PREIMAGE_COMPL_INTER] 3347 >> `COMPL {x | c < x} = {x | x <= c}` 3348 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_COMPL, extreal_lt_def] 3349 >> METIS_TAC []); 3350 3351val IN_MEASURABLE_BOREL_ALT4 = store_thm 3352("IN_MEASURABLE_BOREL_ALT4", ``!f a. f IN measurable a Borel = 3353 sigma_algebra a /\ f IN (space a -> UNIV) /\ 3354 !c d. ({x | c <= f x /\ f x < d} INTER space a) IN subsets a``, 3355 RW_TAC std_ss [] 3356 >> EQ_TAC 3357 >- (STRIP_TAC 3358 >> CONJ_TAC >- METIS_TAC [IN_MEASURABLE_BOREL] 3359 >> CONJ_TAC >- METIS_TAC [IN_MEASURABLE_BOREL] 3360 >> RW_TAC std_ss [] 3361 >> `(!d. {x | f x < d} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL] 3362 >> `(!c. {x | c <= f x} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL_ALT1] 3363 >> `{x | c <= f x /\ f x < d} INTER space a = 3364 ({x | c <= f x} INTER space a) INTER ({x | f x < d} INTER space a)` 3365 by (RW_TAC std_ss [EXTENSION,IN_INTER,GSPECIFICATION] >> METIS_TAC []) 3366 >> METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, algebra_def, IN_MEASURABLE_BOREL]) 3367 >> RW_TAC std_ss [IN_MEASURABLE_BOREL] 3368 >> `{x | f x < c} INTER space a = {x | NegInf <= f x /\ f x < c} INTER space a` 3369 by RW_TAC std_ss [le_infty] 3370 >> METIS_TAC []); 3371 3372val IN_MEASURABLE_BOREL_ALT5 = store_thm 3373("IN_MEASURABLE_BOREL_ALT5", ``!f a. f IN measurable a Borel = 3374 sigma_algebra a /\ f IN (space a -> UNIV) /\ 3375 !c d. ({x | c < f x /\ f x <= d} INTER space a) IN subsets a``, 3376 RW_TAC std_ss [] 3377 >> EQ_TAC 3378 >- (STRIP_TAC 3379 >> CONJ_TAC >- METIS_TAC [IN_MEASURABLE_BOREL] 3380 >> CONJ_TAC >- METIS_TAC [IN_MEASURABLE_BOREL] 3381 >> RW_TAC std_ss [] 3382 >> `(!d. {x | f x <= d} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL_ALT2] 3383 >> `(!c. {x | c < f x} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL_ALT3] 3384 >> `{x | c < f x /\ f x <= d} INTER space a = 3385 ({x | c < f x} INTER space a) INTER ({x | f x <= d} INTER space a)` 3386 by (RW_TAC std_ss [EXTENSION,IN_INTER,GSPECIFICATION] >> METIS_TAC []) 3387 >> METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, algebra_def, IN_MEASURABLE_BOREL]) 3388 >> RW_TAC std_ss [IN_MEASURABLE_BOREL_ALT3] 3389 >> `{x | c < f x} INTER space a = {x | c < f x /\ f x <= PosInf} INTER space a` 3390 by RW_TAC std_ss [le_infty] 3391 >> METIS_TAC []); 3392 3393val IN_MEASURABLE_BOREL_ALT6 = store_thm 3394("IN_MEASURABLE_BOREL_ALT6", ``!f a. f IN measurable a Borel = 3395 sigma_algebra a /\ f IN (space a -> UNIV) /\ 3396 !c d. ({x | c <= f x /\ f x <= d} INTER space a) IN subsets a``, 3397 RW_TAC std_ss [] 3398 >> EQ_TAC 3399 >- (STRIP_TAC 3400 >> CONJ_TAC >- METIS_TAC [IN_MEASURABLE_BOREL] 3401 >> CONJ_TAC >- METIS_TAC [IN_MEASURABLE_BOREL] 3402 >> RW_TAC std_ss [] 3403 >> `(!d. {x | f x <= d} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL_ALT2] 3404 >> `(!c. {x | c <= f x} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL_ALT1] 3405 >> `{x | c <= f x /\ f x <= d} INTER space a = 3406 ({x | c <= f x} INTER space a) INTER ({x | f x <= d} INTER space a)` 3407 by (RW_TAC std_ss [EXTENSION,IN_INTER,GSPECIFICATION] >> METIS_TAC []) 3408 >> METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, algebra_def, IN_MEASURABLE_BOREL]) 3409 >> RW_TAC std_ss [IN_MEASURABLE_BOREL_ALT2] 3410 >> `{x | f x <= c} INTER space a = {x | NegInf <= f x /\ f x <= c} INTER space a` 3411 by RW_TAC std_ss [le_infty] 3412 >> METIS_TAC []); 3413 3414val IN_MEASURABLE_BOREL_ALT7 = store_thm 3415("IN_MEASURABLE_BOREL_ALT7", ``!f a. f IN measurable a Borel ==> 3416 sigma_algebra a /\ f IN (space a -> UNIV) /\ 3417 !c d. ({x | c < f x /\ f x < d} INTER space a) IN subsets a``, 3418 RW_TAC std_ss [] 3419 >| [METIS_TAC [IN_MEASURABLE_BOREL], 3420 METIS_TAC [IN_MEASURABLE_BOREL], 3421 `(!d. {x | f x < d} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL] 3422 >> `(!c. {x | c < f x} INTER space a IN subsets a)` by METIS_TAC [IN_MEASURABLE_BOREL_ALT3] 3423 >> `{x | c < f x /\ f x < d} INTER space a = 3424 ({x | c < f x} INTER space a) INTER ({x | f x < d} INTER space a)` 3425 by (RW_TAC std_ss [EXTENSION, IN_INTER, GSPECIFICATION] >> METIS_TAC []) 3426 >> METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, algebra_def, IN_MEASURABLE_BOREL]]); 3427 3428val IN_MEASURABLE_BOREL_ALT8 = store_thm 3429 ("IN_MEASURABLE_BOREL_ALT8", ``!f a. f IN measurable a Borel ==> 3430 sigma_algebra a /\ f IN (space a -> UNIV) /\ 3431 (!c. ({x| f x = c} INTER space a) IN subsets a)``, 3432 RW_TAC std_ss [IN_MEASURABLE_BOREL_ALT6] 3433 >> `{x | f x = c} = {x | c <= f x /\ f x <= c}` 3434 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, le_antisym, EQ_SYM_EQ] 3435 >> METIS_TAC []); 3436 3437val IN_MEASURABLE_BOREL_ALT9 = store_thm 3438 ("IN_MEASURABLE_BOREL_ALT9", ``!f a. f IN measurable a Borel ==> 3439 sigma_algebra a /\ f IN (space a -> UNIV) /\ 3440 (!c. ({x| f x <> c} INTER space a) IN subsets a)``, 3441 RW_TAC std_ss [IN_FUNSET,IN_UNIV] 3442 >- FULL_SIMP_TAC std_ss [IN_MEASURABLE_BOREL] 3443 >> `{x | f x <> c} INTER space a = space a DIFF ({x | f x = c} INTER space a)` 3444 by (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, GSPECIFICATION, IN_SING] >> METIS_TAC []) 3445 >> METIS_TAC [IN_MEASURABLE_BOREL, IN_MEASURABLE_BOREL_ALT8, sigma_algebra_def, algebra_def]); 3446 3447val IN_MEASURABLE_BOREL_ALL = store_thm 3448 ("IN_MEASURABLE_BOREL_ALL",``!f a. f IN measurable a Borel ==> 3449 (!c. {x | f x < c} INTER space a IN subsets a) /\ 3450 (!c. {x | c <= f x} INTER space a IN subsets a) /\ 3451 (!c. {x | f x <= c} INTER space a IN subsets a) /\ 3452 (!c. {x | c < f x} INTER space a IN subsets a) /\ 3453 (!c d. {x | c < f x /\ f x < d} INTER space a IN subsets a) /\ 3454 (!c d. {x | c <= f x /\ f x < d} INTER space a IN subsets a) /\ 3455 (!c d. {x | c < f x /\ f x <= d} INTER space a IN subsets a) /\ 3456 (!c d. {x | c <= f x /\ f x <= d} INTER space a IN subsets a) /\ 3457 (!c. {x | f x <> c} INTER space a IN subsets a) /\ 3458 (!c. {x | f x = c} INTER space a IN subsets a)``, 3459 RW_TAC std_ss [] 3460 >> METIS_TAC [IN_MEASURABLE_BOREL, IN_MEASURABLE_BOREL_ALT1, IN_MEASURABLE_BOREL_ALT2, 3461 IN_MEASURABLE_BOREL_ALT3, IN_MEASURABLE_BOREL_ALT4, IN_MEASURABLE_BOREL_ALT5, 3462 IN_MEASURABLE_BOREL_ALT6, IN_MEASURABLE_BOREL_ALT7, IN_MEASURABLE_BOREL_ALT8, 3463 IN_MEASURABLE_BOREL_ALT9]); 3464 3465val IN_MEASURABLE_BOREL_ALL_MEASURE = store_thm 3466 ("IN_MEASURABLE_BOREL_ALL_MEASURE",``!f m. f IN measurable (m_space m,measurable_sets m) Borel 3467 ==> 3468 (!c. {x | f x < c} INTER m_space m IN measurable_sets m) /\ 3469 (!c. {x | c <= f x} INTER m_space m IN measurable_sets m) /\ 3470 (!c. {x | f x <= c} INTER m_space m IN measurable_sets m) /\ 3471 (!c. {x | c < f x} INTER m_space m IN measurable_sets m) /\ 3472 (!c d. {x | c < f x /\ f x < d} INTER m_space m IN measurable_sets m) /\ 3473 (!c d. {x | c <= f x /\ f x < d} INTER m_space m IN measurable_sets m) /\ 3474 (!c d. {x | c < f x /\ f x <= d} INTER m_space m IN measurable_sets m) /\ 3475 (!c d. {x | c <= f x /\ f x <= d} INTER m_space m IN measurable_sets m) /\ 3476 (!c. {x | f x = c} INTER m_space m IN measurable_sets m) /\ 3477 (!c. {x | f x <> c} INTER m_space m IN measurable_sets m)``, 3478 METIS_TAC [IN_MEASURABLE_BOREL_ALL, m_space_def, space_def, measurable_sets_def, subsets_def]); 3479 3480val IN_MEASURABLE_BOREL_LT = store_thm 3481 ("IN_MEASURABLE_BOREL_LT", ``!f g a. f IN measurable a Borel /\ g IN measurable a Borel 3482 ==> ({x | f x < g x} INTER space a) IN subsets a``, 3483 RW_TAC std_ss [] 3484 >> `{x | f x < g x} INTER space a = 3485 BIGUNION (IMAGE (\r. {x | f x < r /\ r < g x} INTER space a) Q_set)` 3486 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION_IMAGE, IN_INTER] 3487 >> EQ_TAC 3488 >- RW_TAC std_ss [Q_DENSE_IN_R] 3489 >> METIS_TAC [lt_trans]) 3490 >> POP_ORW 3491 >> MATCH_MP_TAC BIGUNION_IMAGE_Q 3492 >> CONJ_TAC 3493 >- FULL_SIMP_TAC std_ss [IN_MEASURABLE_BOREL] 3494 >> RW_TAC std_ss [IN_FUNSET] 3495 >> `{x | f x < r /\ r < g x} INTER space a = 3496 ({x | f x < r} INTER space a) INTER ({x | r < g x} INTER space a)` 3497 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] >> METIS_TAC []) 3498 >> POP_ORW 3499 >> MATCH_MP_TAC ALGEBRA_INTER 3500 >> CONJ_TAC 3501 >- FULL_SIMP_TAC std_ss [IN_MEASURABLE_BOREL, sigma_algebra_def] 3502 >> `?c. r = Normal c` by METIS_TAC [rat_not_infty, extreal_cases] 3503 >> METIS_TAC [IN_MEASURABLE_BOREL_ALL]); 3504 3505val IN_MEASURABLE_BOREL_LE = store_thm 3506 ("IN_MEASURABLE_BOREL_LE", ``!f g a. f IN measurable a Borel /\ g IN measurable a Borel ==> 3507 ({x | f x <= g x} INTER space a) IN subsets a``, 3508 RW_TAC std_ss [] 3509 >> `{x | f x <= g x} INTER space a = space a DIFF ({x | g x < f x} INTER space a)` 3510 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER, IN_DIFF] 3511 >> METIS_TAC [extreal_lt_def]) 3512 >> `{x | g x < f x} INTER space a IN subsets a` by RW_TAC std_ss [IN_MEASURABLE_BOREL_LT] 3513 >> METIS_TAC [algebra_def, IN_MEASURABLE_BOREL, sigma_algebra_def]); 3514 3515val SPACE_BOREL = store_thm 3516 ("SPACE_BOREL", ``space Borel= UNIV``, 3517 METIS_TAC [Borel_def, sigma_def, space_def]); 3518 3519val BOREL_MEASURABLE_SETS1 = store_thm 3520 ("BOREL_MEASURABLE_SETS1",``!c. {x | x < c} IN subsets Borel``, 3521 RW_TAC std_ss [Borel_def] 3522 >> MATCH_MP_TAC IN_SIGMA 3523 >> RW_TAC std_ss [IN_IMAGE,IN_UNIV] 3524 >> METIS_TAC []); 3525 3526val BOREL_MEASURABLE_SETS2 = store_thm 3527 ("BOREL_MEASURABLE_SETS2",``!c. {x | c <= x} IN subsets Borel``, 3528 RW_TAC std_ss [] 3529 >> `{x | c <= x} = UNIV DIFF {x | x < c}` 3530 by RW_TAC std_ss [extreal_lt_def, EXTENSION, GSPECIFICATION, DIFF_DEF, IN_UNIV, real_lte] 3531 >> METIS_TAC [SPACE_BOREL, SIGMA_ALGEBRA_BOREL, sigma_algebra_def, algebra_def, 3532 BOREL_MEASURABLE_SETS1]); 3533 3534val BOREL_MEASURABLE_SETS3 = store_thm 3535 ("BOREL_MEASURABLE_SETS3",``!c. {x | x <= c} IN subsets Borel``, 3536 RW_TAC std_ss [] 3537 >> ASSUME_TAC SIGMA_ALGEBRA_BOREL 3538 >> (MP_TAC o UNDISCH o Q.SPEC `Borel`) (INST_TYPE [alpha |-> ``:extreal``] 3539 SIGMA_ALGEBRA_FN_BIGINTER) 3540 >> RW_TAC std_ss [] 3541 >> Cases_on `c` 3542 >| [`{x | x = NegInf} = BIGINTER (IMAGE (\n. {x | x < -(&n)}) UNIV)` 3543 by (RW_TAC std_ss [EXTENSION, IN_BIGINTER_IMAGE, IN_UNIV, GSPECIFICATION] 3544 >> EQ_TAC >- METIS_TAC [num_not_infty, lt_infty, extreal_ainv_def, extreal_of_num_def] 3545 >> RW_TAC std_ss [] 3546 >> SPOSE_NOT_THEN ASSUME_TAC 3547 >> METIS_TAC [SIMP_EXTREAL_ARCH, extreal_lt_def, extreal_ainv_def, neg_neg, lt_neg]) 3548 >> RW_TAC std_ss [le_infty] 3549 >> Q.PAT_X_ASSUM `!f. P ==> BIGINTER s IN subsets Borel` MATCH_MP_TAC 3550 >> RW_TAC std_ss [IN_FUNSET,BOREL_MEASURABLE_SETS1], 3551 RW_TAC std_ss [le_infty,GSPEC_T,INTER_UNIV] 3552 >> METIS_TAC [ALGEBRA_SPACE,SPACE_BOREL,sigma_algebra_def], 3553 `!c. {x | x <= Normal c} = 3554 BIGINTER (IMAGE (\n:num. {x | x < Normal (c + (1/2) pow n)}) UNIV)` 3555 by (RW_TAC std_ss [EXTENSION, IN_BIGINTER_IMAGE, IN_UNIV, IN_INTER] 3556 >> EQ_TAC 3557 >- (RW_TAC std_ss [GSPECIFICATION] 3558 >> `0:real < (1/2) pow n` by RW_TAC real_ss [REAL_POW_LT] 3559 >> Cases_on `x = NegInf` >- METIS_TAC [lt_infty] 3560 >> `x <> PosInf` by METIS_TAC [le_infty, extreal_not_infty] 3561 >> `0 < Normal ((1 / 2) pow n)` by METIS_TAC [extreal_lt_eq, extreal_of_num_def] 3562 >> RW_TAC std_ss [GSYM extreal_add_def] 3563 >> METIS_TAC [extreal_of_num_def, extreal_not_infty, let_add2, add_rzero]) 3564 >> RW_TAC std_ss [GSPECIFICATION] 3565 >> `!n. x < Normal (c + (1 / 2) pow n)` by METIS_TAC [] 3566 >> `(\n. c + (1 / 2) pow n) = (\n. (\n. c) n + (\n. (1 / 2) pow n) n) ` 3567 by RW_TAC real_ss [FUN_EQ_THM] 3568 >> `(\n. c) --> c` by RW_TAC std_ss [SEQ_CONST] 3569 >> `(\n. (1 / 2) pow n) --> 0` by RW_TAC real_ss [SEQ_POWER] 3570 >> `(\n. c + (1 / 2) pow n) --> c` 3571 by METIS_TAC [Q.SPECL [`(\n. c)`,`c`,`(\n. (1/2) pow n)`,`0`] 3572 SEQ_ADD,REAL_ADD_RID] 3573 >> Cases_on `x = NegInf` >- RW_TAC std_ss [le_infty] 3574 >> `x <> PosInf` by METIS_TAC [lt_infty] 3575 >> `?r. x = Normal r` by METIS_TAC [extreal_cases] 3576 >> FULL_SIMP_TAC std_ss [extreal_le_def, extreal_lt_eq] 3577 >> METIS_TAC [REAL_LT_IMP_LE,Q.SPECL [`r`,`c`,`(\n. c + (1 / 2) pow n)`] 3578 LE_SEQ_IMP_LE_LIM]) 3579 >> POP_ORW 3580 >> POP_ASSUM MATCH_MP_TAC 3581 >> RW_TAC std_ss [IN_FUNSET,BOREL_MEASURABLE_SETS1]]); 3582 3583val BOREL_MEASURABLE_SETS4 = store_thm 3584 ("BOREL_MEASURABLE_SETS4",``!c. {x | c < x} IN subsets Borel``, 3585 RW_TAC std_ss [] 3586 >> `{x | c < x} = UNIV DIFF {x | x <= c}` 3587 by RW_TAC std_ss [extreal_lt_def, EXTENSION, GSPECIFICATION, DIFF_DEF, 3588 IN_UNIV, real_lte] 3589 >> METIS_TAC [SPACE_BOREL, SIGMA_ALGEBRA_BOREL, sigma_algebra_def, algebra_def, 3590 BOREL_MEASURABLE_SETS3]); 3591 3592val BOREL_MEASURABLE_SETS5 = store_thm 3593 ("BOREL_MEASURABLE_SETS5", ``!c d. {x | c <= x /\ x < d} IN subsets Borel``, 3594 RW_TAC std_ss [] 3595 >> `!d. {x | x < d} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS1] 3596 >> `!c. {x | c <= x} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS2] 3597 >> `{x | c <= x /\ x < d} = {x | c <= x} INTER {x | x < d}` 3598 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3599 >> METIS_TAC [sigma_algebra_def, ALGEBRA_INTER, SIGMA_ALGEBRA_BOREL]); 3600 3601val BOREL_MEASURABLE_SETS6 = store_thm 3602 ("BOREL_MEASURABLE_SETS6", ``!c d. {x | c < x /\ x <= d} IN subsets Borel``, 3603 RW_TAC std_ss [] 3604 >> `!d. {x | x <= d} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS3] 3605 >> `!c. {x | c < x} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS4] 3606 >> `{x | c < x /\ x <= d} = {x | c < x} INTER {x | x <= d}` 3607 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3608 >> METIS_TAC [sigma_algebra_def, ALGEBRA_INTER, SIGMA_ALGEBRA_BOREL]); 3609 3610val BOREL_MEASURABLE_SETS7 = store_thm 3611 ("BOREL_MEASURABLE_SETS7", ``!c d. {x | c <= x /\ x <= d} IN subsets Borel``, 3612 RW_TAC std_ss [] 3613 >> `!d. {x | x <= d} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS3] 3614 >> `!c. {x | c <= x} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS2] 3615 >> `{x | c <= x /\ x <= d} = {x | c <= x} INTER {x | x <= d}` 3616 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3617 >> METIS_TAC [sigma_algebra_def, ALGEBRA_INTER, SIGMA_ALGEBRA_BOREL]); 3618 3619val BOREL_MEASURABLE_SETS8 = store_thm 3620 ("BOREL_MEASURABLE_SETS8", ``!c d. {x | c < x /\ x < d} IN subsets Borel``, 3621 RW_TAC std_ss [] 3622 >> `!d. {x | x < d} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS1] 3623 >> `!c. {x | c < x} IN subsets Borel` by METIS_TAC [BOREL_MEASURABLE_SETS4] 3624 >> `{x | c < x /\ x < d} = {x | c < x} INTER {x | x < d}` 3625 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3626 >> METIS_TAC [sigma_algebra_def, ALGEBRA_INTER, SIGMA_ALGEBRA_BOREL]); 3627 3628val BOREL_MEASURABLE_SETS9 = store_thm 3629 ("BOREL_MEASURABLE_SETS9", ``!c. {c} IN subsets Borel``, 3630 RW_TAC std_ss [] 3631 >> `{c} = {x | c <= x /\ x <= c}` by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_SING, 3632 le_antisym, EQ_SYM_EQ] 3633 >> RW_TAC std_ss [BOREL_MEASURABLE_SETS7]); 3634 3635val BOREL_MEASURABLE_SETS10 = store_thm 3636 ("BOREL_MEASURABLE_SETS10", ``!c. {x | x <> c} IN subsets Borel``, 3637 RW_TAC std_ss [] 3638 >> `{x | x <> c} = (space Borel) DIFF ({c})` 3639 by RW_TAC std_ss [SPACE_BOREL, EXTENSION, IN_DIFF, IN_SING, GSPECIFICATION, IN_UNIV] 3640 >> METIS_TAC [SIGMA_ALGEBRA_BOREL, BOREL_MEASURABLE_SETS9, sigma_algebra_def, algebra_def]); 3641 3642val BOREL_MEASURABLE_SETS = store_thm 3643 ("BOREL_MEASURABLE_SETS", 3644 ``((!c. {x | x < c} IN subsets Borel)) /\ 3645 (!c. {x | c <= x} IN subsets Borel) /\ 3646 (!c. {x | c < x} IN subsets Borel) /\ 3647 (!c. {x | x <= c} IN subsets Borel) /\ 3648 (!c d. {x | c < x /\ x < d} IN subsets Borel) /\ 3649 (!c d. {x | c <= x /\ x < d} IN subsets Borel) /\ 3650 (!c d. {x | c < x /\ x <= d} IN subsets Borel) /\ 3651 (!c d. {x | c <= x /\ x <= d} IN subsets Borel) /\ 3652 (!c. {c} IN subsets Borel) /\ 3653 (!c. {x | x <> c} IN subsets Borel)``, 3654 RW_TAC std_ss [BOREL_MEASURABLE_SETS1, BOREL_MEASURABLE_SETS4, 3655 BOREL_MEASURABLE_SETS3, BOREL_MEASURABLE_SETS2, 3656 BOREL_MEASURABLE_SETS5, BOREL_MEASURABLE_SETS6, 3657 BOREL_MEASURABLE_SETS7, BOREL_MEASURABLE_SETS8, 3658 BOREL_MEASURABLE_SETS9, BOREL_MEASURABLE_SETS10]); 3659 3660 3661(* ******************************************* *) 3662(* Borel measurable functions *) 3663(* ******************************************* *) 3664 3665val IN_MEASURABLE_BOREL_CONST = store_thm 3666 ("IN_MEASURABLE_BOREL_CONST",``!a k f. sigma_algebra a /\ (!x. x IN space a ==> (f x = k)) 3667 ==> f IN measurable a Borel``, 3668 RW_TAC std_ss [IN_MEASURABLE_BOREL,IN_FUNSET, IN_UNIV] 3669 >> Cases_on `c <= k` 3670 >- (`{x | f x < c} INTER space a = {}` 3671 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, NOT_IN_EMPTY, IN_INTER] 3672 >> METIS_TAC [extreal_lt_def]) 3673 >> METIS_TAC [sigma_algebra_def, algebra_def]) 3674 >> `{x | f x < c} INTER space a = space a` 3675 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3676 >> METIS_TAC [extreal_lt_def]) 3677 >> METIS_TAC [sigma_algebra_def, algebra_def, INTER_IDEMPOT, DIFF_EMPTY]); 3678 3679val IN_MEASURABLE_BOREL_INDICATOR = store_thm 3680 ("IN_MEASURABLE_BOREL_INDICATOR",``!a A f. sigma_algebra a /\ A IN subsets a /\ 3681 (!x. x IN space a ==> (f x = (indicator_fn A x))) 3682 ==> f IN measurable a Borel``, 3683 RW_TAC std_ss [IN_MEASURABLE_BOREL] 3684 >- RW_TAC std_ss [IN_FUNSET, UNIV_DEF, indicator_fn_def, IN_DEF] 3685 >> `!x. x IN space a ==> 0 <= f x /\ f x <= 1` 3686 by RW_TAC real_ss [indicator_fn_def, le_01, le_refl] 3687 >> Cases_on `c <= 0` 3688 >- (`{x | f x < c} INTER space a = {}` 3689 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, NOT_IN_EMPTY, IN_INTER, extreal_lt_def] 3690 >> METIS_TAC [le_trans]) 3691 >> METIS_TAC [sigma_algebra_def, algebra_def, DIFF_EMPTY]) 3692 >> Cases_on `1 < c` 3693 >- (`{x | f x < c} INTER space a = space a` 3694 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, NOT_IN_EMPTY, IN_INTER] 3695 >> METIS_TAC [let_trans]) 3696 >> METIS_TAC [sigma_algebra_def, algebra_def, DIFF_EMPTY]) 3697 >> `{x | f x < c} INTER space a = (space a) DIFF A` 3698 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER, IN_DIFF] 3699 >> FULL_SIMP_TAC std_ss [extreal_lt_def, indicator_fn_def] 3700 >> METIS_TAC [extreal_lt_def]) 3701 >> METIS_TAC [sigma_algebra_def, algebra_def, DIFF_EMPTY]); 3702 3703val IN_MEASURABLE_BOREL_CMUL = store_thm 3704 ("IN_MEASURABLE_BOREL_CMUL",``!a f g z. sigma_algebra a /\ f IN measurable a Borel /\ 3705 (!x. x IN space a ==> (g x = Normal (z) * f x)) 3706 ==> g IN measurable a Borel``, 3707 RW_TAC std_ss [] 3708 >> Cases_on `Normal z = 0` 3709 >- METIS_TAC [IN_MEASURABLE_BOREL_CONST,mul_lzero] 3710 >> Cases_on `0 < Normal z` 3711 >- (RW_TAC real_ss [IN_MEASURABLE_BOREL,IN_FUNSET,IN_UNIV] 3712 >> `!c. {x | g x < c} INTER space a = {x | f x < c / Normal z} INTER space a` 3713 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3714 >> METIS_TAC [lt_rdiv, mul_comm, extreal_of_num_def, extreal_lt_eq]) 3715 >> METIS_TAC [IN_MEASURABLE_BOREL_ALL, extreal_div_eq, extreal_of_num_def, extreal_11]) 3716 >> `z < 0` by METIS_TAC [extreal_lt_def, extreal_le_def, extreal_of_num_def, 3717 REAL_LT_LE, GSYM real_lte] 3718 >> RW_TAC real_ss [IN_MEASURABLE_BOREL, IN_FUNSET, IN_UNIV] 3719 >> `!c. {x | g x < c} INTER space a = {x | c / Normal z < f x} INTER space a` 3720 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3721 >> METIS_TAC [lt_rdiv_neg, mul_comm]) 3722 >> METIS_TAC [IN_MEASURABLE_BOREL_ALL]); 3723 3724val IN_MEASURABLE_BOREL_ABS = store_thm 3725 ("IN_MEASURABLE_BOREL_ABS",``!a f g. (sigma_algebra a) /\ f IN measurable a Borel /\ 3726 (!x. x IN space a ==> (g x = abs (f x))) 3727 ==> g IN measurable a Borel``, 3728 RW_TAC real_ss [IN_MEASURABLE_BOREL, IN_UNIV, IN_FUNSET] 3729 >> Cases_on `c <= 0` 3730 >- (`{x | g x < c} INTER space a = {}` 3731 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER, NOT_IN_EMPTY, GSYM real_lte] 3732 >> METIS_TAC [abs_pos,le_trans, extreal_le_def, extreal_of_num_def, extreal_lt_def]) 3733 >> METIS_TAC [sigma_algebra_def, algebra_def]) 3734 >> FULL_SIMP_TAC real_ss [GSYM real_lt] 3735 >> Suff `{x | g x < c} INTER space a = 3736 ({x | f x < c} INTER space a) INTER ({x | -c < f x} INTER space a)` 3737 >- (RW_TAC std_ss [] 3738 >> MATCH_MP_TAC ALGEBRA_INTER 3739 >> METIS_TAC [sigma_algebra_def, IN_MEASURABLE_BOREL_ALL, IN_MEASURABLE_BOREL, IN_FUNSET, 3740 IN_UNIV]) 3741 >> RW_TAC real_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3742 >> EQ_TAC 3743 >- METIS_TAC [abs_bounds_lt] 3744 >> METIS_TAC [abs_bounds_lt]); 3745 3746val IN_MEASURABLE_BOREL_SQR = store_thm 3747 ("IN_MEASURABLE_BOREL_SQR",``!a f g. sigma_algebra a /\ f IN measurable a Borel /\ 3748 (!x. x IN space a ==> (g x = (f x) pow 2)) 3749 ==> g IN measurable a Borel``, 3750 RW_TAC real_ss [] 3751 >> `!c. {x | f x <= c} INTER space a IN subsets a` by RW_TAC std_ss [IN_MEASURABLE_BOREL_ALL] 3752 >> `!c. {x | c <= f x} INTER space a IN subsets a` by RW_TAC std_ss [IN_MEASURABLE_BOREL_ALL] 3753 >> RW_TAC real_ss [IN_UNIV, IN_FUNSET, IN_MEASURABLE_BOREL_ALT2] 3754 >> Cases_on `c < 0` 3755 >- (`{x | g x <= c} INTER space a = {}` 3756 by ( RW_TAC real_ss [EXTENSION, GSPECIFICATION, NOT_IN_EMPTY, IN_INTER, GSYM real_lt] 3757 >> METIS_TAC [le_pow2, lte_trans, extreal_lt_def]) 3758 >> METIS_TAC [sigma_algebra_def, algebra_def]) 3759 >> FULL_SIMP_TAC real_ss [extreal_lt_def] 3760 >> `{x | g x <= c} INTER space a = 3761 ({x | f x <= sqrt (c)} INTER space a) INTER ({x | - (sqrt (c)) <= f x} INTER space a)` 3762 by (RW_TAC real_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3763 >> EQ_TAC 3764 >- (RW_TAC real_ss [] 3765 >- (Cases_on `f x < 0` >- METIS_TAC [lte_trans, lt_imp_le, sqrt_pos_le] 3766 >> METIS_TAC [pow2_sqrt, sqrt_mono_le, le_pow2, extreal_lt_def]) 3767 >> Cases_on `0 <= f x` >- METIS_TAC [le_trans, le_neg, sqrt_pos_le, neg_0] 3768 >> SPOSE_NOT_THEN ASSUME_TAC 3769 >> FULL_SIMP_TAC real_ss [GSYM extreal_lt_def] 3770 >> `sqrt c < - (f x)` by METIS_TAC [lt_neg, neg_neg] 3771 >> `(sqrt c) pow 2 < (- (f x)) pow 2` by RW_TAC real_ss [pow_lt2, sqrt_pos_le] 3772 >> `(sqrt c) pow 2 = c` by METIS_TAC [sqrt_pow2] 3773 >> `(-1) pow 2 = 1` by METIS_TAC [pow_minus1, MULT_RIGHT_1] 3774 >> `(- (f x)) pow 2 = (f x) pow 2` 3775 by RW_TAC std_ss [Once neg_minus1, pow_mul, mul_lone] 3776 >> METIS_TAC [extreal_lt_def]) 3777 >> RW_TAC std_ss [] 3778 >> Cases_on `0 <= f x` >- METIS_TAC [pow_le, sqrt_pow2] 3779 >> FULL_SIMP_TAC real_ss [GSYM extreal_lt_def] 3780 >> `- (f x) <= sqrt c` by METIS_TAC [le_neg, neg_neg] 3781 >> `(- (f x)) pow 2 <= (sqrt c) pow 2` 3782 by METIS_TAC [pow_le, sqrt_pos_le, lt_neg, neg_neg, neg_0, lt_imp_le] 3783 >> `(sqrt c) pow 2 = c` by METIS_TAC [sqrt_pow2] 3784 >> `(-1) pow 2 = 1` by METIS_TAC [pow_minus1,MULT_RIGHT_1] 3785 >> `(- (f x)) pow 2 = (f x) pow 2` 3786 by RW_TAC std_ss [Once neg_minus1, pow_mul, mul_lone] 3787 >> METIS_TAC []) 3788 >> METIS_TAC [sigma_algebra_def, ALGEBRA_INTER, extreal_sqrt_def, extreal_ainv_def]); 3789 3790val IN_MEASURABLE_BOREL_ADD = store_thm 3791 ("IN_MEASURABLE_BOREL_ADD",``!a f g h. sigma_algebra a /\ f IN measurable a Borel /\ 3792 g IN measurable a Borel /\ 3793 (!x. x IN space a ==> (h x = f x + g x)) ==> h IN measurable a Borel``, 3794 REPEAT STRIP_TAC 3795 >> RW_TAC std_ss [IN_MEASURABLE_BOREL] >- RW_TAC std_ss [IN_FUNSET, IN_UNIV] 3796 >> Cases_on `c = NegInf` 3797 >- (RW_TAC std_ss [lt_infty,GSPEC_F,INTER_EMPTY] >> METIS_TAC [sigma_algebra_def, algebra_def]) 3798 >> Cases_on `c = PosInf` 3799 >- (RW_TAC std_ss [GSYM lt_infty] 3800 >> `{x | h x <> PosInf} INTER space a = 3801 ({x | f x <> PosInf} INTER space a) INTER ({x | g x <> PosInf} INTER space a)` 3802 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3803 >> EQ_TAC >- METIS_TAC [add_infty] 3804 >> RW_TAC std_ss [] 3805 >> Cases_on `f x` >> Cases_on `g x` 3806 >> METIS_TAC [extreal_add_def, extreal_not_infty]) 3807 >> METIS_TAC [IN_MEASURABLE_BOREL_ALL, ALGEBRA_INTER, sigma_algebra_def]) 3808 >> `?r1. c = Normal r1` by METIS_TAC [extreal_cases] 3809 >> `{x | h x < Normal r1} INTER (space a) = 3810 BIGUNION (IMAGE (\r. {x | f x < r /\ r < Normal r1 - g x } INTER space a) Q_set)` 3811 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION_IMAGE, IN_UNIV, IN_INTER] 3812 >> EQ_TAC 3813 >- (RW_TAC std_ss [] 3814 >> METIS_TAC [lt_sub_imp, Q_DENSE_IN_R]) 3815 >> REVERSE (RW_TAC std_ss []) 3816 >- METIS_TAC [] 3817 >> METIS_TAC [lt_sub,lt_trans, extreal_not_infty]) 3818 >> FULL_SIMP_TAC std_ss [] 3819 >> MATCH_MP_TAC BIGUNION_IMAGE_Q 3820 >> RW_TAC std_ss [IN_FUNSET] 3821 >> `?y. r = Normal y` by METIS_TAC [Q_not_infty, extreal_cases] 3822 >> `{x | f x < Normal y /\ Normal y < Normal r1 - g x} = 3823 {x | f x < Normal y} INTER {x | Normal y < Normal r1 - g x}` 3824 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3825 >> `({x | f x < Normal y} INTER space a) IN subsets a` 3826 by RW_TAC std_ss [IN_MEASURABLE_BOREL_ALL] 3827 >> `!x. x IN space a ==> ((Normal y < Normal r1 - g x) = (g x < Normal r1 - Normal y))` 3828 by METIS_TAC [lt_sub, extreal_not_infty, add_comm] 3829 >> `{x | Normal y < Normal r1 - g x} INTER space a = 3830 {x | g x < Normal r1 - Normal y} INTER space a` 3831 by (RW_TAC std_ss [IN_INTER, EXTENSION, GSPECIFICATION] 3832 >> METIS_TAC []) 3833 >> `({x | Normal y < Normal r1 - g x} INTER space a) IN subsets a` 3834 by METIS_TAC [IN_MEASURABLE_BOREL_ALL, extreal_sub_def] 3835 >> `(({x | f x < Normal y} INTER space a) INTER 3836 ({x | Normal y < Normal r1 - g x} INTER space a)) = 3837 ({x | f x < Normal y} INTER {x | Normal y < Normal r1 - g x} INTER space a)` 3838 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 3839 >> EQ_TAC >- RW_TAC std_ss [] 3840 >> RW_TAC std_ss []) 3841 >> METIS_TAC [sigma_algebra_def, ALGEBRA_INTER]); 3842 3843val IN_MEASURABLE_BOREL_SUB = store_thm 3844 ("IN_MEASURABLE_BOREL_SUB",``!a f g h. sigma_algebra a /\ f IN measurable a Borel /\ 3845 g IN measurable a Borel /\ 3846 (!x. x IN space a ==> (h x = f x - g x)) ==> h IN measurable a Borel``, 3847 RW_TAC std_ss [] 3848 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_ADD 3849 >> Q.EXISTS_TAC `f` 3850 >> Q.EXISTS_TAC `(\x. - g x)` 3851 >> RW_TAC std_ss [extreal_sub_add] 3852 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_CMUL 3853 >> Q.EXISTS_TAC `g` 3854 >> Q.EXISTS_TAC `-1` 3855 >> RW_TAC std_ss [GSYM extreal_ainv_def, GSYM extreal_of_num_def, GSYM neg_minus1]); 3856 3857val IN_MEASURABLE_BOREL_MUL = store_thm 3858 ("IN_MEASURABLE_BOREL_MUL",``!a f g h. sigma_algebra a /\ f IN measurable a Borel /\ 3859 (!x. x IN space a ==> f x <> NegInf /\ f x <> PosInf /\ 3860 g x <> NegInf /\ g x <> PosInf) /\ 3861 g IN measurable a Borel /\ (!x. x IN space a ==> (h x = f x * g x)) 3862 ==> h IN measurable a Borel``, 3863 RW_TAC std_ss [] 3864 >> `!x. x IN space a ==> (f x * g x = 1 / 2 * ((f x + g x) pow 2 - f x pow 2 - g x pow 2))` 3865 by (RW_TAC std_ss [] 3866 >> (MP_TAC o Q.SPECL [`f x`, `g x`]) add_pow2 3867 >> RW_TAC std_ss [] 3868 >> `?r. f x = Normal r` by METIS_TAC [extreal_cases] 3869 >> `?r. g x = Normal r` by METIS_TAC [extreal_cases] 3870 >> FULL_SIMP_TAC real_ss [extreal_11, extreal_pow_def, extreal_add_def, 3871 extreal_sub_def, extreal_of_num_def, extreal_mul_def, 3872 extreal_div_eq] 3873 >> `r pow 2 + r' pow 2 + 2 * r * r' - r pow 2 - r' pow 2 = 2 * r * r'` 3874 by REAL_ARITH_TAC 3875 >> RW_TAC real_ss [REAL_MUL_ASSOC]) 3876 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_CMUL 3877 >> Q.EXISTS_TAC `(\x. (f x + g x) pow 2 - f x pow 2 - g x pow 2)` 3878 >> Q.EXISTS_TAC `1 / 2` 3879 >> RW_TAC real_ss [extreal_of_num_def, extreal_div_eq] 3880 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_SUB 3881 >> Q.EXISTS_TAC `(\x. (f x + g x) pow 2 - f x pow 2)` 3882 >> Q.EXISTS_TAC `(\x. g x pow 2)` 3883 >> RW_TAC std_ss [] 3884 >-(MATCH_MP_TAC IN_MEASURABLE_BOREL_SUB 3885 >> Q.EXISTS_TAC `(\x. (f x + g x) pow 2)` 3886 >> Q.EXISTS_TAC `(\x. f x pow 2)` 3887 >> RW_TAC std_ss [] 3888 >- (MATCH_MP_TAC IN_MEASURABLE_BOREL_SQR 3889 >> Q.EXISTS_TAC `(\x. (f x + g x))` 3890 >> RW_TAC std_ss [] 3891 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_ADD 3892 >> Q.EXISTS_TAC `f` 3893 >> Q.EXISTS_TAC `g` 3894 >> RW_TAC std_ss []) 3895 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_SQR 3896 >> METIS_TAC []) 3897 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_SQR 3898 >> METIS_TAC []); 3899 3900val IN_MEASURABLE_BOREL_SUM = store_thm 3901 ("IN_MEASURABLE_BOREL_SUM",``!a f g s. FINITE s /\ sigma_algebra a /\ 3902 (!i. i IN s ==> (f i) IN measurable a Borel) /\ 3903 (!x. x IN space a ==> (g x = SIGMA (\i. (f i) x) s)) 3904 ==> g IN measurable a Borel``, 3905 Suff `!s:'b -> bool. FINITE s ==> (\s:'b -> bool. !a f g. FINITE s /\ sigma_algebra a /\ 3906 (!i. i IN s ==> f i IN measurable a Borel) /\ 3907 (!x. x IN space a ==> (g x = SIGMA (\i. f i x) s)) ==> 3908 g IN measurable a Borel) s` 3909 >- METIS_TAC [] 3910 >> MATCH_MP_TAC FINITE_INDUCT 3911 >> RW_TAC std_ss [EXTREAL_SUM_IMAGE_THM, NOT_IN_EMPTY] 3912 >- METIS_TAC [IN_MEASURABLE_BOREL_CONST] 3913 >> FULL_SIMP_TAC std_ss [] 3914 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_ADD 3915 >> Q.EXISTS_TAC `f e` 3916 >> Q.EXISTS_TAC `(\x. SIGMA (\i. f i x) s)` 3917 >> FULL_SIMP_TAC std_ss [IN_INSERT, DELETE_NON_ELEMENT] 3918 >> Q.PAT_X_ASSUM `!a f g. P ==> g IN measurable a Borel` MATCH_MP_TAC 3919 >> Q.EXISTS_TAC `f` 3920 >> RW_TAC std_ss []); 3921 3922val IN_MEASURABLE_BOREL_CMUL_INDICATOR = store_thm 3923 ("IN_MEASURABLE_BOREL_CMUL_INDICATOR",``!a z s. sigma_algebra a /\ s IN subsets a 3924 ==> (\x. Normal z * indicator_fn s x) IN measurable a Borel``, 3925 RW_TAC std_ss [] 3926 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_CMUL 3927 >> Q.EXISTS_TAC `indicator_fn s` 3928 >> Q.EXISTS_TAC `z` 3929 >> RW_TAC std_ss [] 3930 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_INDICATOR 3931 >> METIS_TAC []); 3932 3933val IN_MEASURABLE_BOREL_MUL_INDICATOR = store_thm 3934 ("IN_MEASURABLE_BOREL_MUL_INDICATOR",``!a f s. sigma_algebra a /\ f IN measurable a Borel /\ 3935 s IN subsets a ==> (\x. f x * indicator_fn s x) IN measurable a Borel``, 3936 RW_TAC std_ss [IN_MEASURABLE_BOREL_ALT2, IN_FUNSET, IN_UNIV] 3937 >> Cases_on `0 <= c` 3938 >- (`{x | f x * indicator_fn s x <= c} INTER space a = 3939 (({x | f x <= c} INTER space a) INTER s) UNION (space a DIFF s)` 3940 by (RW_TAC std_ss [indicator_fn_def, EXTENSION, GSPECIFICATION, IN_INTER, 3941 IN_UNION, IN_DIFF] 3942 >> Cases_on `x IN s` >- RW_TAC std_ss [mul_rone, mul_rzero] 3943 >> RW_TAC std_ss [mul_rone, mul_rzero]) 3944 >> POP_ORW 3945 >> MATCH_MP_TAC ALGEBRA_UNION 3946 >> CONJ_TAC >- FULL_SIMP_TAC std_ss [sigma_algebra_def] 3947 >> REVERSE CONJ_TAC >- FULL_SIMP_TAC std_ss [sigma_algebra_def, algebra_def] 3948 >> MATCH_MP_TAC ALGEBRA_INTER 3949 >> FULL_SIMP_TAC std_ss [sigma_algebra_def]) 3950 >> `{x | f x * indicator_fn s x <= c} INTER space a = (({x | f x <= c} INTER space a) INTER s)` 3951 by (RW_TAC std_ss [indicator_fn_def, EXTENSION, GSPECIFICATION, IN_INTER] 3952 >> Cases_on `x IN s` >- RW_TAC std_ss [mul_rone, mul_rzero] 3953 >> RW_TAC std_ss [mul_rone, mul_rzero]) 3954 >> POP_ORW 3955 >> MATCH_MP_TAC ALGEBRA_INTER 3956 >> FULL_SIMP_TAC std_ss [sigma_algebra_def]); 3957 3958val IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ = store_thm 3959 ("IN_MEASURABLE_BOREL_MUL_INDICATOR_EQ",``!a f. sigma_algebra a ==> 3960 (f IN measurable a Borel = (\x. f x * indicator_fn (space a) x) IN measurable a Borel)``, 3961 RW_TAC std_ss [] 3962 >> EQ_TAC >- METIS_TAC [IN_MEASURABLE_BOREL_MUL_INDICATOR, ALGEBRA_SPACE, sigma_algebra_def] 3963 >> RW_TAC std_ss [IN_MEASURABLE_BOREL, IN_UNIV, IN_FUNSET] 3964 >> `{x | f x < c} INTER space a = {x | f x * indicator_fn (space a) x < c} INTER space a` 3965 by (RW_TAC std_ss [IN_INTER, EXTENSION, GSPECIFICATION, indicator_fn_def, 3966 mul_rzero, mul_rone] 3967 >> METIS_TAC [mul_rzero, mul_rone]) 3968 >> RW_TAC std_ss []); 3969 3970 3971val IN_MEASURABLE_BOREL_POS_SIMPLE_FN = store_thm 3972 ("IN_MEASURABLE_BOREL_POS_SIMPLE_FN",``!m f. measure_space m /\ 3973 (?s a x. pos_simple_fn m f s a x) 3974 ==> f IN measurable (m_space m,measurable_sets m) Borel``, 3975 RW_TAC std_ss [pos_simple_fn_def] 3976 >> `!i. i IN s ==> indicator_fn (a i) IN measurable (m_space m,measurable_sets m) Borel` 3977 by METIS_TAC [IN_MEASURABLE_BOREL_INDICATOR, measurable_sets_def, subsets_def, 3978 m_space_def, measure_space_def] 3979 >> `!i x. i IN s ==> (\t. Normal (x i) * indicator_fn (a i) t) 3980 IN measurable (m_space m, measurable_sets m) Borel` 3981 by (RW_TAC std_ss [] 3982 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_CMUL 3983 >> Q.EXISTS_TAC `indicator_fn (a i)` 3984 >> Q.EXISTS_TAC `x' i` 3985 >> RW_TAC std_ss [] 3986 >> FULL_SIMP_TAC std_ss [measure_space_def]) 3987 >> MATCH_MP_TAC (INST_TYPE [beta |-> ``:num``] IN_MEASURABLE_BOREL_SUM) 3988 >> Q.EXISTS_TAC `(\i. (\t. Normal (x i) * indicator_fn (a i) t))` 3989 >> Q.EXISTS_TAC `s` 3990 >> RW_TAC std_ss [space_def] 3991 >- METIS_TAC [measure_space_def] 3992 >> RW_TAC real_ss [indicator_fn_def,mul_rzero,mul_rone] 3993 >> RW_TAC std_ss [extreal_of_num_def]); 3994 3995val IN_MEASURABLE_BOREL_POW = store_thm 3996 ("IN_MEASURABLE_BOREL_POW",``!n a f. sigma_algebra a /\ 3997 f IN measurable a Borel /\ (!x. x IN space a ==> f x <> NegInf /\ f x <> PosInf) 3998 ==> (\x. (f x) pow n) IN measurable a Borel``, 3999 Induct >- (RW_TAC std_ss [pow_0] 4000 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_CONST 4001 >> METIS_TAC []) 4002 >> RW_TAC std_ss [] 4003 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_MUL 4004 >> Q.EXISTS_TAC `f` 4005 >> Q.EXISTS_TAC `(\x. f x pow n)` 4006 >> RW_TAC std_ss [pow_not_infty] 4007 >> METIS_TAC [pow_add,ADD1,pow_1,mul_comm]); 4008 4009val IN_MEASURABLE_BOREL_MAX = store_thm 4010 ("IN_MEASURABLE_BOREL_MAX",``!a f g. sigma_algebra a /\ 4011 f IN measurable a Borel /\ g IN measurable a Borel 4012 ==> (\x. max (f x) (g x)) IN measurable a Borel``, 4013 RW_TAC std_ss [IN_MEASURABLE_BOREL,extreal_max_def,IN_FUNSET, IN_UNIV] 4014 >> `!c. {x | (if f x <= g x then g x else f x) < c} = {x | f x < c} INTER {x | g x < c}` 4015 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] 4016 >> EQ_TAC 4017 >- (RW_TAC std_ss [] 4018 >- METIS_TAC [let_trans] 4019 >> METIS_TAC [extreal_lt_def, lt_trans]) 4020 >> METIS_TAC [extreal_lt_def, lt_trans]) 4021 >> `!c. {x | (if f x <= g x then g x else f x) < c} INTER space a = 4022 ({x | f x < c} INTER space a) INTER ({x | g x < c} INTER space a)` 4023 by METIS_TAC [INTER_ASSOC, INTER_COMM, INTER_IDEMPOT] 4024 >> METIS_TAC [sigma_algebra_def, ALGEBRA_INTER]); 4025 4026val IN_MEASURABLE_BOREL_MONO_SUP = store_thm 4027 ("IN_MEASURABLE_BOREL_MONO_SUP",``!fn f a. (sigma_algebra a /\ 4028 (!n:num. fn n IN measurable a Borel) /\ 4029 (!n x. x IN space a ==> fn n x <= fn (SUC n) x) /\ 4030 (!x. x IN space a ==> 4031 (f x = sup (IMAGE (\n. fn n x) UNIV)))) 4032 ==> f IN measurable a Borel``, 4033 RW_TAC std_ss [IN_MEASURABLE_BOREL_ALT2,IN_FUNSET,IN_UNIV] 4034 >> `{x | sup (IMAGE (\n. fn n x) UNIV) <= c} INTER space a = 4035 BIGINTER (IMAGE (\n. {x | fn n x <= c} INTER space a) UNIV)` 4036 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGINTER_IMAGE, IN_UNIV, IN_INTER, sup_le] 4037 >> EQ_TAC 4038 >- (RW_TAC std_ss [] 4039 >> Q.PAT_X_ASSUM `!y. P y ==> y <= c` MATCH_MP_TAC 4040 >> ONCE_REWRITE_TAC [GSYM SPECIFICATION] 4041 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 4042 >> METIS_TAC []) 4043 >> RW_TAC std_ss [] 4044 >> POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [GSYM SPECIFICATION]) 4045 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 4046 >> METIS_TAC []) 4047 >> `{x | f x <= c} INTER space a = {x | sup (IMAGE (\n. fn n x) UNIV) <= c} INTER space a` 4048 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER] >> METIS_TAC []) 4049 >> `!c. BIGINTER (IMAGE (\n. {x | fn n x <= c} INTER (space a)) UNIV) IN subsets a` 4050 by (RW_TAC std_ss [] 4051 >> (MP_TAC o Q.SPEC `(space a,subsets a)`) SIGMA_ALGEBRA_FN_BIGINTER 4052 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, space_def, subsets_def, SPACE]) 4053 >> METIS_TAC []); 4054 4055val fn_plus_def = Define `fn_plus f = (\x. if 0 < f x then f x else 0)`; 4056 4057val fn_minus_def = Define `fn_minus f = (\x. if f x < 0 then ~ f x else 0)`; 4058 4059val fn_abs_def = Define `fn_abs f = (\x. abs (f x))`; 4060 4061val FN_PLUS_POS = store_thm 4062 ("FN_PLUS_POS",``!g x. 0 <= (fn_plus g) x``, 4063 RW_TAC real_ss [fn_plus_def, FUN_EQ_THM, lt_imp_le, le_refl]); 4064 4065val FN_MINUS_POS = store_thm 4066 ("FN_MINUS_POS",``!g x. 0 <= (fn_minus g) x``, 4067 RW_TAC real_ss [fn_minus_def, FUN_EQ_THM, le_refl] 4068 >> METIS_TAC [le_neg, lt_imp_le, neg_0]); 4069 4070val FN_PLUS_POS_ID = store_thm 4071 ("FN_PLUS_POS_ID",``(!x. 0 <= g x) ==> ((fn_plus g) = g)``, 4072 RW_TAC real_ss [fn_plus_def,FUN_EQ_THM] 4073 >> Cases_on `g x = 0` >- METIS_TAC [] 4074 >> METIS_TAC [le_lt]); 4075 4076val FN_MINUS_POS_ZERO = store_thm 4077 ("FN_MINUS_POS_ZERO",``(!x. 0 <= g x) ==> ((fn_minus g) = (\x. 0))``, 4078 RW_TAC real_ss [fn_minus_def,FUN_EQ_THM] 4079 >> Cases_on `g x = 0` >- METIS_TAC [neg_0] 4080 >> `0 < g x` by METIS_TAC [lt_le] 4081 >> METIS_TAC [extreal_lt_def]); 4082 4083val FN_PLUS_CMUL = store_thm 4084 ("FN_PLUS_CMUL",``!f c. (0 <= c ==> (fn_plus (\x. Normal c * f x) = 4085 (\x. Normal c * fn_plus f x))) /\ 4086 (c <= 0 ==> (fn_plus (\x. Normal c * f x) = 4087 (\x. -Normal c * fn_minus f x)))``, 4088 4089 RW_TAC std_ss [fn_plus_def,fn_minus_def,FUN_EQ_THM] 4090 >- (Cases_on `0 < f x` 4091 >- METIS_TAC [let_mul, extreal_of_num_def, extreal_le_def, extreal_lt_def, le_antisym] 4092 >> RW_TAC std_ss [mul_rzero] 4093 >> METIS_TAC [mul_le, extreal_lt_def, extreal_le_def, extreal_of_num_def, lt_imp_le, 4094 le_antisym]) 4095 >> RW_TAC std_ss [mul_rzero, neg_mul2] 4096 >- METIS_TAC [mul_le, extreal_of_num_def, extreal_le_def, extreal_lt_def, lt_imp_le, 4097 le_antisym, mul_comm] 4098 >> METIS_TAC [le_mul_neg, extreal_of_num_def, extreal_le_def, lt_imp_le, extreal_lt_def, 4099 le_antisym]); 4100 4101val FN_MINUS_CMUL = store_thm 4102 ("FN_MINUS_CMUL",``!f c. (0 <= c ==> (fn_minus (\x. Normal c * f x) = 4103 (\x. Normal c * fn_minus f x))) /\ 4104 (c <= 0 ==> (fn_minus (\x. Normal c * f x) = 4105 (\x. -Normal c * fn_plus f x)))``, 4106 RW_TAC std_ss [fn_plus_def,fn_minus_def,FUN_EQ_THM] 4107 >- (RW_TAC std_ss [mul_rzero, mul_rneg, neg_eq0] 4108 >- METIS_TAC [le_mul, extreal_of_num_def, extreal_le_def, extreal_lt_def, lt_imp_le, 4109 le_antisym] 4110 >> METIS_TAC [mul_le, extreal_of_num_def, extreal_le_def, lt_imp_le, extreal_lt_def, 4111 le_antisym, neg_eq0]) 4112 >> RW_TAC std_ss [mul_rzero, neg_eq0, mul_lneg, neg_0] 4113 >- METIS_TAC [le_mul_neg, extreal_of_num_def, extreal_le_def, extreal_lt_def, lt_imp_le, 4114 le_antisym] 4115 >> METIS_TAC [mul_le, extreal_of_num_def, extreal_le_def, lt_imp_le, extreal_lt_def, 4116 le_antisym, neg_eq0, mul_comm]); 4117 4118val FN_PLUS_ADD_LE = store_thm 4119("FN_PLUS_ADD_LE", ``!f g x. fn_plus (\x. f x + g x) x <= (fn_plus f x) + (fn_plus g x)``, 4120 RW_TAC real_ss[fn_plus_def, add_rzero, add_lzero, le_refl, le_add2] 4121 >> METIS_TAC [le_refl, extreal_lt_def, le_add2, add_lzero, add_rzero, lt_imp_le]); 4122 4123val FN_MINUS_ADD_LE = store_thm 4124 ("FN_MINUS_ADD_LE", ``!f g x. fn_minus (\x. f x + g x) x <= (fn_minus f x) + (fn_minus g x)``, 4125 RW_TAC real_ss[fn_minus_def, add_rzero, add_lzero, le_refl, le_add2] 4126 >| [Cases_on `f x` >> Cases_on `g x` 4127 >> RW_TAC std_ss [extreal_add_def, extreal_sub_def, extreal_ainv_def, lt_infty, 4128 num_not_infty, lte_trans, le_refl, le_infty, extreal_le_def] 4129 >> REAL_ARITH_TAC, 4130 (Cases_on `f x` >> Cases_on `g x` 4131 >> RW_TAC std_ss [extreal_add_def, extreal_sub_def, extreal_ainv_def, lt_infty, 4132 num_not_infty, lte_trans, le_refl, le_infty, extreal_le_def]) 4133 >- METIS_TAC [lt_infty] 4134 >> FULL_SIMP_TAC std_ss [extreal_of_num_def, extreal_lt_eq, extreal_le_def, 4135 extreal_add_def, REAL_LE_NEG, GSYM real_lte] 4136 >> METIS_TAC [REAL_LE_REFL, REAL_LE_ADD2, REAL_ADD_RID], 4137 (Cases_on `f x` >> Cases_on `g x` 4138 >> RW_TAC std_ss [extreal_add_def, extreal_sub_def, extreal_ainv_def, lt_infty, 4139 num_not_infty, lte_trans, le_refl, le_infty, extreal_le_def]) 4140 >- METIS_TAC [lt_infty] 4141 >> FULL_SIMP_TAC std_ss [extreal_of_num_def, extreal_lt_eq, extreal_le_def, 4142 extreal_add_def, REAL_LE_NEG, GSYM real_lte] 4143 >> METIS_TAC [REAL_LE_REFL, REAL_LE_ADD2, REAL_ADD_LID], 4144 METIS_TAC [extreal_lt_def, le_add2, add_rzero], 4145 METIS_TAC [lt_neg,le_add2, add_rzero, neg_0, lt_imp_le], 4146 METIS_TAC [lt_neg, neg_0, lt_imp_le], 4147 METIS_TAC [lt_neg, neg_0, lt_imp_le]]); 4148 4149val IN_MEASURABLE_BOREL_FN_PLUS = store_thm 4150 ("IN_MEASURABLE_BOREL_FN_PLUS",``!a f. f IN measurable a Borel 4151 ==> fn_plus f IN measurable a Borel``, 4152 RW_TAC std_ss [IN_MEASURABLE_BOREL, IN_FUNSET, IN_UNIV, fn_plus_def] 4153 >> Cases_on `c <= 0` 4154 >- (`{x | (if 0 < f x then f x else 0) < c} = {}` 4155 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, NOT_IN_EMPTY] 4156 >> `!x. 0 <= (if 0 < f x then f x else 0)` by RW_TAC real_ss [lt_imp_le, le_refl] 4157 >> METIS_TAC [le_trans, extreal_lt_def, extreal_of_num_def, extreal_le_def]) 4158 >> METIS_TAC [sigma_algebra_def, algebra_def, INTER_EMPTY]) 4159 >> `{x | (if 0 < f x then f x else 0) < c} = {x | f x < c}` 4160 by (RW_TAC real_ss [EXTENSION, GSPECIFICATION] 4161 >> EQ_TAC 4162 >- (RW_TAC real_ss [] 4163 >> METIS_TAC [extreal_lt_def, let_trans]) 4164 >> RW_TAC real_ss [] 4165 >> METIS_TAC [extreal_lt_def]) 4166 >> METIS_TAC []); 4167 4168val IN_MEASURABLE_BOREL_FN_MINUS = store_thm 4169 ("IN_MEASURABLE_BOREL_FN_MINUS",``!a f. f IN measurable a Borel 4170 ==> fn_minus f IN measurable a Borel``, 4171 RW_TAC std_ss [fn_minus_def] 4172 >> RW_TAC std_ss [IN_MEASURABLE_BOREL, IN_FUNSET, IN_UNIV, fn_minus_def] 4173 >- METIS_TAC [IN_MEASURABLE_BOREL] 4174 >> Cases_on `c <= 0` 4175 >- (`{x | (if f x < 0 then -f x else 0) < c} = {}` 4176 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, NOT_IN_EMPTY] 4177 >> `!x. 0 <= (if f x < 0 then -f x else 0)` 4178 by (RW_TAC real_ss [le_refl] 4179 >> METIS_TAC [lt_neg, neg_0, lt_imp_le]) 4180 >> METIS_TAC [extreal_of_num_def, extreal_le_def, le_trans, extreal_lt_def]) 4181 >> METIS_TAC [sigma_algebra_def, algebra_def, INTER_EMPTY, IN_MEASURABLE_BOREL]) 4182 >> `{x | (if f x < 0 then -f x else 0) < c} = {x | -c < f x}` 4183 by (RW_TAC real_ss [EXTENSION, GSPECIFICATION] 4184 >> EQ_TAC 4185 >- (RW_TAC std_ss [] 4186 >- METIS_TAC [lt_neg, neg_neg] 4187 >> METIS_TAC [lt_neg, neg_neg, neg_0, extreal_lt_def, lte_trans, 4188 lt_imp_le, extreal_ainv_def]) 4189 >> RW_TAC std_ss [] 4190 >- METIS_TAC [lt_neg, neg_neg] 4191 >> METIS_TAC [lt_neg, neg_neg,neg_0, extreal_lt_def, lte_trans, lt_imp_le, 4192 extreal_ainv_def]) 4193 >> METIS_TAC [IN_MEASURABLE_BOREL_ALL]); 4194 4195val IN_MEASURABLE_BOREL_PLUS_MINUS = store_thm 4196 ("IN_MEASURABLE_BOREL_PLUS_MINUS",``!a f. f IN measurable a Borel = 4197 (fn_plus f IN measurable a Borel /\ fn_minus f IN measurable a Borel)``, 4198 RW_TAC std_ss [] 4199 >> EQ_TAC >- RW_TAC std_ss [IN_MEASURABLE_BOREL_FN_PLUS, IN_MEASURABLE_BOREL_FN_MINUS] 4200 >> RW_TAC std_ss [] 4201 >> MATCH_MP_TAC IN_MEASURABLE_BOREL_SUB 4202 >> Q.EXISTS_TAC `fn_plus f` 4203 >> Q.EXISTS_TAC `fn_minus f` 4204 >> RW_TAC std_ss [fn_plus_def, fn_minus_def, sub_rzero,lt_antisym, sub_rzero, add_lzero] 4205 >> METIS_TAC [IN_MEASURABLE_BOREL, lt_antisym, sub_rneg, add_lzero,extreal_lt_def, le_antisym]); 4206 4207val INDICATOR_FN_MUL_INTER = store_thm 4208 ("INDICATOR_FN_MUL_INTER",``!A B. (\t. (indicator_fn A t) * (indicator_fn B t)) = 4209 (\t. indicator_fn (A INTER B) t)``, 4210 RW_TAC std_ss [FUN_EQ_THM] 4211 >> `(indicator_fn (A INTER B) t= (if t IN (A INTER B) then 1 else 0))` 4212 by METIS_TAC [indicator_fn_def] 4213 >> RW_TAC std_ss [indicator_fn_def, mul_lone, IN_INTER, mul_lzero] 4214 >> FULL_SIMP_TAC real_ss []); 4215 4216val indicator_fn_split = store_thm 4217 ("indicator_fn_split", ``!(r:num->bool) s (b:num->('a->bool)). FINITE r /\ 4218 (BIGUNION (IMAGE b r) = s) /\ 4219 (!i j. i IN r /\ j IN r /\ (~(i=j)) ==> DISJOINT (b i) (b j)) ==> 4220 !a. a SUBSET s ==> ((indicator_fn a) = 4221 (\x. SIGMA (\i. indicator_fn (a INTER (b i)) x) r))``, 4222 Suff `!r. FINITE r ==> 4223 (\r. !s (b:num->('a->bool)). 4224 FINITE r /\ 4225 (BIGUNION (IMAGE b r) = s) /\ 4226 (!i j. i IN r /\ j IN r /\ (~(i=j)) ==> DISJOINT (b i) (b j)) ==> 4227 !a. a SUBSET s ==> 4228 ((indicator_fn a) = 4229 (\x. SIGMA (\i. indicator_fn (a INTER (b i)) x) r))) r` 4230 >- METIS_TAC [] 4231 >> MATCH_MP_TAC FINITE_INDUCT 4232 >> RW_TAC std_ss [EXTREAL_SUM_IMAGE_THM, IMAGE_EMPTY, BIGUNION_EMPTY, 4233 SUBSET_EMPTY, indicator_fn_def, NOT_IN_EMPTY, 4234 FINITE_INSERT, IMAGE_INSERT, DELETE_NON_ELEMENT, 4235 IN_INSERT, BIGUNION_INSERT] 4236 >> Q.PAT_X_ASSUM `!b. P ==> !a. Q ==> (x = y)` 4237 (MP_TAC o Q.ISPEC `(b :num -> 'a -> bool)`) 4238 >> RW_TAC std_ss [SUBSET_DEF] 4239 >> POP_ASSUM (MP_TAC o Q.ISPEC `a DIFF ((b :num -> 'a -> bool) e)`) 4240 >> Know `(!x. x IN a DIFF b e ==> x IN BIGUNION (IMAGE b s))` 4241 >- METIS_TAC [SUBSET_DEF, IN_UNION, IN_DIFF] 4242 >> RW_TAC std_ss [FUN_EQ_THM] 4243 >> Know `SIGMA (\i. (if x IN a INTER b i then 1 else 0)) s = 4244 SIGMA (\i. (if x IN (a DIFF b e) INTER b i then 1 else 0)) s` 4245 >- (RW_TAC std_ss [Once EXTREAL_SUM_IMAGE_IN_IF] 4246 >> RW_TAC std_ss [(Once o Q.SPEC `(\i. if x IN (a DIFF b e) INTER b i then 1 else 0)` o 4247 UNDISCH o Q.ISPEC `(s :num -> bool)`) EXTREAL_SUM_IMAGE_IN_IF] 4248 >> MATCH_MP_TAC (METIS_PROVE [] ``!f x y z. (x = y) ==> (f x z = f y z)``) 4249 >> RW_TAC std_ss [FUN_EQ_THM, IN_INTER, IN_DIFF] 4250 >> FULL_SIMP_TAC real_ss [GSYM DELETE_NON_ELEMENT, DISJOINT_DEF, IN_INTER, NOT_IN_EMPTY, 4251 EXTENSION, GSPECIFICATION] 4252 >> METIS_TAC []) 4253 >> STRIP_TAC 4254 >> `SIGMA (\i. if x IN a INTER b i then 1 else 0) s = (if x IN a DIFF b e then 1 else 0)` 4255 by METIS_TAC [] 4256 >> POP_ORW 4257 >> RW_TAC real_ss [IN_INTER, IN_DIFF, EXTREAL_SUM_IMAGE_ZERO, add_rzero, add_lzero] 4258 >> FULL_SIMP_TAC std_ss [] 4259 >> `x IN BIGUNION (IMAGE b s)` by METIS_TAC [SUBSET_DEF, IN_UNION] 4260 >> FULL_SIMP_TAC std_ss [IN_BIGUNION_IMAGE] 4261 >> `s = {x'} UNION (s DIFF {x'})` by METIS_TAC [UNION_DIFF, SUBSET_DEF, IN_SING] 4262 >> POP_ORW 4263 >> `FINITE {x'} /\ FINITE (s DIFF {x'})` by METIS_TAC [FINITE_SING, FINITE_DIFF] 4264 >> `DISJOINT {x'} (s DIFF {x'})` by METIS_TAC [EXTENSION, IN_DISJOINT, IN_DIFF, IN_SING] 4265 >> FULL_SIMP_TAC std_ss [EXTREAL_SUM_IMAGE_DISJOINT_UNION] 4266 >> RW_TAC std_ss [EXTREAL_SUM_IMAGE_SING] 4267 >> Suff `SIGMA (\i. if x IN b i then 1 else 0) (s DIFF {x'}) = 0` 4268 >- METIS_TAC [add_rzero] 4269 >> RW_TAC std_ss [Once EXTREAL_SUM_IMAGE_IN_IF] 4270 >> Suff `(\i. if i IN s DIFF {x'} then if x IN b i then 1 else 0 else 0) = (\x. 0)` 4271 >- RW_TAC std_ss [EXTREAL_SUM_IMAGE_ZERO] 4272 >> RW_TAC std_ss [FUN_EQ_THM, IN_DIFF, IN_SING] 4273 >> METIS_TAC [IN_SING, IN_DIFF, IN_DISJOINT]); 4274 4275val indicator_fn_suminf = store_thm 4276 ("indicator_fn_suminf", 4277 ``!a x. (!m n. m <> n ==> DISJOINT (a m) (a n)) ==> 4278 (suminf (\i. indicator_fn (a i) x) = 4279 indicator_fn (BIGUNION (IMAGE a univ(:num))) x)``, 4280 RW_TAC std_ss [ext_suminf_def,sup_eq] 4281 >- (POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [GSYM SPECIFICATION]) 4282 >> RW_TAC std_ss [IN_IMAGE,IN_UNIV] 4283 >> Cases_on `~(x IN BIGUNION (IMAGE a univ(:num)))` 4284 >- (FULL_SIMP_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV] 4285 >> RW_TAC std_ss [indicator_fn_def, EXTREAL_SUM_IMAGE_ZERO, FINITE_COUNT,le_refl,le_01]) 4286 >> FULL_SIMP_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV, indicator_fn_def] 4287 >> REVERSE (RW_TAC std_ss []) 4288 >- METIS_TAC [] 4289 >> `!n. n <> x' ==> ~(x IN a n)` 4290 by METIS_TAC [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 4291 >> Cases_on `~(x' IN count n)` 4292 >- (`SIGMA (\i. if x IN a i then 1 else 0) (count n) = 0` 4293 by (MATCH_MP_TAC EXTREAL_SUM_IMAGE_0 4294 >> RW_TAC real_ss [FINITE_COUNT] 4295 >> METIS_TAC []) 4296 >> RW_TAC std_ss [le_01]) 4297 >> `count n = ((count n) DELETE x') UNION {x'}` 4298 by (RW_TAC std_ss [EXTENSION, IN_DELETE, IN_UNION, IN_SING, IN_COUNT] 4299 >> METIS_TAC []) 4300 >> POP_ORW 4301 >> `DISJOINT ((count n) DELETE x') ({x'})` 4302 by RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY, IN_SING, IN_DELETE] 4303 >> `!n. (\i. if x IN a i then 1 else 0) n <> NegInf` 4304 by RW_TAC std_ss [num_not_infty] 4305 >> FULL_SIMP_TAC std_ss [FINITE_COUNT, FINITE_DELETE, FINITE_SING, 4306 EXTREAL_SUM_IMAGE_DISJOINT_UNION, EXTREAL_SUM_IMAGE_SING] 4307 >> Suff `SIGMA (\i. if x IN a i then 1 else 0) (count n DELETE x') = 0` 4308 >- RW_TAC std_ss [add_lzero, le_refl] 4309 >> MATCH_MP_TAC EXTREAL_SUM_IMAGE_0 4310 >> RW_TAC std_ss [FINITE_COUNT, FINITE_DELETE] 4311 >> METIS_TAC [IN_DELETE]) 4312 >> `!n. SIGMA (\i. indicator_fn (a i) x) (count n) <= y` 4313 by (RW_TAC std_ss [] 4314 >> POP_ASSUM MATCH_MP_TAC 4315 >> ONCE_REWRITE_TAC [GSYM SPECIFICATION] 4316 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 4317 >> METIS_TAC []) 4318 >> ASM_SIMP_TAC std_ss [indicator_fn_def, IN_BIGUNION_IMAGE, IN_UNIV] 4319 >> (REVERSE (Cases_on `?x'. x IN a x'`) >> ASM_SIMP_TAC std_ss []) 4320 >- (`0 <= SIGMA (\i. indicator_fn (a i) x) (count 0)` 4321 by RW_TAC std_ss [COUNT_ZERO, EXTREAL_SUM_IMAGE_THM, le_refl] 4322 >> METIS_TAC [le_trans]) 4323 >> POP_ASSUM (Q.X_CHOOSE_THEN `x'` ASSUME_TAC) 4324 >> Suff `SIGMA (\i. indicator_fn (a i) x) (count (SUC x')) = 1` 4325 >- METIS_TAC [] 4326 >> FULL_SIMP_TAC std_ss [EXTREAL_SUM_IMAGE_THM, FINITE_COUNT, COUNT_SUC] 4327 >> Suff `SIGMA (\i. indicator_fn (a i) x) (count x' DELETE x') = 0` 4328 >- RW_TAC std_ss [indicator_fn_def,add_rzero] 4329 >> `!n. n <> x' ==> ~(x IN a n)` by METIS_TAC [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 4330 >> MATCH_MP_TAC EXTREAL_SUM_IMAGE_0 4331 >> FULL_SIMP_TAC std_ss [FINITE_COUNT, FINITE_DELETE, IN_COUNT, IN_DELETE, indicator_fn_def]); 4332 4333val measure_split = store_thm 4334 ("measure_split", ``!(r:num->bool) (b:num->('a->bool)) m. 4335 measure_space m /\ FINITE r /\ 4336 (BIGUNION (IMAGE b r) = m_space m) /\ 4337 (!i j. i IN r /\ j IN r /\ (~(i = j)) ==> DISJOINT (b i) (b j)) /\ 4338 (!i. i IN r ==> b i IN measurable_sets m) ==> 4339 !a. a IN measurable_sets m ==> 4340 ((measure m) a = SIGMA (\i. (measure m) (a INTER (b i))) r)``, 4341 Suff `!r. FINITE r ==> 4342 (\r. !(b:num->('a->bool)) m. 4343 measure_space m /\ 4344 (BIGUNION (IMAGE b r) = m_space m) /\ 4345 (!i j. i IN r /\ j IN r /\ (~(i=j)) ==> DISJOINT (b i) (b j)) /\ 4346 (!i. i IN r ==> b i IN measurable_sets m) ==> 4347 !a. a IN measurable_sets m ==> 4348 ((measure m) a = 4349 SIGMA (\i. (measure m) (a INTER (b i))) r)) r` 4350 >- RW_TAC std_ss [] 4351 >> MATCH_MP_TAC FINITE_INDUCT 4352 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, IMAGE_EMPTY, BIGUNION_EMPTY, 4353 DELETE_NON_ELEMENT, IN_INSERT, NOT_IN_EMPTY] 4354 >- METIS_TAC [MEASURE_SPACE_SUBSET_MSPACE, SUBSET_EMPTY ,MEASURE_EMPTY] 4355 >> Cases_on `s = {}` 4356 >- (FULL_SIMP_TAC real_ss [REAL_SUM_IMAGE_THM, IMAGE_DEF, IN_SING, BIGUNION, 4357 GSPECIFICATION, GSPEC_ID, SUBSET_DEF,REAL_SUM_IMAGE_SING] 4358 >> METIS_TAC [SUBSET_INTER1,MEASURE_SPACE_SUBSET_MSPACE]) 4359 >> `?x s'. (s = x INSERT s') /\ ~(x IN s')` by METIS_TAC [SET_CASES] 4360 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT, IN_INSERT] 4361 >> Q.PAT_X_ASSUM `!b' m'. P ==> !a'. Q ==> (f = g)` 4362 (MP_TAC o Q.ISPECL [`(\i:num. if i = x then b x UNION b e else b i)`, 4363 `(m :('a -> bool) # (('a -> bool) -> bool) # (('a -> bool) -> real))`]) 4364 >> `IMAGE (\i. (if i = x then b x UNION b e else b i)) s' = IMAGE b s'` 4365 by (RW_TAC std_ss [Once EXTENSION, IN_IMAGE] 4366 >> EQ_TAC 4367 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `i` >> METIS_TAC []) 4368 >> RW_TAC std_ss [] >> Q.EXISTS_TAC `x''` >> METIS_TAC []) 4369 >> FULL_SIMP_TAC std_ss [IMAGE_INSERT, BIGUNION_INSERT, UNION_ASSOC] 4370 >> POP_ASSUM (K ALL_TAC) 4371 >> `(b x UNION (b e UNION BIGUNION (IMAGE b s')) = m_space m)` 4372 by METIS_TAC [UNION_COMM,UNION_ASSOC] 4373 >> ASM_REWRITE_TAC [] 4374 >> `(!i j. ((i = x) \/ i IN s') /\ ((j = x) \/ j IN s') /\ ~(i = j) ==> 4375 DISJOINT (if i = x then b x UNION b e else b i) 4376 (if j = x then b x UNION b e else b j))` 4377 by (FULL_SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, GSPECIFICATION, IN_INSERT, 4378 IN_INTER, NOT_IN_EMPTY] 4379 >> METIS_TAC [IN_UNION]) 4380 >> ASM_REWRITE_TAC [GSYM UNION_ASSOC] >> POP_ASSUM (K ALL_TAC) 4381 >> `(!i. (i = x) \/ i IN s' ==> (if i = x then b x UNION b e else b i) IN measurable_sets m)` 4382 by METIS_TAC [ALGEBRA_UNION, sigma_algebra_def, measure_space_def, subsets_def] 4383 >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 4384 >> STRIP_TAC 4385 >> FULL_SIMP_TAC std_ss [UNION_ASSOC] 4386 >> POP_ASSUM ((fn thm => ONCE_REWRITE_TAC [thm]) o UNDISCH o Q.SPEC `a`) 4387 >> `(x INSERT s') DELETE e = x INSERT s'` by METIS_TAC [EXTENSION, IN_DELETE, IN_INSERT] 4388 >> FULL_SIMP_TAC real_ss [FINITE_INSERT, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, 4389 REAL_ADD_ASSOC] 4390 >> Suff `(measure m (a INTER (b x UNION b e)) = 4391 measure m (a INTER b e) + measure m (a INTER b x)) /\ 4392 (SIGMA (\i. measure m (a INTER 4393 (if i = x then b x UNION b e else b i))) s' = 4394 SIGMA (\i. measure m (a INTER b i)) s')` 4395 >- RW_TAC std_ss [] 4396 >> CONJ_TAC 4397 >- (`a INTER (b x UNION b e) = (a INTER b e) UNION (a INTER b x)` 4398 by (FULL_SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, GSPECIFICATION, 4399 NOT_IN_EMPTY, IN_INTER, IN_UNION] 4400 >> METIS_TAC []) 4401 >> POP_ORW 4402 >> (MATCH_MP_TAC o REWRITE_RULE [additive_def] o UNDISCH o Q.SPEC `m`) 4403 MEASURE_SPACE_ADDITIVE 4404 >> CONJ_TAC 4405 >- METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, measure_space_def, subsets_def] 4406 >> CONJ_TAC 4407 >- METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, measure_space_def, subsets_def] 4408 >> FULL_SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, IN_INTER] 4409 >> METIS_TAC []) 4410 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s' :num -> bool)`) REAL_SUM_IMAGE_IN_IF] 4411 >> MATCH_MP_TAC (METIS_PROVE [] ``!f x y z. (x = y) ==> (f x z = f y z)``) 4412 >> RW_TAC std_ss [FUN_EQ_THM] 4413 >> RW_TAC std_ss [] 4414 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]); 4415 4416val _ = export_theory (); 4417