1(* 2 3app load ["bossLib", "metisLib", "arithmeticTheory", "pred_setTheory", "listTheory", 4 "state_transformerTheory", "formalizeUseful", 5 "combinTheory", "pairTheory", "realTheory", "realLib", "extra_boolTheory", "jrhUtils", 6 "extra_pred_setTheory", "realSimps", "extra_realTheory", 7 "measureTheory", "numTheory", "simpLib", 8 "seqTheory", "subtypeTheory", 9 "transcTheory", "limTheory", "stringTheory", "rich_listTheory", "stringSimps", 10 "listSimps"]; 11 12*) 13 14open HolKernel Parse boolLib bossLib metisLib arithmeticTheory pred_setTheory 15 listTheory state_transformerTheory formalizeUseful extra_numTheory combinTheory 16 pairTheory realTheory realLib extra_boolTheory jrhUtils 17 extra_pred_setTheory realSimps extra_realTheory measureTheory numTheory 18 simpLib seqTheory subtypeTheory 19 transcTheory limTheory stringTheory rich_listTheory stringSimps listSimps; 20 21open real_sigmaTheory; 22 23(* ------------------------------------------------------------------------- *) 24(* Start a new theory called "borel" *) 25(* ------------------------------------------------------------------------- *) 26 27val _ = new_theory "borel"; 28 29(* ------------------------------------------------------------------------- *) 30(* Helpful proof tools *) 31(* ------------------------------------------------------------------------- *) 32 33val REVERSE = Tactical.REVERSE; 34val lemma = I prove; 35 36val Simplify = RW_TAC arith_ss; 37val Suff = PARSE_TAC SUFF_TAC; 38val Know = PARSE_TAC KNOW_TAC; 39val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 40val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 41val Cond = 42 DISCH_THEN 43 (fn mp_th => 44 let 45 val cond = fst (dest_imp (concl mp_th)) 46 in 47 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 48 end); 49 50val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 51 52val safe_list_ss = (simpLib.++ (bool_ss, LIST_ss)); 53 54val safe_string_ss = (simpLib.++ (bool_ss, STRING_ss)); 55 56val arith_string_ss = (simpLib.++ (arith_ss, STRING_ss)); 57 58 59(* ************************************************************************* *) 60(* ************************************************************************* *) 61(* Basic Definitions *) 62(* ************************************************************************* *) 63(* ************************************************************************* *) 64 65val borel_space_def = Define 66 `borel_space = sigma (UNIV:real->bool) (IMAGE (\a:real. {x:real | x <= a}) (UNIV:real->bool))`; 67 68 69val borel_measurable_def = Define 70 `borel_measurable a = measurable a borel_space`; 71 72val mono_convergent_def = Define 73 `mono_convergent u f s = 74 (!x m n. m <= n /\ x IN s ==> u m x <= u n x) /\ 75 (!x. x IN s ==> (\i. u i x) --> f x)`; 76 77(* ************************************************************************* *) 78(* ************************************************************************* *) 79(* Proofs *) 80(* ************************************************************************* *) 81(* ************************************************************************* *) 82 83val in_borel_measurable = store_thm 84 ("in_borel_measurable", 85 ``!f s. f IN borel_measurable s = 86 sigma_algebra s /\ 87 (!s'. s' IN subsets (sigma UNIV (IMAGE (\a. {x | x <= a}) UNIV)) ==> 88 PREIMAGE f s' INTER space s IN subsets s)``, 89 RW_TAC std_ss [borel_measurable_def, IN_MEASURABLE, borel_space_def, 90 SPACE_SIGMA, IN_FUNSET, IN_UNIV] 91 >> `sigma_algebra (sigma UNIV (IMAGE (\a. {x | x <= a}) UNIV))` 92 by (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA 93 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, IN_UNIV]) 94 >> ASM_REWRITE_TAC []); 95 96 97val borel_measurable_const = store_thm 98 ("borel_measurable_const", 99 ``!s c. sigma_algebra s ==> 100 (\x. c) IN borel_measurable s``, 101 RW_TAC std_ss [in_borel_measurable] 102 >> Cases_on `c IN s'` 103 >- (`PREIMAGE (\x. c) s' INTER space s = space s` 104 by RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] 105 >> POP_ORW 106 >> MATCH_MP_TAC ALGEBRA_SPACE >> MATCH_MP_TAC SIGMA_ALGEBRA_ALGEBRA 107 >> ASM_REWRITE_TAC []) 108 >> `PREIMAGE (\x. c) s' INTER space s = {}` 109 by RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, NOT_IN_EMPTY] 110 >> POP_ORW 111 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA]); 112 113 114val borel_measurable_indicator = store_thm 115 ("borel_measurable_indicator", 116 ``!s a. sigma_algebra s /\ a IN subsets s ==> 117 indicator_fn a IN borel_measurable s``, 118 RW_TAC std_ss [indicator_fn_def, in_borel_measurable] 119 >> Cases_on `1 IN s'` 120 >- (Cases_on `0 IN s'` 121 >- (`PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = space s` 122 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] 123 >> METIS_TAC []) 124 >> POP_ORW 125 >> MATCH_MP_TAC ALGEBRA_SPACE >> MATCH_MP_TAC SIGMA_ALGEBRA_ALGEBRA 126 >> ASM_REWRITE_TAC []) 127 >> `PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = a` 128 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] 129 >> METIS_TAC [SIGMA_ALGEBRA, algebra_def, subset_class_def, SUBSET_DEF]) 130 >> ASM_REWRITE_TAC []) 131 >> Cases_on `0 IN s'` 132 >- (`PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = space s DIFF a` 133 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, IN_DIFF] 134 >> METIS_TAC [SIGMA_ALGEBRA, algebra_def, subset_class_def, SUBSET_DEF]) 135 >> METIS_TAC [SIGMA_ALGEBRA, algebra_def]) 136 >> `PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = {}` 137 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, NOT_IN_EMPTY] >> METIS_TAC []) 138 >> POP_ORW >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, algebra_def]); 139 140 141val borel_measurable_le_iff = store_thm 142 ("borel_measurable_le_iff", 143 ``!m. measure_space m ==> 144 !f. f IN borel_measurable (m_space m, measurable_sets m) = 145 (!a. {w | w IN m_space m /\ f w <= a} IN measurable_sets m)``, 146 NTAC 3 STRIP_TAC >> EQ_TAC 147 >- (RW_TAC std_ss [in_borel_measurable, subsets_def, space_def] 148 >> POP_ASSUM (MP_TAC o REWRITE_RULE [PREIMAGE_def] o Q.SPEC `{b | b <= a}`) 149 >> RW_TAC std_ss [GSPECIFICATION] 150 >> `{x | f x <= a} INTER m_space m = 151 {w | w IN m_space m /\ f w <= a}` 152 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, GSPECIFICATION] 153 >> DECIDE_TAC) 154 >> FULL_SIMP_TAC std_ss [] >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM MATCH_MP_TAC 155 >> MATCH_MP_TAC IN_SIGMA 156 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV, Once EXTENSION, GSPECIFICATION] 157 >> Q.EXISTS_TAC `a` >> SIMP_TAC std_ss []) 158 >> RW_TAC std_ss [borel_measurable_def, borel_space_def] 159 >> MATCH_MP_TAC MEASURABLE_SIGMA 160 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, subset_class_def, space_def, subsets_def, SUBSET_UNIV, 161 IN_IMAGE] 162 >- FULL_SIMP_TAC std_ss [measure_space_def] 163 >> `PREIMAGE f {x | x <= a} INTER m_space m = 164 {w | w IN m_space m /\ f w <= a}` 165 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, GSPECIFICATION, IN_PREIMAGE] 166 >> DECIDE_TAC) 167 >> RW_TAC std_ss []); 168 169 170val sigma_le_less = store_thm 171 ("sigma_le_less", 172 ``!f A. sigma_algebra A /\ (!(a:real). {w | w IN space A /\ f w <= a} IN subsets A) ==> 173 !a. {w | w IN space A /\ f w < a} IN subsets A``, 174 REPEAT STRIP_TAC 175 >> `BIGUNION (IMAGE (\n. {w | w IN space A /\ f w <= a - inv(&(SUC n))}) (UNIV:num->bool)) = 176 {w | w IN space A /\ f w < a}` 177 by (ONCE_REWRITE_TAC [EXTENSION] 178 >> RW_TAC std_ss [GSPECIFICATION, IN_BIGUNION, IN_IMAGE, IN_UNIV] 179 >> `(?s. x IN s /\ ?n. s = {w | w IN space A /\ f w <= a - inv (&SUC n)}) = 180 (?n. x IN {w | w IN space A /\ f w <= a - inv (& (SUC n))})` 181 by METIS_TAC [GSYM EXTENSION] 182 >> POP_ORW 183 >> RW_TAC std_ss [GSPECIFICATION] 184 >> EQ_TAC 185 >- (RW_TAC std_ss [] >- METIS_TAC [] >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `a - inv (& (SUC n))` 186 >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_INV_EQ] >> METIS_TAC []) 187 >> RW_TAC std_ss [] 188 >> `(\n. inv (($& o SUC) n)) --> 0` 189 by (MATCH_MP_TAC SEQ_INV0 190 >> RW_TAC std_ss [o_DEF] 191 >> Q.EXISTS_TAC `clg y` 192 >> RW_TAC std_ss [GREATER_EQ, real_gt] 193 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `&(clg y)` 194 >> RW_TAC std_ss [REAL_LT, LE_NUM_CEILING] 195 >> MATCH_MP_TAC LESS_EQ_LESS_TRANS >> Q.EXISTS_TAC `n` 196 >> RW_TAC arith_ss []) 197 >> FULL_SIMP_TAC real_ss [SEQ, o_DEF] 198 >> POP_ASSUM (MP_TAC o REWRITE_RULE [REAL_LT_SUB_LADD] o Q.SPEC `a - f x`) 199 >> RW_TAC real_ss [ABS_INV, ABS_N, REAL_LE_SUB_LADD] 200 >> Q.EXISTS_TAC `N` >> MATCH_MP_TAC REAL_LT_IMP_LE 201 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> POP_ASSUM MATCH_MP_TAC >> RW_TAC std_ss []) 202 >> POP_ASSUM (MP_TAC o GSYM) >> RW_TAC std_ss [] 203 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA] 204 >> Q.PAT_ASSUM `!c. P c ==> BIGUNION c IN subsets A` MATCH_MP_TAC 205 >> RW_TAC std_ss [COUNTABLE_NUM, image_countable, SUBSET_DEF, IN_IMAGE, IN_UNIV] 206 >> METIS_TAC []); 207 208 209val sigma_less_ge = store_thm 210 ("sigma_less_ge", 211 ``!f A. sigma_algebra A /\ (!(a:real). {w | w IN space A /\ f w < a} IN subsets A) ==> 212 !a. {w | w IN space A /\ a <= f w} IN subsets A``, 213 REPEAT STRIP_TAC 214 >> `{w | w IN space A /\ a <= f w} = 215 space A DIFF {w | w IN space A /\ f w < a}` 216 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] 217 >> DECIDE_TAC) 218 >> POP_ORW 219 >> METIS_TAC [SIGMA_ALGEBRA]); 220 221 222val sigma_ge_gr = store_thm 223 ("sigma_ge_gr", 224 ``!f A. sigma_algebra A /\ (!(a:real). {w | w IN space A /\ a <= f w} IN subsets A) ==> 225 !a. {w | w IN space A /\ a < f w} IN subsets A``, 226 REPEAT STRIP_TAC 227 >> `BIGUNION (IMAGE (\n. {w | w IN space A /\ a <= f w - inv(&(SUC n))}) (UNIV:num->bool)) = 228 {w | w IN space A /\ a < f w}` 229 by (ONCE_REWRITE_TAC [EXTENSION] 230 >> RW_TAC std_ss [GSPECIFICATION, IN_BIGUNION, IN_IMAGE, IN_UNIV] 231 >> `(?s. x IN s /\ ?n. s = {w | w IN space A /\ a <= f w - inv (& (SUC n))}) = 232 (?n. x IN {w | w IN space A /\ a <= f w - inv (& (SUC n))})` 233 by METIS_TAC [] 234 >> POP_ORW 235 >> RW_TAC std_ss [GSPECIFICATION] 236 >> EQ_TAC 237 >- (RW_TAC std_ss [] >- ASM_REWRITE_TAC [] >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f x - inv (& (SUC n))` 238 >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_INV_EQ]) 239 >> RW_TAC std_ss [] 240 >> `(\n. inv (($& o SUC) n)) --> 0` 241 by (MATCH_MP_TAC SEQ_INV0 242 >> RW_TAC std_ss [o_DEF] 243 >> Q.EXISTS_TAC `clg y` 244 >> RW_TAC std_ss [GREATER_EQ, real_gt] 245 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `&(clg y)` 246 >> RW_TAC std_ss [REAL_LT, LE_NUM_CEILING] 247 >> MATCH_MP_TAC LESS_EQ_LESS_TRANS >> Q.EXISTS_TAC `n` 248 >> RW_TAC arith_ss []) 249 >> FULL_SIMP_TAC real_ss [SEQ, o_DEF] 250 >> POP_ASSUM (MP_TAC o REWRITE_RULE [REAL_LT_SUB_LADD] o Q.SPEC `f x - a`) 251 >> RW_TAC real_ss [ABS_INV, ABS_N, REAL_LE_SUB_LADD] 252 >> Q.EXISTS_TAC `N` >> MATCH_MP_TAC REAL_LT_IMP_LE 253 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> POP_ASSUM MATCH_MP_TAC >> RW_TAC std_ss []) 254 >> POP_ASSUM (MP_TAC o GSYM) >> RW_TAC std_ss [] 255 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA] 256 >> Q.PAT_ASSUM `!c. P c ==> BIGUNION c IN subsets A` MATCH_MP_TAC 257 >> RW_TAC std_ss [COUNTABLE_NUM, image_countable, SUBSET_DEF, IN_IMAGE, IN_UNIV, REAL_LE_SUB_LADD] 258 >> METIS_TAC []); 259 260 261val sigma_gr_le = store_thm 262 ("sigma_gr_le", 263 ``!f A. sigma_algebra A /\ (!(a:real). {w | w IN space A /\ a < f w} IN subsets A) ==> 264 !a. {w | w IN space A /\ f w <= a} IN subsets A``, 265 REPEAT STRIP_TAC 266 >> `{w | w IN space A /\ f w <= a} = 267 space A DIFF {w | w IN space A /\ a < f w}` 268 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] 269 >> DECIDE_TAC) 270 >> POP_ORW 271 >> METIS_TAC [SIGMA_ALGEBRA]); 272 273 274val borel_measurable_gr_iff = store_thm 275 ("borel_measurable_gr_iff", 276 ``!m. measure_space m ==> 277 !f. f IN borel_measurable (m_space m, measurable_sets m) = 278 (!a. {w | w IN m_space m /\ a < f w} IN measurable_sets m)``, 279 RW_TAC std_ss [measure_space_def, borel_measurable_le_iff] 280 >> EQ_TAC 281 >- (REPEAT STRIP_TAC 282 >> `{w | w IN m_space m /\ a < f w} = 283 m_space m DIFF {w | w IN m_space m /\ f w <= a}` 284 by (ONCE_REWRITE_TAC [EXTENSION] 285 >> RW_TAC std_ss [IN_DIFF, GSPECIFICATION, real_lt] 286 >> DECIDE_TAC) 287 >> POP_ORW 288 >> METIS_TAC [SIGMA_ALGEBRA, space_def, subsets_def]) 289 >> METIS_TAC [sigma_gr_le, SPACE, subsets_def, space_def, measurable_sets_def, m_space_def]); 290 291 292val borel_measurable_less_iff = store_thm 293 ("borel_measurable_less_iff", 294 ``!m. measure_space m ==> 295 !f. f IN borel_measurable (m_space m, measurable_sets m) = 296 (!a. {w | w IN m_space m /\ f w < a} IN measurable_sets m)``, 297 RW_TAC std_ss [measure_space_def, borel_measurable_le_iff] 298 >> EQ_TAC 299 >- METIS_TAC [sigma_le_less, SPACE, subsets_def, space_def, measurable_sets_def, m_space_def] 300 >> REPEAT STRIP_TAC 301 >> `BIGUNION (IMAGE (\n. {w | w IN m_space m /\ a <= f w - inv(&(SUC n))}) (UNIV:num->bool)) = 302 {w | w IN m_space m /\ a < f w}` 303 by (ONCE_REWRITE_TAC [EXTENSION] 304 >> RW_TAC std_ss [GSPECIFICATION, IN_BIGUNION, IN_IMAGE, IN_UNIV] 305 >> `(?s. x IN s /\ ?n. s = {w | w IN m_space m /\ a <= f w - inv (& (SUC n))}) = 306 (?n. x IN {w | w IN m_space m /\ a <= f w - inv (& (SUC n))})` 307 by METIS_TAC [] 308 >> POP_ORW 309 >> RW_TAC std_ss [GSPECIFICATION] 310 >> EQ_TAC 311 >- (RW_TAC std_ss [] >- ASM_REWRITE_TAC [] >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f x - inv (& (SUC n))` 312 >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_INV_EQ]) 313 >> RW_TAC std_ss [] 314 >> `(\n. inv (($& o SUC) n)) --> 0` 315 by (MATCH_MP_TAC SEQ_INV0 316 >> RW_TAC std_ss [o_DEF] 317 >> Q.EXISTS_TAC `clg y` 318 >> RW_TAC std_ss [GREATER_EQ, real_gt] 319 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `&(clg y)` 320 >> RW_TAC std_ss [REAL_LT, LE_NUM_CEILING] 321 >> MATCH_MP_TAC LESS_EQ_LESS_TRANS >> Q.EXISTS_TAC `n` 322 >> RW_TAC arith_ss []) 323 >> FULL_SIMP_TAC real_ss [SEQ, o_DEF] 324 >> POP_ASSUM (MP_TAC o REWRITE_RULE [REAL_LT_SUB_LADD] o Q.SPEC `f x - a`) 325 >> RW_TAC real_ss [ABS_INV, ABS_N, REAL_LE_SUB_LADD] 326 >> Q.EXISTS_TAC `N` >> MATCH_MP_TAC REAL_LT_IMP_LE 327 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> POP_ASSUM MATCH_MP_TAC >> RW_TAC std_ss []) 328 >> `{w | w IN m_space m /\ f w <= a} = 329 m_space m DIFF {w | w IN m_space m /\ a < f w}` 330 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] 331 >> DECIDE_TAC) 332 >> POP_ORW 333 >> Suff `{w | w IN m_space m /\ a < f w} IN measurable_sets m` 334 >- METIS_TAC [SPACE, subsets_def, space_def, measurable_sets_def, m_space_def, SIGMA_ALGEBRA] 335 >> POP_ASSUM (MP_TAC o GSYM) >> RW_TAC std_ss [] 336 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subsets_def] 337 >> Q.PAT_ASSUM `!c. P c ==> BIGUNION c IN (measurable_sets m)` MATCH_MP_TAC 338 >> RW_TAC std_ss [COUNTABLE_NUM, image_countable, SUBSET_DEF, IN_IMAGE, IN_UNIV, REAL_LE_SUB_LADD] 339 >> `{w | w IN m_space m /\ a + inv (& (SUC n)) <= f w} = 340 m_space m DIFF {w | w IN m_space m /\ f w < a + inv (& (SUC n))}` 341 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] 342 >> DECIDE_TAC) 343 >> POP_ORW 344 >> Suff `{w | w IN m_space m /\ f w < a + inv (& (SUC n))} IN measurable_sets m` 345 >- METIS_TAC [SPACE, subsets_def, space_def, measurable_sets_def, m_space_def, SIGMA_ALGEBRA] 346 >> METIS_TAC []); 347 348 349val borel_measurable_ge_iff = store_thm 350 ("borel_measurable_ge_iff", 351 ``!m. measure_space m ==> 352 !f. f IN borel_measurable (m_space m, measurable_sets m) = 353 (!a. {w | w IN m_space m /\ a <= f w} IN measurable_sets m)``, 354 RW_TAC std_ss [measure_space_def, borel_measurable_less_iff] 355 >> EQ_TAC 356 >- (REPEAT STRIP_TAC 357 >> `{w | w IN m_space m /\ a <= f w} = 358 m_space m DIFF {w | w IN m_space m /\ f w < a}` 359 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] 360 >> DECIDE_TAC) 361 >> POP_ORW 362 >> METIS_TAC [SIGMA_ALGEBRA, space_def, subsets_def]) 363 >> METIS_TAC [sigma_ge_gr, sigma_gr_le, sigma_le_less, SPACE, subsets_def, space_def, measurable_sets_def, m_space_def]); 364 365 366val affine_borel_measurable = store_thm 367 ("affine_borel_measurable", 368 ``!m g. measure_space m /\ g IN borel_measurable (m_space m, measurable_sets m) ==> 369 !(a:real) (b:real). (\x. a + (g x) * b) IN borel_measurable (m_space m, measurable_sets m)``, 370 REPEAT STRIP_TAC 371 >> Cases_on `b=0` 372 >- (RW_TAC real_ss [] >> FULL_SIMP_TAC std_ss [measure_space_def, borel_measurable_const]) 373 >> `!x c. (a + g x * b <= c) = (g x * b <= c - a)` 374 by (REPEAT STRIP_TAC >> REAL_ARITH_TAC) 375 >> RW_TAC std_ss [borel_measurable_le_iff] 376 >> POP_ASSUM (K ALL_TAC) 377 >> REVERSE (Cases_on `b < 0`) 378 >- (`0 < b` by METIS_TAC [REAL_LT_LE, real_lt] 379 >> `! x c. (g x * b <= c - a) = (g x <= (c - a) / b)` 380 by (REPEAT STRIP_TAC 381 >> MATCH_MP_TAC (GSYM REAL_LE_RDIV_EQ) 382 >> ASM_REWRITE_TAC []) 383 >> `!c. {w | w IN m_space m /\ a + g w * b <= c} = 384 {w | w IN m_space m /\ g w <= (c - a) / b}` 385 by (RW_TAC std_ss [Once EXTENSION, GSPECIFICATION] 386 >> FULL_SIMP_TAC std_ss [REAL_LE_SUB_LADD] 387 >> FULL_SIMP_TAC std_ss [Once REAL_ADD_COMM]) 388 >> RW_TAC std_ss [REAL_LE_SUB_LADD] 389 >> METIS_TAC [borel_measurable_le_iff]) 390 >> RW_TAC std_ss [Once (GSYM REAL_LE_NEG), Once (GSYM REAL_MUL_RNEG)] 391 >> `!x. (~(a' - a) <= g x * ~b) = ((~(a' - a))/(~b) <= g x)` 392 by (STRIP_TAC >> MATCH_MP_TAC (GSYM REAL_LE_LDIV_EQ) 393 >> RW_TAC std_ss [REAL_NEG_GT0]) 394 >> POP_ORW 395 >> `{x | x IN m_space m /\ ~(a' - a) / ~b <= g x} = 396 m_space m DIFF {x | x IN m_space m /\ g x < ~(a' - a) / ~b}` 397 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] 398 >> DECIDE_TAC) 399 >> POP_ORW 400 >> Suff `{x | x IN m_space m /\ g x < ~(a' - a) / ~b} IN measurable_sets m` 401 >- METIS_TAC [SPACE, subsets_def, space_def, measurable_sets_def, m_space_def, SIGMA_ALGEBRA, measure_space_def] 402 >> METIS_TAC [borel_measurable_less_iff]); 403 404 405val NON_NEG_REAL_RAT_DENSE = store_thm 406 ("NON_NEG_REAL_RAT_DENSE", 407 ``!(x:real)(y:real). 0 <= x /\ x < y ==> ?(m:num)(n:num). x < &m / & n /\ &m / &n < y``, 408 REPEAT STRIP_TAC 409 >> `0 < y - x` by RW_TAC real_ss [REAL_SUB_LT] 410 >> (MP_TAC o Q.SPEC `y - x`) REAL_ARCH >> RW_TAC bool_ss [] 411 >> POP_ASSUM (MP_TAC o Q.SPEC `1`) >> RW_TAC bool_ss [] 412 >> Q.ABBREV_TAC `m = minimal (\a. y <= & (SUC a) / & n)` 413 >> Q.EXISTS_TAC `m` >> Q.EXISTS_TAC `n` 414 >> `0 < n` 415 by (ONCE_REWRITE_TAC [GSYM REAL_LT] 416 >> MATCH_MP_TAC REAL_LT_TRANS 417 >> Q.EXISTS_TAC `1/(y-x)` 418 >> CONJ_TAC >- (MATCH_MP_TAC REAL_LT_DIV >> RW_TAC real_ss []) 419 >> METIS_TAC [REAL_LT_LDIV_EQ]) 420 >> (MP_TAC o Q.SPEC `inv (&n)`) REAL_ARCH >> ASM_SIMP_TAC real_ss [REAL_INV_POS] 421 >> STRIP_TAC 422 >> POP_ASSUM (MP_TAC o Q.SPEC `y`) >> STRIP_TAC 423 >> `y * &n < &n'` 424 by (FULL_SIMP_TAC std_ss [GSYM real_div] 425 >> METIS_TAC [REAL_LT, REAL_LT_RDIV_EQ]) 426 >> FULL_SIMP_TAC std_ss [GSYM real_div] 427 >> `minimal (\a. y <= & a / & n) = SUC m` 428 by (MATCH_MP_TAC (GSYM MINIMAL_SUC_IMP) 429 >> REVERSE CONJ_TAC 430 >- (RW_TAC real_ss [o_DEF,GSYM real_lt] >> METIS_TAC [REAL_LET_TRANS]) 431 >> Suff `(\a. y <= & (SUC a) / & n) m` >- RW_TAC std_ss [] 432 >> Q.UNABBREV_TAC `m` 433 >> Q.ABBREV_TAC `P = (\a. y <= & (SUC a) / & n)` 434 >> Suff `?a. P a` >- METIS_TAC [MINIMAL_EXISTS] 435 >> Q.UNABBREV_TAC `P` 436 >> RW_TAC std_ss [] 437 >> Cases_on `n' = 0` 438 >- (FULL_SIMP_TAC real_ss [] >> METIS_TAC [REAL_LT_ANTISYM, REAL_LET_TRANS]) 439 >> METIS_TAC [num_CASES,REAL_LT_IMP_LE]) 440 >> `y <= & (SUC m) / & n` 441 by (POP_ASSUM (MP_TAC o GSYM) >> RW_TAC std_ss [] 442 >> Q.ABBREV_TAC `P = (\a. y <= & a / & n)` 443 >> METIS_TAC [MINIMAL_EXISTS, REAL_LT_IMP_LE]) 444 >> CONJ_TAC 445 >- (Suff `y - (y - x) < (&(SUC m))/(&n) - inv(&n)` 446 >- (SIMP_TAC bool_ss [real_div] 447 >> ONCE_REWRITE_TAC [REAL_ARITH ``& m * inv (& n) - inv (& n) = (&m - 1) * inv (&n)``] 448 >> SIMP_TAC real_ss [ADD1] >> ONCE_REWRITE_TAC [GSYM REAL_ADD] 449 >> SIMP_TAC bool_ss [REAL_ADD_SUB_ALT]) 450 >> RW_TAC bool_ss [real_div] 451 >> ONCE_REWRITE_TAC [REAL_ARITH ``& m * inv (& n) - inv (& n) = (&m - 1) * inv (&n)``] 452 >> RW_TAC bool_ss [GSYM real_div] 453 >> (MP_TAC o Q.SPECL [`y - (y - x)`,`&(SUC m) - 1`,`&n`]) REAL_LT_RDIV_EQ 454 >> RW_TAC arith_ss [REAL_LT] >> ONCE_REWRITE_TAC [REAL_SUB_RDISTRIB] 455 >> RW_TAC std_ss [REAL_LT_SUB_RADD] 456 >> (MP_TAC o GSYM o Q.SPECL [`y`,`(&(SUC m)) - 1 + ((y-x)*(&n))`,`&n`]) REAL_LT_RDIV_EQ 457 >> RW_TAC arith_ss [REAL_LT] 458 >> RW_TAC bool_ss [real_div] 459 >> ONCE_REWRITE_TAC [REAL_ARITH ``(& (SUC m) - 1 + (y - x) * & n) * inv (& n) = 460 ((&(SUC m))*(inv(&n))) + ((y - x)*(&n)*inv(&n) - inv (&n))``] 461 >> `(y - x) * (& n) * inv (& n) = (y - x)` 462 by METIS_TAC [REAL_MUL_RINV, GSYM REAL_MUL_ASSOC, REAL_INJ, 463 DECIDE ``!(n:num). 0 < n ==> ~(n=0)``, REAL_MUL_RID] 464 >> POP_ORW 465 >> RW_TAC bool_ss [GSYM real_div] 466 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `& (SUC m)/(&n)` 467 >> RW_TAC bool_ss [REAL_LT_ADDR, Once REAL_SUB_LT, REAL_INV_1OVER] 468 >> (MP_TAC o Q.SPECL [`1`,`y - x`,`&n`]) REAL_LT_LDIV_EQ 469 >> RW_TAC arith_ss [REAL_LT, REAL_MUL_COMM]) 470 >> RW_TAC std_ss [real_lt] 471 >> Q.ABBREV_TAC `P = (\a. y <= & a / & n)` 472 >> Suff `?n. P n` >- METIS_TAC [DECIDE ``m < SUC m``, MINIMAL_EXISTS] 473 >> Q.UNABBREV_TAC `P` 474 >> RW_TAC std_ss [] 475 >> Cases_on `n' = 0` 476 >- (FULL_SIMP_TAC real_ss [] >> METIS_TAC [REAL_LT_ANTISYM, REAL_LET_TRANS]) 477 >> METIS_TAC [num_CASES,REAL_LT_IMP_LE]); 478 479 480val real_rat_set_def = Define 481 `real_rat_set = (IMAGE (\(a:num,b:num). (&a)/(&b)) ((UNIV:num->bool) CROSS (UNIV:num->bool))) UNION 482 (IMAGE (\(a:num,b:num). ~((&a)/(&b))) ((UNIV:num->bool) CROSS (UNIV:num->bool)))`; 483 484 485val countable_real_rat_set = store_thm 486 ("countable_real_rat_set", 487 ``countable real_rat_set``, 488 RW_TAC std_ss [real_rat_set_def] >> MATCH_MP_TAC union_countable 489 >> Suff `countable ((UNIV:num->bool) CROSS (UNIV:num->bool))` >- RW_TAC std_ss [image_countable] 490 >> RW_TAC std_ss [COUNTABLE_ALT_BIJ] >> DISJ2_TAC 491 >> RW_TAC std_ss [enumerate_def] 492 >> METIS_TAC [SELECT_THM, NUM_2D_BIJ_INV]); 493 494 495val REAL_RAT_DENSE = store_thm 496 ("REAL_RAT_DENSE", 497 ``!(x:real)(y:real). x < y ==> ?i. i IN real_rat_set /\ x < i /\ i < y``, 498 RW_TAC std_ss [real_rat_set_def, IN_UNION, IN_IMAGE, IN_CROSS, IN_UNIV] 499 >> Suff `?(a:num)(b:num). (x < (&a)/(&b) /\ (&a)/(&b) < y) \/ (x < ~((&a)/(&b)) /\ ~((&a)/(&b)) < y)` 500 >- (RW_TAC std_ss [] 501 >- (Q.EXISTS_TAC `&a/(&b)` >> RW_TAC std_ss [] 502 >> DISJ1_TAC >> Q.EXISTS_TAC `(a,b)` >> RW_TAC std_ss []) 503 >> Q.EXISTS_TAC `~ (&a/(&b))` >> RW_TAC std_ss [] 504 >> DISJ2_TAC >> Q.EXISTS_TAC `(a,b)` >> RW_TAC std_ss []) 505 >> Cases_on `0 <= x` >- METIS_TAC [NON_NEG_REAL_RAT_DENSE] 506 >> FULL_SIMP_TAC std_ss [GSYM real_lt] 507 >> Cases_on `0 < y` 508 >- (Q.EXISTS_TAC `0` >> Q.EXISTS_TAC `1` >> RW_TAC real_ss []) 509 >> POP_ASSUM (MP_TAC o REWRITE_RULE [real_lt]) >> STRIP_TAC 510 >> ONCE_REWRITE_TAC [REAL_ARITH ``((x:real) = ~~x) /\ ((y:real)= ~~y)``] 511 >> ONCE_REWRITE_TAC [REAL_LT_NEG] 512 >> RW_TAC real_ss [] 513 >> `0 <= ~y` by METIS_TAC [real_lt, REAL_LE_NEG, REAL_NEG_0] 514 >> `~y < ~x` by METIS_TAC [REAL_LT_NEG, REAL_LT_IMP_LE] 515 >> METIS_TAC [NON_NEG_REAL_RAT_DENSE]); 516 517 518val borel_measurable_less_borel_measurable = store_thm 519 ("borel_measurable_less_borel_measurable", 520 ``!m f g. measure_space m /\ 521 f IN borel_measurable (m_space m, measurable_sets m) /\ 522 g IN borel_measurable (m_space m, measurable_sets m) ==> 523 {w | w IN m_space m /\ f w < g w} IN measurable_sets m``, 524 REPEAT STRIP_TAC 525 >> `{w | w IN m_space m /\ f w < g w} = 526 BIGUNION (IMAGE (\i. {w | w IN m_space m /\ f w < i} INTER {w | w IN m_space m /\ i < g w }) 527 real_rat_set)` 528 by (MATCH_MP_TAC SUBSET_ANTISYM 529 >> CONJ_TAC 530 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_BIGUNION, IN_IMAGE, IN_INTER] 531 >> Suff `?i. x IN {w | w IN m_space m /\ f w < i} INTER 532 {w | w IN m_space m /\ i < g w} /\ i IN real_rat_set` 533 >- METIS_TAC [] 534 >> RW_TAC std_ss [IN_INTER, GSPECIFICATION] 535 >> METIS_TAC [REAL_RAT_DENSE]) 536 >> RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE] 537 >> FULL_SIMP_TAC std_ss [IN_INTER, GSPECIFICATION] 538 >> METIS_TAC [REAL_LT_TRANS]) 539 >> POP_ORW 540 >> `sigma_algebra (m_space m,measurable_sets m)` by FULL_SIMP_TAC std_ss [measure_space_def] 541 >> FULL_SIMP_TAC std_ss [sigma_algebra_def, subsets_def, space_def] 542 >> Q.PAT_ASSUM `!c. P c ==> BIGUNION c IN measurable_sets m` MATCH_MP_TAC 543 >> RW_TAC std_ss [image_countable, countable_real_rat_set, SUBSET_DEF, IN_IMAGE, IN_INTER] 544 >> `measurable_sets m = subsets (m_space m, measurable_sets m)` by RW_TAC std_ss [subsets_def] 545 >> POP_ORW >> MATCH_MP_TAC ALGEBRA_INTER 546 >> RW_TAC std_ss [subsets_def] 547 >> METIS_TAC [borel_measurable_less_iff, borel_measurable_gr_iff]); 548 549 550val borel_measurable_leq_borel_measurable = store_thm 551 ("borel_measurable_leq_borel_measurable", 552 ``!m f g. measure_space m /\ 553 f IN borel_measurable (m_space m, measurable_sets m) /\ 554 g IN borel_measurable (m_space m, measurable_sets m) ==> 555 {w | w IN m_space m /\ f w <= g w} IN measurable_sets m``, 556 REPEAT STRIP_TAC 557 >> `{w | w IN m_space m /\ f w <= g w} = 558 m_space m DIFF {w | w IN m_space m /\ g w < f w}` 559 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] >> DECIDE_TAC) 560 >> POP_ORW 561 >> `{w | w IN m_space m /\ g w < f w} IN measurable_sets m` 562 by RW_TAC std_ss [borel_measurable_less_borel_measurable] 563 >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, subsets_def, space_def]); 564 565 566val borel_measurable_eq_borel_measurable = store_thm 567 ("borel_measurable_eq_borel_measurable", 568 ``!m f g. measure_space m /\ 569 f IN borel_measurable (m_space m, measurable_sets m) /\ 570 g IN borel_measurable (m_space m, measurable_sets m) ==> 571 {w | w IN m_space m /\ (f w = g w)} IN measurable_sets m``, 572 REPEAT STRIP_TAC 573 >> `{w | w IN m_space m /\ (f w = g w)} = 574 {w | w IN m_space m /\ f w <= g w} DIFF {w | w IN m_space m /\ f w < g w}` 575 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt] >> METIS_TAC [REAL_LE_ANTISYM]) 576 >> POP_ORW 577 >> `{w | w IN m_space m /\ f w < g w} IN measurable_sets m` 578 by RW_TAC std_ss [borel_measurable_less_borel_measurable] 579 >> `{w | w IN m_space m /\ f w <= g w} IN measurable_sets m` 580 by RW_TAC std_ss [borel_measurable_leq_borel_measurable] 581 582 >> FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def, subsets_def, space_def] 583 >> `measurable_sets m = subsets (m_space m, measurable_sets m)` by RW_TAC std_ss [subsets_def] 584 >> POP_ORW >> MATCH_MP_TAC ALGEBRA_DIFF 585 >> RW_TAC std_ss [subsets_def]); 586 587 588val borel_measurable_neq_borel_measurable = store_thm 589 ("borel_measurable_neq_borel_measurable", 590 ``!m f g. measure_space m /\ 591 f IN borel_measurable (m_space m, measurable_sets m) /\ 592 g IN borel_measurable (m_space m, measurable_sets m) ==> 593 {w | w IN m_space m /\ ~(f w = g w)} IN measurable_sets m``, 594 REPEAT STRIP_TAC 595 >> `{w | w IN m_space m /\ ~(f w = g w)} = 596 m_space m DIFF {w | w IN m_space m /\ (f w = g w)}` 597 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION] >> DECIDE_TAC) 598 >> POP_ORW 599 >> `{w | w IN m_space m /\ (f w = g w)} IN measurable_sets m` 600 by RW_TAC std_ss [borel_measurable_eq_borel_measurable] 601 >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, subsets_def, space_def]); 602 603 604val sigma_algebra_borel_space = store_thm 605 ("sigma_algebra_borel_space", 606 ``sigma_algebra borel_space``, 607 RW_TAC std_ss [borel_space_def] 608 >> MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA 609 >> RW_TAC std_ss [subset_class_def, IN_UNIV, IN_IMAGE, SUBSET_DEF]); 610 611 612val borel_measurable_plus_borel_measurable = store_thm 613 ("borel_measurable_plus_borel_measurable", 614 ``!m f g. measure_space m /\ 615 f IN borel_measurable (m_space m, measurable_sets m) /\ 616 g IN borel_measurable (m_space m, measurable_sets m) ==> 617 (\x. f x + g x) IN borel_measurable (m_space m, measurable_sets m)``, 618 REPEAT STRIP_TAC 619 >> `!a. {w | w IN m_space m /\ a <= f w + g w} = 620 {w | w IN m_space m /\ a + (g w) * (~1) <= f w}` 621 by RW_TAC real_ss [Once EXTENSION, GSPECIFICATION, GSYM real_sub, REAL_LE_SUB_RADD] 622 >> `!a. (\w. a + (g w) * (~1)) IN borel_measurable (m_space m, measurable_sets m)` 623 by RW_TAC std_ss [affine_borel_measurable] 624 >> `!a. {w | w IN m_space m /\ (\w. a + (g w)*(~1)) w <= f w} IN measurable_sets m` 625 by RW_TAC std_ss [borel_measurable_leq_borel_measurable] 626 >> `!a. {w | w IN m_space m /\ a <= f w + g w} IN measurable_sets m` 627 by FULL_SIMP_TAC std_ss [] 628 >> RW_TAC bool_ss [borel_measurable_ge_iff]); 629 630 631val borel_measurable_square = store_thm 632 ("borel_measurable_square", 633 ``!m f g. measure_space m /\ 634 f IN borel_measurable (m_space m, measurable_sets m) ==> 635 (\x. (f x) pow 2) IN borel_measurable (m_space m, measurable_sets m)``, 636 REPEAT STRIP_TAC 637 >> RW_TAC std_ss [borel_measurable_le_iff] 638 >> `!a. 0 <= a pow 2` 639 by (STRIP_TAC 640 >> Cases_on `a = 0` >- RW_TAC real_ss [POW_0] 641 >> RW_TAC bool_ss [Once (GSYM REAL_POW2_ABS)] 642 >> `0 < abs (a)` by METIS_TAC [REAL_LT_LE, REAL_ABS_POS, ABS_ZERO] 643 >> METIS_TAC [REAL_POW_LT, REAL_LT_IMP_LE]) 644 >> `!a. (a pow 2 = 0) = (a = 0)` 645 by (STRIP_TAC >> EQ_TAC >> RW_TAC real_ss [POW_0] 646 >> POP_ASSUM MP_TAC >> RW_TAC bool_ss [Once (GSYM REAL_POW2_ABS)] 647 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 648 >> `0 < abs a` by METIS_TAC [REAL_LT_LE, REAL_ABS_POS, ABS_ZERO] 649 >> (MP_TAC o Q.SPECL [`2`,`0`, `abs a`]) REAL_POW_LT2 650 >> RW_TAC real_ss [POW_0]) 651 >> Cases_on `a < 0` 652 >- (`{x | x IN m_space m /\ f x pow 2 <= a} = {}` 653 by (RW_TAC std_ss [Once EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] 654 >> REVERSE (Cases_on `(x IN m_space m)`) >> RW_TAC std_ss [] 655 >> RW_TAC std_ss [GSYM real_lt] >> MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `0` 656 >> RW_TAC std_ss []) 657 >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, subsets_def]) 658 >> Cases_on `a = 0` 659 >- (ASM_REWRITE_TAC [] 660 >> `{x | x IN m_space m /\ f x pow 2 <= 0} = 661 {x | x IN m_space m /\ f x <= 0} INTER 662 {x | x IN m_space m /\ 0 <= f x}` 663 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, GSPECIFICATION] 664 >> METIS_TAC [REAL_LE_ANTISYM]) 665 >> POP_ORW 666 >> `{x | x IN m_space m /\ f x <= 0} IN measurable_sets m /\ 667 {x | x IN m_space m /\ 0 <= f x} IN measurable_sets m` 668 by METIS_TAC [borel_measurable_le_iff, borel_measurable_ge_iff] 669 >> `measurable_sets m = subsets (m_space m, measurable_sets m)` by RW_TAC std_ss [subsets_def] 670 >> POP_ORW >> MATCH_MP_TAC ALGEBRA_INTER 671 >> FULL_SIMP_TAC std_ss [subsets_def, measure_space_def, sigma_algebra_def]) 672 >> `0 < a` by METIS_TAC [REAL_LT_TOTAL] 673 >> `!b. 0 < b ==> ?q. 0 < q /\ (q pow 2 = b)` 674 by METIS_TAC [SQRT_POS_LT, SQRT_POW_2, REAL_LT_IMP_LE] 675 >> POP_ASSUM (MP_TAC o Q.SPEC `a`) >> RW_TAC std_ss [] 676 >> `!x. (f x pow 2 <= q pow 2) = 677 (~ q <= f x /\ f x <= q)` 678 by (STRIP_TAC >> RW_TAC bool_ss [Once (GSYM REAL_POW2_ABS)] 679 >> ONCE_REWRITE_TAC [GSYM ABS_BOUNDS] 680 >> RW_TAC std_ss [GSYM REAL_NOT_LT] 681 >> REVERSE EQ_TAC 682 >- (STRIP_TAC >> MATCH_MP_TAC REAL_POW_LT2 >> RW_TAC real_ss [REAL_LT_IMP_LE]) 683 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 684 >> POP_ASSUM MP_TAC 685 >> RW_TAC std_ss [REAL_LT_LE] 686 >- (SIMP_TAC std_ss [GSYM REAL_NOT_LT] >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 687 >> (MP_TAC o Q.SPECL [`2`, `abs (f x)`, `q`]) REAL_POW_LT2 688 >> RW_TAC real_ss [REAL_ABS_POS] 689 >> METIS_TAC [REAL_LT_ANTISYM]) 690 >> METIS_TAC [REAL_LT_ANTISYM]) 691 >> POP_ORW 692 >> `{x | x IN m_space m /\ ~q <= f x /\ f x <= q} = 693 {x | x IN m_space m /\ ~q <= f x} INTER 694 {x | x IN m_space m /\ f x <= q}` 695 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, GSPECIFICATION] 696 >> METIS_TAC [REAL_LE_ANTISYM]) 697 >> POP_ORW 698 >> `{x | x IN m_space m /\ ~q <= f x} IN measurable_sets m /\ 699 {x | x IN m_space m /\ f x <= q} IN measurable_sets m` 700 by METIS_TAC [borel_measurable_le_iff, borel_measurable_ge_iff] 701 >> `measurable_sets m = subsets (m_space m, measurable_sets m)` by RW_TAC std_ss [subsets_def] 702 >> POP_ORW >> MATCH_MP_TAC ALGEBRA_INTER 703 >> FULL_SIMP_TAC std_ss [subsets_def, measure_space_def, sigma_algebra_def]); 704 705 706val pow2_binomial = lemma 707 (``!(f:real) g. (f+g) pow 2 = f pow 2 + 2 * (f*g) + g pow 2``, 708 RW_TAC std_ss [POW_2, REAL_ADD_LDISTRIB, REAL_ADD_RDISTRIB] >> REAL_ARITH_TAC); 709 710 711val times_eq_sum_squares = lemma 712 (``!(f:real) g. f*g = ((f+g) pow 2)/4 - ((f-g)pow 2)/4``, 713 RW_TAC std_ss [real_sub, pow2_binomial, real_div, REAL_MUL_RNEG] 714 >> `~g pow 2 = g pow 2` by METIS_TAC [GSYM REAL_POW2_ABS, ABS_NEG] 715 >> POP_ORW 716 >> Q.ABBREV_TAC `a = f * g` >> Q.ABBREV_TAC `b = f pow 2` >> Q.ABBREV_TAC `c = g pow 2` 717 >> ONCE_REWRITE_TAC [GSYM REAL_MUL_LNEG] 718 >> ONCE_REWRITE_TAC [GSYM REAL_ADD_RDISTRIB] 719 >> ONCE_REWRITE_TAC [GSYM real_div] 720 >> (MP_TAC o Q.SPECL [`a`, `(b + 2 * a + c + ~(b + ~(2 * a) + c))`, `4`]) REAL_EQ_RDIV_EQ 721 >> RW_TAC real_ss [GSYM real_sub] 722 >> REAL_ARITH_TAC); 723 724 725val borel_measurable_times_borel_measurable = store_thm 726 ("borel_measurable_times_borel_measurable", 727 ``!m f g. measure_space m /\ 728 f IN borel_measurable (m_space m, measurable_sets m) /\ 729 g IN borel_measurable (m_space m, measurable_sets m) ==> 730 (\x. f x * g x) IN borel_measurable (m_space m, measurable_sets m)``, 731 REPEAT STRIP_TAC 732 >> `(\x. f x * g x) = (\x. ((f x + g x) pow 2)/4 - ((f x - g x) pow 2)/4)` 733 by RW_TAC std_ss [times_eq_sum_squares] 734 >> POP_ORW 735 >> RW_TAC bool_ss [real_div, real_sub] 736 >> Suff `(\x. (f x + g x) pow 2 * inv 4) IN borel_measurable (m_space m,measurable_sets m) /\ 737 (\x. ~((f x + ~g x) pow 2 * inv 4)) IN borel_measurable (m_space m,measurable_sets m)` 738 >- RW_TAC std_ss [borel_measurable_plus_borel_measurable] 739 >> ONCE_REWRITE_TAC [GSYM REAL_ADD_LID] 740 >> CONJ_TAC >- METIS_TAC [affine_borel_measurable, borel_measurable_square, borel_measurable_plus_borel_measurable] 741 >> ONCE_REWRITE_TAC [GSYM REAL_MUL_RNEG] 742 >> Suff `(\x. ~ g x) IN borel_measurable (m_space m,measurable_sets m)` 743 >- METIS_TAC [affine_borel_measurable, borel_measurable_square, borel_measurable_plus_borel_measurable] 744 >> `!x. ~ g x = 0 + (g x) * ~1` by RW_TAC real_ss [] 745 >> POP_ORW 746 >> RW_TAC std_ss [affine_borel_measurable]); 747 748 749val borel_measurable_sub_borel_measurable = store_thm 750 ("borel_measurable_sub_borel_measurable", 751 ``!m f g. measure_space m /\ 752 f IN borel_measurable (m_space m, measurable_sets m) /\ 753 g IN borel_measurable (m_space m, measurable_sets m) ==> 754 (\x. f x - g x) IN borel_measurable (m_space m, measurable_sets m)``, 755 RW_TAC bool_ss [real_sub] 756 >> Suff `(\x. ~ g x) IN borel_measurable (m_space m,measurable_sets m)` 757 >- METIS_TAC [borel_measurable_plus_borel_measurable] 758 >> `!x. ~ g x = 0 + (g x) * ~1` by RW_TAC real_ss [] 759 >> POP_ORW 760 >> RW_TAC std_ss [affine_borel_measurable]); 761 762 763val mono_convergent_borel_measurable = store_thm 764 ("mono_convergent_borel_measurable", 765 ``!u m f. measure_space m /\ (!n. u n IN borel_measurable (m_space m, measurable_sets m)) /\ 766 mono_convergent u f (m_space m) ==> 767 f IN borel_measurable (m_space m, measurable_sets m)``, 768 REPEAT STRIP_TAC 769 >> RW_TAC std_ss [borel_measurable_le_iff] 770 >> `!w. w IN m_space m /\ f w <= a = w IN m_space m /\ !i. u i w <= a` 771 by (FULL_SIMP_TAC std_ss [mono_convergent_def] >> STRIP_TAC >> EQ_TAC 772 >- (RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `f w` 773 >> ASM_REWRITE_TAC [] >> `u i w = (\i. u i w) i` by SIMP_TAC std_ss [] >> POP_ORW 774 >> MATCH_MP_TAC SEQ_MONO_LE >> RW_TAC arith_ss []) 775 >> RW_TAC std_ss [] >> MATCH_MP_TAC SEQ_LE_IMP_LIM_LE 776 >> Q.EXISTS_TAC `(\i. u i w)` >> RW_TAC std_ss []) 777 >> POP_ORW 778 >> `{w: 'a | w IN m_space m /\ !i:num. (u :num -> 'a -> real) i w <= (a:real)} = 779 (m_space m) DIFF 780 (BIGUNION (IMAGE (\i. (m_space m) DIFF 781 {w | w IN m_space m /\ (u :num -> 'a -> real) i w <= (a:real)}) 782 (UNIV:num->bool)))` 783 by (RW_TAC std_ss [Once EXTENSION, GSPECIFICATION, IN_DIFF, IN_BIGUNION_IMAGE, IN_UNIV] 784 >> METIS_TAC []) 785 >> POP_ORW 786 >> `sigma_algebra (m_space m, measurable_sets m)` by FULL_SIMP_TAC std_ss [measure_space_def] 787 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, space_def, subsets_def] 788 >> Suff `(BIGUNION (IMAGE (\i. (m_space m) DIFF 789 {w | w IN m_space m /\ (u :num -> 'a -> real) i w <= (a:real)}) 790 (UNIV:num->bool))) IN measurable_sets m` 791 >- RW_TAC std_ss [] 792 >> Q.PAT_X_ASSUM `!c. P c ==> BIGUNION c IN measurable_sets m` MATCH_MP_TAC 793 >> RW_TAC std_ss [image_countable, COUNTABLE_NUM, SUBSET_DEF, IN_IMAGE, IN_UNIV] 794 >> POP_ASSUM MATCH_MP_TAC 795 >> METIS_TAC [borel_measurable_le_iff]); 796 797 798val borel_measurable_SIGMA_borel_measurable = store_thm 799 ("borel_measurable_SIGMA_borel_measurable", 800 ``!m f s. measure_space m /\ FINITE s /\ 801 (!i. i IN s ==> f i IN borel_measurable (m_space m, measurable_sets m)) ==> 802 (\x. SIGMA (\i. f i x) s) IN borel_measurable (m_space m, measurable_sets m)``, 803 REPEAT STRIP_TAC 804 >> Suff `!s. FINITE s ==> (\s. !f. (!i. i IN s ==> f i IN borel_measurable (m_space m, measurable_sets m)) ==> 805 (\x. SIGMA (\i. f i x) s) IN borel_measurable (m_space m, measurable_sets m)) s` 806 >- METIS_TAC [] 807 >> MATCH_MP_TAC FINITE_INDUCT 808 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, IN_INSERT, DELETE_NON_ELEMENT] 809 >- FULL_SIMP_TAC std_ss [measure_space_def, borel_measurable_const] 810 >> METIS_TAC [borel_measurable_plus_borel_measurable]); 811 812 813val _ = export_theory (); 814