1(* ========================================================================= *) 2(* Create "lebesgueTheory" setting up the theory of Lebesgue Integration *) 3(* ========================================================================= *) 4 5(* ------------------------------------------------------------------------- *) 6(* Load and open relevant theories *) 7(* (Comment out "load" and "loadPath"s for compilation) *) 8(* ------------------------------------------------------------------------- *) 9(* 10 11app load ["bossLib", "metisLib", "arithmeticTheory", "pred_setTheory", "listTheory", 12 "state_transformerTheory", "formalizeUseful", 13 "combinTheory", "pairTheory", "realTheory", "realLib", "extra_boolTheory", "jrhUtils", 14 "extra_pred_setTheory", "realSimps", "extra_realTheory", 15 "measureTheory", "numTheory", "simpLib", 16 "seqTheory", "subtypeTheory", 17 "transcTheory", "limTheory", "stringTheory", "rich_listTheory", "stringSimps", 18 "listSimps", "borelTheory", "whileTheory"]; 19 20*) 21 22open HolKernel Parse boolLib bossLib metisLib arithmeticTheory pred_setTheory 23 listTheory state_transformerTheory formalizeUseful extra_numTheory combinTheory 24 pairTheory realTheory realLib extra_boolTheory jrhUtils 25 extra_pred_setTheory realSimps extra_realTheory measureTheory numTheory 26 simpLib seqTheory subtypeTheory 27 transcTheory limTheory stringTheory rich_listTheory stringSimps listSimps 28 borelTheory whileTheory; 29 30open real_sigmaTheory; 31 32(* ------------------------------------------------------------------------- *) 33(* Start a new theory called "lebesgue" *) 34(* ------------------------------------------------------------------------- *) 35 36val _ = new_theory "lebesgue"; 37 38(* ------------------------------------------------------------------------- *) 39(* Helpful proof tools *) 40(* ------------------------------------------------------------------------- *) 41 42val REVERSE = Tactical.REVERSE; 43val lemma = I prove; 44 45val Simplify = RW_TAC arith_ss; 46val Suff = PARSE_TAC SUFF_TAC; 47val Know = PARSE_TAC KNOW_TAC; 48val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 49val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 50val Cond = 51 DISCH_THEN 52 (fn mp_th => 53 let 54 val cond = fst (dest_imp (concl mp_th)) 55 in 56 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 57 end); 58 59val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 60 61val safe_list_ss = bool_ss ++ LIST_ss; 62 63val safe_string_ss = bool_ss ++ STRING_ss; 64 65val arith_string_ss = arith_ss ++ STRING_ss; 66 67 68(* ************************************************************************* *) 69(* ************************************************************************* *) 70(* Basic Definitions *) 71(* ************************************************************************* *) 72(* ************************************************************************* *) 73 74 75val pos_simple_fn_def = Define 76 `pos_simple_fn m f (s:num->bool) a x = 77 (!t. 0 <= f t) /\ 78 (!t. t IN m_space m ==> (f t = SIGMA (\i. (x i) * (indicator_fn (a i) t)) s)) /\ 79 (!i. i IN s ==> a i IN measurable_sets m) /\ 80 (!i. 0 <= x i) /\ 81 FINITE s /\ 82 (!i j. i IN s /\ j IN s /\ (~(i=j)) ==> DISJOINT (a i) (a j)) /\ 83 (BIGUNION (IMAGE a s) = m_space m)`; 84 85 86val pos_simple_fn_integral_def = Define 87 `pos_simple_fn_integral m s a x = 88 SIGMA (\i. (x i) * ((measure m) (a i))) s`; 89 90 91val psfs_def = Define 92 `psfs m f = {(s,a,x) | pos_simple_fn m f s a x}`; 93 94 95val psfis_def = Define 96 `psfis m f = IMAGE (\(s,a,x). pos_simple_fn_integral m s a x) (psfs m f)`; 97 98 99val pos_fn_integral_def = Define 100 `pos_fn_integral m f = sup {r:real | ?g. r IN psfis m g /\ 101 !x. g x <= f x}`; 102 103 104val nonneg_def = Define 105 `nonneg f = !x. 0<= f x`; 106 107 108val pos_part_def = Define 109 `pos_part f = (\x. if 0 <= f x then f x else 0)`; 110 111 112val neg_part_def = Define 113 `neg_part f = (\x. if 0 <= f x then 0 else ~ f x)`; 114 115 116val mono_increasing_def = Define 117 `mono_increasing (f:num->real) = !m n. m <= n ==> f m <= f n`; 118 119 120val nnfis_def = Define 121 `nnfis m f = {y | ?u x. mono_convergent u f (m_space m) /\ 122 (!n. x n IN psfis m (u n)) /\ 123 x --> y}`; 124 125 126val upclose_def = Define 127 `upclose f g = (\t. max (f t) (g t))`; 128 129 130val mon_upclose_help_def = Define 131 `(mon_upclose_help 0 u m = u m 0) /\ 132 (mon_upclose_help (SUC n) u m = upclose (u m (SUC n)) (mon_upclose_help n u m))`; 133 134 135val mon_upclose_def = Define 136 `mon_upclose u m = mon_upclose_help m u m`; 137 138 139val integrable_def = Define 140 `integrable m f = measure_space m /\ 141 (?x. x IN nnfis m (pos_part f)) /\ 142 (?y. y IN nnfis m (neg_part f))`; 143 144 145val integral_def = Define 146 `integral m f = (@i. i IN nnfis m (pos_part f)) - (@j. j IN nnfis m (neg_part f))`; 147 148 149val finite_space_integral_def = Define 150 `finite_space_integral m f = 151 SIGMA (\r. r * measure m (PREIMAGE f {r} INTER m_space m)) (IMAGE f (m_space m))`; 152 153 154val countable_space_integral_def = Define 155 `countable_space_integral m f = 156 let e = enumerate (IMAGE f (m_space m)) in 157 suminf ((\r. r * measure m (PREIMAGE f {r} INTER m_space m)) o e)`; 158 159 160val prod_measure_def = Define 161 `prod_measure m0 m1 = 162 (\a. integral m0 (\s0. (measure m1) (PREIMAGE (\s1. (s0,s1)) a)))`; 163 164 165val prod_measure_space_def = Define 166 `prod_measure_space m0 m1 = 167 ((m_space m0) CROSS (m_space m1), 168 subsets (sigma ((m_space m0) CROSS (m_space m1)) 169 (prod_sets (measurable_sets m0) (measurable_sets m1))), 170 prod_measure m0 m1)`; 171 172 173val RN_deriv_def = Define 174 `RN_deriv m v = 175 @f. measure_space m /\ measure_space (m_space m, measurable_sets m, v) /\ 176 f IN borel_measurable (m_space m, measurable_sets m) /\ 177 (!a. a IN measurable_sets m ==> 178 (integral m (\x. f x * indicator_fn a x) = v a))`; 179 180 181(* ************************************************************************* *) 182(* ************************************************************************* *) 183(* Proofs *) 184(* ************************************************************************* *) 185(* ************************************************************************* *) 186 187 188val indicator_fn_split = store_thm 189 ("indicator_fn_split", 190 ``!(r:num->bool) s (b:num->('a->bool)). 191 FINITE r /\ 192 (BIGUNION (IMAGE b r) = s) /\ 193 (!i j. i IN r /\ j IN r /\ (~(i=j)) ==> DISJOINT (b i) (b j)) ==> 194 !a. a SUBSET s ==> 195 ((indicator_fn a) = 196 (\x. SIGMA (\i. indicator_fn (a INTER (b i)) x) r))``, 197 Suff `!r. FINITE r ==> 198 (\r. !s (b:num->('a->bool)). 199 FINITE r /\ 200 (BIGUNION (IMAGE b r) = s) /\ 201 (!i j. i IN r /\ j IN r /\ (~(i=j)) ==> DISJOINT (b i) (b j)) ==> 202 !a. a SUBSET s ==> 203 ((indicator_fn a) = 204 (\x. SIGMA (\i. indicator_fn (a INTER (b i)) x) r))) r` 205 >- METIS_TAC [] 206 >> MATCH_MP_TAC FINITE_INDUCT 207 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, IMAGE_EMPTY, BIGUNION_EMPTY, SUBSET_EMPTY, 208 indicator_fn_def, NOT_IN_EMPTY, FINITE_INSERT, IMAGE_INSERT, 209 DELETE_NON_ELEMENT, IN_INSERT, BIGUNION_INSERT] 210 >> Q.PAT_X_ASSUM `!b. P ==> !a. Q ==> (x = y)` 211 (MP_TAC o Q.ISPEC `(b :num -> 'a -> bool)`) 212 >> RW_TAC std_ss [SUBSET_DEF] 213 >> POP_ASSUM (MP_TAC o Q.ISPEC `a DIFF ((b :num -> 'a -> bool) e)`) 214 >> Know `(!x. x IN a DIFF b e ==> x IN BIGUNION (IMAGE b s))` 215 >- METIS_TAC [SUBSET_DEF, IN_UNION, IN_DIFF] 216 >> RW_TAC std_ss [FUN_EQ_THM] 217 >> Know `SIGMA (\i. (if x IN a INTER b i then 1 else 0)) s = 218 SIGMA (\i. (if x IN (a DIFF b e) INTER b i then 1 else 0)) s` 219 >- (ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s :num -> bool)`) REAL_SUM_IMAGE_IN_IF] 220 >> MATCH_MP_TAC (METIS_PROVE [] ``!f x y z. (x = y) ==> (f x z = f y z)``) 221 >> RW_TAC std_ss [FUN_EQ_THM, IN_INTER, IN_DIFF] 222 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT, DISJOINT_DEF, 223 IN_INTER, NOT_IN_EMPTY, 224 EXTENSION, GSPECIFICATION] 225 >> RW_TAC real_ss [] >> METIS_TAC []) 226 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [GSYM thm]) 227 >> RW_TAC real_ss [IN_DIFF, IN_INTER] >> METIS_TAC []); 228 229 230val measure_split = store_thm 231 ("measure_split", 232 ``!(r:num->bool) (b:num->('a->bool)) m. 233 measure_space m /\ 234 FINITE r /\ 235 (BIGUNION (IMAGE b r) = m_space m) /\ 236 (!i j. i IN r /\ j IN r /\ (~(i=j)) ==> DISJOINT (b i) (b j)) /\ 237 (!i. i IN r ==> b i IN measurable_sets m) ==> 238 !a. a IN measurable_sets m ==> 239 ((measure m) a = 240 SIGMA (\i. (measure m) (a INTER (b i))) r)``, 241 Suff `!r. FINITE r ==> 242 (\r. !(b:num->('a->bool)) m. 243 measure_space m /\ 244 (BIGUNION (IMAGE b r) = m_space m) /\ 245 (!i j. i IN r /\ j IN r /\ (~(i=j)) ==> DISJOINT (b i) (b j)) /\ 246 (!i. i IN r ==> b i IN measurable_sets m) ==> 247 !a. a IN measurable_sets m ==> 248 ((measure m) a = 249 SIGMA (\i. (measure m) (a INTER (b i))) r)) r` 250 >- METIS_TAC [] 251 >> MATCH_MP_TAC FINITE_INDUCT 252 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, IMAGE_EMPTY, BIGUNION_EMPTY, 253 DELETE_NON_ELEMENT, 254 IN_INSERT] 255 >- (`!a m. measure_space m /\ 256 a IN measurable_sets m ==> a SUBSET m_space m` 257 by RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, 258 subset_class_def, subsets_def, space_def] 259 >> METIS_TAC [SUBSET_EMPTY, MEASURE_EMPTY]) 260 >> `!a m. measure_space m /\ 261 a IN measurable_sets m ==> a SUBSET m_space m` 262 by RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, 263 subset_class_def, subsets_def, space_def] 264 >> POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 265 Q.SPECL [`a`,`m`]) 266 >> Cases_on `s = {}` 267 >- (FULL_SIMP_TAC std_ss [REAL_SUM_IMAGE_THM, IMAGE_DEF, IN_SING, BIGUNION, 268 GSPECIFICATION, GSPEC_ID, SUBSET_DEF] 269 >> Know `a INTER m_space m = a` 270 >- (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER] >> METIS_TAC []) 271 >> RW_TAC real_ss []) 272 >> `?x s'. (s = x INSERT s') /\ ~(x IN s')` by METIS_TAC [SET_CASES] 273 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT, IN_INSERT] 274 >> Q.PAT_X_ASSUM `!b' m'. P ==> !a'. Q ==> (f = g)` 275 (MP_TAC o Q.ISPECL [`(\i:num. if i = x then b x UNION b e else b i)`, 276 `(m :('a -> bool) # (('a -> bool) -> bool) # (('a -> bool) -> real))`]) 277 >> `IMAGE (\i. (if i = x then b x UNION b e else b i)) s' = IMAGE b s'` 278 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE] 279 >> EQ_TAC 280 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `i` >> METIS_TAC []) 281 >> RW_TAC std_ss [] >> Q.EXISTS_TAC `x''` >> METIS_TAC []) 282 >> FULL_SIMP_TAC std_ss [IMAGE_INSERT, BIGUNION_INSERT, UNION_ASSOC] 283 >> POP_ASSUM (K ALL_TAC) 284 >> `(b x UNION b e UNION BIGUNION (IMAGE b s') = m_space m)` 285 by METIS_TAC [UNION_COMM] 286 >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 287 >> `(!i j. 288 ((i = x) \/ i IN s') /\ ((j = x) \/ j IN s') /\ ~(i = j) ==> 289 DISJOINT (if i = x then b x UNION b e else b i) 290 (if j = x then b x UNION b e else b j))` 291 by (FULL_SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, GSPECIFICATION, IN_INSERT, 292 IN_INTER, NOT_IN_EMPTY] 293 >> METIS_TAC [IN_UNION]) 294 >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 295 >> `(!i. 296 (i = x) \/ i IN s' ==> 297 (if i = x then b x UNION b e else b i) IN measurable_sets m)` 298 by METIS_TAC [ALGEBRA_UNION, sigma_algebra_def, measure_space_def, subsets_def] 299 >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 300 >> STRIP_TAC 301 >> POP_ASSUM ((fn thm => ONCE_REWRITE_TAC [thm]) o UNDISCH o Q.SPEC `a`) 302 >> FULL_SIMP_TAC real_ss [FINITE_INSERT, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, 303 REAL_ADD_ASSOC] 304 >> Suff `(measure m (a INTER (b x UNION b e)) = 305 measure m (a INTER b e) + measure m (a INTER b x)) /\ 306 (SIGMA (\i. measure m (a INTER 307 (if i = x then b x UNION b e else b i))) s' = 308 SIGMA (\i. measure m (a INTER b i)) s')` 309 >- RW_TAC std_ss [] 310 >> CONJ_TAC 311 >- (`a INTER (b x UNION b e) = (a INTER b e) UNION (a INTER b x)` 312 by (FULL_SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, GSPECIFICATION, 313 NOT_IN_EMPTY, IN_INTER, IN_UNION] 314 >> METIS_TAC []) 315 >> POP_ORW 316 >> (MATCH_MP_TAC o REWRITE_RULE [additive_def] o UNDISCH o Q.SPEC `m`) 317 MEASURE_SPACE_ADDITIVE 318 >> CONJ_TAC 319 >- METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, measure_space_def, subsets_def] 320 >> CONJ_TAC 321 >- METIS_TAC [ALGEBRA_INTER, sigma_algebra_def, measure_space_def, subsets_def] 322 >> FULL_SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, IN_INTER] 323 >> METIS_TAC []) 324 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s' :num -> bool)`) REAL_SUM_IMAGE_IN_IF] 325 >> MATCH_MP_TAC (METIS_PROVE [] ``!f x y z. (x = y) ==> (f x z = f y z)``) 326 >> RW_TAC std_ss [FUN_EQ_THM] 327 >> RW_TAC std_ss [] 328 >> FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT]); 329 330 331val pos_simple_fn_integral_present = store_thm 332 ("pos_simple_fn_integral_present", 333 ``!m f (s:num->bool) a (x:num->real) 334 g (s':num->bool) b (y:num->real). 335 measure_space m /\ 336 pos_simple_fn m f s a x /\ pos_simple_fn m g s' b y ==> 337 (?(z:num->real) (z':num->real) c (k:num->bool). 338 (!t. t IN m_space m ==> (f t = SIGMA (\i. (z i) * (indicator_fn (c i) t)) k)) /\ 339 (!t. t IN m_space m ==> (g t = SIGMA (\i. (z' i) * (indicator_fn (c i) t)) k)) /\ 340 (pos_simple_fn_integral m s a x = pos_simple_fn_integral m k c z) /\ 341 (pos_simple_fn_integral m s' b y = pos_simple_fn_integral m k c z') /\ 342 FINITE k /\ 343 (!i j. i IN k /\ j IN k /\ (~(i=j)) ==> DISJOINT (c i) (c j)) /\ 344 (!i. i IN k ==> c i IN measurable_sets m) /\ 345 (BIGUNION (IMAGE c k) = m_space m) /\ 346 (!i. 0 <= z i) /\ (!i. 0 <= z' i))``, 347 RW_TAC std_ss [] 348 >> `?p n. BIJ p (count n) (s CROSS s')` 349 by FULL_SIMP_TAC std_ss [GSYM FINITE_BIJ_COUNT_EQ, pos_simple_fn_def, FINITE_CROSS] 350 >> `?p'. BIJ p' (s CROSS s') (count n) /\ 351 (!x. x IN (count n) ==> ((p' o p) x = x)) /\ 352 (!x. x IN (s CROSS s') ==> ((p o p') x = x))` 353 by (MATCH_MP_TAC BIJ_INV >> RW_TAC std_ss []) 354 >> Q.EXISTS_TAC `x o FST o p` 355 >> Q.EXISTS_TAC `y o SND o p` 356 >> Q.EXISTS_TAC `(\(i,j). a i INTER b j) o p` 357 >> Q.EXISTS_TAC `IMAGE p' (s CROSS s')` 358 >> Q.ABBREV_TAC `G = IMAGE (\i j. p' (i,j)) s'` 359 >> Q.ABBREV_TAC `H = IMAGE (\j i. p' (i,j)) s` 360 >> CONJ_TAC 361 >- (RW_TAC std_ss [FUN_EQ_THM] >> FULL_SIMP_TAC std_ss [pos_simple_fn_def] 362 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s :num -> bool)`) REAL_SUM_IMAGE_IN_IF] 363 >> `(\x'. (if x' IN s then (\i. x i * indicator_fn (a i) t) x' else 0)) = 364 (\x'. (if x' IN s then (\i. x i * 365 SIGMA (\j. indicator_fn (a i INTER b j) t) s') x' else 0))` 366 by (RW_TAC std_ss [FUN_EQ_THM] 367 >> RW_TAC std_ss [] 368 >> FULL_SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 369 >> (MP_TAC o Q.ISPEC `(a :num -> 'a -> bool) (x' :num)` o 370 UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 371 Q.ISPECL 372 [`(s' :num -> bool)`, 373 `m_space (m:('a -> bool) # 374 (('a -> bool) -> bool) # (('a -> bool) -> real))`, 375 `(b :num -> 'a -> bool)`]) indicator_fn_split 376 >> Q.PAT_X_ASSUM `!i. i IN s ==> (a:num->'a->bool) i IN measurable_sets m` 377 (ASSUME_TAC o UNDISCH o Q.SPEC `x'`) 378 >> `!a m. measure_space m /\ 379 a IN measurable_sets m ==> a SUBSET m_space m` 380 by RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, 381 subset_class_def, subsets_def, space_def] 382 >> POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 383 Q.ISPECL [`(a :num -> 'a -> bool) (x' :num)`, 384 `(m : ('a -> bool) # 385 (('a -> bool) -> bool) # (('a -> bool) -> real))`]) 386 >> ASM_SIMP_TAC std_ss []) 387 >> POP_ORW 388 >> `!(x':num) (i:num). x i * SIGMA (\j. indicator_fn (a i INTER b j) t) s' = 389 SIGMA (\j. x i * indicator_fn (a i INTER b j) t) s'` 390 by METIS_TAC [REAL_SUM_IMAGE_CMUL] 391 >> POP_ORW 392 >> `FINITE (s CROSS s')` by RW_TAC std_ss [FINITE_CROSS] 393 >> `INJ p' (s CROSS s') 394 (IMAGE p' (s CROSS s'))` 395 by METIS_TAC [INJ_IMAGE_BIJ, BIJ_DEF] 396 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `p'` o UNDISCH o 397 Q.ISPEC `((s:num->bool) CROSS (s':num->bool))` o 398 INST_TYPE [``:'b``|->``:num``]) REAL_SUM_IMAGE_IMAGE] 399 >> RW_TAC std_ss [o_DEF] 400 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s :num -> bool)CROSS(s' :num -> bool)`) 401 REAL_SUM_IMAGE_IN_IF] 402 >> `(\x'. (if x' IN s CROSS s' then 403 (\x'. x (FST (p (p' x'))) * 404 indicator_fn ((\(i,j). a i INTER b j) (p (p' x'))) t) x' 405 else 0)) = 406 (\x'. (if x' IN s CROSS s' then 407 (\x'. x (FST x') * 408 indicator_fn ((\(i,j). a i INTER b j) x') t) x' 409 else 0))` by METIS_TAC [] 410 >> POP_ORW 411 >> RW_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 412 >> `!x'. (\j. x x' * indicator_fn (a x' INTER b j) t) = 413 (\x' j. x x' * indicator_fn (a x' INTER b j) t) x'` 414 by METIS_TAC [] 415 >> POP_ORW 416 >> (MP_TAC o Q.ISPECL [`s:num->bool`,`s':num->bool`]) REAL_SUM_IMAGE_REAL_SUM_IMAGE 417 >> RW_TAC std_ss [] 418 >> Suff `(\x'. x (FST x') * indicator_fn (a (FST x') INTER b (SND x')) t) = 419 (\x'. x (FST x') * indicator_fn ((\(i,j). a i INTER b j) x') t)` 420 >- RW_TAC std_ss [] 421 >> RW_TAC std_ss [FUN_EQ_THM] 422 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 423 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND]) 424 >> CONJ_TAC 425 >- (RW_TAC std_ss [FUN_EQ_THM] >> FULL_SIMP_TAC std_ss [pos_simple_fn_def] 426 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s' :num -> bool)`) REAL_SUM_IMAGE_IN_IF] 427 >> `(\x. (if x IN s' then (\i. y i * indicator_fn (b i) t) x else 0)) = 428 (\x. (if x IN s' then (\i. y i * 429 SIGMA (\j. indicator_fn (a j INTER b i) t) s) x else 0))` 430 by (RW_TAC std_ss [FUN_EQ_THM] 431 >> RW_TAC std_ss [] 432 >> FULL_SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 433 >> (MP_TAC o REWRITE_RULE [Once INTER_COMM] o 434 Q.ISPEC `(b :num -> 'a -> bool) (x' :num)` o 435 UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 436 Q.ISPECL 437 [`(s :num -> bool)`, 438 `m_space (m:('a -> bool) # 439 (('a -> bool) -> bool) # (('a -> bool) -> real))`, 440 `(a :num -> 'a -> bool)`]) indicator_fn_split 441 >> Q.PAT_X_ASSUM `!i. i IN s' ==> (b:num->'a->bool) i IN measurable_sets m` 442 (ASSUME_TAC o UNDISCH o Q.SPEC `x'`) 443 >> `!a m. measure_space m /\ 444 a IN measurable_sets m ==> a SUBSET m_space m` 445 by RW_TAC std_ss [measure_space_def, sigma_algebra_def, algebra_def, 446 subset_class_def, subsets_def, space_def] 447 >> POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 448 Q.ISPECL [`(b :num -> 'a -> bool) (x' :num)`, 449 `(m : ('a -> bool) # 450 (('a -> bool) -> bool) # (('a -> bool) -> real))`]) 451 >> ASM_SIMP_TAC std_ss []) 452 >> POP_ORW 453 >> `!(x:num) (i:num). y i * SIGMA (\j. indicator_fn (a j INTER b i) t) s = 454 SIGMA (\j. y i * indicator_fn (a j INTER b i) t) s` 455 by METIS_TAC [REAL_SUM_IMAGE_CMUL] 456 >> POP_ORW 457 >> `FINITE (s CROSS s')` by RW_TAC std_ss [FINITE_CROSS] 458 >> `INJ p' (s CROSS s') 459 (IMAGE p' (s CROSS s'))` 460 by METIS_TAC [INJ_IMAGE_BIJ, BIJ_DEF] 461 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `p'` o UNDISCH o 462 Q.ISPEC `((s:num->bool) CROSS (s':num->bool))` o 463 INST_TYPE [``:'b``|->``:num``]) REAL_SUM_IMAGE_IMAGE] 464 >> RW_TAC std_ss [o_DEF] 465 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s :num -> bool)CROSS(s' :num -> bool)`) 466 REAL_SUM_IMAGE_IN_IF] 467 >> `(\x. (if x IN s CROSS s' then 468 (\x. y (SND (p (p' x))) * 469 indicator_fn ((\(i,j). a i INTER b j) (p (p' x))) t) x else 0)) = 470 (\x. (if x IN s CROSS s' then 471 (\x. y (SND x) * 472 indicator_fn ((\(i,j). a i INTER b j) x) t) x else 0))` by METIS_TAC [] 473 >> POP_ORW 474 >> RW_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 475 >> `!x. (\j. y x * indicator_fn (a j INTER b x) t) = 476 (\x j. y x * indicator_fn (a j INTER b x) t) x` 477 by METIS_TAC [] 478 >> POP_ORW 479 >> (MP_TAC o Q.ISPECL [`s':num->bool`,`s:num->bool`]) REAL_SUM_IMAGE_REAL_SUM_IMAGE 480 >> RW_TAC std_ss [] 481 >> `(s' CROSS s) = IMAGE (\x. (SND x, FST x)) (s CROSS s')` 482 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_CROSS, IN_IMAGE] 483 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 484 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 485 >> EQ_TAC 486 >- (STRIP_TAC >> Q.EXISTS_TAC `(r,q)` >> RW_TAC std_ss [FST,SND]) 487 >> RW_TAC std_ss [] >> RW_TAC std_ss []) 488 >> POP_ORW 489 >> `INJ (\x. (SND x,FST x)) (s CROSS s') 490 (IMAGE (\x. (SND x,FST x)) (s CROSS s'))` 491 by (RW_TAC std_ss [INJ_DEF, IN_CROSS, IN_IMAGE] 492 >- METIS_TAC [] 493 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 494 >> (MP_TAC o Q.ISPEC `x'':num#num`) pair_CASES 495 >> RW_TAC std_ss [] 496 >> FULL_SIMP_TAC std_ss [FST,SND]) 497 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `(\x. (SND x, FST x))` o UNDISCH o 498 Q.ISPEC `((s:num->bool) CROSS (s':num->bool))` o 499 INST_TYPE [``:'b``|->``:num#num``]) REAL_SUM_IMAGE_IMAGE] 500 >> RW_TAC std_ss [o_DEF] 501 >> Suff `(\x. y (SND x) * indicator_fn (a (FST x) INTER b (SND x)) t) = 502 (\x. y (SND x) * indicator_fn ((\(i,j). a i INTER b j) x) t)` 503 >- RW_TAC std_ss [] 504 >> RW_TAC std_ss [FUN_EQ_THM] 505 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 506 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND]) 507 >> CONJ_TAC 508 >- (RW_TAC std_ss [pos_simple_fn_integral_def] >> FULL_SIMP_TAC std_ss [pos_simple_fn_def] 509 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s :num -> bool)`) REAL_SUM_IMAGE_IN_IF] 510 >> `(\x'. (if x' IN s then (\i. x i * measure m (a i)) x' else 0)) = 511 (\x'. (if x' IN s then (\i. x i * 512 SIGMA (\j. measure m (a i INTER b j)) s') x' else 0))` 513 by (RW_TAC std_ss [FUN_EQ_THM] 514 >> RW_TAC std_ss [] 515 >> FULL_SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 516 >> (MP_TAC o Q.SPEC `a (x' :num)` o 517 UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 518 Q.SPECL 519 [`s'`, `b`, `m`]) measure_split 520 >> RW_TAC std_ss []) 521 >> POP_ORW 522 >> `!(x':num) (i:num). x i * SIGMA (\j. measure m (a i INTER b j)) s' = 523 SIGMA (\j. x i * measure m (a i INTER b j)) s'` 524 by METIS_TAC [REAL_SUM_IMAGE_CMUL] 525 >> POP_ORW 526 >> `FINITE (s CROSS s')` by RW_TAC std_ss [FINITE_CROSS] 527 >> `INJ p' (s CROSS s') 528 (IMAGE p' (s CROSS s'))` 529 by METIS_TAC [INJ_IMAGE_BIJ, BIJ_DEF] 530 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `p'` o UNDISCH o 531 Q.ISPEC `((s:num->bool) CROSS (s':num->bool))` o 532 INST_TYPE [``:'b``|->``:num``]) REAL_SUM_IMAGE_IMAGE] 533 >> RW_TAC std_ss [o_DEF] 534 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s :num -> bool)CROSS(s' :num -> bool)`) 535 REAL_SUM_IMAGE_IN_IF] 536 >> `(\x'. (if x' IN s CROSS s' then 537 (\x'. x (FST (p (p' x'))) * 538 measure m ((\(i,j). a i INTER b j) (p (p' x')))) x' 539 else 0)) = 540 (\x'. (if x' IN s CROSS s' then 541 (\x'. x (FST x') * 542 measure m ((\(i,j). a i INTER b j) x')) x' 543 else 0))` by METIS_TAC [] 544 >> POP_ORW 545 >> RW_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 546 >> `!x'. (\j. x x' * measure m (a x' INTER b j)) = 547 (\x' j. x x' * measure m (a x' INTER b j)) x'` 548 by METIS_TAC [] 549 >> POP_ORW 550 >> (MP_TAC o Q.ISPECL [`s:num->bool`,`s':num->bool`]) REAL_SUM_IMAGE_REAL_SUM_IMAGE 551 >> RW_TAC std_ss [] 552 >> Suff `(\x'. x (FST x') * measure m (a (FST x') INTER b (SND x'))) = 553 (\x'. x (FST x') * measure m ((\(i,j). a i INTER b j) x'))` 554 >- RW_TAC std_ss [] 555 >> RW_TAC std_ss [FUN_EQ_THM] 556 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 557 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND]) 558 >> CONJ_TAC 559 >- (RW_TAC std_ss [pos_simple_fn_integral_def] >> FULL_SIMP_TAC std_ss [pos_simple_fn_def] 560 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s' :num -> bool)`) REAL_SUM_IMAGE_IN_IF] 561 >> `(\x. (if x IN s' then (\i. y i * measure m (b i)) x else 0)) = 562 (\x. (if x IN s' then (\i. y i * 563 SIGMA (\j. measure m (a j INTER b i)) s) x else 0))` 564 by (RW_TAC std_ss [FUN_EQ_THM] 565 >> RW_TAC std_ss [] 566 >> FULL_SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 567 >> (MP_TAC o Q.SPEC `b (x' :num)` o 568 UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 569 Q.SPECL 570 [`s`, `a`, `m`]) measure_split 571 >> RW_TAC std_ss [INTER_COMM]) 572 >> POP_ORW 573 >> `!(x:num) (i:num). y i * SIGMA (\j. measure m (a j INTER b i)) s = 574 SIGMA (\j. y i * measure m (a j INTER b i)) s` 575 by METIS_TAC [REAL_SUM_IMAGE_CMUL] 576 >> POP_ORW 577 >> `FINITE (s CROSS s')` by RW_TAC std_ss [FINITE_CROSS] 578 >> `INJ p' (s CROSS s') 579 (IMAGE p' (s CROSS s'))` 580 by METIS_TAC [INJ_IMAGE_BIJ, BIJ_DEF] 581 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `p'` o UNDISCH o 582 Q.ISPEC `((s:num->bool) CROSS (s':num->bool))` o 583 INST_TYPE [``:'b``|->``:num``]) REAL_SUM_IMAGE_IMAGE] 584 >> RW_TAC std_ss [o_DEF] 585 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(s :num -> bool)CROSS(s' :num -> bool)`) 586 REAL_SUM_IMAGE_IN_IF] 587 >> `(\x. (if x IN s CROSS s' then 588 (\x. y (SND (p (p' x))) * 589 measure m ((\(i,j). a i INTER b j) (p (p' x)))) x else 0)) = 590 (\x. (if x IN s CROSS s' then 591 (\x. y (SND x) * 592 measure m ((\(i,j). a i INTER b j) x)) x else 0))` by METIS_TAC [] 593 >> POP_ORW 594 >> RW_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 595 >> `!x. (\j. y x * measure m (a j INTER b x)) = 596 (\x j. y x * measure m (a j INTER b x)) x` 597 by METIS_TAC [] 598 >> POP_ORW 599 >> (MP_TAC o Q.ISPECL [`s':num->bool`,`s:num->bool`]) REAL_SUM_IMAGE_REAL_SUM_IMAGE 600 >> RW_TAC std_ss [] 601 >> `(s' CROSS s) = IMAGE (\x. (SND x, FST x)) (s CROSS s')` 602 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_CROSS, IN_IMAGE] 603 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 604 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 605 >> EQ_TAC 606 >- (STRIP_TAC >> Q.EXISTS_TAC `(r,q)` >> RW_TAC std_ss [FST,SND]) 607 >> RW_TAC std_ss [] >> RW_TAC std_ss []) 608 >> POP_ORW 609 >> `INJ (\x. (SND x,FST x)) (s CROSS s') 610 (IMAGE (\x. (SND x,FST x)) (s CROSS s'))` 611 by (RW_TAC std_ss [INJ_DEF, IN_CROSS, IN_IMAGE] 612 >- METIS_TAC [] 613 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 614 >> (MP_TAC o Q.ISPEC `x'':num#num`) pair_CASES 615 >> RW_TAC std_ss [] 616 >> FULL_SIMP_TAC std_ss [FST,SND]) 617 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `(\x. (SND x, FST x))` o UNDISCH o 618 Q.ISPEC `((s:num->bool) CROSS (s':num->bool))` o 619 INST_TYPE [``:'b``|->``:num#num``]) REAL_SUM_IMAGE_IMAGE] 620 >> RW_TAC std_ss [o_DEF] 621 >> Suff `(\x. y (SND x) * measure m (a (FST x) INTER b (SND x))) = 622 (\x. y (SND x) * measure m ((\(i,j). a i INTER b j) x))` 623 >- RW_TAC std_ss [] 624 >> RW_TAC std_ss [FUN_EQ_THM] 625 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 626 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND]) 627 >> CONJ_TAC 628 >- FULL_SIMP_TAC std_ss [IMAGE_FINITE, FINITE_CROSS, pos_simple_fn_def] 629 >> CONJ_TAC 630 >- (RW_TAC std_ss [DISJOINT_DEF, IN_IMAGE] 631 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY, IN_INTER] 632 >> FULL_SIMP_TAC std_ss [o_DEF] 633 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 634 >> (MP_TAC o Q.ISPEC `x'':num#num`) pair_CASES 635 >> RW_TAC std_ss [] 636 >> RW_TAC std_ss [] 637 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 638 >> FULL_SIMP_TAC std_ss [IN_INTER, IN_CROSS, FST, SND, pos_simple_fn_def, 639 DISJOINT_DEF] 640 >> METIS_TAC [EXTENSION, NOT_IN_EMPTY, IN_INTER]) 641 >> CONJ_TAC 642 >- (RW_TAC std_ss [IN_IMAGE] 643 >> FULL_SIMP_TAC std_ss [o_DEF] 644 >> (MP_TAC o Q.ISPEC `x':num#num`) pair_CASES 645 >> RW_TAC std_ss [] 646 >> FULL_SIMP_TAC std_ss [IN_CROSS, FST, SND, pos_simple_fn_def] 647 >> METIS_TAC [ALGEBRA_INTER, subsets_def, space_def, 648 sigma_algebra_def, measure_space_def]) 649 >> CONJ_TAC 650 >- (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_CROSS] 651 >> `!s'' x. (?x'. ((x = p' x') /\ FST x' IN s /\ SND x' IN s')) = 652 (?x1 x2. ((x = p' (x1,x2)) /\ x1 IN s /\ x2 IN s'))` 653 by METIS_TAC [PAIR, FST, SND] 654 >> POP_ORW 655 >> `!s''. (?x. (s'' = (\(i,j). a i INTER b j) (p x)) /\ 656 ?x1 x2. (x = p' (x1,x2)) /\ x1 IN s /\ x2 IN s') = 657 (?x1 x2. (s'' = (\(i,j). a i INTER b j) (p (p' (x1,x2)))) /\ 658 x1 IN s /\ x2 IN s')` 659 by METIS_TAC [] 660 >> POP_ORW 661 >> FULL_SIMP_TAC std_ss [o_DEF, IN_CROSS] 662 >> `!s''. (?x1 x2. (s'' = (\(i,j). a i INTER b j) (p (p' (x1,x2)))) /\ 663 x1 IN s /\ x2 IN s') = 664 (?x1 x2. (s'' = (\(i,j). a i INTER b j) (x1,x2)) /\ 665 x1 IN s /\ x2 IN s')` 666 by METIS_TAC [FST,SND] 667 >> POP_ORW 668 >> RW_TAC std_ss [] 669 >> Suff `(?x1 x2. x' IN a x1 INTER b x2 /\ x1 IN s /\ x2 IN s') = 670 x' IN m_space m` 671 >- METIS_TAC [] 672 >> RW_TAC std_ss [IN_INTER] 673 >> FULL_SIMP_TAC std_ss [pos_simple_fn_def] 674 >> `m_space m = (BIGUNION (IMAGE a s)) INTER (BIGUNION (IMAGE b s'))` 675 by METIS_TAC [INTER_IDEMPOT] 676 >> POP_ORW 677 >> Q.PAT_X_ASSUM `BIGUNION (IMAGE b s') = m_space m` (K ALL_TAC) 678 >> Q.PAT_X_ASSUM `BIGUNION (IMAGE a s) = m_space m` (K ALL_TAC) 679 >> RW_TAC std_ss [IN_INTER, IN_BIGUNION, IN_IMAGE] 680 >> METIS_TAC []) 681 >> FULL_SIMP_TAC std_ss [o_DEF, pos_simple_fn_def]); 682 683 684val psfis_present = store_thm 685 ("psfis_present", 686 ``!m f g a b. 687 measure_space m /\ 688 a IN psfis m f /\ b IN psfis m g ==> 689 (?(z:num->real) (z':num->real) c (k:num->bool). 690 (!t. t IN m_space m ==> (f t = SIGMA (\i. (z i) * (indicator_fn (c i) t)) k)) /\ 691 (!t. t IN m_space m ==> (g t = SIGMA (\i. (z' i) * (indicator_fn (c i) t)) k)) /\ 692 (a = pos_simple_fn_integral m k c z) /\ 693 (b = pos_simple_fn_integral m k c z') /\ 694 FINITE k /\ 695 (!i j. i IN k /\ j IN k /\ (~(i=j)) ==> DISJOINT (c i) (c j)) /\ 696 (!i. i IN k ==> c i IN measurable_sets m) /\ 697 (BIGUNION (IMAGE c k) = m_space m) /\ 698 (!i. 0 <= z i) /\ (!i. 0 <= z' i))``, 699 RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 700 >> (MP_TAC o Q.ISPEC `(x' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 701 pair_CASES 702 >> (MP_TAC o Q.ISPEC `(x :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 703 pair_CASES 704 >> (MP_TAC o Q.ISPEC `(x'' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) pair_CASES 705 >> (MP_TAC o Q.ISPEC `(x''' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 706 pair_CASES 707 >> RW_TAC std_ss [] 708 >> (MP_TAC o Q.ISPEC `(r' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 709 >> (MP_TAC o Q.ISPEC `(r :(num -> 'a -> bool) # (num -> real))`) pair_CASES 710 >> (MP_TAC o Q.ISPEC `(r'' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 711 >> (MP_TAC o Q.ISPEC `(r''' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 712 >> RW_TAC std_ss [] 713 >> FULL_SIMP_TAC std_ss [PAIR_EQ] 714 >> MATCH_MP_TAC pos_simple_fn_integral_present 715 >> METIS_TAC []); 716 717 718val pos_simple_fn_integral_add = store_thm 719 ("pos_simple_fn_integral_add", 720 ``!m f (s:num->bool) a (x:num->real) 721 g (s':num->bool) b (y:num->real). 722 measure_space m /\ 723 pos_simple_fn m f s a x /\ pos_simple_fn m g s' b y ==> 724 ?s'' c z. pos_simple_fn m (\x. f x + g x) s'' c z /\ 725 (pos_simple_fn_integral m s a x + 726 pos_simple_fn_integral m s' b y = 727 pos_simple_fn_integral m s'' c z)``, 728 REPEAT STRIP_TAC 729 >> (MP_TAC o Q.SPECL [`m`,`f`,`s`,`a`,`x`,`g`,`s'`,`b`,`y`]) pos_simple_fn_integral_present 730 >> RW_TAC std_ss [] >> ASM_SIMP_TAC std_ss [] 731 >> Q.EXISTS_TAC `k` >> Q.EXISTS_TAC `c` >> Q.EXISTS_TAC `(\i. z i + z' i)` 732 >> FULL_SIMP_TAC std_ss [pos_simple_fn_def, pos_simple_fn_integral_def] 733 >> REVERSE CONJ_TAC 734 >- (RW_TAC std_ss [GSYM REAL_SUM_IMAGE_ADD] 735 >> `!i. z i * measure m (c i) + z' i * measure m (c i) = 736 (z i + z' i) * measure m (c i)` 737 by (STRIP_TAC >> REAL_ARITH_TAC) 738 >> RW_TAC std_ss []) 739 >> CONJ_TAC >- RW_TAC std_ss [REAL_LE_ADD] 740 >> REVERSE CONJ_TAC 741 >- RW_TAC std_ss [REAL_LE_ADD] 742 >> REPEAT STRIP_TAC 743 >> `SIGMA (\i. x i * indicator_fn (a i) x') s = 744 SIGMA (\i. z i * indicator_fn (c i) x') k` by METIS_TAC [] 745 >> POP_ORW 746 >> `SIGMA (\i. y i * indicator_fn (b i) x') s' = 747 SIGMA (\i. z' i * indicator_fn (c i) x') k` by METIS_TAC [] 748 >> POP_ORW 749 >> RW_TAC std_ss [GSYM REAL_SUM_IMAGE_ADD] 750 >> `!i. z i * indicator_fn (c i) x' + z' i * indicator_fn (c i) x' = 751 (z i + z' i) * indicator_fn (c i) x'` 752 by (REPEAT STRIP_TAC >> REAL_ARITH_TAC) 753 >> RW_TAC std_ss []); 754 755 756val psfis_add = store_thm 757 ("psfis_add", 758 ``!m f g a b. 759 measure_space m /\ 760 a IN psfis m f /\ b IN psfis m g ==> 761 a + b IN psfis m (\x. f x + g x)``, 762 RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 763 >> (MP_TAC o Q.ISPEC `(x' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 764 pair_CASES 765 >> (MP_TAC o Q.ISPEC `(x :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 766 pair_CASES 767 >> (MP_TAC o Q.ISPEC `(x'' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) pair_CASES 768 >> (MP_TAC o Q.ISPEC `(x''' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 769 pair_CASES 770 >> RW_TAC std_ss [] 771 >> (MP_TAC o Q.ISPEC `(r' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 772 >> (MP_TAC o Q.ISPEC `(r :(num -> 'a -> bool) # (num -> real))`) pair_CASES 773 >> (MP_TAC o Q.ISPEC `(r'' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 774 >> (MP_TAC o Q.ISPEC `(r''' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 775 >> RW_TAC std_ss [] 776 >> FULL_SIMP_TAC std_ss [PAIR_EQ] 777 >> Suff `?s a x. (pos_simple_fn_integral m q''' q'''' r'''' + 778 pos_simple_fn_integral m q q'''''' r'''''' = 779 pos_simple_fn_integral m s a x) /\ 780 pos_simple_fn m (\x. f x + g x) s a x` 781 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `(s,a,x)` 782 >> RW_TAC std_ss [] >> Q.EXISTS_TAC `(s,a,x)` 783 >> RW_TAC std_ss [PAIR_EQ]) 784 >> ONCE_REWRITE_TAC [CONJ_COMM] 785 >> MATCH_MP_TAC pos_simple_fn_integral_add >> RW_TAC std_ss []); 786 787 788val pos_simple_fn_integral_mono = store_thm 789 ("pos_simple_fn_integral_mono", 790 ``!m f (s:num->bool) a (x:num->real) 791 g (s':num->bool) b (y:num->real). 792 measure_space m /\ 793 pos_simple_fn m f s a x /\ pos_simple_fn m g s' b y /\ 794 (!x. f x <= g x) ==> 795 pos_simple_fn_integral m s a x <= pos_simple_fn_integral m s' b y``, 796 REPEAT STRIP_TAC 797 >> (MP_TAC o Q.SPECL [`m`,`f`,`s`,`a`,`x`,`g`,`s'`,`b`,`y`]) pos_simple_fn_integral_present 798 >> RW_TAC std_ss [] >> ASM_SIMP_TAC std_ss [] 799 >> RW_TAC std_ss [pos_simple_fn_integral_def] 800 >> (MATCH_MP_TAC o UNDISCH o Q.ISPEC `k:num->bool`) REAL_SUM_IMAGE_MONO 801 >> RW_TAC std_ss [] 802 >> Cases_on `c x' = {}` 803 >- RW_TAC real_ss [MEASURE_EMPTY] 804 >> `!x. x IN m_space m ==> 805 SIGMA (\i. z i * indicator_fn (c i) x) k <= 806 SIGMA (\i. z' i * indicator_fn (c i) x) k` 807 by METIS_TAC [] 808 >> `?t ss. (c x' = t INSERT ss) /\ ~(t IN ss)` 809 by METIS_TAC [SET_CASES] 810 >> Q.PAT_X_ASSUM `!x. x IN m_space m ==> SIGMA (\i. z i * indicator_fn (c i) x) k <= 811 SIGMA (\i. z' i * indicator_fn (c i) x) k` 812 (MP_TAC o Q.SPEC `t`) 813 >> `k = x' INSERT (k DELETE x')` 814 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INSERT, IN_DELETE] >> METIS_TAC []) 815 >> POP_ORW 816 >> ASM_SIMP_TAC std_ss [REAL_SUM_IMAGE_THM, FINITE_INSERT, FINITE_DELETE, DELETE_DELETE] 817 >> `FINITE (k DELETE x')` by RW_TAC std_ss [FINITE_DELETE] 818 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(k :num -> bool)DELETE x'`) 819 REAL_SUM_IMAGE_IN_IF] 820 >> `(\x. (if x IN k DELETE x' then (\i. z i * indicator_fn (c i) t) x else 0)) = 821 (\x. 0)` 822 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_DELETE, indicator_fn_def] 823 >> Q.PAT_X_ASSUM 824 `!i j. i IN k /\ j IN k /\ ~(i = j) ==> DISJOINT (c i) (c j)` 825 (MP_TAC o UNDISCH_ALL o 826 REWRITE_RULE [GSYM AND_IMP_INTRO] o Q.SPECL [`x''`, `x'`]) 827 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, IN_INTER, IN_INSERT] 828 >> METIS_TAC []) 829 >> POP_ORW 830 >> `(\x. (if x IN k DELETE x' then (\i. z' i * indicator_fn (c i) t) x else 0)) = 831 (\x. 0)` 832 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_DELETE, indicator_fn_def] 833 >> Q.PAT_X_ASSUM 834 `!i j. i IN k /\ j IN k /\ ~(i = j) ==> DISJOINT (c i) (c j)` 835 (MP_TAC o UNDISCH_ALL o 836 REWRITE_RULE [GSYM AND_IMP_INTRO] o Q.SPECL [`x''`, `x'`]) 837 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, IN_INTER, IN_INSERT] 838 >> METIS_TAC []) 839 >> POP_ORW 840 >> Know `t IN BIGUNION (IMAGE c k)` 841 >- (RW_TAC std_ss [IN_BIGUNION, IN_IMAGE] >> METIS_TAC [IN_INSERT]) 842 >> (MP_TAC o Q.SPECL [`(\x.0)`,`0`] o UNDISCH o Q.ISPEC `(k :num -> bool)DELETE x'`) 843 REAL_SUM_IMAGE_FINITE_CONST 844 >> RW_TAC real_ss [indicator_fn_def, IN_INSERT] 845 >> METIS_TAC [REAL_LE_MUL2, measure_space_def, positive_def, REAL_LE_REFL]); 846 847 848 849val pos_simple_fn_integral_mono_on_mspace = store_thm 850 ("pos_simple_fn_integral_mono_on_mspace", 851 ``!m f (s:num->bool) a (x:num->real) 852 g (s':num->bool) b (y:num->real). 853 measure_space m /\ 854 pos_simple_fn m f s a x /\ pos_simple_fn m g s' b y /\ 855 (!x. x IN m_space m ==> f x <= g x) ==> 856 pos_simple_fn_integral m s a x <= pos_simple_fn_integral m s' b y``, 857 REPEAT STRIP_TAC 858 >> (MP_TAC o Q.SPECL [`m`,`f`,`s`,`a`,`x`,`g`,`s'`,`b`,`y`]) pos_simple_fn_integral_present 859 >> RW_TAC std_ss [] >> ASM_SIMP_TAC std_ss [] 860 >> RW_TAC std_ss [pos_simple_fn_integral_def] 861 >> (MATCH_MP_TAC o UNDISCH o Q.ISPEC `k:num->bool`) REAL_SUM_IMAGE_MONO 862 >> RW_TAC std_ss [] 863 >> Cases_on `c x' = {}` 864 >- RW_TAC real_ss [MEASURE_EMPTY] 865 >> `!x. x IN m_space m ==> 866 SIGMA (\i. z i * indicator_fn (c i) x) k <= 867 SIGMA (\i. z' i * indicator_fn (c i) x) k` 868 by METIS_TAC [] 869 >> `?t ss. (c x' = t INSERT ss) /\ ~(t IN ss)` 870 by METIS_TAC [SET_CASES] 871 >> Q.PAT_X_ASSUM `!x. x IN m_space m ==> SIGMA (\i. z i * indicator_fn (c i) x) k <= 872 SIGMA (\i. z' i * indicator_fn (c i) x) k` 873 (MP_TAC o Q.SPEC `t`) 874 >> `k = x' INSERT (k DELETE x')` 875 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INSERT, IN_DELETE] >> METIS_TAC []) 876 >> POP_ORW 877 >> ASM_SIMP_TAC std_ss [REAL_SUM_IMAGE_THM, FINITE_INSERT, FINITE_DELETE, DELETE_DELETE] 878 >> `FINITE (k DELETE x')` by RW_TAC std_ss [FINITE_DELETE] 879 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(k :num -> bool)DELETE x'`) 880 REAL_SUM_IMAGE_IN_IF] 881 >> `(\x. (if x IN k DELETE x' then (\i. z i * indicator_fn (c i) t) x else 0)) = 882 (\x. 0)` 883 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_DELETE, indicator_fn_def] 884 >> Q.PAT_X_ASSUM 885 `!i j. i IN k /\ j IN k /\ ~(i = j) ==> DISJOINT (c i) (c j)` 886 (MP_TAC o UNDISCH_ALL o 887 REWRITE_RULE [GSYM AND_IMP_INTRO] o Q.SPECL [`x''`, `x'`]) 888 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, IN_INTER, IN_INSERT] 889 >> METIS_TAC []) 890 >> POP_ORW 891 >> `(\x. (if x IN k DELETE x' then (\i. z' i * indicator_fn (c i) t) x else 0)) = 892 (\x. 0)` 893 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_DELETE, indicator_fn_def] 894 >> Q.PAT_X_ASSUM 895 `!i j. i IN k /\ j IN k /\ ~(i = j) ==> DISJOINT (c i) (c j)` 896 (MP_TAC o UNDISCH_ALL o 897 REWRITE_RULE [GSYM AND_IMP_INTRO] o Q.SPECL [`x''`, `x'`]) 898 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, IN_INTER, IN_INSERT] 899 >> METIS_TAC []) 900 >> POP_ORW 901 >> Know `t IN BIGUNION (IMAGE c k)` 902 >- (RW_TAC std_ss [IN_BIGUNION, IN_IMAGE] >> METIS_TAC [IN_INSERT]) 903 >> (MP_TAC o Q.SPECL [`(\x.0)`,`0`] o UNDISCH o Q.ISPEC `(k :num -> bool)DELETE x'`) 904 REAL_SUM_IMAGE_FINITE_CONST 905 >> RW_TAC real_ss [indicator_fn_def, IN_INSERT] 906 >> METIS_TAC [REAL_LE_MUL2, measure_space_def, positive_def, REAL_LE_REFL]); 907 908 909 910val psfis_mono = store_thm 911 ("psfis_mono", 912 ``!m f g a b. 913 measure_space m /\ 914 a IN psfis m f /\ b IN psfis m g /\ 915 (!x. x IN m_space m ==> f x <= g x) ==> 916 a <= b``, 917 RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 918 >> (MP_TAC o Q.ISPEC `(x' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 919 pair_CASES 920 >> (MP_TAC o Q.ISPEC `(x :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 921 pair_CASES 922 >> (MP_TAC o Q.ISPEC `(x'' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) pair_CASES 923 >> (MP_TAC o Q.ISPEC `(x''' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 924 pair_CASES 925 >> RW_TAC std_ss [] 926 >> (MP_TAC o Q.ISPEC `(r' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 927 >> (MP_TAC o Q.ISPEC `(r :(num -> 'a -> bool) # (num -> real))`) pair_CASES 928 >> (MP_TAC o Q.ISPEC `(r'' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 929 >> (MP_TAC o Q.ISPEC `(r''' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 930 >> RW_TAC std_ss [] 931 >> FULL_SIMP_TAC std_ss [PAIR_EQ] 932 >> MATCH_MP_TAC pos_simple_fn_integral_mono_on_mspace 933 >> METIS_TAC []); 934 935 936val pos_simple_fn_integral_unique = store_thm 937 ("pos_simple_fn_integral_unique", 938 ``!m f (s:num->bool) a (x:num->real) 939 (s':num->bool) b (y:num->real). 940 measure_space m /\ 941 pos_simple_fn m f s a x /\ pos_simple_fn m f s' b y ==> 942 (pos_simple_fn_integral m s a x = pos_simple_fn_integral m s' b y)``, 943 METIS_TAC [REAL_LE_ANTISYM, REAL_LE_REFL, pos_simple_fn_integral_mono]); 944 945 946val psfis_unique = store_thm 947 ("psfis_unique", 948 ``!m f a b. 949 measure_space m /\ 950 a IN psfis m f /\ b IN psfis m f ==> 951 (a = b)``, 952 METIS_TAC [REAL_LE_ANTISYM, REAL_LE_REFL, psfis_mono]); 953 954 955val pos_simple_fn_integral_indicator = store_thm 956 ("pos_simple_fn_integral_indicator", 957 ``!m A. 958 measure_space m /\ A IN measurable_sets m ==> 959 (?s a x. pos_simple_fn m (indicator_fn A) s a x /\ 960 (pos_simple_fn_integral m s a x = measure m A))``, 961 RW_TAC std_ss [pos_simple_fn_integral_def, pos_simple_fn_def] 962 >> `!x. x IN A ==> x IN m_space m` 963 by METIS_TAC [measure_space_def, sigma_algebra_def, algebra_def, 964 subset_class_def, subsets_def, space_def, SUBSET_DEF] 965 >> `m_space m DIFF A IN measurable_sets m` 966 by METIS_TAC [measure_space_def, sigma_algebra_def, ALGEBRA_COMPL, 967 subsets_def, space_def] 968 >> `{1:num} DELETE 0 = {1}` 969 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_SING, IN_DELETE]) 970 >> `IMAGE (\i:num. (if i = 0 then A else m_space m DIFF A)) {0; 1} = 971 {A; m_space m DIFF A}` 972 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_INSERT, IN_SING, IN_IMAGE] 973 >> METIS_TAC [DECIDE ``~(1:num = 0)``]) 974 >> Q.EXISTS_TAC `{0;1}` 975 >> Q.EXISTS_TAC `\i. if i = 0 then A else m_space m DIFF A` 976 >> Q.EXISTS_TAC `\i. if i = 0 then 1 else 0` 977 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, IN_DISJOINT, IN_DIFF, FINITE_INSERT, FINITE_SING, 978 IN_INSERT, IN_SING, REAL_SUM_IMAGE_SING, BIGUNION_PAIR, EXTENSION, 979 IN_UNION, IN_DIFF, indicator_fn_def] 980 >> METIS_TAC []); 981 982 983val psfis_indicator = store_thm 984 ("psfis_indicator", 985 ``!m A. measure_space m /\ A IN measurable_sets m ==> 986 measure m A IN psfis m (indicator_fn A)``, 987 RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 988 >> (MP_TAC o Q.ISPEC `(x' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 989 pair_CASES 990 >> (MP_TAC o Q.ISPEC `(x :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 991 pair_CASES 992 >> (MP_TAC o Q.ISPEC `(x'' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) pair_CASES 993 >> (MP_TAC o Q.ISPEC `(x''' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 994 pair_CASES 995 >> RW_TAC std_ss [] 996 >> (MP_TAC o Q.ISPEC `(r' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 997 >> (MP_TAC o Q.ISPEC `(r :(num -> 'a -> bool) # (num -> real))`) pair_CASES 998 >> (MP_TAC o Q.ISPEC `(r'' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 999 >> (MP_TAC o Q.ISPEC `(r''' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 1000 >> RW_TAC std_ss [] 1001 >> Suff `?s a x. pos_simple_fn m (indicator_fn A) s a x /\ 1002 (pos_simple_fn_integral m s a x = measure m A)` 1003 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `(s,a,x)` 1004 >> RW_TAC std_ss [] >> Q.EXISTS_TAC `(s,a,x)` 1005 >> RW_TAC std_ss [PAIR_EQ]) 1006 >> MATCH_MP_TAC pos_simple_fn_integral_indicator 1007 >> ASM_REWRITE_TAC []); 1008 1009 1010val pos_simple_fn_integral_mult = store_thm 1011 ("pos_simple_fn_integral_mult", 1012 ``!m f s a x. 1013 measure_space m /\ pos_simple_fn m f s a x ==> 1014 (!z. 0 <= z ==> 1015 ?s' b y. 1016 pos_simple_fn m (\x. z * f x) s' b y /\ 1017 (pos_simple_fn_integral m s' b y = 1018 z * pos_simple_fn_integral m s a x))``, 1019 RW_TAC std_ss [pos_simple_fn_integral_def, pos_simple_fn_def] 1020 >> Q.EXISTS_TAC `s` >> Q.EXISTS_TAC `a` >> Q.EXISTS_TAC `(\i. z * x i)` 1021 >> RW_TAC real_ss [GSYM REAL_SUM_IMAGE_CMUL, REAL_LE_MUL, REAL_MUL_ASSOC]); 1022 1023 1024 val psfis_mult = store_thm 1025 ("psfis_mult", 1026 ``!m f a. measure_space m /\ a IN psfis m f ==> 1027 (!z. 0 <= z ==> 1028 z * a IN psfis m (\x. z * f x))``, 1029 RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 1030 >> (MP_TAC o Q.ISPEC `(x' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 1031 pair_CASES 1032 >> (MP_TAC o Q.ISPEC `(x :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 1033 pair_CASES 1034 >> (MP_TAC o Q.ISPEC `(x'' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) pair_CASES 1035 >> (MP_TAC o Q.ISPEC `(x''' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 1036 pair_CASES 1037 >> RW_TAC std_ss [] 1038 >> (MP_TAC o Q.ISPEC `(r' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 1039 >> (MP_TAC o Q.ISPEC `(r :(num -> 'a -> bool) # (num -> real))`) pair_CASES 1040 >> (MP_TAC o Q.ISPEC `(r'' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 1041 >> (MP_TAC o Q.ISPEC `(r''' :(num -> 'a -> bool) # (num -> real))`) pair_CASES 1042 >> RW_TAC std_ss [] 1043 >> FULL_SIMP_TAC std_ss [PAIR_EQ] 1044 >> Suff `?s a x. pos_simple_fn m (\x. z * f x) s a x /\ 1045 (pos_simple_fn_integral m s a x = 1046 z * pos_simple_fn_integral m q''' q r'''')` 1047 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `(s,a,x)` 1048 >> RW_TAC std_ss [] >> Q.EXISTS_TAC `(s,a,x)` 1049 >> RW_TAC std_ss [PAIR_EQ]) 1050 >> METIS_TAC [pos_simple_fn_integral_mult]); 1051 1052 1053val pos_simple_fn_integral_REAL_SUM_IMAGE = store_thm 1054 ("pos_simple_fn_integral_REAL_SUM_IMAGE", 1055 ``!m f s a x P. 1056 measure_space m /\ 1057 (!i. i IN P ==> pos_simple_fn m (f i) (s i) (a i) (x i)) /\ 1058 FINITE P ==> 1059 (?s' a' x'. pos_simple_fn m (\t. SIGMA (\i. f i t) P) s' a' x' /\ 1060 (pos_simple_fn_integral m s' a' x' = 1061 SIGMA (\i. pos_simple_fn_integral m (s i) (a i) (x i)) P))``, 1062 Suff `!P:'b->bool. FINITE P ==> 1063 (\P:'b->bool. !(m :('a -> bool) # (('a -> bool) -> bool) # (('a -> bool) -> real)) 1064 (f :'b -> 'a -> real) (s :'b -> num -> bool) 1065 (a :'b -> num -> 'a -> bool) (x :'b -> num -> real). 1066 measure_space m /\ 1067 (!i:'b. i IN P ==> pos_simple_fn m (f i) (s i) (a i) (x i)) ==> 1068 (?(s' :num -> bool) (a' :num -> 'a -> bool) (x' :num -> real). 1069 pos_simple_fn m (\t. SIGMA (\i. f i t) P) s' a' x' /\ 1070 (pos_simple_fn_integral m s' a' x' = 1071 SIGMA (\i. pos_simple_fn_integral m (s i) (a i) (x i)) P))) P` 1072 >- METIS_TAC [] 1073 >> MATCH_MP_TAC FINITE_INDUCT 1074 >> RW_TAC std_ss [NOT_IN_EMPTY, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT] 1075 >- ((MP_TAC o Q.SPECL [`m`,`{}`]) pos_simple_fn_integral_indicator 1076 >> SIMP_TAC std_ss [MEASURE_EMPTY, indicator_fn_def, NOT_IN_EMPTY] 1077 >> METIS_TAC [measure_space_def, sigma_algebra_def, 1078 ALGEBRA_EMPTY, subsets_def, space_def]) 1079 >> Q.PAT_X_ASSUM `!m f s' a x. M` 1080 (MP_TAC o Q.SPECL [`m`,`f`,`s'`,`a`,`x`]) 1081 >> RW_TAC std_ss [] 1082 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [GSYM thm]) 1083 >> `!s''' a'' x''. (\t. f e t + SIGMA (\i. f i t) s) = 1084 (\t. f e t + (\t. SIGMA (\i. f i t) s) t)` 1085 by METIS_TAC [] 1086 >> POP_ORW 1087 >> MATCH_MP_TAC (GSYM pos_simple_fn_integral_add) 1088 >> RW_TAC std_ss []); 1089 1090 1091val psfis_REAL_SUM_IMAGE = store_thm 1092 ("psfis_REAL_SUM_IMAGE", 1093 ``!m f a P. 1094 measure_space m /\ 1095 (!i. i IN P ==> a i IN psfis m (f i)) /\ 1096 FINITE P ==> 1097 (SIGMA a P) IN psfis m (\t. SIGMA (\i. f i t) P)``, 1098 Suff `!P:'b->bool. FINITE P ==> 1099 (\P:'b->bool. !(m :('a -> bool) # (('a -> bool) -> bool) # (('a -> bool) -> real)) 1100 (f :'b -> 'a -> real) (a :'b -> real). 1101 measure_space m /\ (!(i :'b). i IN P ==> a i IN psfis m (f i)) ==> 1102 SIGMA a P IN 1103 psfis m (\(t :'a). SIGMA (\(i :'b). f i t) P)) P` 1104 >- RW_TAC std_ss [] 1105 >> MATCH_MP_TAC FINITE_INDUCT 1106 >> RW_TAC std_ss [NOT_IN_EMPTY, REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT] 1107 >- ((MP_TAC o Q.SPECL [`m`,`{}`]) psfis_indicator 1108 >> SIMP_TAC std_ss [MEASURE_EMPTY, indicator_fn_def, NOT_IN_EMPTY] 1109 >> METIS_TAC [measure_space_def, sigma_algebra_def, 1110 ALGEBRA_EMPTY, subsets_def, space_def]) 1111 >> Q.PAT_X_ASSUM `!m f a. M` 1112 (MP_TAC o Q.SPECL [`m`,`f`,`a`]) 1113 >> RW_TAC std_ss [] 1114 >> `(\t. f e t + SIGMA (\i. f i t) s) = 1115 (\t. f e t + (\t. SIGMA (\i. f i t) s) t)` 1116 by METIS_TAC [] 1117 >> POP_ORW 1118 >> MATCH_MP_TAC psfis_add 1119 >> RW_TAC std_ss []); 1120 1121 1122val psfis_intro = store_thm 1123 ("psfis_intro", 1124 ``!m a x P. 1125 measure_space m /\ (!i. i IN P ==> a i IN measurable_sets m) /\ 1126 (!i. 0 <= x i) /\ FINITE P ==> 1127 (SIGMA (\i. x i * measure m (a i)) P) IN 1128 psfis m (\t. SIGMA (\i. x i * indicator_fn (a i) t) P)``, 1129 RW_TAC std_ss [] 1130 >> `!t. (\i. x i * indicator_fn (a i) t) = 1131 (\i. (\i t. x i * indicator_fn (a i) t) i t)` 1132 by METIS_TAC [] 1133 >> POP_ORW 1134 >> MATCH_MP_TAC psfis_REAL_SUM_IMAGE 1135 >> RW_TAC std_ss [] 1136 >> METIS_TAC [psfis_mult, psfis_indicator]); 1137 1138 1139val psfis_nonneg = store_thm 1140 ("psfis_nonneg", 1141 ``!m f a. a IN psfis m f ==> nonneg f``, 1142 RW_TAC std_ss [nonneg_def, psfis_def, IN_IMAGE, psfs_def, 1143 GSPECIFICATION] 1144 >> (MP_TAC o Q.ISPEC `(x' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 1145 pair_CASES 1146 >> RW_TAC std_ss [] 1147 >> (MP_TAC o Q.ISPEC `(r :(num -> 'a -> bool) # (num -> real))`) pair_CASES 1148 >> RW_TAC std_ss [] 1149 >> FULL_SIMP_TAC std_ss [PAIR_EQ, pos_simple_fn_def]); 1150 1151val mono_increasing_converges_to_sup = store_thm 1152 ("mono_increasing_converges_to_sup", 1153 ``!f r. (!i. 0 <= f i) /\ 1154 mono_increasing f /\ 1155 f --> r ==> 1156 (r = sup (IMAGE f UNIV))``, 1157 RW_TAC std_ss [mono_increasing_def] 1158 >> Suff `f --> sup (IMAGE f UNIV)` 1159 >- METIS_TAC [SEQ_UNIQ] 1160 >> RW_TAC std_ss [SEQ] 1161 >> (MP_TAC o Q.ISPECL [`IMAGE (f:num->real) UNIV`,`e:real/2`]) SUP_EPSILON 1162 >> SIMP_TAC std_ss [REAL_LT_HALF1] 1163 >> `!y x z. IMAGE f UNIV x = x IN IMAGE f UNIV` by RW_TAC std_ss [IN_DEF] 1164 >> POP_ORW 1165 >> Know `(?z. !x. x IN IMAGE f UNIV ==> x <= z)` 1166 >- (Q.EXISTS_TAC `r` >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1167 >> MATCH_MP_TAC SEQ_MONO_LE 1168 >> RW_TAC std_ss [DECIDE ``!n:num. n <= n + 1``]) 1169 >> SIMP_TAC std_ss [] >> STRIP_TAC >> POP_ASSUM (K ALL_TAC) 1170 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV, GSYM ABS_BETWEEN, GREATER_EQ] 1171 >> Q.EXISTS_TAC `x'` 1172 >> RW_TAC std_ss [REAL_LT_SUB_RADD] 1173 >- (MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f x' + e / 2` 1174 >> RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LET_TRANS 1175 >> Q.EXISTS_TAC `f n + e / 2` >> RW_TAC std_ss [REAL_LE_ADD2, REAL_LE_REFL] 1176 >> MATCH_MP_TAC REAL_LT_IADD >> RW_TAC std_ss [REAL_LT_HALF2]) 1177 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `sup (IMAGE f UNIV)` 1178 >> RW_TAC std_ss [REAL_LT_ADDR] 1179 >> Suff `!y. (\y. y IN IMAGE f UNIV) y ==> y <= sup (IMAGE f UNIV)` 1180 >- METIS_TAC [IN_IMAGE, IN_UNIV] 1181 >> SIMP_TAC std_ss [IN_DEF] 1182 >> MATCH_MP_TAC REAL_SUP_UBOUND_LE 1183 >> `!y x z. IMAGE f UNIV x = x IN IMAGE f UNIV` by RW_TAC std_ss [IN_DEF] 1184 >> POP_ORW 1185 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1186 >> Q.EXISTS_TAC `r` 1187 >> RW_TAC std_ss [] 1188 >> MATCH_MP_TAC SEQ_MONO_LE 1189 >> RW_TAC std_ss [DECIDE ``!n:num. n <= n + 1``]); 1190 1191 1192val IN_psfis = store_thm 1193 ("IN_psfis", 1194 ``!m r f. r IN psfis m f ==> 1195 ?s a x. pos_simple_fn m f s a x /\ 1196 (r = pos_simple_fn_integral m s a x)``, 1197 RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 1198 >> (MP_TAC o Q.ISPEC `(x' :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 1199 pair_CASES 1200 >> RW_TAC std_ss [] 1201 >> (MP_TAC o Q.ISPEC `(x :(num -> bool) # (num -> 'a -> bool) # (num -> real))`) 1202 pair_CASES 1203 >> RW_TAC std_ss [] 1204 >> (MP_TAC o Q.ISPEC `(r :(num -> 'a -> bool) # (num -> real))`) 1205 pair_CASES 1206 >> RW_TAC std_ss [] 1207 >> (MP_TAC o Q.ISPEC `(r' :(num -> 'a -> bool) # (num -> real))`) 1208 pair_CASES 1209 >> RW_TAC std_ss [] 1210 >> FULL_SIMP_TAC std_ss [PAIR_EQ] 1211 >> METIS_TAC []); 1212 1213 1214val pos_psfis = store_thm 1215 ("pos_psfis", 1216 ``!r m f. measure_space m /\ 1217 r IN psfis m f ==> 1218 0 <= r``, 1219 REPEAT STRIP_TAC 1220 >> `positive m` by FULL_SIMP_TAC std_ss [measure_space_def] 1221 >> `?s a x. pos_simple_fn m f s a x /\ 1222 (r = pos_simple_fn_integral m s a x)` 1223 by METIS_TAC [IN_psfis] 1224 >> RW_TAC std_ss [pos_simple_fn_integral_def] >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 1225 >> FULL_SIMP_TAC std_ss [pos_simple_fn_def, positive_def, REAL_LE_MUL]); 1226 1227 1228val f_plus_minus = lemma 1229 (``!f x. f x = pos_part f x - neg_part f x``, 1230 RW_TAC real_ss [pos_part_def, neg_part_def] 1231 >> REAL_ARITH_TAC); 1232 1233 1234val f_plus_minus2 = lemma 1235 (``!f. f = (\x. pos_part f x - neg_part f x)``, 1236 RW_TAC std_ss [GSYM f_plus_minus, ETA_THM]); 1237 1238 1239val f_abs_plus_minus = lemma 1240 (``!f x. abs (f x) = pos_part f x + neg_part f x``, 1241 RW_TAC std_ss [abs, pos_part_def, neg_part_def] 1242 >> REAL_ARITH_TAC); 1243 1244 1245val nonneg_pos_part_neg_part = lemma 1246 (``!f. nonneg f ==> 1247 (pos_part f = f) /\ (neg_part f = (\x. 0))``, 1248 RW_TAC std_ss [nonneg_def, pos_part_def, neg_part_def, ETA_THM]); 1249 1250 1251val pos_pos_part_neg_part_help = lemma 1252 (``!x. 0 <= f x ==> (pos_part f x = f x) /\ (neg_part f x = 0)``, 1253 RW_TAC std_ss [pos_part_def, neg_part_def]); 1254 1255 1256val real_neg_pos_part_neg_part_help = lemma 1257 (``!x. f x <= 0 ==> (neg_part f x = ~ f x) /\ (pos_part f x = 0)``, 1258 RW_TAC std_ss [pos_part_def, neg_part_def] >> METIS_TAC [REAL_LE_ANTISYM, REAL_NEG_EQ0]); 1259 1260 1261val real_neg_pos_part_neg_part = lemma 1262 (``!f. (!x. f x <= 0) ==> 1263 (neg_part f = (\x. ~ f x)) /\ (pos_part f = (\x. 0))``, 1264 RW_TAC std_ss [real_neg_pos_part_neg_part_help, FUN_EQ_THM]); 1265 1266 1267val real_pos_part_neg_part_pos_times = lemma 1268 (``!a. 0 <= a ==> (pos_part (\x. a * f x) = (\x. a * pos_part f x)) /\ 1269 (neg_part (\x. a * f x) = (\x. a * neg_part f x))``, 1270 RW_TAC std_ss [pos_part_def, neg_part_def, FUN_EQ_THM] 1271 >> ( REVERSE (RW_TAC real_ss [REAL_ENTIRE, REAL_NEG_EQ0]) 1272 >- METIS_TAC [REAL_LE_MUL] 1273 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1274 >> `0 < a * f x` by METIS_TAC [REAL_LE_LT, REAL_ENTIRE] 1275 >> METIS_TAC [real_lt, REAL_LE_LT, REAL_LT_LMUL_0] ) ); 1276 1277 1278val real_pos_part_neg_part_neg_times = lemma 1279 (``!a. a <= 0 ==> (pos_part (\x. a * f x) = (\x. ~a * neg_part f x)) /\ 1280 (neg_part (\x. a * f x) = (\x. ~a * pos_part f x))``, 1281 RW_TAC std_ss [pos_part_def, neg_part_def, FUN_EQ_THM] 1282 >> ( RW_TAC real_ss [REAL_ENTIRE, REAL_NEG_EQ0] 1283 >- METIS_TAC [REAL_LT_RMUL_0, REAL_LT_LE, REAL_ENTIRE, real_lt, REAL_NEG_EQ0] 1284 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1285 >> FULL_SIMP_TAC std_ss [GSYM real_lt] 1286 >> FULL_SIMP_TAC std_ss [REAL_LE_LT] 1287 >> FULL_SIMP_TAC std_ss [GSYM REAL_NEG_GT0, GSYM REAL_MUL_RNEG] 1288 >> METIS_TAC [REAL_LT_ANTISYM, REAL_LT_RMUL_0, REAL_NEG_GT0] )); 1289 1290 1291val pos_part_neg_part_borel_measurable = store_thm 1292 ("pos_part_neg_part_borel_measurable", 1293 ``!f m. measure_space m /\ f IN borel_measurable (m_space m, measurable_sets m) ==> 1294 (pos_part f) IN borel_measurable (m_space m, measurable_sets m) /\ 1295 (neg_part f) IN borel_measurable (m_space m, measurable_sets m)``, 1296 (REPEAT STRIP_TAC >> RW_TAC std_ss [borel_measurable_le_iff]) 1297 >- (Cases_on `0 <= a` 1298 >- (`!w. pos_part f w <= a = f w <= a` 1299 by (RW_TAC real_ss [pos_part_def] >> METIS_TAC [REAL_LTE_TRANS, REAL_LT_IMP_LE, GSYM real_lt]) 1300 >> POP_ORW >> METIS_TAC [borel_measurable_le_iff]) 1301 >> `{w | w IN m_space m /\ pos_part f w <= a} = {}` 1302 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [GSPECIFICATION, NOT_IN_EMPTY, pos_part_def] 1303 >> RW_TAC real_ss [] >> METIS_TAC [REAL_LE_TRANS]) 1304 >> POP_ORW >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, space_def, subsets_def]) 1305 >> Cases_on `0 <= a` 1306 >- (`!w. neg_part f w <= a = ~a <= f w` 1307 by (RW_TAC real_ss [neg_part_def] 1308 >> METIS_TAC [REAL_NEG_GE0, REAL_LE_TRANS, REAL_LE_NEGR, REAL_NEG_NEG, REAL_LE_NEG]) 1309 >> POP_ORW 1310 >> METIS_TAC [borel_measurable_ge_iff]) 1311 >> `{w | w IN m_space m /\ neg_part f w <= a} = {}` 1312 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [GSPECIFICATION, NOT_IN_EMPTY, neg_part_def] 1313 >> RW_TAC real_ss [] 1314 >> METIS_TAC [REAL_LET_TRANS, REAL_LTE_TRANS, REAL_LT_IMP_LE, GSYM real_lt, 1315 REAL_LE_NEGR, REAL_NEG_NEG, REAL_LE_NEG, REAL_NEG_GE0]) 1316 >> POP_ORW >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, space_def, subsets_def]); 1317 1318 1319val pos_part_neg_part_borel_measurable_iff = store_thm 1320 ("pos_part_neg_part_borel_measurable_iff", 1321 ``!f m. measure_space m ==> 1322 (f IN borel_measurable (m_space m, measurable_sets m) = 1323 (pos_part f) IN borel_measurable (m_space m, measurable_sets m) /\ 1324 (neg_part f) IN borel_measurable (m_space m, measurable_sets m))``, 1325 REPEAT STRIP_TAC >> EQ_TAC 1326 >- RW_TAC std_ss [pos_part_neg_part_borel_measurable] 1327 >> STRIP_TAC >> ONCE_REWRITE_TAC [f_plus_minus2] 1328 >> MATCH_MP_TAC borel_measurable_sub_borel_measurable 1329 >> RW_TAC std_ss []); 1330 1331 1332val psfis_borel_measurable = store_thm 1333 ("psfis_borel_measurable", 1334 ``!m f a. measure_space m /\ a IN psfis m f ==> 1335 f IN borel_measurable (m_space m, measurable_sets m)``, 1336 REPEAT STRIP_TAC 1337 >> (MP_TAC o Q.SPECL [`m`,`a`,`f`]) IN_psfis 1338 >> RW_TAC std_ss [pos_simple_fn_def] 1339 >> RW_TAC std_ss [borel_measurable_le_iff] 1340 >> `!w. w IN m_space m /\ f w <= a = 1341 w IN m_space m /\ 1342 (\w. SIGMA (\i. x i * indicator_fn (a' i) w) s) w <= a` 1343 by (RW_TAC std_ss [] >> METIS_TAC []) 1344 >> POP_ORW 1345 >> Suff `(\w. SIGMA (\i. x i * indicator_fn (a' i) w) s) IN 1346 borel_measurable (m_space m, measurable_sets m)` 1347 >- METIS_TAC [GSYM borel_measurable_le_iff] 1348 >> `!w i. x i * indicator_fn (a' i) w = (\i w. x i * indicator_fn (a' i) w) i w` 1349 by RW_TAC std_ss [] 1350 >> POP_ORW >> MATCH_MP_TAC borel_measurable_SIGMA_borel_measurable 1351 >> RW_TAC std_ss [] 1352 >> `!w. x i * indicator_fn (a' i) w = 1353 0 + indicator_fn (a' i) w * x i` 1354 by RW_TAC real_ss [REAL_MUL_COMM] 1355 >> POP_ORW 1356 >> Suff `indicator_fn (a' i) IN borel_measurable (m_space m, measurable_sets m)` 1357 >- METIS_TAC [affine_borel_measurable] 1358 >> MATCH_MP_TAC borel_measurable_indicator 1359 >> FULL_SIMP_TAC std_ss [measure_space_def, subsets_def]); 1360 1361 1362val real_le_mult_sustain = lemma 1363 (``!r y. (!z. 0 < z /\ z < 1 ==> z * r <= y) ==> r <= y``, 1364 REPEAT STRIP_TAC 1365 >> REVERSE (Cases_on `0<y`) 1366 >- (`0<(1:real)` by RW_TAC real_ss [] 1367 >> `?z. 0 < z /\ z < 1` by (MATCH_MP_TAC REAL_MEAN >> RW_TAC std_ss []) 1368 >> `z * r <= y` by RW_TAC std_ss [] 1369 >> FULL_SIMP_TAC std_ss [REAL_NOT_LT] 1370 >> `z * r <= 0` by METIS_TAC [REAL_LE_TRANS] 1371 >> `z <= 1 /\ r <= 0` 1372 by (RW_TAC std_ss [REAL_LT_IMP_LE] 1373 >> METIS_TAC [GSYM REAL_LE_RDIV_EQ, REAL_DIV_LZERO, REAL_MUL_COMM]) 1374 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `z * r` 1375 >> ASM_REWRITE_TAC [] 1376 >> ONCE_REWRITE_TAC [GSYM REAL_LE_NEG] 1377 >> ONCE_REWRITE_TAC [GSYM REAL_MUL_RNEG] 1378 >> (MP_TAC o Q.SPECL [`~r`,`z`,`1`]) REAL_LE_RMUL_IMP 1379 >> RW_TAC real_ss [REAL_NEG_GE0, REAL_LT_IMP_LE]) 1380 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1381 >> FULL_SIMP_TAC std_ss [GSYM real_lt] 1382 >> `?q. y < q /\ q < r` by (MATCH_MP_TAC REAL_MEAN >> RW_TAC std_ss []) 1383 >> `0 < r` by METIS_TAC [REAL_LT_TRANS] 1384 >> `q / r < 1` by (RW_TAC real_ss [REAL_LT_LDIV_EQ]) 1385 >> `0 < q / r` by METIS_TAC [REAL_LT_DIV, REAL_LT_TRANS] 1386 >> Q.PAT_X_ASSUM `!z. P z` (MP_TAC o Q.SPEC `q/r`) 1387 >> RW_TAC std_ss [REAL_DIV_RMUL, REAL_LT_IMP_NE, GSYM real_lt]); 1388 1389 1390val mono_conv_outgrow = lemma 1391 (``!(x:num->real) y (z:real). (!(a:num) b. a <= b ==> x a <= x b) /\ x --> y /\ z < y ==> 1392 (?(b:num). !a. b <= a ==> z < x a)``, 1393 REPEAT STRIP_TAC 1394 >> `0 < y - z` by RW_TAC real_ss [REAL_LT_SUB_LADD] 1395 >> `?n. !m. n <= m ==> abs (x m + ~y) < y-z` 1396 by FULL_SIMP_TAC std_ss [SEQ, GSYM real_sub, GREATER_EQ] 1397 >> `!m. x m <= y` 1398 by (STRIP_TAC >> MATCH_MP_TAC SEQ_MONO_LE >> RW_TAC real_ss []) 1399 >> `!m. abs (x m + ~y) = y - x m` 1400 by (RW_TAC std_ss [abs] 1401 >- (FULL_SIMP_TAC real_ss [GSYM real_sub, REAL_LE_SUB_LADD] 1402 >> METIS_TAC [REAL_SUB_REFL, REAL_LE_ANTISYM]) 1403 >> REAL_ARITH_TAC) 1404 >> `!m. y - x m + z = (y + z) - x m` by (STRIP_TAC >> REAL_ARITH_TAC) 1405 >> FULL_SIMP_TAC std_ss [REAL_LT_SUB_LADD, REAL_LT_SUB_RADD, REAL_LT_LADD] 1406 >> Q.EXISTS_TAC `n` >> RW_TAC std_ss []); 1407 1408 1409val psfis_mono_conv_mono = store_thm 1410 ("psfis_mono_conv_mono", 1411 ``!m f u x y r s. 1412 measure_space m /\ 1413 mono_convergent u f (m_space m) /\ 1414 (!n. x n IN psfis m (u n)) /\ 1415 (!m n. m <= n ==> x m <= x n) /\ 1416 x --> y /\ 1417 r IN psfis m s /\ 1418 (!a. a IN m_space m ==> s a <= f a) ==> 1419 r <= y``, 1420 REPEAT STRIP_TAC 1421 >> MATCH_MP_TAC real_le_mult_sustain 1422 >> REPEAT STRIP_TAC 1423 >> (MP_TAC o Q.SPECL [`m`, `r`, `s`]) (GSYM IN_psfis) 1424 >> RW_TAC std_ss [pos_simple_fn_integral_def] 1425 >> Q.ABBREV_TAC `B' = (\n:num. {w | w IN m_space m /\ z * s w <= u n w})` 1426 >> `!n. B' n IN measurable_sets m` 1427 by (Q.UNABBREV_TAC `B'` >> RW_TAC std_ss [] 1428 >> `!w. z * s w = (\w. z * s w) w` by RW_TAC std_ss [] >> POP_ORW 1429 >> MATCH_MP_TAC borel_measurable_leq_borel_measurable 1430 >> RW_TAC std_ss [] 1431 >- (`!w. z = (\w. z) w` by RW_TAC std_ss [] >> POP_ORW 1432 >> MATCH_MP_TAC borel_measurable_times_borel_measurable 1433 >> RW_TAC std_ss [] 1434 >- (MATCH_MP_TAC borel_measurable_const >> FULL_SIMP_TAC std_ss [measure_space_def]) 1435 >> MATCH_MP_TAC psfis_borel_measurable 1436 >> Q.EXISTS_TAC `SIGMA (\i. x' i * measure m (a i)) s'` >> RW_TAC std_ss []) 1437 >> MATCH_MP_TAC psfis_borel_measurable 1438 >> Q.EXISTS_TAC `x n` >> RW_TAC std_ss []) 1439 >> `!n. (z * (SIGMA (\i. x' i * measure m (a i INTER B' n)) s') <= x n) /\ 1440 (!i. i IN s' ==> (a i INTER B' n) IN measurable_sets m)` 1441 by (STRIP_TAC >> ONCE_REWRITE_TAC [CONJ_SYM] >> STRONG_CONJ_TAC 1442 >- (REPEAT STRIP_TAC >> FULL_SIMP_TAC std_ss [pos_simple_fn_def] 1443 >> `measurable_sets m = subsets (m_space m, measurable_sets m)` by RW_TAC std_ss [subsets_def] 1444 >> POP_ORW 1445 >> MATCH_MP_TAC ALGEBRA_INTER 1446 >> FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def, subsets_def]) 1447 >> STRIP_TAC >> (MP_TAC o Q.SPECL [`m`, `(x:num->real) n`, `(u :num -> 'a -> real) n`]) (GSYM IN_psfis) 1448 >> RW_TAC std_ss [pos_simple_fn_integral_def] 1449 >> Q.PAT_X_ASSUM `pos_simple_fn m s s' a x'` MP_TAC 1450 >> RW_TAC std_ss [pos_simple_fn_def] 1451 >> MATCH_MP_TAC psfis_mono 1452 >> Q.EXISTS_TAC `m` 1453 >> Q.EXISTS_TAC `(\t. z * (\t. SIGMA (\i. x' i * indicator_fn (a i INTER B' n) t) s') t)` 1454 >> Q.EXISTS_TAC `u n` 1455 >> CONJ_TAC >- ASM_REWRITE_TAC [] 1456 >> CONJ_TAC 1457 >- (Suff `SIGMA (\i. x' i * measure m (a i INTER B' n)) s' IN 1458 psfis m (\t. SIGMA (\i. x' i * indicator_fn (a i INTER B' n) t) s')` 1459 >- METIS_TAC [REAL_LT_IMP_LE, psfis_mult] 1460 >> `!t i. a i INTER B' n = (\i. a i INTER B' n) i` by RW_TAC std_ss [] 1461 >> POP_ORW 1462 >> MATCH_MP_TAC psfis_intro 1463 >> RW_TAC std_ss []) 1464 >> RW_TAC std_ss [] 1465 >> `!i. (x' i * indicator_fn (a i INTER B' n) x''' = 1466 indicator_fn (B' n) x''' * (\i.(x' i * indicator_fn (a i) x''')) i)` 1467 by (RW_TAC real_ss [indicator_fn_def, IN_INTER] >> FULL_SIMP_TAC bool_ss [DE_MORGAN_THM]) 1468 >> POP_ORW 1469 >> ASM_SIMP_TAC std_ss [REAL_SUM_IMAGE_CMUL] 1470 >> Cases_on `x''' IN m_space m` 1471 >- (`SIGMA (\i. x' i * indicator_fn (a i) x''') s' = s x'''` by METIS_TAC [] 1472 >> POP_ORW 1473 >> Q.UNABBREV_TAC `B'` 1474 >> SIMP_TAC real_ss [indicator_fn_def, GSPECIFICATION] 1475 >> RW_TAC real_ss [] 1476 >> METIS_TAC [nonneg_def, psfis_nonneg]) 1477 >> (MP_TAC o Q.SPECL [`(\i. x' i * indicator_fn (a i) x''')`, `0`] 1478 o UNDISCH o Q.ISPEC `s':num->bool`) REAL_SUM_IMAGE_FINITE_CONST2 1479 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] 1480 >> Suff `(!y. y IN s' ==> (x' y * indicator_fn (a y) x''' = 0))` 1481 >- (ASM_SIMP_TAC real_ss [] >> METIS_TAC [nonneg_def, psfis_nonneg]) 1482 >> RW_TAC std_ss [REAL_ENTIRE, indicator_fn_def] 1483 >> Cases_on `x' y' = 0` >> RW_TAC real_ss [] 1484 >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, subset_class_def, space_def, subsets_def, SUBSET_DEF] 1485 >> METIS_TAC []) 1486 >> MATCH_MP_TAC SEQ_LE 1487 >> Q.EXISTS_TAC `(\n. ((\n. z) n) * (\n. SIGMA (\i. x' i * measure m (a i INTER B' n)) s') n)` 1488 >> Q.EXISTS_TAC `x` 1489 >> REVERSE CONJ_TAC 1490 >- (ASM_REWRITE_TAC [GREATER_EQ] >> Q.EXISTS_TAC `0` >> RW_TAC arith_ss []) 1491 >> MATCH_MP_TAC SEQ_MUL 1492 >> RW_TAC std_ss [SEQ_CONST] 1493 >> FULL_SIMP_TAC std_ss [pos_simple_fn_def] 1494 >> `!n. (\i. x' i * measure m (a i INTER B' n)) = 1495 (\n i. x' i * measure m (a i INTER B' n)) n` by RW_TAC std_ss [] 1496 >> POP_ORW 1497 >> (MATCH_MP_TAC o UNDISCH o Q.ISPEC `s':num->bool`) SEQ_REAL_SUM_IMAGE 1498 >> RW_TAC std_ss [] 1499 >> `(\n. x' x'' * measure m (a x'' INTER B' n)) = 1500 (\n. (\n. x' x'') n * (\n. measure m (a x'' INTER B' n)) n)` by RW_TAC std_ss [] 1501 >> POP_ORW >> MATCH_MP_TAC SEQ_MUL 1502 >> RW_TAC std_ss [SEQ_CONST] 1503 >> `(\n. measure m (a x'' INTER B' n)) = 1504 measure m o (\n. a x'' INTER B' n)` 1505 by RW_TAC std_ss [o_DEF] 1506 >> POP_ORW 1507 >> MATCH_MP_TAC MONOTONE_CONVERGENCE 1508 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF, IN_INTER] 1509 >- (Q.PAT_X_ASSUM `!t. 1510 t IN m_space m ==> 1511 (s t = SIGMA (\i. x' i * indicator_fn (a i) t) s')` (K ALL_TAC) 1512 >> Q.UNABBREV_TAC `B'` 1513 >> FULL_SIMP_TAC std_ss [GSPECIFICATION, mono_convergent_def] 1514 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `u n x'''` 1515 >> RW_TAC arith_ss []) 1516 >> Q.UNABBREV_TAC `B'` >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV, GSPECIFICATION, IN_INTER] 1517 >> Suff `x''' IN a x'' ==> x''' IN m_space m /\ (?n. z * s x''' <= u n x''')` 1518 >- METIS_TAC [] 1519 >> STRIP_TAC 1520 >> STRONG_CONJ_TAC 1521 >- (FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, subset_class_def, space_def, subsets_def, SUBSET_DEF] 1522 >> METIS_TAC []) 1523 >> Cases_on `s x''' = 0` 1524 >- (RW_TAC real_ss [] >> METIS_TAC [nonneg_def, psfis_nonneg]) 1525 >> STRIP_TAC 1526 >> `0 < s x'''` by METIS_TAC [REAL_LT_LE, psfis_nonneg, nonneg_def] 1527 >> `z * s x''' < 1 * s x'''` by (MATCH_MP_TAC REAL_LT_RMUL_IMP >> RW_TAC real_ss [REAL_LT_IMP_LE]) 1528 >> `z * s x''' < f x'''` by METIS_TAC [REAL_LTE_TRANS, REAL_MUL_LID] 1529 >> (MP_TAC o Q.SPECL [`(\n. u n x''')`, `f x'''`, `z * s x'''`]) mono_conv_outgrow 1530 >> FULL_SIMP_TAC std_ss [mono_convergent_def] 1531 >> RW_TAC std_ss [] 1532 >> METIS_TAC [LESS_EQ_REFL, REAL_LT_IMP_LE]); 1533 1534 1535val psfis_nnfis = store_thm 1536 ("psfis_nnfis", 1537 ``!m f a. measure_space m /\ a IN psfis m f ==> 1538 a IN nnfis m f``, 1539 RW_TAC std_ss [nnfis_def, GSPECIFICATION] 1540 >> Q.EXISTS_TAC `(\n. f)` >> Q.EXISTS_TAC `(\n. a)` 1541 >> RW_TAC real_ss [SEQ_CONST, mono_convergent_def]); 1542 1543 1544val nnfis_times = store_thm 1545 ("nnfis_times", 1546 ``!f m a z. measure_space m /\ a IN nnfis m f /\ 0<=z ==> 1547 z*a IN nnfis m (\w. z * f w)``, 1548 RW_TAC std_ss [nnfis_def, GSPECIFICATION] 1549 >> Q.EXISTS_TAC `(\n w. z * u n w)` >> Q.EXISTS_TAC `(\n. z * x n)` 1550 >> CONJ_TAC 1551 >- (RW_TAC std_ss [mono_convergent_def] 1552 >- (MATCH_MP_TAC REAL_LE_MUL2 1553 >> FULL_SIMP_TAC real_ss [mono_convergent_def, REAL_LT_IMP_LE] 1554 >> METIS_TAC [nonneg_def, psfis_nonneg]) 1555 >> `(\n. z * u n w) = (\n. (\n. z) n * (\n. u n w) n)` 1556 by RW_TAC std_ss [] 1557 >> POP_ORW 1558 >> MATCH_MP_TAC SEQ_MUL 1559 >> FULL_SIMP_TAC std_ss [SEQ_CONST, mono_convergent_def]) 1560 >> CONJ_TAC >- METIS_TAC [psfis_mult] 1561 >> `(\n. z * x n) = (\n. (\n. z) n * (\n. x n) n)` 1562 by RW_TAC std_ss [] 1563 >> POP_ORW 1564 >> MATCH_MP_TAC SEQ_MUL 1565 >> FULL_SIMP_TAC std_ss [SEQ_CONST, ETA_THM]); 1566 1567 1568val nnfis_add = store_thm 1569 ("nnfis_add", 1570 ``!f g m a b. measure_space m /\ a IN nnfis m f /\ b IN nnfis m g ==> 1571 (a + b) IN nnfis m (\w. f w + g w)``, 1572 RW_TAC std_ss [nnfis_def, GSPECIFICATION] 1573 >> Q.EXISTS_TAC `(\n w. u n w + u' n w)` >> Q.EXISTS_TAC `(\n. x n + x' n)` 1574 >> CONJ_TAC 1575 >- (RW_TAC std_ss [mono_convergent_def] 1576 >- (MATCH_MP_TAC REAL_LE_ADD2 1577 >> FULL_SIMP_TAC real_ss [mono_convergent_def]) 1578 >> `(\n. u n w + u' n w) = (\n. (\n. u n w) n + (\n. u' n w) n)` 1579 by RW_TAC std_ss [] 1580 >> POP_ORW 1581 >> MATCH_MP_TAC SEQ_ADD 1582 >> FULL_SIMP_TAC std_ss [mono_convergent_def]) 1583 >> CONJ_TAC >- METIS_TAC [psfis_add] 1584 >> RW_TAC std_ss [] 1585 >> RW_TAC std_ss [SEQ_ADD]); 1586 1587 1588val nnfis_mono = store_thm 1589 ("nnfis_mono", 1590 ``!f g m a b. measure_space m /\ a IN nnfis m f /\ b IN nnfis m g /\ 1591 (!w. w IN m_space m ==> f w <= g w) ==> 1592 a <= b``, 1593 RW_TAC std_ss [nnfis_def, GSPECIFICATION] 1594 >> `!n x. x IN m_space m ==> u n x <= f x` 1595 by (REPEAT STRIP_TAC >> FULL_SIMP_TAC std_ss [mono_convergent_def] 1596 >> `u n x'' = (\n. u n x'') n` by RW_TAC std_ss [] 1597 >> POP_ORW 1598 >> MATCH_MP_TAC SEQ_MONO_LE 1599 >> RW_TAC std_ss [DECIDE ``!(n:num). n <= n + 1``]) 1600 >> `!n x. x IN m_space m ==> u n x <= g x` 1601 by METIS_TAC [REAL_LE_TRANS] 1602 >> `!n. x n <= b` 1603 by (STRIP_TAC >> MATCH_MP_TAC psfis_mono_conv_mono 1604 >> Q.EXISTS_TAC `m` >> Q.EXISTS_TAC `g` >> Q.EXISTS_TAC `u'` 1605 >> Q.EXISTS_TAC `x'` >> Q.EXISTS_TAC `u n` 1606 >> FULL_SIMP_TAC real_ss [mono_convergent_def] 1607 >> REPEAT STRIP_TAC >> MATCH_MP_TAC psfis_mono 1608 >> Q.EXISTS_TAC `m` >> Q.EXISTS_TAC `u' m'` >> Q.EXISTS_TAC `u' n` 1609 >> RW_TAC std_ss []) 1610 >> MATCH_MP_TAC SEQ_LE_IMP_LIM_LE 1611 >> Q.EXISTS_TAC `x` >> RW_TAC std_ss []); 1612 1613 1614val nnfis_unique = store_thm 1615 ("nnfis_unique", 1616 ``!f m a b. measure_space m /\ a IN nnfis m f /\ b IN nnfis m f ==> 1617 (a = b)``, 1618 REPEAT STRIP_TAC 1619 >> ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 1620 >> CONJ_TAC >> MATCH_MP_TAC nnfis_mono 1621 >> Q.EXISTS_TAC `f` >> Q.EXISTS_TAC `f` >> Q.EXISTS_TAC `m` 1622 >> RW_TAC std_ss [REAL_LE_REFL]); 1623 1624 1625val psfis_equiv = store_thm 1626 ("psfis_equiv", 1627 ``!f g a m. measure_space m /\ 1628 a IN psfis m f /\ 1629 (!t. 0 <= g t) /\ 1630 (!t. t IN m_space m ==> (f t = g t)) ==> 1631 a IN psfis m g``, 1632 REPEAT STRIP_TAC 1633 >> (MP_TAC o Q.SPECL [`m`, `a`, `f`]) IN_psfis 1634 >> RW_TAC std_ss [] 1635 >> RW_TAC std_ss [psfis_def, IN_IMAGE] 1636 >> Q.EXISTS_TAC `(s, a', x)` 1637 >> RW_TAC std_ss [psfs_def, GSPECIFICATION] 1638 >> Q.EXISTS_TAC `(s, a', x)` 1639 >> RW_TAC std_ss [] 1640 >> FULL_SIMP_TAC std_ss [pos_simple_fn_def]); 1641 1642 1643val upclose_psfis = store_thm 1644 ("upclose_psfis", 1645 ``!f g a b m. measure_space m /\ a IN psfis m f /\ b IN psfis m g ==> 1646 (?c. c IN psfis m (upclose f g))``, 1647 REPEAT STRIP_TAC 1648 >> (MP_TAC o Q.SPECL [`m`, `f`, `g`, `a`, `b`]) psfis_present 1649 >> RW_TAC std_ss [upclose_def] 1650 >> Q.EXISTS_TAC `REAL_SUM_IMAGE (\i.max (z i) (z' i) * measure m (c i)) k` 1651 >> MATCH_MP_TAC psfis_equiv 1652 >> Q.EXISTS_TAC `(\t. REAL_SUM_IMAGE (\i.max (z i) (z' i) * indicator_fn (c i) t) k)` 1653 >> RW_TAC std_ss [REAL_LE_MAX] 1654 >| [`!t i. max (z i) (z' i) = (\i. max (z i) (z' i)) i` by RW_TAC std_ss [] 1655 >> POP_ORW >> MATCH_MP_TAC psfis_intro 1656 >> RW_TAC std_ss [REAL_LE_MAX], 1657 METIS_TAC [psfis_nonneg, nonneg_def], 1658 Cases_on `?i. i IN k /\ t IN (c i)` 1659 >- (FULL_SIMP_TAC std_ss [] 1660 >> `k = i INSERT k` 1661 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INSERT] >> METIS_TAC []) 1662 >> POP_ORW 1663 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, FINITE_INSERT] 1664 >> `FINITE (k DELETE i)` by RW_TAC std_ss [FINITE_DELETE] 1665 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 1666 o Q.SPECL [`\i. max (z i) (z' i) * indicator_fn (c i) t`, `0`] o UNDISCH 1667 o Q.SPEC `k DELETE i` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 1668 >> RW_TAC real_ss [] 1669 >> `SIGMA (\i. max (z i) (z' i) * indicator_fn (c i) t) (k DELETE i) = 0` 1670 by (POP_ASSUM MATCH_MP_TAC 1671 >> RW_TAC real_ss [indicator_fn_def, REAL_ENTIRE] 1672 >> METIS_TAC [IN_DISJOINT]) 1673 >> POP_ORW >> POP_ASSUM (K ALL_TAC) 1674 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 1675 o Q.SPECL [`\i. z i * indicator_fn (c i) t`, `0`] o UNDISCH 1676 o Q.SPEC `k DELETE i` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 1677 >> RW_TAC real_ss [] 1678 >> `SIGMA (\i. z i * indicator_fn (c i) t) (k DELETE i) = 0` 1679 by (POP_ASSUM MATCH_MP_TAC 1680 >> RW_TAC real_ss [indicator_fn_def, REAL_ENTIRE] 1681 >> METIS_TAC [IN_DISJOINT]) 1682 >> POP_ORW >> POP_ASSUM (K ALL_TAC) 1683 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 1684 o Q.SPECL [`\i. z' i * indicator_fn (c i) t`, `0`] o UNDISCH 1685 o Q.SPEC `k DELETE i` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 1686 >> RW_TAC real_ss [] 1687 >> `SIGMA (\i. z' i * indicator_fn (c i) t) (k DELETE i) = 0` 1688 by (POP_ASSUM MATCH_MP_TAC 1689 >> RW_TAC real_ss [indicator_fn_def, REAL_ENTIRE] 1690 >> METIS_TAC [IN_DISJOINT]) 1691 >> POP_ORW >> POP_ASSUM (K ALL_TAC) 1692 >> RW_TAC real_ss [indicator_fn_def]) 1693 >> FULL_SIMP_TAC std_ss [] 1694 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 1695 o Q.SPECL [`\i. max (z i) (z' i) * indicator_fn (c i) t`, `0`] o UNDISCH 1696 o Q.SPEC `k` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 1697 >> RW_TAC real_ss [] 1698 >> `SIGMA (\i. max (z i) (z' i) * indicator_fn (c i) t) k = 0` 1699 by (POP_ASSUM MATCH_MP_TAC 1700 >> RW_TAC real_ss [indicator_fn_def, REAL_ENTIRE] 1701 >> METIS_TAC [IN_DISJOINT]) 1702 >> POP_ORW >> POP_ASSUM (K ALL_TAC) 1703 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 1704 o Q.SPECL [`\i. z i * indicator_fn (c i) t`, `0`] o UNDISCH 1705 o Q.SPEC `k` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 1706 >> RW_TAC real_ss [] 1707 >> `SIGMA (\i. z i * indicator_fn (c i) t) k = 0` 1708 by (POP_ASSUM MATCH_MP_TAC 1709 >> RW_TAC real_ss [indicator_fn_def, REAL_ENTIRE] 1710 >> METIS_TAC [IN_DISJOINT]) 1711 >> POP_ORW >> POP_ASSUM (K ALL_TAC) 1712 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 1713 o Q.SPECL [`\i. (z' i) * indicator_fn (c i) t`, `0`] o UNDISCH 1714 o Q.SPEC `k` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 1715 >> RW_TAC real_ss [] 1716 >> `SIGMA (\i. (z' i) * indicator_fn (c i) t) k = 0` 1717 by (POP_ASSUM MATCH_MP_TAC 1718 >> RW_TAC real_ss [indicator_fn_def, REAL_ENTIRE] 1719 >> METIS_TAC [IN_DISJOINT]) 1720 >> POP_ORW >> POP_ASSUM (K ALL_TAC) 1721 >> RW_TAC real_ss []]); 1722 1723 1724val mon_upclose_psfis = store_thm 1725 ("mon_upclose_psfis", 1726 ``!m u. measure_space m /\ 1727 (!(n:num) (n':num). ?a. a IN psfis m (u n n')) ==> 1728 (?c. !(n:num). (c n) IN psfis m (mon_upclose u n))``, 1729 REPEAT STRIP_TAC 1730 >> `!(n':num) (n:num). ?c. c IN psfis m (mon_upclose_help n u n')` 1731 by (STRIP_TAC >> Induct 1732 >> RW_TAC std_ss [mon_upclose_help_def] 1733 >> MATCH_MP_TAC upclose_psfis 1734 >> METIS_TAC []) 1735 >> RW_TAC std_ss [mon_upclose_def] 1736 >> Q.ABBREV_TAC `P = (\n c. c IN psfis m (mon_upclose_help n u n))` 1737 >> Q.EXISTS_TAC `(\n. @c. P n c)` 1738 >> RW_TAC std_ss [] 1739 >> Suff `P n (@c. P n c)` >- METIS_TAC [] 1740 >> Q.ABBREV_TAC `P' = P n` 1741 >> RW_TAC std_ss [SELECT_THM] 1742 >> Q.UNABBREV_TAC `P'` >> Q.UNABBREV_TAC `P` 1743 >> RW_TAC std_ss []); 1744 1745 1746val mon_upclose_help_lemma = lemma 1747 (``!f u h s. (!n. mono_convergent (\m. u m n) (f n) s) /\ 1748 (!m n x. x IN s ==> 0 <= u m n x) /\ 1749 mono_convergent f h s ==> 1750 mono_convergent (mon_upclose u) h s /\ 1751 (!n x. x IN s ==> mon_upclose u n x <= f n x)``, 1752 NTAC 5 STRIP_TAC 1753 >> ONCE_REWRITE_TAC [CONJ_SYM] 1754 >> STRONG_CONJ_TAC 1755 >- (RW_TAC std_ss [mon_upclose_def] 1756 >> Suff `!m. mon_upclose_help n u m x <= f n x` 1757 >- RW_TAC std_ss [] 1758 >> Induct_on `n` 1759 >- (RW_TAC std_ss [mon_upclose_help_def] 1760 >> FULL_SIMP_TAC std_ss [mono_convergent_def] 1761 >> `u m 0 x = (\m. u m 0 x) m` by RW_TAC std_ss [] 1762 >> POP_ORW >> MATCH_MP_TAC SEQ_MONO_LE 1763 >> RW_TAC arith_ss []) 1764 >> RW_TAC std_ss [mon_upclose_help_def, upclose_def, REAL_MAX_LE] 1765 >- (`u m (SUC n) x = (\m. u m (SUC n) x) m` by RW_TAC std_ss [] 1766 >> POP_ORW >> MATCH_MP_TAC SEQ_MONO_LE 1767 >> FULL_SIMP_TAC arith_ss [mono_convergent_def]) 1768 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `f n x` 1769 >> FULL_SIMP_TAC arith_ss [mono_convergent_def]) 1770 >> STRIP_TAC 1771 >> `!t m n n'. t IN s /\ n <= n' ==> mon_upclose_help n u m t <= mon_upclose_help n' u m t` 1772 by (RW_TAC std_ss [mon_upclose_help_def, upclose_def, REAL_LE_MAX, REAL_LE_REFL] 1773 >> Suff `!n' n. n <= n' ==> mon_upclose_help n u m t <= mon_upclose_help n' u m t` 1774 >- RW_TAC std_ss [] 1775 >> Induct >- RW_TAC arith_ss [REAL_LE_REFL] 1776 >> RW_TAC arith_ss [DECIDE ``!(m:num) n. m <= SUC n = ((m = SUC n) \/ m <= n)``] 1777 >> RW_TAC real_ss [] 1778 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `mon_upclose_help n'' u m t` 1779 >> RW_TAC arith_ss [REAL_LE_REFL] 1780 >> ASM_SIMP_TAC arith_ss [] 1781 >> RW_TAC real_ss [mon_upclose_help_def, upclose_def]) 1782 >> `!t m m' n. t IN s /\ m <= m' ==> u m n t <= u m' n t` 1783 by FULL_SIMP_TAC arith_ss [mono_convergent_def] 1784 >> `!t n n'. t IN s /\ n <= n' ==> mon_upclose u n t <= mon_upclose u n' t` 1785 by (REPEAT STRIP_TAC 1786 >> `!m m'. m <= m' ==> mon_upclose_help n u m t <= mon_upclose_help n u m' t` 1787 by (Induct_on `n` 1788 >- FULL_SIMP_TAC real_ss [mon_upclose_help_def, mono_convergent_def] 1789 >> RW_TAC real_ss [mon_upclose_help_def, upclose_def] 1790 >> MATCH_MP_TAC REAL_IMP_MAX_LE2 >> RW_TAC std_ss [DECIDE ``!(n:num) m. SUC n <= m ==> n <= m``]) 1791 >> RW_TAC std_ss [mon_upclose_def] >> METIS_TAC [REAL_LE_TRANS, REAL_LE_REFL]) 1792 >> `!t n n'. t IN s /\ n <= n' ==> mon_upclose_help n u n t <= mon_upclose_help n' u n' t` 1793 by METIS_TAC [mon_upclose_def] 1794 >> `!t n. t IN s ==> mon_upclose u n t <= h t` 1795 by (REPEAT STRIP_TAC >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `f n t` 1796 >> RW_TAC std_ss [] >> `f n t = (\n. f n t) n` by RW_TAC std_ss [] 1797 >> POP_ORW >> MATCH_MP_TAC SEQ_MONO_LE 1798 >> FULL_SIMP_TAC arith_ss [mono_convergent_def]) 1799 >> RW_TAC std_ss [mono_convergent_def] 1800 >> `!n. 0 <= mon_upclose u n x` 1801 by (STRIP_TAC >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `mon_upclose u 0 x` 1802 >> ASM_SIMP_TAC arith_ss [] >> RW_TAC std_ss [mon_upclose_def, mon_upclose_help_def]) 1803 >> `convergent (\i. mon_upclose u i x)` 1804 by (MATCH_MP_TAC SEQ_ICONV 1805 >> CONJ_TAC 1806 >- (MATCH_MP_TAC SEQ_BOUNDED_2 >> Q.EXISTS_TAC `0` >> Q.EXISTS_TAC `h x` 1807 >> RW_TAC std_ss []) 1808 >> RW_TAC std_ss [GREATER_EQ, real_ge]) 1809 >> FULL_SIMP_TAC std_ss [convergent] 1810 >> `l <= h x` 1811 by (MATCH_MP_TAC SEQ_LE_IMP_LIM_LE >> Q.EXISTS_TAC `(\i. mon_upclose u i x)` >> RW_TAC std_ss []) 1812 >> Suff `h x <= l` >- METIS_TAC [REAL_LE_ANTISYM] 1813 >> Suff `!n. f n x <= l` 1814 >- (FULL_SIMP_TAC std_ss [mono_convergent_def] 1815 >> STRIP_TAC >> MATCH_MP_TAC SEQ_LE_IMP_LIM_LE >> Q.EXISTS_TAC `(\i. f i x)` >> RW_TAC std_ss []) 1816 >> STRIP_TAC >> FULL_SIMP_TAC std_ss [mono_convergent_def] 1817 >> MATCH_MP_TAC SEQ_LE >> Q.EXISTS_TAC `(\m. u m n x)` >> Q.EXISTS_TAC `(\i. mon_upclose u i x)` 1818 >> RW_TAC std_ss [real_ge, GREATER_EQ] 1819 >> Suff `!n m. n <= m ==> u m n x <= mon_upclose u m x` 1820 >- (STRIP_TAC >> Q.EXISTS_TAC `n` >> RW_TAC std_ss []) 1821 >> RW_TAC std_ss [mon_upclose_def] 1822 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `mon_upclose_help n u m x` 1823 >> RW_TAC std_ss [] 1824 >> Induct_on `n` >- RW_TAC real_ss [mon_upclose_help_def] 1825 >> RW_TAC real_ss [mon_upclose_help_def, upclose_def]); 1826 1827 1828(* Beppo-Levi monotone convergence theorem *) 1829 1830val nnfis_mon_conv = store_thm 1831 ("nnfis_mon_conv", 1832 ``!f m h x y. measure_space m /\ 1833 mono_convergent f h (m_space m) /\ 1834 (!n. x n IN nnfis m (f n)) /\ 1835 x --> y ==> 1836 y IN nnfis m h``, 1837 REPEAT STRIP_TAC 1838 >> Q.ABBREV_TAC `u = (\n. @u. mono_convergent u (f n) (m_space m) /\ 1839 (!n'. ?a. a IN psfis m (u n')))` 1840 >> Q.ABBREV_TAC `urev = (\m n. u n m)` 1841 >> (MP_TAC o Q.SPECL [`f`, `urev`, `h`, `m_space m`]) mon_upclose_help_lemma 1842 >> ASM_SIMP_TAC std_ss [] 1843 >> Q.ABBREV_TAC `P = \n u. mono_convergent u (f n) (m_space m) /\ 1844 !n'. ?a. a IN psfis m (u n')` 1845 >> `(!n. P n (@u. P n u)) ==> 1846 (!n. mono_convergent (\m. urev m n) (f n) (m_space m)) /\ 1847 (!m' n x. x IN m_space m ==> 0 <= urev m' n x) /\ 1848 (!n n'. ?a. a IN psfis m (urev n n'))` 1849 by (RW_TAC std_ss [] 1850 >| [POP_ASSUM (MP_TAC o Q.SPEC `n`) 1851 >> Q.UNABBREV_TAC `P` 1852 >> Q.UNABBREV_TAC `urev` 1853 >> Q.UNABBREV_TAC `u` 1854 >> METIS_TAC [], 1855 Q.PAT_X_ASSUM `!n. P n @u. P n u` (MP_TAC o Q.SPEC `n`) 1856 >> Q.UNABBREV_TAC `P` 1857 >> Q.UNABBREV_TAC `urev` 1858 >> Q.UNABBREV_TAC `u` 1859 >> METIS_TAC [psfis_nonneg, nonneg_def], 1860 Q.PAT_X_ASSUM `!n. P n @u. P n u` (MP_TAC o Q.SPEC `n'`) 1861 >> Q.UNABBREV_TAC `P` 1862 >> Q.UNABBREV_TAC `urev` 1863 >> Q.UNABBREV_TAC `u` 1864 >> RW_TAC std_ss [] 1865 >> METIS_TAC []]) 1866 >> `!n. P n @u. P n u` 1867 by (STRIP_TAC >> Q.ABBREV_TAC `P' = P n` >> RW_TAC std_ss [SELECT_THM] 1868 >> Q.UNABBREV_TAC `P'` >> Q.UNABBREV_TAC `P` 1869 >> RW_TAC std_ss [] 1870 >> Q.PAT_X_ASSUM `!n. x n IN nnfis m (f n)` (MP_TAC o Q.SPEC `n`) 1871 >> RW_TAC std_ss [nnfis_def, GSPECIFICATION] 1872 >> Q.EXISTS_TAC `u'` 1873 >> RW_TAC std_ss [] 1874 >> Q.EXISTS_TAC `x' n'` 1875 >> RW_TAC std_ss []) 1876 >> FULL_SIMP_TAC std_ss [] 1877 >> POP_ASSUM (K ALL_TAC) >> Q.UNABBREV_TAC `P` 1878 >> STRIP_TAC 1879 >> (MP_TAC o Q.SPECL [`m`, `urev`]) mon_upclose_psfis 1880 >> ASM_SIMP_TAC std_ss [] 1881 >> STRIP_TAC 1882 >> `!n'. c n' IN nnfis m (mon_upclose urev n')` by RW_TAC std_ss [psfis_nnfis] 1883 >> `!n'. c n' <= x n'` 1884 by (STRIP_TAC >> MATCH_MP_TAC nnfis_mono 1885 >> Q.EXISTS_TAC `(mon_upclose urev n')` >> Q.EXISTS_TAC `f n'` >> Q.EXISTS_TAC `m` 1886 >> RW_TAC std_ss []) 1887 >> `!n n'. n <= n' ==> c n <= c n'` 1888 by (RW_TAC std_ss [] >> MATCH_MP_TAC psfis_mono 1889 >> Q.EXISTS_TAC `m` >> Q.EXISTS_TAC `mon_upclose urev n` >> Q.EXISTS_TAC `mon_upclose urev n'` 1890 >> RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [mono_convergent_def]) 1891 >> `!n. c n <= y` 1892 by (STRIP_TAC >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `x n` 1893 >> ASM_REWRITE_TAC [] >> MATCH_MP_TAC SEQ_MONO_LE 1894 >> RW_TAC arith_ss [] 1895 >> MATCH_MP_TAC nnfis_mono >> Q.EXISTS_TAC `f n` >> Q.EXISTS_TAC `f (n+1)` >> Q.EXISTS_TAC `m` 1896 >> FULL_SIMP_TAC arith_ss [mono_convergent_def]) 1897 >> `convergent c` 1898 by (MATCH_MP_TAC SEQ_ICONV 1899 >> CONJ_TAC 1900 >- (MATCH_MP_TAC SEQ_BOUNDED_2 >> Q.EXISTS_TAC `0` >> Q.EXISTS_TAC `y` >> METIS_TAC [pos_psfis]) 1901 >> RW_TAC std_ss [GREATER_EQ, real_ge]) 1902 >> FULL_SIMP_TAC std_ss [convergent] 1903 >> `l <= y` 1904 by (MATCH_MP_TAC SEQ_LE_IMP_LIM_LE >> Q.EXISTS_TAC `c` >> RW_TAC std_ss []) 1905 >> `l IN nnfis m h` 1906 by (RW_TAC std_ss [nnfis_def, GSPECIFICATION] 1907 >> Q.EXISTS_TAC `(mon_upclose urev)` >> Q.EXISTS_TAC `c` 1908 >> RW_TAC std_ss []) 1909 >> Suff `y <= l` >- METIS_TAC [REAL_LE_ANTISYM] 1910 >> Suff `!n. x n <= l` 1911 >- (STRIP_TAC >> MATCH_MP_TAC SEQ_LE_IMP_LIM_LE >> Q.EXISTS_TAC `x` >> RW_TAC std_ss []) 1912 1913 >> STRIP_TAC >> MATCH_MP_TAC nnfis_mono 1914 >> Q.EXISTS_TAC `f n` >> Q.EXISTS_TAC `h` >> Q.EXISTS_TAC `m` 1915 >> RW_TAC std_ss [] 1916 >> `f n w = (\n. f n w) n` by RW_TAC std_ss [] >> POP_ORW 1917 >> MATCH_MP_TAC SEQ_MONO_LE 1918 >> FULL_SIMP_TAC std_ss [mono_convergent_def]); 1919 1920 1921val nnfis_pos_on_mspace = store_thm 1922 ("nnfis_pos_on_mspace", 1923 ``!f m a. measure_space m /\ a IN nnfis m f ==> (!x. x IN m_space m ==> 0 <= f x)``, 1924 RW_TAC std_ss [nonneg_def, nnfis_def, GSPECIFICATION] 1925 >> `!n. nonneg (u n)` by METIS_TAC [psfis_nonneg] 1926 >> MATCH_MP_TAC LE_SEQ_IMP_LE_LIM 1927 >> Q.EXISTS_TAC `(\n. u n x')` 1928 >> FULL_SIMP_TAC std_ss [nonneg_def, mono_convergent_def]); 1929 1930 1931val nnfis_borel_measurable = store_thm 1932 ("nnfis_borel_measurable", 1933 ``!m f a. measure_space m /\ a IN nnfis m f ==> 1934 f IN borel_measurable (m_space m, measurable_sets m)``, 1935 RW_TAC std_ss [nnfis_def, GSPECIFICATION] 1936 >> MATCH_MP_TAC mono_convergent_borel_measurable 1937 >> Q.EXISTS_TAC `u` >> RW_TAC std_ss [] 1938 >> MATCH_MP_TAC psfis_borel_measurable 1939 >> Q.EXISTS_TAC `x n` >> RW_TAC std_ss []); 1940 1941 1942val SEQ_OFFSET = lemma 1943 (``!f l a. (f o (\n. n + a)) --> l ==> f --> l``, 1944 STRIP_TAC >> STRIP_TAC >> Induct 1945 >> RW_TAC arith_ss [o_DEF, ETA_THM] 1946 >> Q.PAT_X_ASSUM `f o (\n. n + a) --> l ==> f --> l` MATCH_MP_TAC 1947 >> ONCE_REWRITE_TAC [SEQ_SUC] 1948 >> RW_TAC arith_ss [o_DEF, ETA_THM] 1949 >> `!n. a + SUC n = n + SUC a` by (STRIP_TAC >> DECIDE_TAC) 1950 >> POP_ORW 1951 >> RW_TAC std_ss []); 1952 1953 1954val borel_measurable_mon_conv_psfis = store_thm 1955 ("borel_measurable_mon_conv_psfis", 1956 ``!m f. measure_space m /\ f IN borel_measurable (m_space m, measurable_sets m) /\ 1957 (!t. t IN m_space m ==> 0 <= f t) ==> 1958 (?u x. mono_convergent u f (m_space m) /\ (!n. x n IN psfis m (u n)))``, 1959 REPEAT STRIP_TAC 1960 >> Q.ABBREV_TAC `A = (\n i. {w | w IN m_space m /\ & i / (2 pow n) <= f w} INTER 1961 {w | w IN m_space m /\ f w < & (SUC i) / (2 pow n)})` 1962 >> Q.ABBREV_TAC `u = (\n t. REAL_SUM_IMAGE (\i. &i / (2 pow n) * (indicator_fn (A n i) t)) 1963 {i:num | 0 < i /\ &i < (&n * 2 pow n)})` 1964 1965 >> Q.ABBREV_TAC `x = (\n. REAL_SUM_IMAGE (\i. &i / (2 pow n) * measure m (A n i)) 1966 {i:num | 0 < i /\ &i < (&n * 2 pow n)})` 1967 >> Q.EXISTS_TAC `u` >> Q.EXISTS_TAC `x` 1968 >> `!n. FINITE {i | 0 < i /\ & i < & n * 2 pow n}` 1969 by (STRIP_TAC 1970 >> `!i. & i < &n * 2 pow n = i < n * 2 ** n` 1971 by (STRIP_TAC >> `&2 = 2` by RW_TAC real_ss [] >> POP_ORW 1972 >> RW_TAC std_ss [REAL_OF_NUM_POW, REAL_MUL, REAL_LT]) 1973 >> POP_ORW 1974 >> (MATCH_MP_TAC o REWRITE_RULE [FINITE_COUNT] o Q.ISPEC `count (n * 2 ** n)`) SUBSET_FINITE 1975 >> RW_TAC std_ss [SUBSET_DEF, IN_COUNT, GSPECIFICATION]) 1976 >> ONCE_REWRITE_TAC [CONJ_SYM] >> STRONG_CONJ_TAC 1977 >- (STRIP_TAC 1978 >> Q.UNABBREV_TAC `u` >> Q.UNABBREV_TAC `x` 1979 >> RW_TAC std_ss [ETA_THM] 1980 >> `!n t i. & i / 2 pow n = (\i. & i / 2 pow n) i` by RW_TAC std_ss [] >> POP_ORW 1981 >> MATCH_MP_TAC psfis_intro 1982 >> ASM_SIMP_TAC real_ss [POW_POS, REAL_LE_DIV] 1983 >> Q.UNABBREV_TAC `A` 1984 >> RW_TAC std_ss [GSPECIFICATION] 1985 >> `measurable_sets m = subsets (m_space m, measurable_sets m)` by RW_TAC std_ss [subsets_def] 1986 >> POP_ORW 1987 >> MATCH_MP_TAC ALGEBRA_INTER >> CONJ_TAC >- FULL_SIMP_TAC std_ss [measure_space_def, sigma_algebra_def] 1988 >> METIS_TAC [borel_measurable_less_iff, borel_measurable_ge_iff, subsets_def]) 1989 >> STRIP_TAC >> SIMP_TAC std_ss [mono_convergent_def] 1990 >> `!n t i. &i < (&n * 2 pow n) /\ t IN A n i ==> 1991 (u n t = & i / (2 pow n))` 1992 by (REPEAT STRIP_TAC 1993 >> `!j. (~(i = j)) ==> ~(t IN A n j)` 1994 by (REPEAT STRIP_TAC >> Cases_on `i < j` 1995 >- (`f t < & (SUC i) / (2 pow n)` by (Q.UNABBREV_TAC `A` >> FULL_SIMP_TAC std_ss [GSPECIFICATION, IN_INTER]) 1996 >> `&(SUC i) / (2 pow n) <= &j / (2 pow n)` 1997 by (FULL_SIMP_TAC std_ss [LESS_EQ, real_div] >> MATCH_MP_TAC REAL_LE_MUL2 1998 >> RW_TAC real_ss [REAL_LE_INV] 1999 >> `&2 = 2` by RW_TAC real_ss [] >> POP_ORW 2000 >> RW_TAC std_ss [REAL_OF_NUM_POW, REAL_LE_INV, REAL_LE]) 2001 >> Q.UNABBREV_TAC `A` >> FULL_SIMP_TAC std_ss [GSPECIFICATION, IN_INTER] 2002 >> METIS_TAC [REAL_LT_TRANS, REAL_LT_ANTISYM, REAL_LTE_TRANS]) 2003 >> `j < i` by METIS_TAC [LESS_LESS_CASES] 2004 >> `& (SUC j) / (2 pow n) <= &i / (2 pow n)` 2005 by (FULL_SIMP_TAC std_ss [LESS_EQ, real_div] >> MATCH_MP_TAC REAL_LE_MUL2 2006 >> RW_TAC real_ss [REAL_LE_INV] 2007 >> `&2 = 2` by RW_TAC real_ss [] >> POP_ORW 2008 >> RW_TAC std_ss [REAL_OF_NUM_POW, REAL_LE_INV, REAL_LE]) 2009 >> `& i / (2 pow n) <= f t` by (Q.UNABBREV_TAC `A` >> FULL_SIMP_TAC std_ss [GSPECIFICATION, IN_INTER]) 2010 >> Q.UNABBREV_TAC `A` >> FULL_SIMP_TAC std_ss [GSPECIFICATION, IN_INTER, GSYM real_lt] 2011 >> METIS_TAC [REAL_LT_TRANS, REAL_LT_ANTISYM, REAL_LET_TRANS]) 2012 >> `!j. (~(i = j)) ==> (indicator_fn (A n j) t = 0)` by RW_TAC real_ss [indicator_fn_def] 2013 >> Q.UNABBREV_TAC `u` 2014 >> Cases_on `i = 0` 2015 >- (RW_TAC real_ss [] >> Q.PAT_X_ASSUM `!n. FINITE P` (ASSUME_TAC o Q.SPEC `n`) 2016 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 2017 o Q.SPECL [`\i. & i / 2 pow n * indicator_fn (A n i) t`, `0`] o UNDISCH 2018 o Q.SPEC `{i | 0 < i /\ & i < & n * 2 pow n}` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 2019 >> ASM_SIMP_TAC real_ss [DECIDE ``!n:num. 0 < n ==> ~(0 = n)``, GSPECIFICATION]) 2020 >> RW_TAC std_ss [] 2021 >> `{i | 0 < i /\ & i < & n * 2 pow n} = i INSERT {i | 0 < i /\ & i < & n * 2 pow n}` 2022 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INSERT, GSPECIFICATION] 2023 >> METIS_TAC [DECIDE ``!n:num. 0 < n = ~(0 = n)``]) 2024 >> POP_ORW 2025 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM] 2026 >> `FINITE ({i | 0 < i /\ & i < & n * 2 pow n} DELETE i)` by RW_TAC std_ss [FINITE_DELETE] 2027 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 2028 o Q.SPECL [`\i. & i / 2 pow n * indicator_fn (A n i) t`, `0`] o UNDISCH 2029 o Q.SPEC `{i | 0 < i /\ & i < & n * 2 pow n} DELETE i` o INST_TYPE [``:'a``|->``:num``]) 2030 REAL_SUM_IMAGE_FINITE_CONST2 2031 >> ASM_SIMP_TAC real_ss [DECIDE ``!n:num. 0 < n = ~(0 = n)``, GSPECIFICATION, indicator_fn_def]) 2032 >> `!t n. t IN m_space m ==> 2033 u n t <= u (SUC n) t /\ 2034 (f t < & n ==> u n t <= f t) /\ 2035 (f t < & n ==> f t < u n t + 1 / (2 pow n))` 2036 by (NTAC 3 STRIP_TAC 2037 >> `0 <= f t * (2 pow n)` 2038 by (FULL_SIMP_TAC std_ss [nonneg_def] >> `&2 = 2` by RW_TAC real_ss [] 2039 >> POP_ORW >> RW_TAC real_ss [REAL_LE, REAL_OF_NUM_POW, REAL_LE_MUL]) 2040 >> `(\i. f t * 2 pow n < & i) ($LEAST (\i. f t * 2 pow n < & i))` 2041 by (MATCH_MP_TAC LEAST_INTRO >> (MP_TAC o Q.SPEC `1`) REAL_ARCH 2042 >> RW_TAC real_ss []) 2043 >> FULL_SIMP_TAC std_ss [] 2044 >> `0 < ($LEAST (\i. f t * 2 pow n < & i))` 2045 by (ONCE_REWRITE_TAC [GSYM REAL_LT] >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f t * 2 pow n` >> RW_TAC std_ss []) 2046 >> `($LEAST (\i. f t * 2 pow n < & i)) - 1 < ($LEAST (\i. f t * 2 pow n < & i))` 2047 by (POP_ASSUM MP_TAC >> DECIDE_TAC) 2048 >> `~(f t * 2 pow n < &(LEAST i. f t * 2 pow n < & i) - 1)` 2049 by (SPOSE_NOT_THEN STRIP_ASSUME_TAC 2050 >> `~((\i. f t * 2 pow n < & i) ((LEAST i. f t * 2 pow n < & i) - 1))` 2051 by (MATCH_MP_TAC LESS_LEAST >> ASM_REWRITE_TAC []) 2052 >> `& ((LEAST i. f t * 2 pow n < & i) - 1) = & (LEAST i. f t * 2 pow n < & i) - 1` 2053 by (RW_TAC real_ss [REAL_SUB]) 2054 >> FULL_SIMP_TAC real_ss []) 2055 >> `0 < 2 pow n` by (`&2 = 2` by RW_TAC real_ss [] >> POP_ORW 2056 >> RW_TAC std_ss [REAL_OF_NUM_POW, REAL_LE_INV, REAL_LT]) 2057 >> `t IN A n (($LEAST (\i. f t * (2 pow n) < & i)) - 1)` 2058 by (Q.UNABBREV_TAC `A` >> RW_TAC real_ss [IN_INTER, GSPECIFICATION, REAL_LE_LDIV_EQ, REAL_LT_RDIV_EQ, ADD1] 2059 >> `& ((LEAST i. f t * 2 pow n < & i) - 1) = & (LEAST i. f t * 2 pow n < & i) - 1` 2060 by (RW_TAC real_ss [REAL_SUB]) 2061 >> FULL_SIMP_TAC std_ss [real_lt]) 2062 >> `& ((LEAST i. f t * 2 pow n < & i) - 1) = & (LEAST i. f t * 2 pow n < & i) - 1` 2063 by (RW_TAC real_ss [REAL_SUB]) 2064 >> FULL_SIMP_TAC std_ss [] 2065 >> Q.ABBREV_TAC `i = (LEAST i. f t * 2 pow n < & i) - 1` 2066 >> Cases_on `f t < & n` 2067 >- (`&i <= f t * (2 pow n)` 2068 by (Q.UNABBREV_TAC `A` >> FULL_SIMP_TAC std_ss [IN_INTER, GSPECIFICATION, GSYM REAL_LE_LDIV_EQ]) 2069 >> `f t * (2 pow n) < & n * (2 pow n)` by RW_TAC std_ss [REAL_LT_RMUL] 2070 >> `& i < & n * 2 pow n` by METIS_TAC [REAL_LET_TRANS] 2071 >> `i < n * 2**n` 2072 by (`2 = &2` by RW_TAC real_ss [] 2073 >> FULL_SIMP_TAC real_ss [REAL_OF_NUM_POW]) 2074 >> `u n t = & i / (2 pow n)` by RW_TAC std_ss [] 2075 >> `u n t <= f t` by RW_TAC std_ss [REAL_LE_LDIV_EQ] 2076 >> `f t < u n t + 1 / 2 pow n` 2077 by (ASM_SIMP_TAC std_ss [] 2078 >> FULL_SIMP_TAC std_ss [real_div] 2079 >> RW_TAC std_ss [GSYM REAL_ADD_RDISTRIB] 2080 >> RW_TAC std_ss [GSYM real_div, REAL_LT_RDIV_EQ] 2081 >> Q.UNABBREV_TAC `i` >> RW_TAC real_ss []) 2082 >> REVERSE CONJ_TAC >- RW_TAC std_ss [] 2083 >> Cases_on `f t < &(2*i+1)/(2 * (2 pow n))` 2084 >- (RW_TAC std_ss [] 2085 >> `t IN A (n+1) (2 * i)` 2086 by (Q.UNABBREV_TAC `A` >> RW_TAC real_ss [IN_INTER, GSPECIFICATION, ADD1, POW_ADD, POW_1, REAL_MUL_COMM] 2087 >> RW_TAC real_ss [real_div, REAL_INV_MUL, REAL_LT_IMP_NE] 2088 >> ONCE_REWRITE_TAC [GSYM REAL_MUL] 2089 >> `2 * & i * (inv 2 * inv (2 pow n)) = (& i * inv (2 pow n)) * (2 * inv 2)` by REAL_ARITH_TAC 2090 >> POP_ORW >> RW_TAC real_ss [REAL_MUL_RINV] >> RW_TAC std_ss [GSYM real_div, REAL_LE_LDIV_EQ]) 2091 >> `&(2 * i) < & (n + 1) * 2 pow (n+1)` 2092 by (RW_TAC real_ss [POW_ADD] 2093 >> `& (2 * i) = 2 * &i` by RW_TAC real_ss [] >> POP_ORW 2094 >> `& (n + 1) * (2 pow n * 2) = 2 * (& (n + 1) * (2 pow n))` by REAL_ARITH_TAC >> POP_ORW 2095 >> RW_TAC real_ss [REAL_LT_LMUL] 2096 >> MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `& n * 2 pow n` 2097 >> RW_TAC real_ss [REAL_LE_RMUL]) 2098 >> `u (n + 1) t = &(2 * i) / 2 pow (n + 1)` by METIS_TAC [] 2099 >> RW_TAC real_ss [ADD1, POW_ADD, POW_1] 2100 >> RW_TAC real_ss [real_div, REAL_INV_MUL, REAL_LT_IMP_NE] 2101 >> RW_TAC std_ss [GSYM REAL_MUL] 2102 >> `2 * & i * (inv (2 pow n) * inv 2) = (2 * inv 2) * (&i * inv (2 pow n))` by REAL_ARITH_TAC 2103 >> POP_ORW >> RW_TAC real_ss [REAL_MUL_RINV]) 2104 >> `t IN A (n+1) (2*i+1)` 2105 by (Q.UNABBREV_TAC `A` >> RW_TAC real_ss [IN_INTER, GSPECIFICATION, ADD1, POW_ADD, POW_1, REAL_MUL_COMM] 2106 >- FULL_SIMP_TAC std_ss [IN_INTER, GSPECIFICATION, REAL_NOT_LT] 2107 >> FULL_SIMP_TAC std_ss [IN_INTER, GSPECIFICATION] 2108 >> `2 * i + 2 = 2 * (i + 1)` by DECIDE_TAC >> POP_ORW 2109 >> RW_TAC real_ss [real_div, REAL_INV_MUL, REAL_LT_IMP_NE] 2110 >> RW_TAC std_ss [GSYM REAL_MUL] 2111 >> `2 * & (i + 1) * (inv 2 * inv (2 pow n)) = 2112 (2 * inv 2) * (&(i+1) * inv (2 pow n))` by REAL_ARITH_TAC 2113 >> POP_ORW >> RW_TAC real_ss [REAL_MUL_RINV] 2114 >> RW_TAC std_ss [GSYM REAL_ADD, REAL_ADD_RDISTRIB] 2115 >> FULL_SIMP_TAC std_ss [real_div] >> METIS_TAC []) 2116 >> `&(2*i + 1) < & (n+1) * 2 pow (n+1)` 2117 by (RW_TAC std_ss [GSYM REAL_ADD, REAL_ADD_RDISTRIB] 2118 >> MATCH_MP_TAC REAL_LT_ADD2 2119 >> RW_TAC real_ss [POW_ADD, POW_1] 2120 >- (`& n * (2 pow n * 2) = 2 * (&n * 2 pow n)` by REAL_ARITH_TAC 2121 >> POP_ORW >> RW_TAC std_ss [GSYM REAL_MUL] 2122 >> RW_TAC real_ss [REAL_LT_LMUL]) 2123 >> REPEAT (POP_ASSUM (K ALL_TAC)) 2124 >> Induct_on `n` >> RW_TAC real_ss [] 2125 >> MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC `2 pow n * 2` 2126 >> RW_TAC real_ss [REAL_LT_RMUL, REAL_POW_MONO_LT]) 2127 >> `u (n+1) t = &(2*i + 1) / (2 pow (n+1))` by METIS_TAC [] 2128 >> RW_TAC real_ss [ADD1, POW_ADD, POW_1] 2129 >> RW_TAC real_ss [real_div, REAL_INV_MUL, REAL_LT_IMP_NE] 2130 >> RW_TAC std_ss [GSYM REAL_MUL, GSYM REAL_ADD, REAL_ADD_RDISTRIB] 2131 >> `2 * & i * (inv (2 pow n) * inv 2) = (2 * inv 2) * (&i * inv (2 pow n))` by REAL_ARITH_TAC 2132 >> POP_ORW >> RW_TAC real_ss [REAL_MUL_RINV, REAL_LE_ADDR, REAL_LE_MUL, REAL_LE_INV, REAL_LT_IMP_LE]) 2133 >> RW_TAC std_ss [] 2134 >> `u n t = 0` 2135 by (Q.UNABBREV_TAC `u` >> RW_TAC std_ss [] 2136 >> `FINITE {i | 0 < i /\ & i < & n * 2 pow n}` by RW_TAC std_ss [] 2137 >> (MP_TAC o REWRITE_RULE [IN_DELETE, REAL_ENTIRE] 2138 o Q.SPECL [`\i. & i / 2 pow n * indicator_fn (A n i) t`, `0`] o UNDISCH 2139 o Q.SPEC `{i | 0 < i /\ & i < & n * 2 pow n}` o INST_TYPE [``:'a``|->``:num``]) REAL_SUM_IMAGE_FINITE_CONST2 2140 >> RW_TAC real_ss [] >> POP_ASSUM MATCH_MP_TAC 2141 >> RW_TAC std_ss [GSPECIFICATION] 2142 >> Suff `~(t IN A n y)` >- RW_TAC real_ss [indicator_fn_def] 2143 >> Q.UNABBREV_TAC `A` >> FULL_SIMP_TAC std_ss [IN_INTER, GSPECIFICATION] 2144 >> REVERSE (Cases_on `& y / 2 pow n <= f t`) >> RW_TAC std_ss [] 2145 >> FULL_SIMP_TAC std_ss [REAL_NOT_LT] 2146 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `&n` 2147 >> FULL_SIMP_TAC std_ss [REAL_LE_LDIV_EQ, REAL_OF_NUM_POW, REAL_MUL, REAL_LE, REAL_LT] 2148 >> Q.PAT_X_ASSUM `y < n * 2 ** n` MP_TAC >> DECIDE_TAC) 2149 >> RW_TAC real_ss [] >> Q.UNABBREV_TAC `u` >> RW_TAC std_ss [] 2150 >> `!n. 0 < 2 pow n` 2151 by (Induct >> RW_TAC real_ss [] 2152 >> MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC `2 pow n'` 2153 >> RW_TAC real_ss [REAL_POW_MONO_LT]) 2154 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 2155 >> RW_TAC real_ss [REAL_LE_MUL, indicator_fn_def, GSPECIFICATION, REAL_LE_DIV, REAL_LT_IMP_LE]) 2156 >> STRONG_CONJ_TAC 2157 >- (REPEAT STRIP_TAC >> Induct_on `n` >- RW_TAC arith_ss [REAL_LE_REFL] 2158 >> RW_TAC arith_ss [DECIDE ``!(m:num) n. m <= SUC n = ((m = SUC n) \/ m <= n)``] 2159 >- RW_TAC real_ss [] 2160 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `u n x'` >> RW_TAC std_ss []) 2161 >> REPEAT STRIP_TAC 2162 >> `?n0. f x' < & n0` 2163 by ((MP_TAC o Q.SPEC `1`) REAL_ARCH >> RW_TAC real_ss []) 2164 >> `!n. &n0 <= &(n+n0)` by (RW_TAC real_ss [REAL_LE] >> DECIDE_TAC) 2165 >> `!n. f x' < & (n+n0)` by METIS_TAC [REAL_LTE_TRANS] 2166 >> `!n. u (n+n0) x' <= f x'` by METIS_TAC [] 2167 >> `convergent (\n. u (n+n0) x')` 2168 by (MATCH_MP_TAC SEQ_ICONV 2169 >> CONJ_TAC 2170 >- (MATCH_MP_TAC SEQ_BOUNDED_2 >> Q.EXISTS_TAC `0` >> Q.EXISTS_TAC `f x'` 2171 >> RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `u n0 x'` 2172 >> METIS_TAC [psfis_nonneg, nonneg_def, REAL_LE]) 2173 >> RW_TAC std_ss [GREATER_EQ, real_ge]) 2174 >> FULL_SIMP_TAC std_ss [convergent] 2175 >> `l <= f x'` 2176 by (MATCH_MP_TAC SEQ_LE_IMP_LIM_LE >> Q.EXISTS_TAC `(\n. u (n + n0) x')` >> RW_TAC std_ss []) 2177 >> `(\i. u i x') --> l` 2178 by (MATCH_MP_TAC SEQ_OFFSET >> Q.EXISTS_TAC `n0` >> RW_TAC std_ss [o_DEF]) 2179 >> Suff `f x' <= l` >- METIS_TAC [REAL_LE_ANTISYM] 2180 >> `!n. f x' <= u (n+n0) x' + 1/(2 pow (n+n0))` 2181 by METIS_TAC [REAL_LT_IMP_LE] 2182 >> MATCH_MP_TAC LE_SEQ_IMP_LE_LIM 2183 >> Q.EXISTS_TAC `\n. u (n + n0) x' + 1 / 2 pow (n + n0)` 2184 >> RW_TAC std_ss [] 2185 >> `(\n. u (n + n0) x' + 1 / 2 pow (n + n0)) = (\n. (\n. u (n + n0) x') n + (\n. 1 / 2 pow (n+n0)) n)` 2186 by RW_TAC std_ss [] 2187 >> POP_ORW 2188 >> `l = l + 0` by RW_TAC real_ss [] 2189 >> POP_ORW 2190 >> MATCH_MP_TAC SEQ_ADD 2191 >> RW_TAC std_ss [] 2192 >> `(\n. 1 / 2 pow (n + n0)) = (\n. inv ((\n. 2 pow (n+n0)) n))` 2193 by RW_TAC real_ss [real_div] 2194 >> POP_ORW >> MATCH_MP_TAC SEQ_INV0 2195 >> RW_TAC std_ss [GREATER_EQ, real_gt] 2196 >> `?n. y < &n` by ((MP_TAC o Q.SPEC `1`) REAL_ARCH >> RW_TAC real_ss []) 2197 >> Q.EXISTS_TAC `n` 2198 >> RW_TAC std_ss [] 2199 >> MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC `&n` >> RW_TAC std_ss [] 2200 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `&n'` >> RW_TAC std_ss [REAL_LE] 2201 >> MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `2 pow n'` >> RW_TAC std_ss [POW_2_LT] 2202 >> Cases_on `n0 = 0` 2203 >- RW_TAC arith_ss [REAL_LE_REFL] 2204 >> MATCH_MP_TAC REAL_LT_IMP_LE 2205 >> MATCH_MP_TAC REAL_POW_MONO_LT 2206 >> RW_TAC arith_ss [] >> RW_TAC real_ss []); 2207 2208 2209val nnfis_dom_conv = store_thm 2210 ("nnfis_dom_conv", 2211 ``!m f g b. measure_space m /\ 2212 f IN borel_measurable (m_space m, measurable_sets m) /\ 2213 b IN nnfis m g /\ (!t. t IN m_space m ==> f t <= g t) /\ 2214 (!t. t IN m_space m ==> 0 <= f t) ==> 2215 (?a. a IN nnfis m f /\ a <= b)``, 2216 REPEAT STRIP_TAC 2217 >> (MP_TAC o Q.SPECL [`m`, `f`]) borel_measurable_mon_conv_psfis 2218 >> RW_TAC std_ss [] 2219 >> `!n t. t IN m_space m ==> u n t <= f t` 2220 by (REPEAT STRIP_TAC >> FULL_SIMP_TAC std_ss [mono_convergent_def] 2221 >> `u n t = (\n. u n t) n` by RW_TAC std_ss [] >> POP_ORW 2222 >> MATCH_MP_TAC SEQ_MONO_LE 2223 >> RW_TAC std_ss []) 2224 >> `!n. x n IN nnfis m (u n)` by METIS_TAC [psfis_nnfis] 2225 >> `!n. x n <= b` 2226 by (STRIP_TAC >> MATCH_MP_TAC nnfis_mono 2227 >> Q.EXISTS_TAC `(u n)` >> Q.EXISTS_TAC `g` >> Q.EXISTS_TAC `m` 2228 >> RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `f w` 2229 >> RW_TAC std_ss []) 2230 >> `!n n'. n <= n' ==> x n <= x n'` 2231 by (REPEAT STRIP_TAC >> MATCH_MP_TAC psfis_mono 2232 >> Q.EXISTS_TAC `m` >> Q.EXISTS_TAC `(u n)` >> Q.EXISTS_TAC `(u n')` 2233 >> FULL_SIMP_TAC std_ss [mono_convergent_def]) 2234 >> `convergent x` 2235 by (MATCH_MP_TAC SEQ_ICONV 2236 >> CONJ_TAC 2237 >- (MATCH_MP_TAC SEQ_BOUNDED_2 >> Q.EXISTS_TAC `0` >> Q.EXISTS_TAC `b` 2238 >> METIS_TAC [pos_psfis]) 2239 >> RW_TAC std_ss [GREATER_EQ, real_ge]) 2240 >> FULL_SIMP_TAC std_ss [convergent] 2241 >> Q.EXISTS_TAC `l` >> RW_TAC std_ss [nnfis_def, GSPECIFICATION] 2242 >- (Q.EXISTS_TAC `u` >> Q.EXISTS_TAC `x` >> RW_TAC std_ss []) 2243 >> MATCH_MP_TAC SEQ_LE_IMP_LIM_LE 2244 >> Q.EXISTS_TAC `x` >> RW_TAC std_ss []); 2245 2246 2247val nnfis_integral = store_thm 2248 ("nnfis_integral", 2249 ``!m f a. measure_space m /\ a IN nnfis m f ==> 2250 integrable m f /\ (integral m f = a)``, 2251 NTAC 4 STRIP_TAC 2252 >> `!t. t IN m_space m ==> 0 <= f t` by METIS_TAC [nnfis_pos_on_mspace] 2253 >> `a IN nnfis m (pos_part f)` 2254 by (MATCH_MP_TAC nnfis_mon_conv 2255 >> Q.EXISTS_TAC `(\i. f )` >> Q.EXISTS_TAC `(\i. a)` 2256 >> RW_TAC std_ss [REAL_LE_REFL, SEQ_CONST, mono_convergent_def, pos_part_def]) 2257 >> `0 IN nnfis m (neg_part f)` 2258 by (MATCH_MP_TAC nnfis_mon_conv 2259 >> Q.EXISTS_TAC `(\i x. 0)` >> Q.EXISTS_TAC `(\i. 0)` 2260 >> RW_TAC std_ss [REAL_LE_REFL, SEQ_CONST, mono_convergent_def, neg_part_def] 2261 >> MATCH_MP_TAC psfis_nnfis 2262 >> ASM_REWRITE_TAC [] 2263 >> (MP_TAC o Q.SPECL [`m`, `{}`]) psfis_indicator 2264 >> RW_TAC real_ss [indicator_fn_def, NOT_IN_EMPTY, MEASURE_EMPTY] 2265 >> POP_ASSUM MATCH_MP_TAC 2266 >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, subsets_def]) 2267 >> RW_TAC std_ss [integrable_def, integral_def] 2268 >| [Q.EXISTS_TAC `a` >> RW_TAC std_ss [], 2269 Q.EXISTS_TAC `0` >> RW_TAC std_ss [], 2270 Suff `((@i. i IN nnfis m (pos_part f)) = a) /\ 2271 ((@j. j IN nnfis m (neg_part f)) = 0)` 2272 >- RW_TAC real_ss [] 2273 >> CONJ_TAC 2274 >> MATCH_MP_TAC SELECT_UNIQUE 2275 >> METIS_TAC [nnfis_unique]]); 2276 2277 2278val nnfis_minus_nnfis_integral = store_thm 2279 ("nnfis_minus_nnfis_integral", 2280 ``!m f g a b. measure_space m /\ 2281 a IN nnfis m f /\ 2282 b IN nnfis m g ==> 2283 integrable m (\t. f t - g t) /\ 2284 (integral m (\t. f t - g t) = a - b)``, 2285 NTAC 6 STRIP_TAC 2286 >> `(\t. f t - g t) IN borel_measurable (m_space m, measurable_sets m)` 2287 by (MATCH_MP_TAC borel_measurable_sub_borel_measurable 2288 >> METIS_TAC [nnfis_borel_measurable]) 2289 >> `pos_part (\t. f t - g t) IN borel_measurable (m_space m, measurable_sets m) /\ 2290 neg_part (\t. f t - g t) IN borel_measurable (m_space m, measurable_sets m)` 2291 by (MATCH_MP_TAC pos_part_neg_part_borel_measurable >> RW_TAC std_ss []) 2292 >> `nonneg (pos_part (\t. f t - g t)) /\ 2293 nonneg (neg_part (\t. f t - g t))` 2294 by (RW_TAC real_ss [nonneg_def, pos_part_def, neg_part_def] 2295 >> RW_TAC real_ss [GSYM real_lt, REAL_LE, REAL_LE_SUB_LADD, REAL_LT_IMP_LE, REAL_LT_SUB_RADD] 2296 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_IMP_LE]) 2297 >> `a + b IN nnfis m (\t. f t + g t)` by RW_TAC std_ss [nnfis_add] 2298 >> `!t. t IN m_space m ==> 0 <= f t /\ 0 <= g t` by METIS_TAC [nnfis_pos_on_mspace] 2299 2300 >> `!t. t IN m_space m ==> pos_part (\t. f t - g t) t <= (\t. f t + g t) t` 2301 by (RW_TAC real_ss [pos_part_def, GSYM real_lt, REAL_LE_SUB_RADD, REAL_LE_ADD] 2302 >> ONCE_REWRITE_TAC [GSYM REAL_ADD_ASSOC] >> RW_TAC std_ss [REAL_LE_ADDR, REAL_LE_ADD]) 2303 >> `!t. t IN m_space m ==> neg_part (\t. f t - g t) t <= (\t. f t + g t) t` 2304 by (RW_TAC real_ss [neg_part_def, GSYM real_lt, REAL_LE_SUB_RADD, REAL_LE_ADD] 2305 >> FULL_SIMP_TAC std_ss [GSYM real_lt] 2306 >> `f t + g t + f t = g t + (f t + f t)` by REAL_ARITH_TAC >> POP_ORW 2307 >> RW_TAC std_ss [REAL_LE_ADDR, REAL_LE_ADD]) 2308 >> `!t. 0 <= pos_part (\t. f t - g t) t /\ 0 <= neg_part (\t. f t - g t) t` 2309 by (RW_TAC real_ss [pos_part_def, neg_part_def] 2310 >> FULL_SIMP_TAC real_ss [REAL_LE_SUB_LADD, GSYM real_lt, REAL_LT_IMP_LE, REAL_LT_SUB_RADD]) 2311 >> (MP_TAC o Q.SPECL [`m`, `(pos_part (\t. f t - g t))`, `(\t. f t + g t)`, `a+b`]) nnfis_dom_conv 2312 >> (MP_TAC o Q.SPECL [`m`, `(neg_part (\t. f t - g t))`, `(\t. f t + g t)`, `a+b`]) nnfis_dom_conv 2313 >> ASM_SIMP_TAC std_ss [nonneg_def] 2314 >> NTAC 2 STRIP_TAC >> CONJ_TAC 2315 >- (RW_TAC std_ss [integrable_def] 2316 >- (Q.EXISTS_TAC `a''` >> RW_TAC std_ss []) 2317 >> Q.EXISTS_TAC `a'` >> RW_TAC std_ss []) 2318 >> `a + a' IN nnfis m (\t. f t + (neg_part (\t. f t - g t)) t)` 2319 by (MATCH_MP_TAC nnfis_add >> RW_TAC std_ss []) 2320 >> `b + a'' IN nnfis m (\t. g t + (pos_part (\t. f t - g t)) t)` 2321 by (MATCH_MP_TAC nnfis_add >> RW_TAC std_ss []) 2322 >> `(\t. f t + neg_part (\t. f t - g t) t) = 2323 (\t. g t + pos_part (\t. f t - g t) t)` 2324 by (RW_TAC std_ss [Once FUN_EQ_THM, neg_part_def, pos_part_def] 2325 >> RW_TAC real_ss []) 2326 >> FULL_SIMP_TAC std_ss [] 2327 >> `a + a' = b + a''` 2328 by (MATCH_MP_TAC nnfis_unique 2329 >> Q.EXISTS_TAC `(\t. g t + pos_part (\t. f t - g t) t)` 2330 >> Q.EXISTS_TAC `m` 2331 >> RW_TAC std_ss []) 2332 >> `a - b = a'' - a'` 2333 by (RW_TAC std_ss [REAL_EQ_SUB_RADD] 2334 >> `a'' - a' + b = (a'' + b) - a'` by REAL_ARITH_TAC 2335 >> POP_ORW 2336 >> RW_TAC std_ss [REAL_EQ_SUB_LADD, REAL_ADD_COMM]) 2337 >> RW_TAC std_ss [integral_def] 2338 >> Suff `((@i. i IN nnfis m (pos_part (\t. f t - g t))) = a'') /\ 2339 ((@j. j IN nnfis m (neg_part (\t. f t - g t))) = a')` 2340 >- RW_TAC std_ss [] 2341 >> CONJ_TAC 2342 >> MATCH_MP_TAC SELECT_UNIQUE 2343 >> METIS_TAC [nnfis_unique]); 2344 2345 2346val integral_borel_measurable = store_thm 2347 ("integral_borel_measurable", 2348 ``!m f. integrable m f ==> 2349 f IN borel_measurable (m_space m, measurable_sets m)``, 2350 RW_TAC std_ss [integrable_def] 2351 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPECL [`f`, `m`]) pos_part_neg_part_borel_measurable_iff] 2352 >> METIS_TAC [nnfis_borel_measurable]); 2353 2354 2355val integral_indicator_fn = store_thm 2356 ("integral_indicator_fn", 2357 ``!m a. measure_space m /\ a IN measurable_sets m ==> 2358 (integral m (indicator_fn a) = (measure m a)) /\ 2359 integrable m (indicator_fn a)``, 2360 METIS_TAC [psfis_indicator, psfis_nnfis, nnfis_integral]); 2361 2362 2363val integral_add = store_thm 2364 ("integral_add", 2365 ``!m f g. integrable m f /\ integrable m g ==> 2366 integrable m (\t. f t + g t) /\ 2367 (integral m (\t. f t + g t) = integral m f + integral m g)``, 2368 NTAC 4 STRIP_TAC 2369 >> NTAC 2 (POP_ASSUM (MP_TAC o REWRITE_RULE [integrable_def])) 2370 >> NTAC 2 STRIP_TAC 2371 >> Q.ABBREV_TAC `u = (\t. pos_part f t + pos_part g t)` 2372 >> Q.ABBREV_TAC `v = (\t. neg_part f t + neg_part g t)` 2373 >> `x + x' IN nnfis m u` 2374 by (Q.UNABBREV_TAC `u` >> MATCH_MP_TAC nnfis_add >> RW_TAC std_ss []) 2375 >> `y + y' IN nnfis m v` 2376 by (Q.UNABBREV_TAC `v` >> MATCH_MP_TAC nnfis_add >> RW_TAC std_ss []) 2377 >> `!f. (\t. pos_part f t - neg_part f t) = f` 2378 by (RW_TAC real_ss [pos_part_def, neg_part_def, Once FUN_EQ_THM] 2379 >> RW_TAC real_ss []) 2380 >> `integral m f = x - y` 2381 by ((MP_TAC o Q.SPECL [`m`, `pos_part f`, `neg_part f`, `x`, `y`]) nnfis_minus_nnfis_integral 2382 >> RW_TAC std_ss []) 2383 >> `integral m g = x' - y'` 2384 by ((MP_TAC o Q.SPECL [`m`, `pos_part g`, `neg_part g`, `x'`, `y'`]) nnfis_minus_nnfis_integral 2385 >> RW_TAC std_ss []) 2386 >> `(\t. f t + g t) = (\t. u t - v t)` 2387 by (Q.UNABBREV_TAC `u` >> Q.UNABBREV_TAC `v` 2388 >> RW_TAC real_ss [Once FUN_EQ_THM] 2389 >> `pos_part f t + pos_part g t - (neg_part f t + neg_part g t) = 2390 (\t. pos_part f t - neg_part f t) t + (\t. pos_part g t - neg_part g t) t` 2391 by (RW_TAC std_ss [] >> REAL_ARITH_TAC) 2392 >> ASM_SIMP_TAC std_ss [] 2393 >> FULL_SIMP_TAC std_ss [FUN_EQ_THM]) 2394 >> ASM_SIMP_TAC std_ss [] 2395 >> `x - y + (x' - y') = (x + x') - (y + y')` by REAL_ARITH_TAC 2396 >> POP_ORW 2397 >> MATCH_MP_TAC nnfis_minus_nnfis_integral 2398 >> RW_TAC std_ss []); 2399 2400 2401val integral_mono = store_thm 2402 ("integral_mono", 2403 ``!m f g. integrable m f /\ integrable m g /\ 2404 (!t. t IN m_space m ==> f t <= g t) ==> 2405 integral m f <= integral m g``, 2406 RW_TAC std_ss [integrable_def] 2407 >> `!f. (\t. pos_part f t - neg_part f t) = f` 2408 by (RW_TAC real_ss [pos_part_def, neg_part_def, Once FUN_EQ_THM] 2409 >> RW_TAC real_ss []) 2410 >> `integral m f = x - y` 2411 by ((MP_TAC o Q.SPECL [`m`, `pos_part f`, `neg_part f`, `x`, `y`]) nnfis_minus_nnfis_integral 2412 >> RW_TAC std_ss []) 2413 >> `integral m g = x' - y'` 2414 by ((MP_TAC o Q.SPECL [`m`, `pos_part g`, `neg_part g`, `x'`, `y'`]) nnfis_minus_nnfis_integral 2415 >> RW_TAC std_ss []) 2416 >> ASM_REWRITE_TAC [REAL_LE_SUB_RADD] 2417 >> `x' - y' + y = (x' + y) - y'` by REAL_ARITH_TAC >> POP_ORW >> RW_TAC std_ss [REAL_LE_SUB_LADD] 2418 >> MATCH_MP_TAC REAL_LE_ADD2 2419 >> CONJ_TAC 2420 >- (MATCH_MP_TAC nnfis_mono >> Q.EXISTS_TAC `pos_part f` >> Q.EXISTS_TAC `pos_part g` >> Q.EXISTS_TAC `m` 2421 >> RW_TAC real_ss [pos_part_def] 2422 >> METIS_TAC [REAL_LE_TRANS]) 2423 >> MATCH_MP_TAC nnfis_mono >> Q.EXISTS_TAC `neg_part g` >> Q.EXISTS_TAC `neg_part f` >> Q.EXISTS_TAC `m` 2424 >> RW_TAC real_ss [neg_part_def] 2425 >> METIS_TAC [REAL_LE_TRANS, REAL_LE_NEGTOTAL]); 2426 2427 2428val integral_times = store_thm 2429 ("integral_times", 2430 ``!m f a. integrable m f ==> 2431 integrable m (\t. a * f t) /\ 2432 (integral m (\t. a * f t) = a * integral m f)``, 2433 NTAC 4 STRIP_TAC >> POP_ASSUM (MP_TAC o REWRITE_RULE [integrable_def]) 2434 >> STRIP_TAC 2435 >> Cases_on `0 <= a` 2436 >- (`a * x IN nnfis m (pos_part (\t. a * f t))` 2437 by (`pos_part (\t. a * f t) = (\t. a * pos_part f t)` 2438 by (RW_TAC real_ss [FUN_EQ_THM, pos_part_def] >> RW_TAC real_ss [] 2439 >- (Cases_on `a = 0` >- RW_TAC real_ss [] 2440 >> METIS_TAC [GSYM REAL_LE_LDIV_EQ, REAL_LT_LE, REAL_DIV_LZERO, REAL_MUL_COMM]) 2441 >> METIS_TAC [REAL_LE_MUL]) 2442 >> POP_ORW 2443 >> MATCH_MP_TAC nnfis_times >> RW_TAC std_ss []) 2444 >> `a * y IN nnfis m (neg_part (\t. a * f t))` 2445 by (`neg_part (\t. a * f t) = (\t. a * neg_part f t)` 2446 by (RW_TAC real_ss [FUN_EQ_THM, neg_part_def] >> RW_TAC real_ss [] 2447 >- (Cases_on `a = 0` >- RW_TAC real_ss [] 2448 >> METIS_TAC [GSYM REAL_LE_LDIV_EQ, REAL_LT_LE, REAL_DIV_LZERO, REAL_MUL_COMM]) 2449 >> METIS_TAC [REAL_LE_MUL]) 2450 >> POP_ORW 2451 >> MATCH_MP_TAC nnfis_times >> RW_TAC std_ss []) 2452 >> ASM_SIMP_TAC std_ss [integrable_def, integral_def] 2453 >> CONJ_TAC >- (CONJ_TAC >- (Q.EXISTS_TAC `a * x` >> RW_TAC std_ss []) 2454 >> Q.EXISTS_TAC `a * y` >> RW_TAC std_ss []) 2455 >> `(@i. i IN nnfis m (pos_part (\t. a * f t))) = a * x` 2456 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2457 >> POP_ORW 2458 >> `(@j. j IN nnfis m (neg_part (\t. a * f t))) = a * y` 2459 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2460 >> POP_ORW 2461 >> `(@i. i IN nnfis m (pos_part f)) = x` 2462 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2463 >> POP_ORW 2464 >> `(@j. j IN nnfis m (neg_part f)) = y` 2465 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2466 >> POP_ORW 2467 >> RW_TAC std_ss [REAL_SUB_LDISTRIB]) 2468 >> `0 <= ~a` by METIS_TAC [REAL_LE_NEGTOTAL] 2469 >> `(pos_part (\t. a * f t) = (\t. ~a * neg_part f t)) /\ 2470 (neg_part (\t. a * f t) = (\t. ~a * pos_part f t))` 2471 by METIS_TAC [REAL_NEG_GE0, real_pos_part_neg_part_neg_times] 2472 >> `~a * x IN nnfis m (neg_part (\t. a * f t))` 2473 by (ASM_SIMP_TAC std_ss [] >> MATCH_MP_TAC nnfis_times >> RW_TAC std_ss []) 2474 >> `~a * y IN nnfis m (pos_part (\t. a * f t))` 2475 by (ASM_SIMP_TAC std_ss [] >> MATCH_MP_TAC nnfis_times >> RW_TAC std_ss []) 2476 >> ASM_SIMP_TAC std_ss [integrable_def, integral_def] 2477 >> Q.PAT_X_ASSUM `P = Q` (MP_TAC o GSYM) 2478 >> Q.PAT_X_ASSUM `P = Q` (MP_TAC o GSYM) 2479 >> STRIP_TAC >> STRIP_TAC 2480 >> CONJ_TAC >- (CONJ_TAC >- (Q.EXISTS_TAC `~a * y` >> RW_TAC std_ss []) 2481 >> Q.EXISTS_TAC `~a * x` >> RW_TAC std_ss []) 2482 >> ASM_REWRITE_TAC [] 2483 >> `(@j. j IN nnfis m (neg_part (\t. a * f t))) = ~a * x` 2484 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2485 >> POP_ORW 2486 >> `(@i. i IN nnfis m (pos_part (\t. a * f t))) = ~a * y` 2487 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2488 >> POP_ORW 2489 >> `(@i. i IN nnfis m (pos_part f)) = x` 2490 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2491 >> POP_ORW 2492 >> `(@j. j IN nnfis m (neg_part f)) = y` 2493 by (MATCH_MP_TAC SELECT_UNIQUE >> METIS_TAC [nnfis_unique]) 2494 >> POP_ORW 2495 >> RW_TAC real_ss [REAL_SUB_LDISTRIB, REAL_ADD_COMM, GSYM real_sub]); 2496 2497 2498val markov_ineq = store_thm 2499 ("markov_ineq", 2500 ``!m f a n. integrable m f /\ 0 < a /\ integrable m (\x. (abs (f x)) pow n) ==> 2501 measure m ((PREIMAGE f {y | a <= y}) INTER m_space m) <= 2502 (integral m (\x. (abs (f x)) pow n)) / (a pow n)``, 2503 REPEAT STRIP_TAC 2504 >> `0 < a pow n` by (Cases_on `n` >> RW_TAC real_ss [POW_POS_LT]) 2505 >> RW_TAC real_ss [REAL_LE_RDIV_EQ] 2506 >> ONCE_REWRITE_TAC [REAL_MUL_COMM] 2507 >> `f IN borel_measurable (m_space m, measurable_sets m)` 2508 by METIS_TAC [integral_borel_measurable] 2509 >> `measure_space m` by FULL_SIMP_TAC std_ss [integrable_def] 2510 >> `{w | w IN m_space m /\ a <= f w} IN measurable_sets m` 2511 by FULL_SIMP_TAC std_ss [borel_measurable_ge_iff] 2512 >> `(a pow n) * (measure m ((PREIMAGE f {y | a <= y}) INTER m_space m)) = 2513 (a pow n) * measure m {w | w IN m_space m /\ a <= f w}` 2514 by RW_TAC std_ss [PREIMAGE_def, GSPECIFICATION, INTER_DEF, CONJ_COMM] 2515 >> POP_ORW 2516 >> `integrable m (indicator_fn {w | w IN m_space m /\ a <= f w}) /\ 2517 ((a pow n) * measure m {w | w IN m_space m /\ a <= f w} = 2518 (a pow n) * integral m (indicator_fn {w | w IN m_space m /\ a <= f w}))` 2519 by ((MP_TAC o Q.SPECL [`m`, `{w | w IN m_space m /\ a <= f w}`]) integral_indicator_fn 2520 >> ASM_SIMP_TAC std_ss []) 2521 >> POP_ORW 2522 >> `a pow n * integral m (indicator_fn {w | w IN m_space m /\ a <= f w}) = 2523 integral m (\t. a pow n * (indicator_fn {w | w IN m_space m /\ a <= f w}) t)` 2524 by METIS_TAC [integral_times] 2525 >> POP_ORW 2526 >> MATCH_MP_TAC integral_mono 2527 >> ASM_SIMP_TAC std_ss [] 2528 >> CONJ_TAC 2529 >- METIS_TAC [integral_times] 2530 >> REPEAT STRIP_TAC 2531 >> REVERSE (Cases_on `a <= f t`) 2532 >- RW_TAC real_ss [indicator_fn_def, GSPECIFICATION, POW_POS, ABS_POS] 2533 >> `abs (f t) pow n = abs (f t) pow n * 1` by RW_TAC real_ss [] 2534 >> POP_ORW >> MATCH_MP_TAC REAL_LE_MUL2 2535 >> RW_TAC real_ss [REAL_LT_IMP_LE, indicator_fn_def, GSPECIFICATION] 2536 >> MATCH_MP_TAC POW_LE 2537 >> `0 <= f t` by METIS_TAC [REAL_LE_TRANS, REAL_LT_IMP_LE] 2538 >> RW_TAC real_ss [abs, REAL_LT_IMP_LE]); 2539 2540 2541val finite_space_integral_reduce = store_thm 2542 ("finite_space_integral_reduce", 2543 ``!m f. measure_space m /\ 2544 f IN borel_measurable (m_space m, measurable_sets m) /\ 2545 FINITE (m_space m) ==> 2546 (integral m f = 2547 finite_space_integral m f)``, 2548 REPEAT STRIP_TAC 2549 >> `?c n. BIJ c (count n) (IMAGE f (m_space m))` by RW_TAC std_ss [GSYM FINITE_BIJ_COUNT_EQ, IMAGE_FINITE] 2550 >> `pos_simple_fn m (pos_part f) 2551 (count n) (\i. PREIMAGE f {c i} INTER m_space m) (\i. if 0 <= c i then c i else 0) /\ 2552 pos_simple_fn m (neg_part f) 2553 (count n) (\i. PREIMAGE f {c i} INTER m_space m) (\i. if c i <= 0 then ~ c i else 0)` 2554 by (RW_TAC std_ss [pos_simple_fn_def, FINITE_COUNT] 2555 >| [RW_TAC real_ss [pos_part_def], 2556 `FINITE (count n)` by RW_TAC std_ss [FINITE_COUNT] 2557 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n`) REAL_SUM_IMAGE_IN_IF] 2558 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2559 >> `?i. i IN count n /\ (f t = c i)` by METIS_TAC [] 2560 >> `(\x. (if x IN count n then (if 0 <= c x then c x else 0) * 2561 indicator_fn (PREIMAGE f {c x} INTER m_space m) t else 0)) = 2562 (\x. if (x = i) /\ 0 <= c i then c i else 0)` 2563 by (RW_TAC std_ss [FUN_EQ_THM] 2564 >> RW_TAC real_ss [indicator_fn_def, IN_PREIMAGE, IN_INTER] 2565 >> FULL_SIMP_TAC real_ss [IN_SING] 2566 >> METIS_TAC []) 2567 >> POP_ORW 2568 >> `count n = i INSERT ((count n) DELETE i)` 2569 by (RW_TAC std_ss [EXTENSION, IN_INSERT, IN_DELETE] >> METIS_TAC []) 2570 >> POP_ORW 2571 >> ASM_SIMP_TAC std_ss [FINITE_INSERT, FINITE_DELETE, FINITE_COUNT, 2572 REAL_SUM_IMAGE_THM, DELETE_DELETE] 2573 >> `FINITE (count n DELETE i)` by RW_TAC std_ss [FINITE_COUNT, FINITE_DELETE] 2574 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n DELETE i`) REAL_SUM_IMAGE_IN_IF] 2575 >> SIMP_TAC std_ss [IN_DELETE] 2576 >> (MP_TAC o Q.SPECL [`\x.0`, `0`] o UNDISCH o Q.ISPEC `count n DELETE i`) 2577 REAL_SUM_IMAGE_FINITE_CONST 2578 >> RW_TAC real_ss [pos_part_def], 2579 `PREIMAGE f {c i} INTER m_space m = 2580 {w | w IN m_space m /\ (f w = (\n. c i) w)}` 2581 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, GSPECIFICATION, CONJ_SYM]) 2582 >> POP_ORW 2583 >> MATCH_MP_TAC borel_measurable_eq_borel_measurable 2584 >> METIS_TAC [borel_measurable_const, measure_space_def], 2585 RW_TAC real_ss [], 2586 RW_TAC std_ss [DISJOINT_DEF] 2587 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, NOT_IN_EMPTY, IN_PREIMAGE, IN_SING] 2588 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] >> METIS_TAC [], 2589 ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_INTER, IN_PREIMAGE, IN_SING] 2590 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2591 >> METIS_TAC [], 2592 RW_TAC real_ss [neg_part_def, REAL_LT_IMP_LE, REAL_LE_RNEG] 2593 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_IMP_LE], 2594 `FINITE (count n)` by RW_TAC std_ss [FINITE_COUNT] 2595 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n`) REAL_SUM_IMAGE_IN_IF] 2596 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2597 >> `?i. i IN count n /\ (f t = c i)` by METIS_TAC [] 2598 >> `(\x. (if x IN count n then (if c x <= 0 then ~ c x else 0) * 2599 indicator_fn (PREIMAGE f {c x} INTER m_space m) t else 0)) = 2600 (\x. if (x = i) /\ c i <= 0 then ~ c i else 0)` 2601 by (RW_TAC std_ss [FUN_EQ_THM] 2602 >> RW_TAC real_ss [indicator_fn_def, IN_PREIMAGE, IN_INTER] 2603 >> FULL_SIMP_TAC real_ss [IN_SING] 2604 >> METIS_TAC []) 2605 >> POP_ORW 2606 >> `count n = i INSERT ((count n) DELETE i)` 2607 by (RW_TAC std_ss [EXTENSION, IN_INSERT, IN_DELETE] >> METIS_TAC []) 2608 >> POP_ORW 2609 >> ASM_SIMP_TAC std_ss [FINITE_INSERT, FINITE_DELETE, FINITE_COUNT, 2610 REAL_SUM_IMAGE_THM, DELETE_DELETE] 2611 >> `FINITE (count n DELETE i)` by RW_TAC std_ss [FINITE_COUNT, FINITE_DELETE] 2612 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n DELETE i`) REAL_SUM_IMAGE_IN_IF] 2613 >> SIMP_TAC std_ss [IN_DELETE] 2614 >> (MP_TAC o Q.SPECL [`\x.0`, `0`] o UNDISCH o Q.ISPEC `count n DELETE i`) 2615 REAL_SUM_IMAGE_FINITE_CONST 2616 >> RW_TAC real_ss [neg_part_def] >> METIS_TAC [real_lt, REAL_LT_ANTISYM, REAL_LE_ANTISYM, REAL_NEG_0], 2617 `PREIMAGE f {c i} INTER m_space m = 2618 {w | w IN m_space m /\ (f w = (\n. c i) w)}` 2619 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, GSPECIFICATION, CONJ_SYM]) 2620 >> POP_ORW 2621 >> MATCH_MP_TAC borel_measurable_eq_borel_measurable 2622 >> METIS_TAC [borel_measurable_const, measure_space_def], 2623 RW_TAC real_ss [REAL_LE_RNEG], 2624 RW_TAC std_ss [DISJOINT_DEF] 2625 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, NOT_IN_EMPTY, IN_PREIMAGE, IN_SING] 2626 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] >> METIS_TAC [], 2627 ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_INTER, IN_PREIMAGE, IN_SING] 2628 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2629 >> METIS_TAC []]) 2630 >> RW_TAC std_ss [finite_space_integral_def] 2631 >> `pos_simple_fn_integral m (count n) (\i. PREIMAGE f {c i} INTER m_space m) (\i. (if 0 <= c i then c i else 0)) 2632 IN nnfis m (pos_part f)` 2633 by (MATCH_MP_TAC psfis_nnfis 2634 >> RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 2635 >> Q.EXISTS_TAC `((count n), (\i. PREIMAGE f {c i} INTER m_space m), (\i. (if 0 <= c i then c i else 0)))` 2636 >> RW_TAC std_ss [] 2637 >> Q.EXISTS_TAC `((count n), (\i. PREIMAGE f {c i} INTER m_space m), (\i. (if 0 <= c i then c i else 0)))` 2638 >> RW_TAC std_ss []) 2639 >> `pos_simple_fn_integral m (count n) (\i. PREIMAGE f {c i} INTER m_space m) (\i. (if c i <= 0 then ~ c i else 0)) 2640 IN nnfis m (neg_part f)` 2641 by (MATCH_MP_TAC psfis_nnfis 2642 >> RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 2643 >> Q.EXISTS_TAC `((count n), (\i. PREIMAGE f {c i} INTER m_space m), (\i. (if c i <= 0 then ~ c i else 0)))` 2644 >> RW_TAC std_ss [] 2645 >> Q.EXISTS_TAC `((count n), (\i. PREIMAGE f {c i} INTER m_space m), (\i. (if c i <= 0 then ~ c i else 0)))` 2646 >> RW_TAC std_ss []) 2647 >> `!f. (\t. pos_part f t - neg_part f t) = f` 2648 by (RW_TAC real_ss [pos_part_def, neg_part_def, Once FUN_EQ_THM] 2649 >> RW_TAC real_ss []) 2650 >> (MP_TAC o Q.SPECL [`m`, `pos_part f`, `neg_part f`, 2651 `pos_simple_fn_integral m (count n) (\i. PREIMAGE f {c i} INTER m_space m) (\i. (if 0 <= c i then c i else 0))`, 2652 `pos_simple_fn_integral m (count n) (\i. PREIMAGE f {c i} INTER m_space m) (\i. (if c i <= 0 then ~ c i else 0))`]) 2653 nnfis_minus_nnfis_integral 2654 >> RW_TAC std_ss [pos_simple_fn_integral_def, real_sub] 2655 >> `!x. ~x = ~1 * x` by RW_TAC real_ss [] >> POP_ORW 2656 >> RW_TAC std_ss [GSYM REAL_SUM_IMAGE_CMUL, FINITE_COUNT, GSYM REAL_SUM_IMAGE_ADD] 2657 >> `(\i. 2658 (if 0 <= c i then c i else 0) * measure m (PREIMAGE f {c i} INTER m_space m) + 2659 ~1 * 2660 ((if c i <= 0 then ~c i else 0) * measure m (PREIMAGE f {c i} INTER m_space m))) = 2661 (\i. c i * measure m (PREIMAGE f {c i} INTER m_space m))` 2662 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [] 2663 >> METIS_TAC [REAL_LE_TOTAL, REAL_LE_ANTISYM, REAL_MUL_LZERO, REAL_ADD_RID]) 2664 >> POP_ORW 2665 >> `FINITE (count n)` by RW_TAC std_ss [FINITE_COUNT] 2666 >> (MP_TAC o Q.ISPEC `c:num->real` o UNDISCH o Q.ISPEC `count n` o GSYM) REAL_SUM_IMAGE_IMAGE 2667 >> Know `INJ c (count n) (IMAGE c (count n))` 2668 >- (FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, IN_IMAGE] >> METIS_TAC []) 2669 >> SIMP_TAC std_ss [] >> STRIP_TAC >> STRIP_TAC 2670 >> POP_ASSUM (MP_TAC o Q.SPEC `(\x:real. x * measure m (PREIMAGE f {x} INTER m_space m))`) 2671 >> RW_TAC std_ss [o_DEF] 2672 >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM (K ALL_TAC) 2673 >> `(IMAGE c (count n)) = (IMAGE f (m_space m))` 2674 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE] 2675 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2676 >> METIS_TAC []) 2677 >> RW_TAC std_ss []); 2678 2679 2680val integral_cmul_indicator = store_thm 2681 ("integral_cmul_indicator", 2682 ``!m s c. measure_space m /\ s IN measurable_sets m ==> 2683 (integral m (\x. c * indicator_fn s x) = c * (measure m s))``, 2684 METIS_TAC [integral_times, integral_indicator_fn]); 2685 2686 2687val integral_zero = store_thm 2688 ("integral_zero", 2689 ``!m. measure_space m ==> (integral m (\x. 0) = 0)``, 2690 REPEAT STRIP_TAC 2691 >> (MP_TAC o Q.SPECL [`m`, `{}`, `0`]) integral_cmul_indicator 2692 >> ASM_SIMP_TAC real_ss [] >> FULL_SIMP_TAC std_ss [measure_space_def, SIGMA_ALGEBRA, subsets_def]); 2693 2694 2695val finite_integral_on_set = store_thm 2696 ("finite_integral_on_set", 2697 ``!m f a. measure_space m /\ FINITE (m_space m) /\ 2698 f IN borel_measurable (m_space m, measurable_sets m) /\ a IN measurable_sets m ==> 2699 (integral m (\x. f x * indicator_fn a x) = 2700 SIGMA (\r. r * measure m (PREIMAGE f {r} INTER a)) (IMAGE f a))``, 2701 REPEAT STRIP_TAC 2702 >> (MP_TAC o Q.SPECL [`m`, `(\x. f x * indicator_fn a x)`]) finite_space_integral_reduce 2703 >> `(\x. f x * indicator_fn a x) IN borel_measurable (m_space m,measurable_sets m)` 2704 by (MATCH_MP_TAC borel_measurable_times_borel_measurable 2705 >> ASM_SIMP_TAC std_ss [] 2706 >> MATCH_MP_TAC borel_measurable_indicator 2707 >> FULL_SIMP_TAC std_ss [measure_space_def, subsets_def]) 2708 >> `a SUBSET m_space m` by METIS_TAC [MEASURABLE_SETS_SUBSET_SPACE] 2709 >> RW_TAC std_ss [finite_space_integral_def] 2710 >> `FINITE a` by METIS_TAC [SUBSET_FINITE] 2711 >> Cases_on `0 IN (IMAGE f a)` 2712 >- (`(IMAGE f a) = 2713 0 INSERT (IMAGE f a)` 2714 by METIS_TAC [IN_INSERT, EXTENSION] 2715 >> POP_ORW 2716 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, FINITE_INSERT, IMAGE_FINITE] 2717 >> `0 IN (IMAGE (\x. f x * indicator_fn a x) (m_space m))` 2718 by (FULL_SIMP_TAC std_ss [IN_IMAGE] >> Q.EXISTS_TAC `x` 2719 >> RW_TAC real_ss [indicator_fn_def] 2720 >> `a SUBSET m_space m` 2721 by METIS_TAC [MEASURABLE_SETS_SUBSET_SPACE] 2722 >> FULL_SIMP_TAC std_ss [SUBSET_DEF]) 2723 >> `(IMAGE (\x. f x * indicator_fn a x) (m_space m)) = 2724 0 INSERT (IMAGE (\x. f x * indicator_fn a x) (m_space m))` 2725 by METIS_TAC [IN_INSERT, EXTENSION] 2726 >> POP_ORW 2727 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, FINITE_INSERT, IMAGE_FINITE] 2728 >> `(IMAGE (\x. f x * indicator_fn a x) (m_space m) DELETE 0) = 2729 (IMAGE f a DELETE 0)` 2730 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_IMAGE, IN_DELETE, indicator_fn_def] 2731 >> Cases_on `x = 0` >> RW_TAC real_ss [] 2732 >> EQ_TAC >> RW_TAC real_ss [REAL_ENTIRE] 2733 >> Q.EXISTS_TAC `x'` >> Cases_on `x' IN a` >> FULL_SIMP_TAC real_ss [REAL_ENTIRE, SUBSET_DEF]) 2734 >> POP_ORW 2735 >> ASM_SIMP_TAC std_ss [Once REAL_SUM_IMAGE_IN_IF, FINITE_DELETE, IMAGE_FINITE] 2736 >> `(\r. (if r IN IMAGE f a DELETE 0 then 2737 r * measure m (PREIMAGE (\x. f x * indicator_fn a x) {r} INTER m_space m) 2738 else 0)) = 2739 (\r. if r IN IMAGE f a DELETE 0 then 2740 (\r. r * measure m (PREIMAGE f {r} INTER a)) r 2741 else 0)` 2742 by (RW_TAC real_ss [FUN_EQ_THM, IN_DELETE, IN_IMAGE] 2743 >> RW_TAC real_ss [indicator_fn_def] 2744 >> Suff `(PREIMAGE (\x. f x * (if x IN a then 1 else 0)) {f x} INTER m_space m) = 2745 (PREIMAGE f {f x} INTER a)` 2746 >- RW_TAC std_ss [] 2747 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_INTER, IN_PREIMAGE, IN_SING] 2748 >> Cases_on `x' IN a` >> RW_TAC real_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF]) 2749 >> POP_ORW 2750 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF, FINITE_DELETE, IMAGE_FINITE]) 2751 >> `IMAGE f a = (IMAGE f a) DELETE 0` 2752 by METIS_TAC [DELETE_NON_ELEMENT] 2753 >> POP_ORW 2754 >> Cases_on `0 IN (IMAGE (\x. f x * indicator_fn a x) (m_space m))` 2755 >- (`(IMAGE (\x. f x * indicator_fn a x) (m_space m)) = 2756 0 INSERT (IMAGE (\x. f x * indicator_fn a x) (m_space m))` 2757 by METIS_TAC [IN_INSERT, EXTENSION] 2758 >> POP_ORW 2759 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, FINITE_INSERT, IMAGE_FINITE] 2760 >> `(IMAGE (\x. f x * indicator_fn a x) (m_space m) DELETE 0) = 2761 (IMAGE f a DELETE 0)` 2762 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_IMAGE, IN_DELETE, indicator_fn_def] 2763 >> Cases_on `x = 0` >> RW_TAC real_ss [] 2764 >> EQ_TAC >> RW_TAC real_ss [REAL_ENTIRE] 2765 >> Q.EXISTS_TAC `x'` >> Cases_on `x' IN a` >> FULL_SIMP_TAC real_ss [REAL_ENTIRE, SUBSET_DEF]) 2766 >> POP_ORW 2767 >> ASM_SIMP_TAC std_ss [Once REAL_SUM_IMAGE_IN_IF, FINITE_DELETE, IMAGE_FINITE] 2768 >> `(\r. (if r IN IMAGE f a DELETE 0 then 2769 r * measure m (PREIMAGE (\x. f x * indicator_fn a x) {r} INTER m_space m) 2770 else 0)) = 2771 (\r. if r IN IMAGE f a DELETE 0 then 2772 (\r. r * measure m (PREIMAGE f {r} INTER a)) r 2773 else 0)` 2774 by (RW_TAC real_ss [FUN_EQ_THM, IN_DELETE, IN_IMAGE] 2775 >> RW_TAC real_ss [indicator_fn_def] 2776 >> Suff `(PREIMAGE (\x. f x * (if x IN a then 1 else 0)) {f x} INTER m_space m) = 2777 (PREIMAGE f {f x} INTER a)` 2778 >- RW_TAC std_ss [] 2779 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_INTER, IN_PREIMAGE, IN_SING] 2780 >> Cases_on `x' IN a` >> RW_TAC real_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF]) 2781 >> POP_ORW 2782 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF, FINITE_DELETE, IMAGE_FINITE]) 2783 >> `(IMAGE (\x. f x * indicator_fn a x) (m_space m)) = 2784 (IMAGE f a) DELETE 0` 2785 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_IMAGE, IN_DELETE, indicator_fn_def] 2786 >> FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, REAL_ENTIRE, SUBSET_DEF] 2787 >> EQ_TAC 2788 >- (RW_TAC real_ss [REAL_ENTIRE] 2789 >- (Q.EXISTS_TAC `x'` >> Cases_on `x' IN a` >> FULL_SIMP_TAC real_ss [REAL_ENTIRE] 2790 >> METIS_TAC [REAL_ARITH ``~((1:real) = 0)``]) 2791 >> METIS_TAC [REAL_ARITH ``~((1:real) = 0)``, REAL_ENTIRE]) 2792 >> RW_TAC real_ss [REAL_ENTIRE] 2793 >> Q.EXISTS_TAC `x'` >> RW_TAC real_ss []) 2794 >> POP_ORW 2795 >> ASM_SIMP_TAC std_ss [Once REAL_SUM_IMAGE_IN_IF, FINITE_DELETE, IMAGE_FINITE] 2796 >> `(\r. (if r IN IMAGE f a DELETE 0 then 2797 r * measure m (PREIMAGE (\x. f x * indicator_fn a x) {r} INTER m_space m) 2798 else 0)) = 2799 (\r. if r IN IMAGE f a DELETE 0 then 2800 (\r. r * measure m (PREIMAGE f {r} INTER a)) r 2801 else 0)` 2802 by (RW_TAC real_ss [FUN_EQ_THM, IN_DELETE, IN_IMAGE] 2803 >> RW_TAC real_ss [indicator_fn_def] 2804 >> Suff `(PREIMAGE (\x. f x * (if x IN a then 1 else 0)) {f x} INTER m_space m) = 2805 (PREIMAGE f {f x} INTER a)` 2806 >- RW_TAC std_ss [] 2807 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC real_ss [IN_INTER, IN_PREIMAGE, IN_SING] 2808 >> Cases_on `x' IN a` >> RW_TAC real_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF]) 2809 >> POP_ORW 2810 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF, FINITE_DELETE, IMAGE_FINITE]); 2811 2812 2813val finite_space_POW_integral_reduce = store_thm 2814 ("finite_space_POW_integral_reduce", 2815 ``!m f. 2816 measure_space m /\ 2817 (POW (m_space m) = measurable_sets m) /\ 2818 FINITE (m_space m) ==> 2819 (integral m f = 2820 SIGMA (\x. f x * measure m {x}) 2821 (m_space m))``, 2822 REPEAT STRIP_TAC 2823 >> `f IN borel_measurable (m_space m, measurable_sets m)` 2824 by (Q.PAT_X_ASSUM `P = Q` (MP_TAC o GSYM) 2825 >> RW_TAC std_ss [borel_measurable_le_iff, IN_POW, SUBSET_DEF, GSPECIFICATION]) 2826 >> `?c n. BIJ c (count n) (m_space m)` by RW_TAC std_ss [GSYM FINITE_BIJ_COUNT_EQ] 2827 >> `pos_simple_fn m (pos_part f) 2828 (count n) (\i. {c i}) (\i. if 0 <= f(c i) then f(c i) else 0) /\ 2829 pos_simple_fn m (neg_part f) 2830 (count n) (\i. {c i}) (\i. if f(c i) <= 0 then ~ f(c i) else 0)` 2831 by (RW_TAC std_ss [pos_simple_fn_def, FINITE_COUNT] 2832 >| [RW_TAC real_ss [pos_part_def], 2833 `FINITE (count n)` by RW_TAC std_ss [FINITE_COUNT] 2834 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n`) REAL_SUM_IMAGE_IN_IF] 2835 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2836 >> `?i. i IN count n /\ (t = c i)` by METIS_TAC [] 2837 >> `(\x. (if x IN count n then (if 0 <= f(c x) then f(c x) else 0) * 2838 indicator_fn {c x} t else 0)) = 2839 (\x. if (x = i) /\ 0 <= f (c i) then f(c i) else 0)` 2840 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> POP_ORW 2841 >> STRIP_TAC >> SIMP_TAC real_ss [indicator_fn_def, IN_SING] 2842 >> REVERSE (Cases_on `x IN count n`) >- METIS_TAC [] 2843 >> ASM_SIMP_TAC std_ss [] 2844 >> Cases_on `x = i` 2845 >> RW_TAC real_ss [] 2846 >> METIS_TAC []) 2847 >> POP_ORW 2848 >> `count n = i INSERT ((count n) DELETE i)` 2849 by (RW_TAC std_ss [EXTENSION, IN_INSERT, IN_DELETE] >> METIS_TAC []) 2850 >> POP_ORW 2851 >> ASM_SIMP_TAC std_ss [FINITE_INSERT, FINITE_DELETE, FINITE_COUNT, 2852 REAL_SUM_IMAGE_THM, DELETE_DELETE] 2853 >> `FINITE (count n DELETE i)` by RW_TAC std_ss [FINITE_COUNT, FINITE_DELETE] 2854 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n DELETE i`) REAL_SUM_IMAGE_IN_IF] 2855 >> SIMP_TAC std_ss [IN_DELETE] 2856 >> (MP_TAC o Q.SPECL [`\x.0`, `0`] o UNDISCH o Q.ISPEC `count n DELETE i`) 2857 REAL_SUM_IMAGE_FINITE_CONST 2858 >> RW_TAC real_ss [pos_part_def], 2859 Q.PAT_X_ASSUM `P = Q` (MP_TAC o GSYM) 2860 >> RW_TAC std_ss [IN_POW, SUBSET_DEF, IN_SING] 2861 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF], 2862 RW_TAC real_ss [], 2863 RW_TAC std_ss [DISJOINT_DEF, IN_SING, IN_INTER, NOT_IN_EMPTY, Once EXTENSION] 2864 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF] >> METIS_TAC [], 2865 ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_SING] 2866 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2867 >> METIS_TAC [], 2868 RW_TAC real_ss [neg_part_def, REAL_LT_IMP_LE, REAL_LE_RNEG] 2869 >> FULL_SIMP_TAC std_ss [GSYM real_lt, REAL_LT_IMP_LE], 2870 `FINITE (count n)` by RW_TAC std_ss [FINITE_COUNT] 2871 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n`) REAL_SUM_IMAGE_IN_IF] 2872 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2873 >> `?i. i IN count n /\ (t = c i)` by METIS_TAC [] 2874 >> `(\x. (if x IN count n then (if f(c x) <= 0 then ~f(c x) else 0) * 2875 indicator_fn {c x} t else 0)) = 2876 (\x. if (x = i) /\ f (c i) <= 0 then ~f(c i) else 0)` 2877 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> POP_ORW 2878 >> STRIP_TAC >> SIMP_TAC real_ss [indicator_fn_def, IN_SING] 2879 >> REVERSE (Cases_on `x IN count n`) >- METIS_TAC [] 2880 >> ASM_SIMP_TAC std_ss [] 2881 >> Cases_on `x = i` 2882 >> RW_TAC real_ss [] 2883 >> METIS_TAC []) 2884 >> POP_ORW 2885 >> `count n = i INSERT ((count n) DELETE i)` 2886 by (RW_TAC std_ss [EXTENSION, IN_INSERT, IN_DELETE] >> METIS_TAC []) 2887 >> POP_ORW 2888 >> ASM_SIMP_TAC std_ss [FINITE_INSERT, FINITE_DELETE, FINITE_COUNT, 2889 REAL_SUM_IMAGE_THM, DELETE_DELETE] 2890 >> `FINITE (count n DELETE i)` by RW_TAC std_ss [FINITE_COUNT, FINITE_DELETE] 2891 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `count n DELETE i`) REAL_SUM_IMAGE_IN_IF] 2892 >> SIMP_TAC std_ss [IN_DELETE] 2893 >> (MP_TAC o Q.SPECL [`\x.0`, `0`] o UNDISCH o Q.ISPEC `count n DELETE i`) 2894 REAL_SUM_IMAGE_FINITE_CONST 2895 >> RW_TAC real_ss [neg_part_def] >> METIS_TAC [real_lt, REAL_LT_ANTISYM, REAL_LE_ANTISYM, REAL_NEG_0], 2896 Q.PAT_X_ASSUM `P = Q` (MP_TAC o GSYM) 2897 >> RW_TAC std_ss [IN_POW, SUBSET_DEF, IN_SING] 2898 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF], 2899 RW_TAC real_ss [REAL_LE_RNEG], 2900 RW_TAC std_ss [Once EXTENSION, DISJOINT_DEF, IN_SING, IN_INTER, NOT_IN_EMPTY] 2901 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF] >> METIS_TAC [], 2902 ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_SING] 2903 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2904 >> METIS_TAC []]) 2905 >> `pos_simple_fn_integral m (count n) (\i. {c i}) (\i. (if 0 <= f(c i) then f(c i) else 0)) 2906 IN nnfis m (pos_part f)` 2907 by (MATCH_MP_TAC psfis_nnfis 2908 >> RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 2909 >> Q.EXISTS_TAC `((count n), (\i. {c i}), (\i. (if 0 <= f(c i) then f(c i) else 0)))` 2910 >> RW_TAC std_ss [] 2911 >> Q.EXISTS_TAC `((count n), (\i. {c i}), (\i. (if 0 <= f(c i) then f(c i) else 0)))` 2912 >> RW_TAC std_ss []) 2913 >> `pos_simple_fn_integral m (count n) (\i. {c i}) (\i. (if f(c i) <= 0 then ~f(c i) else 0)) 2914 IN nnfis m (neg_part f)` 2915 by (MATCH_MP_TAC psfis_nnfis 2916 >> RW_TAC std_ss [psfis_def, IN_IMAGE, psfs_def, GSPECIFICATION] 2917 >> Q.EXISTS_TAC `((count n), (\i. {c i}), (\i. (if f(c i) <= 0 then ~f(c i) else 0)))` 2918 >> RW_TAC std_ss [] 2919 >> Q.EXISTS_TAC `((count n), (\i. {c i}), (\i. (if f(c i) <= 0 then ~f(c i) else 0)))` 2920 >> RW_TAC std_ss []) 2921 >> `!f. (\t. pos_part f t - neg_part f t) = f` 2922 by (RW_TAC real_ss [pos_part_def, neg_part_def, Once FUN_EQ_THM] 2923 >> RW_TAC real_ss []) 2924 >> (MP_TAC o Q.SPECL [`m`, `pos_part f`, `neg_part f`, 2925 `pos_simple_fn_integral m (count n) (\i. {c i}) (\i. (if 0 <= f(c i) then f(c i) else 0))`, 2926 `pos_simple_fn_integral m (count n) (\i. {c i}) (\i. (if f(c i) <= 0 then ~f(c i) else 0))`]) 2927 nnfis_minus_nnfis_integral 2928 >> RW_TAC std_ss [pos_simple_fn_integral_def, real_sub] 2929 >> `!x. ~x = ~1 * x` by RW_TAC real_ss [] >> POP_ORW 2930 >> RW_TAC std_ss [GSYM REAL_SUM_IMAGE_CMUL, FINITE_COUNT, GSYM REAL_SUM_IMAGE_ADD] 2931 >> `(\i. 2932 (if 0 <= f (c i) then f (c i) else 0) * measure m {c i} + 2933 ~1 * ((if f (c i) <= 0 then ~f (c i) else 0) * measure m {c i})) = 2934 (\i. f (c i) * measure m {c i})` 2935 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [] 2936 >> METIS_TAC [REAL_LE_TOTAL, REAL_LE_ANTISYM, REAL_MUL_LZERO, REAL_ADD_RID]) 2937 >> POP_ORW 2938 >> `FINITE (count n)` by RW_TAC std_ss [FINITE_COUNT] 2939 >> (MP_TAC o Q.ISPEC `c:num->'a` o UNDISCH o Q.ISPEC `count n` o GSYM) REAL_SUM_IMAGE_IMAGE 2940 >> Know `INJ c (count n) (IMAGE c (count n))` 2941 >- (FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, IN_IMAGE] >> METIS_TAC []) 2942 >> SIMP_TAC std_ss [] >> STRIP_TAC >> STRIP_TAC 2943 >> POP_ASSUM (MP_TAC o Q.SPEC `(\x:'a. f x * measure m {x})`) 2944 >> RW_TAC std_ss [o_DEF] 2945 >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM (K ALL_TAC) 2946 >> `(IMAGE c (count n)) = (m_space m)` 2947 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE] 2948 >> FULL_SIMP_TAC std_ss [BIJ_DEF, INJ_DEF, SURJ_DEF, IN_IMAGE] 2949 >> METIS_TAC []) 2950 >> RW_TAC std_ss []); 2951 2952 2953val finite_POW_RN_deriv_reduce = store_thm 2954 ("finite_POW_RN_deriv_reduce", 2955 ``!m v. measure_space m /\ 2956 FINITE (m_space m) /\ 2957 measure_space (m_space m, measurable_sets m, v) /\ 2958 (POW (m_space m) = measurable_sets m) /\ 2959 (!x. (measure m {x} = 0) ==> (v {x} = 0)) ==> 2960 (!x. x IN m_space m /\ ~ (measure m {x} = 0) ==> (RN_deriv m v x = v {x} / (measure m {x})))``, 2961 RW_TAC std_ss [RN_deriv_def] 2962 >> Suff `(\f. f x = v {x} / measure m {x}) 2963 (@f.f IN borel_measurable (m_space m,measurable_sets m) /\ 2964 !a. 2965 a IN measurable_sets m ==> 2966 (integral m (\x. f x * indicator_fn a x) = v a))` 2967 >- RW_TAC std_ss [] 2968 >> MATCH_MP_TAC SELECT_ELIM_THM 2969 >> RW_TAC std_ss [] 2970 >- (Q.EXISTS_TAC `\x. v {x} / (measure m {x})` 2971 >> SIMP_TAC std_ss [] 2972 >> STRONG_CONJ_TAC 2973 >- (Q.PAT_X_ASSUM `P = Q` (MP_TAC o GSYM) 2974 >> RW_TAC std_ss [borel_measurable_le_iff, IN_POW, SUBSET_DEF, GSPECIFICATION]) 2975 >> RW_TAC std_ss [] 2976 >> (MP_TAC o Q.ISPECL [`(m :('a -> bool) # (('a -> bool) -> bool) # (('a -> bool) -> real))`, 2977 `\x':'a. v {x'} / measure m {x'} * indicator_fn a x'`]) finite_space_POW_integral_reduce 2978 >> RW_TAC std_ss [] 2979 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `m_space m`) REAL_SUM_IMAGE_IN_IF] 2980 >> `(\x. 2981 (if x IN m_space m then 2982 (\x'. v {x'} / measure m {x'} * indicator_fn a x' * measure m {x'}) x 2983 else 2984 0)) = 2985 (\x. if x IN m_space m then 2986 (\x'. (\x'. v {x'}) x' * indicator_fn a x') x else 0)` 2987 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC std_ss [real_div] 2988 >> Cases_on `measure m {x'} = 0` 2989 >- RW_TAC real_ss [] 2990 >> `v {x'} * inv (measure m {x'}) * indicator_fn a x' * measure m {x'} = 2991 (inv (measure m {x'}) * measure m {x'}) * v {x'} * indicator_fn a x'` 2992 by REAL_ARITH_TAC 2993 >> POP_ORW 2994 >> RW_TAC real_ss [REAL_MUL_LINV]) 2995 >> POP_ORW 2996 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 2997 >> `a SUBSET m_space m` by METIS_TAC [IN_POW] 2998 >> `m_space m = a UNION (m_space m DIFF a)` 2999 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_DIFF, IN_UNION] >> METIS_TAC [SUBSET_DEF]) 3000 >> POP_ORW 3001 >> `DISJOINT a (m_space m DIFF a)` 3002 by (RW_TAC std_ss [IN_DISJOINT, IN_DIFF] >> DECIDE_TAC) 3003 >> `SIGMA (\x'. v {x'} * indicator_fn a x') (a UNION (m_space m DIFF a)) = 3004 SIGMA (\x'. v {x'} * indicator_fn a x') a + 3005 SIGMA (\x'. v {x'} * indicator_fn a x') (m_space m DIFF a)` 3006 by (MATCH_MP_TAC REAL_SUM_IMAGE_DISJOINT_UNION >> METIS_TAC [FINITE_DIFF, SUBSET_FINITE]) 3007 >> POP_ORW 3008 >> `FINITE a` by METIS_TAC [SUBSET_FINITE] 3009 >> `FINITE (m_space m DIFF a)` by RW_TAC std_ss [FINITE_DIFF] 3010 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `a`) REAL_SUM_IMAGE_IN_IF] 3011 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `m_space m DIFF a`) REAL_SUM_IMAGE_IN_IF] 3012 >> `(\x. 3013 (if x IN m_space m DIFF a then 3014 (\x'. v {x'} * indicator_fn a x') x 3015 else 3016 0)) = (\x. 0)` 3017 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_DIFF, indicator_fn_def]) 3018 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] 3019 >> `(\x'. (if x' IN a then v {x'} * indicator_fn a x' else 0)) = 3020 (\x'. if x' IN a then (\x'. v {x'}) x' else 0)` 3021 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [indicator_fn_def]) 3022 >> POP_ORW >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 3023 >> `!x. v = measure (m_space m,measurable_sets m,v)` by RW_TAC std_ss [measure_def] 3024 >> POP_ORW 3025 >> ONCE_REWRITE_TAC [EQ_SYM_EQ] 3026 >> MATCH_MP_TAC MEASURE_REAL_SUM_IMAGE 3027 >> RW_TAC std_ss [measurable_sets_def] 3028 >> METIS_TAC [SUBSET_DEF, IN_POW, IN_SING]) 3029 >> POP_ASSUM (MP_TAC o Q.SPEC `{x}`) 3030 >> `{x} IN measurable_sets m` by METIS_TAC [SUBSET_DEF, IN_POW, IN_SING] 3031 >> ASM_SIMP_TAC std_ss [] 3032 >> (MP_TAC o Q.SPECL [`m`,`(\x''. x' x'' * indicator_fn {x} x'')`]) finite_space_POW_integral_reduce 3033 >> ASM_SIMP_TAC std_ss [] 3034 >> STRIP_TAC >> POP_ASSUM (K ALL_TAC) 3035 >> `x IN m_space m` by METIS_TAC [IN_POW, SUBSET_DEF, IN_SING] 3036 >> `m_space m = {x} UNION (m_space m DIFF {x})` 3037 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_DIFF, IN_SING] >> METIS_TAC []) 3038 >> POP_ORW 3039 >> `DISJOINT {x} (m_space m DIFF {x})` 3040 by (RW_TAC std_ss [IN_DISJOINT, IN_DIFF, IN_SING] >> METIS_TAC []) 3041 >> `SIGMA (\x''. x' x'' * indicator_fn {x} x'' * measure m {x''}) ({x} UNION (m_space m DIFF {x})) = 3042 SIGMA (\x''. x' x'' * indicator_fn {x} x'' * measure m {x''}) {x} + 3043 SIGMA (\x''. x' x'' * indicator_fn {x} x'' * measure m {x''}) (m_space m DIFF {x})` 3044 by (MATCH_MP_TAC REAL_SUM_IMAGE_DISJOINT_UNION >> METIS_TAC [FINITE_DIFF, FINITE_SING]) 3045 >> POP_ORW 3046 >> SIMP_TAC std_ss [REAL_SUM_IMAGE_SING] 3047 >> `FINITE (m_space m DIFF {x})` by RW_TAC std_ss [FINITE_DIFF] 3048 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `m_space m DIFF {x}`) REAL_SUM_IMAGE_IN_IF] 3049 >> `(\x''. 3050 (if x'' IN m_space m DIFF {x} then 3051 (\x''. x' x'' * indicator_fn {x} x'' * measure m {x''}) x'' 3052 else 3053 0)) = (\x. 0)` 3054 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_DIFF, indicator_fn_def]) 3055 >> POP_ORW 3056 >> ASM_SIMP_TAC real_ss [REAL_SUM_IMAGE_0] 3057 >> `0 < measure m {x}` 3058 by METIS_TAC [measure_space_def, positive_def, REAL_LE_LT] 3059 >> ASM_SIMP_TAC real_ss [REAL_EQ_RDIV_EQ, indicator_fn_def, IN_SING]); 3060 3061 3062val finite_POW_prod_measure_reduce = store_thm 3063 ("finite_POW_prod_measure_reduce", 3064 ``!m0 m1. measure_space m0 /\ measure_space m1 /\ 3065 FINITE (m_space m0) /\ FINITE (m_space m1) /\ 3066 (POW (m_space m0) = measurable_sets m0) /\ 3067 (POW (m_space m1) = measurable_sets m1) ==> 3068 (!a0 a1. a0 IN measurable_sets m0 /\ 3069 a1 IN measurable_sets m1 ==> 3070 ((prod_measure m0 m1) (a0 CROSS a1) = 3071 measure m0 a0 * measure m1 a1))``, 3072 RW_TAC std_ss [prod_measure_def, measure_def, 3073 finite_space_POW_integral_reduce] 3074 >> `(m_space m0) = a0 UNION ((m_space m0) DIFF a0)` 3075 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_DIFF] 3076 >> METIS_TAC [MEASURABLE_SETS_SUBSET_SPACE, SUBSET_DEF]) 3077 >> POP_ORW 3078 >> `DISJOINT a0 (m_space m0 DIFF a0)` 3079 by (RW_TAC std_ss [IN_DISJOINT, IN_DIFF] >> DECIDE_TAC) 3080 >> `FINITE a0` by METIS_TAC [MEASURABLE_SETS_SUBSET_SPACE, SUBSET_FINITE] 3081 >> RW_TAC std_ss [REAL_SUM_IMAGE_DISJOINT_UNION, FINITE_DIFF] 3082 >> `FINITE (m_space m0 DIFF a0)` by RW_TAC std_ss [FINITE_DIFF] 3083 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `(m_space m0 DIFF a0)`) REAL_SUM_IMAGE_IN_IF] 3084 >> `(\x. 3085 (if x IN m_space m0 DIFF a0 then 3086 (\s0. 3087 measure m1 (PREIMAGE (\s1. (s0,s1)) (a0 CROSS a1)) * 3088 measure m0 {s0}) x 3089 else 3090 0)) = (\x. 0)` 3091 by (RW_TAC std_ss [FUN_EQ_THM, IN_DIFF] 3092 >> RW_TAC std_ss [] 3093 >> `PREIMAGE (\s1. (x,s1)) (a0 CROSS a1) = {}` 3094 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY, IN_PREIMAGE, IN_CROSS]) 3095 >> RW_TAC real_ss [MEASURE_EMPTY]) 3096 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] 3097 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `a0`) REAL_SUM_IMAGE_IN_IF] 3098 >> `(\x. 3099 (if x IN a0 then 3100 (\s0. 3101 measure m1 (PREIMAGE (\s1. (s0,s1)) (a0 CROSS a1)) * 3102 measure m0 {s0}) x 3103 else 3104 0)) = 3105 (\x. if x IN a0 then 3106 (\s0. measure m1 a1 * measure m0 {s0}) x else 0)` 3107 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC std_ss [] 3108 >> `PREIMAGE (\s1. (x,s1)) (a0 CROSS a1) = a1` 3109 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_PREIMAGE, IN_CROSS]) 3110 >> RW_TAC std_ss []) 3111 >> POP_ORW >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 3112 >> `(\x. measure m1 a1 * measure m0 {x}) = 3113 (\x. measure m1 a1 * (\x. measure m0 {x}) x)` 3114 by RW_TAC std_ss [] 3115 >> POP_ORW >> ASM_SIMP_TAC std_ss [REAL_SUM_IMAGE_CMUL] 3116 >> Suff `SIGMA (\x. measure m0 {x}) a0 = measure m0 a0` 3117 >- RW_TAC real_ss [REAL_MUL_COMM] 3118 >> MATCH_MP_TAC (GSYM MEASURE_REAL_SUM_IMAGE) 3119 >> METIS_TAC [IN_SING, IN_POW, SUBSET_DEF]); 3120 3121 3122val measure_space_finite_prod_measure_POW1 = store_thm 3123 ("measure_space_finite_prod_measure_POW1", 3124 ``!m0 m1. measure_space m0 /\ measure_space m1 /\ 3125 FINITE (m_space m0) /\ FINITE (m_space m1) /\ 3126 (POW (m_space m0) = measurable_sets m0) /\ 3127 (POW (m_space m1) = measurable_sets m1) ==> 3128 measure_space (prod_measure_space m0 m1)``, 3129 REPEAT STRIP_TAC 3130 >> RW_TAC std_ss [prod_measure_space_def] 3131 >> `(m_space m0 CROSS m_space m1, 3132 subsets 3133 (sigma (m_space m0 CROSS m_space m1) 3134 (prod_sets (measurable_sets m0) (measurable_sets m1))), 3135 prod_measure m0 m1) = 3136 (space (sigma (m_space m0 CROSS m_space m1) 3137 (prod_sets (measurable_sets m0) (measurable_sets m1))), 3138 subsets 3139 (sigma (m_space m0 CROSS m_space m1) 3140 (prod_sets (measurable_sets m0) (measurable_sets m1))), 3141 prod_measure m0 m1)` 3142 by RW_TAC std_ss [sigma_def, space_def] 3143 >> POP_ORW 3144 >> MATCH_MP_TAC finite_additivity_sufficient_for_finite_spaces 3145 >> RW_TAC std_ss [m_space_def, SPACE_SIGMA, FINITE_CROSS, 3146 measurable_sets_def, m_space_def, SIGMA_REDUCE] 3147 >| [MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA 3148 >> RW_TAC std_ss [subset_class_def, prod_sets_def, GSPECIFICATION, IN_CROSS] 3149 >> (MP_TAC o Q.ISPEC `(x' :('a -> bool) # ('b -> bool))`) pair_CASES 3150 >> RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [PAIR_EQ] 3151 >> RW_TAC std_ss [SUBSET_DEF, IN_CROSS] 3152 >> (MP_TAC o Q.ISPEC `(x :('a # 'b))`) pair_CASES 3153 >> RW_TAC std_ss [] 3154 >> FULL_SIMP_TAC std_ss [FST, SND] 3155 >> METIS_TAC [MEASURABLE_SETS_SUBSET_SPACE, SUBSET_DEF], 3156 RW_TAC std_ss [positive_def, measure_def, measurable_sets_def] 3157 >- (`{} = {} CROSS {}` by RW_TAC std_ss [CROSS_EMPTY] 3158 >> POP_ORW 3159 >> METIS_TAC [finite_POW_prod_measure_reduce, 3160 measure_space_def, SIGMA_ALGEBRA, subsets_def, space_def, 3161 MEASURE_EMPTY, REAL_MUL_LZERO]) 3162 >> RW_TAC std_ss [prod_measure_def, finite_space_POW_integral_reduce] 3163 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 3164 >> RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LE_MUL 3165 >> FULL_SIMP_TAC std_ss [measure_space_def, positive_def] 3166 >> `(PREIMAGE (\s1. (x,s1)) s) SUBSET m_space m1` 3167 by (RW_TAC std_ss [IN_PREIMAGE, SUBSET_DEF] 3168 >> FULL_SIMP_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER, GSPECIFICATION] 3169 >> Q.PAT_X_ASSUM `!s'. P s' ==> s IN s'` 3170 (MP_TAC o Q.SPEC `POW (m_space m0 CROSS m_space m1)`) 3171 >> SIMP_TAC std_ss [POW_SIGMA_ALGEBRA] 3172 >> `prod_sets (measurable_sets m0) (measurable_sets m1) SUBSET 3173 POW (m_space m0 CROSS m_space m1)` 3174 by (RW_TAC std_ss [SUBSET_DEF, IN_POW, IN_CROSS, prod_sets_def, GSPECIFICATION] 3175 >> (MP_TAC o Q.ISPEC `(x''' :('a -> bool) # ('b -> bool))`) pair_CASES 3176 >> RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [PAIR_EQ] 3177 >> `x'''' IN q CROSS r` by RW_TAC std_ss [] 3178 >> FULL_SIMP_TAC std_ss [IN_CROSS] 3179 >> METIS_TAC [MEASURABLE_SETS_SUBSET_SPACE, SUBSET_DEF, IN_POW]) 3180 >> ASM_SIMP_TAC std_ss [] 3181 >> RW_TAC std_ss [IN_POW, SUBSET_DEF, IN_CROSS] 3182 >> METIS_TAC [SND]) 3183 >> METIS_TAC [IN_POW, IN_SING, SUBSET_DEF], 3184 RW_TAC std_ss [additive_def, measure_def, measurable_sets_def] 3185 >> RW_TAC std_ss [prod_measure_def, finite_space_POW_integral_reduce, 3186 GSYM REAL_SUM_IMAGE_ADD] 3187 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `m_space m0`) REAL_SUM_IMAGE_IN_IF] 3188 >> Suff `(\x. 3189 (if x IN m_space m0 then 3190 (\s0. 3191 measure m1 (PREIMAGE (\s1. (s0,s1)) (s UNION t)) * 3192 measure m0 {s0}) x 3193 else 3194 0)) = 3195 (\x. 3196 (if x IN m_space m0 then 3197 (\s0. 3198 measure m1 (PREIMAGE (\s1. (s0,s1)) s) * measure m0 {s0} + 3199 measure m1 (PREIMAGE (\s1. (s0,s1)) t) * measure m0 {s0}) x 3200 else 3201 0))` 3202 >- RW_TAC std_ss [] 3203 >> RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC std_ss [] 3204 >> `measure m1 (PREIMAGE (\s1. (x,s1)) s) * measure m0 {x} + 3205 measure m1 (PREIMAGE (\s1. (x,s1)) t) * measure m0 {x} = 3206 (measure m1 (PREIMAGE (\s1. (x,s1)) s) + 3207 measure m1 (PREIMAGE (\s1. (x,s1)) t)) * measure m0 {x}` 3208 by REAL_ARITH_TAC 3209 >> POP_ORW 3210 >> RW_TAC std_ss [REAL_EQ_RMUL] 3211 >> DISJ2_TAC 3212 >> FULL_SIMP_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER, 3213 GSPECIFICATION] 3214 >> Q.PAT_X_ASSUM `!s. P s ==> t IN s` 3215 (MP_TAC o Q.SPEC `POW (m_space m0 CROSS m_space m1)`) 3216 >> Q.PAT_X_ASSUM `!ss. P ss ==> s IN s'` 3217 (MP_TAC o Q.SPEC `POW (m_space m0 CROSS m_space m1)`) 3218 >> SIMP_TAC std_ss [prod_sets_def, POW_SIGMA_ALGEBRA] 3219 >> `{s CROSS t | s IN measurable_sets m0 /\ t IN measurable_sets m1} SUBSET 3220 POW (m_space m0 CROSS m_space m1)` 3221 by (RW_TAC std_ss [Once SUBSET_DEF, GSPECIFICATION, IN_POW] 3222 >> (MP_TAC o Q.ISPEC `(x'' :('a -> bool) # ('b -> bool))`) pair_CASES 3223 >> RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [PAIR_EQ] 3224 >> RW_TAC std_ss [SUBSET_DEF, IN_CROSS] 3225 >> METIS_TAC [MEASURABLE_SETS_SUBSET_SPACE, SUBSET_DEF, IN_POW]) 3226 >> ASM_SIMP_TAC std_ss [] 3227 >> RW_TAC std_ss [IN_POW] 3228 >> MATCH_MP_TAC MEASURE_ADDITIVE 3229 >> Q.PAT_X_ASSUM `POW (m_space m1) = measurable_sets m1` (MP_TAC o GSYM) 3230 >> Q.PAT_X_ASSUM `POW (m_space m0) = measurable_sets m0` (MP_TAC o GSYM) 3231 >> FULL_SIMP_TAC std_ss [IN_POW, SUBSET_DEF, IN_PREIMAGE, IN_CROSS, IN_DISJOINT] 3232 >> RW_TAC std_ss [] 3233 >| [METIS_TAC [SND], METIS_TAC [SND], ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_PREIMAGE]]]); 3234 3235 3236val measure_space_finite_prod_measure_POW2 = store_thm 3237 ("measure_space_finite_prod_measure_POW2", 3238 ``!m0 m1. measure_space m0 /\ measure_space m1 /\ 3239 FINITE (m_space m0) /\ FINITE (m_space m1) /\ 3240 (POW (m_space m0) = measurable_sets m0) /\ 3241 (POW (m_space m1) = measurable_sets m1) ==> 3242 measure_space (m_space m0 CROSS m_space m1, 3243 POW (m_space m0 CROSS m_space m1), 3244 prod_measure m0 m1)``, 3245 REPEAT STRIP_TAC 3246 >> `(m_space m0 CROSS m_space m1, 3247 POW (m_space m0 CROSS m_space m1), 3248 prod_measure m0 m1) = 3249 (space (m_space m0 CROSS m_space m1, 3250 POW (m_space m0 CROSS m_space m1)), 3251 subsets 3252 (m_space m0 CROSS m_space m1, 3253 POW (m_space m0 CROSS m_space m1)), 3254 prod_measure m0 m1)` 3255 by RW_TAC std_ss [space_def, subsets_def] 3256 >> POP_ORW 3257 >> MATCH_MP_TAC finite_additivity_sufficient_for_finite_spaces 3258 >> RW_TAC std_ss [POW_SIGMA_ALGEBRA, space_def, FINITE_CROSS, subsets_def] 3259 >- (RW_TAC std_ss [positive_def, measure_def, measurable_sets_def] 3260 >- (`{} = {} CROSS {}` by RW_TAC std_ss [CROSS_EMPTY] 3261 >> POP_ORW 3262 >> METIS_TAC [finite_POW_prod_measure_reduce, 3263 measure_space_def, SIGMA_ALGEBRA, subsets_def, space_def, 3264 MEASURE_EMPTY, REAL_MUL_LZERO]) 3265 >> RW_TAC std_ss [prod_measure_def, finite_space_POW_integral_reduce] 3266 >> MATCH_MP_TAC REAL_SUM_IMAGE_POS 3267 >> RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LE_MUL 3268 >> FULL_SIMP_TAC std_ss [measure_space_def, positive_def] 3269 >> `(PREIMAGE (\s1. (x,s1)) s) SUBSET m_space m1` 3270 by (RW_TAC std_ss [IN_PREIMAGE, SUBSET_DEF] 3271 >> FULL_SIMP_TAC std_ss [IN_POW, SUBSET_DEF, IN_CROSS] 3272 >> METIS_TAC [SND]) 3273 >> METIS_TAC [IN_POW, IN_SING, SUBSET_DEF]) 3274 >> RW_TAC std_ss [additive_def, measure_def, measurable_sets_def] 3275 >> RW_TAC std_ss [prod_measure_def, finite_space_POW_integral_reduce, 3276 GSYM REAL_SUM_IMAGE_ADD] 3277 >> ONCE_REWRITE_TAC [(UNDISCH o Q.SPEC `m_space m0`) REAL_SUM_IMAGE_IN_IF] 3278 >> Suff `(\x. 3279 (if x IN m_space m0 then 3280 (\s0. 3281 measure m1 (PREIMAGE (\s1. (s0,s1)) (s UNION t)) * 3282 measure m0 {s0}) x 3283 else 3284 0)) = 3285 (\x. 3286 (if x IN m_space m0 then 3287 (\s0. 3288 measure m1 (PREIMAGE (\s1. (s0,s1)) s) * measure m0 {s0} + 3289 measure m1 (PREIMAGE (\s1. (s0,s1)) t) * measure m0 {s0}) x 3290 else 3291 0))` 3292 >- RW_TAC std_ss [] 3293 >> RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC std_ss [] 3294 >> `measure m1 (PREIMAGE (\s1. (x,s1)) s) * measure m0 {x} + 3295 measure m1 (PREIMAGE (\s1. (x,s1)) t) * measure m0 {x} = 3296 (measure m1 (PREIMAGE (\s1. (x,s1)) s) + 3297 measure m1 (PREIMAGE (\s1. (x,s1)) t)) * measure m0 {x}` 3298 by REAL_ARITH_TAC 3299 >> POP_ORW 3300 >> RW_TAC std_ss [REAL_EQ_RMUL] 3301 >> DISJ2_TAC 3302 >> MATCH_MP_TAC MEASURE_ADDITIVE 3303 >> Q.PAT_X_ASSUM `POW (m_space m1) = measurable_sets m1` (MP_TAC o GSYM) 3304 >> Q.PAT_X_ASSUM `POW (m_space m0) = measurable_sets m0` (MP_TAC o GSYM) 3305 >> FULL_SIMP_TAC std_ss [IN_POW, SUBSET_DEF, IN_PREIMAGE, IN_CROSS, IN_DISJOINT] 3306 >> RW_TAC std_ss [] 3307 >| [ METIS_TAC [SND], 3308 METIS_TAC [SND], 3309 ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_PREIMAGE] ]); 3310 3311val countable_space_integral_reduce = store_thm 3312 ("countable_space_integral_reduce", 3313 ``!m f p n. measure_space m /\ 3314 positive m /\ 3315 f IN borel_measurable (m_space m, measurable_sets m) /\ 3316 countable (IMAGE f (m_space m)) /\ 3317 ~(FINITE (IMAGE (pos_part f) (m_space m))) /\ 3318 ~(FINITE (IMAGE (neg_part f) (m_space m))) /\ 3319 (\r. r * 3320 measure m (PREIMAGE (neg_part f) {r} INTER m_space m)) o 3321 enumerate ((IMAGE (neg_part f) (m_space m))) sums n /\ 3322 (\r. r * 3323 measure m (PREIMAGE (pos_part f) {r} INTER m_space m)) o 3324 enumerate ((IMAGE (pos_part f) (m_space m))) sums p ==> 3325 (integral m f = p - n)``, 3326 RW_TAC std_ss [integral_def] 3327 >> Suff `((@i. i IN nnfis m (pos_part f)) = p) /\ ((@i. i IN nnfis m (neg_part f)) = n)` 3328 >- RW_TAC std_ss [] 3329 >> (CONJ_TAC >> MATCH_MP_TAC SELECT_UNIQUE >> RW_TAC std_ss []) 3330 >- (Suff `p IN nnfis m (pos_part f)` >- METIS_TAC [nnfis_unique] 3331 >> MATCH_MP_TAC nnfis_mon_conv 3332 >> Know `BIJ (enumerate(IMAGE (pos_part f) (m_space m))) UNIV (IMAGE (pos_part f) (m_space m))` 3333 >- ( `countable (IMAGE (pos_part f) (m_space m))` 3334 by (MATCH_MP_TAC COUNTABLE_SUBSET 3335 >> Q.EXISTS_TAC `0 INSERT (IMAGE f (m_space m))` 3336 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, countable_INSERT, IN_INSERT] 3337 >> METIS_TAC []) 3338 >> METIS_TAC [COUNTABLE_ALT_BIJ] ) 3339 >> DISCH_TAC 3340 >> FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV] 3341 >> Q.EXISTS_TAC `(\n t. if t IN m_space m /\ pos_part f t IN IMAGE (enumerate (IMAGE (pos_part f) (m_space m))) 3342 (pred_set$count n) then pos_part f t else 0)` 3343 >> Q.EXISTS_TAC `(\n. 3344 sum (0,n) 3345 ((\r. 3346 r * 3347 measure m (PREIMAGE (pos_part f) {r} INTER m_space m)) o 3348 enumerate (IMAGE (pos_part f) (m_space m))))` 3349 >> ASM_SIMP_TAC std_ss [] 3350 >> CONJ_TAC 3351 >- (RW_TAC std_ss [mono_convergent_def] 3352 >- (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] >> METIS_TAC [LESS_LESS_EQ_TRANS]) 3353 >> RW_TAC std_ss [SEQ] 3354 >> `?N. enumerate (IMAGE (pos_part f) (m_space m)) N = (pos_part f) t` 3355 by METIS_TAC [IN_IMAGE] 3356 >> Q.EXISTS_TAC `SUC N` 3357 >> RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO] 3358 >> FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT] 3359 >> METIS_TAC [DECIDE ``!n:num. n < SUC n``, LESS_LESS_EQ_TRANS, pos_part_def]) 3360 >> STRIP_TAC >> MATCH_MP_TAC psfis_nnfis 3361 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT] 3362 >> `(\t. (if t IN m_space m /\ pos_part f t IN IMAGE (enumerate (IMAGE (pos_part f) (m_space m))) (pred_set$count n') 3363 then pos_part f t else 0)) = 3364 (\t. SIGMA (\i. (\i. enumerate (IMAGE (pos_part f) (m_space m)) i) i * 3365 indicator_fn ((\i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (m_space m)) i} 3366 INTER (m_space m)) i) t) 3367 (pred_set$count n'))` 3368 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_IMAGE] 3369 >- (`pred_set$count n' = x INSERT (pred_set$count n')` 3370 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INSERT] >> METIS_TAC []) 3371 >> POP_ORW 3372 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT] 3373 >> ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o 3374 REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF] 3375 >> RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE] 3376 >> `(\x'. (if x' IN pred_set$count n' /\ ~(x' = x) then 3377 enumerate (IMAGE (pos_part f) (m_space m)) x' * 3378 (if enumerate (IMAGE (pos_part f) (m_space m)) x = 3379 enumerate (IMAGE (pos_part f) (m_space m)) x' 3380 then 1 else 0) else 0)) = (\x. 0)` 3381 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [] >> METIS_TAC []) 3382 >> POP_ORW 3383 >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]) 3384 >> FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING] 3385 >- RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE] 3386 >> ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`) 3387 REAL_SUM_IMAGE_IN_IF] 3388 >> `(\x. (if x IN pred_set$count n' then 3389 (\i. enumerate (IMAGE (pos_part f) (m_space m)) i * 3390 (if (pos_part f t = enumerate (IMAGE (pos_part f) (m_space m)) i) /\ 3391 t IN m_space m then 1 else 0)) x else 0)) = (\x. 0)` 3392 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [] >> METIS_TAC []) 3393 >> POP_ORW 3394 >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT]) 3395 >> POP_ORW 3396 >> `((\r. r * measure m (PREIMAGE (pos_part f) {r} INTER m_space m)) o 3397 enumerate (IMAGE (pos_part f) (m_space m))) = 3398 (\i. (\i. enumerate (IMAGE (pos_part f) (m_space m)) i) i * 3399 measure m ((\i. 3400 PREIMAGE (pos_part f) 3401 {enumerate (IMAGE (pos_part f) (m_space m)) i} INTER 3402 m_space m) i))` 3403 by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] >> RW_TAC real_ss []) 3404 >> POP_ORW 3405 >> MATCH_MP_TAC psfis_intro 3406 >> ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT] 3407 >> REVERSE CONJ_TAC 3408 >- (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def] 3409 >> METIS_TAC [REAL_LE_REFL]) 3410 >> `(pos_part f) IN borel_measurable (m_space m, measurable_sets m)` 3411 by METIS_TAC [pos_part_neg_part_borel_measurable] 3412 >> REPEAT STRIP_TAC 3413 >> `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (m_space m)) i} INTER m_space m = 3414 {w | w IN m_space m /\ ((pos_part f) w = (\w. enumerate (IMAGE (pos_part f) (m_space m)) i) w)}` 3415 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING] 3416 >> DECIDE_TAC) 3417 >> POP_ORW 3418 >> MATCH_MP_TAC borel_measurable_eq_borel_measurable 3419 >> METIS_TAC [borel_measurable_const, measure_space_def]) 3420 >> Suff `n IN nnfis m (neg_part f)` >- METIS_TAC [nnfis_unique] 3421 >> MATCH_MP_TAC nnfis_mon_conv 3422 >> `BIJ (enumerate(IMAGE (neg_part f) (m_space m))) UNIV (IMAGE (neg_part f) (m_space m))` 3423 by (`countable (IMAGE (neg_part f) (m_space m))` 3424 by (MATCH_MP_TAC COUNTABLE_SUBSET 3425 >> Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (m_space m)))` 3426 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, countable_INSERT, IN_INSERT, image_countable] 3427 >> METIS_TAC []) 3428 >> METIS_TAC [COUNTABLE_ALT_BIJ]) 3429 >> FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV] 3430 >> Q.EXISTS_TAC `(\n t. if t IN m_space m /\ neg_part f t IN IMAGE (enumerate (IMAGE (neg_part f) (m_space m))) 3431 (pred_set$count n) then neg_part f t else 0)` 3432 >> Q.EXISTS_TAC `(\n. 3433 sum (0,n) 3434 ((\r. 3435 r * 3436 measure m (PREIMAGE (neg_part f) {r} INTER m_space m)) o 3437 enumerate (IMAGE (neg_part f) (m_space m))))` 3438 >> ASM_SIMP_TAC std_ss [] 3439 >> CONJ_TAC 3440 >- (RW_TAC std_ss [mono_convergent_def] 3441 >- (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] >> METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL]) 3442 >> RW_TAC std_ss [SEQ] 3443 >> `?N. enumerate (IMAGE (neg_part f) (m_space m)) N = (neg_part f) t` 3444 by METIS_TAC [IN_IMAGE] 3445 >> Q.EXISTS_TAC `SUC N` 3446 >> RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO] 3447 >> FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT] 3448 >> METIS_TAC [DECIDE ``!n:num. n < SUC n``, LESS_LESS_EQ_TRANS, neg_part_def]) 3449 >> STRIP_TAC >> MATCH_MP_TAC psfis_nnfis 3450 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT] 3451 >> `(\t. (if t IN m_space m /\ neg_part f t IN IMAGE (enumerate (IMAGE (neg_part f) (m_space m))) (pred_set$count n') 3452 then neg_part f t else 0)) = 3453 (\t. SIGMA (\i. (\i. enumerate (IMAGE (neg_part f) (m_space m)) i) i * 3454 indicator_fn ((\i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (m_space m)) i} 3455 INTER (m_space m)) i) t) 3456 (pred_set$count n'))` 3457 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [IN_IMAGE] 3458 >- (`pred_set$count n' = x INSERT (pred_set$count n')` 3459 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INSERT] >> METIS_TAC []) 3460 >> POP_ORW 3461 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT] 3462 >> ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o 3463 REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF] 3464 >> RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE] 3465 >> `(\x'. (if x' IN pred_set$count n' /\ ~(x' = x) then 3466 enumerate (IMAGE (neg_part f) (m_space m)) x' * 3467 (if enumerate (IMAGE (neg_part f) (m_space m)) x = 3468 enumerate (IMAGE (neg_part f) (m_space m)) x' 3469 then 1 else 0) else 0)) = (\x. 0)` 3470 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [] >> METIS_TAC []) 3471 >> POP_ORW 3472 >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]) 3473 >> FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING] 3474 >- RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE] 3475 >> ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`) 3476 REAL_SUM_IMAGE_IN_IF] 3477 >> `(\x. (if x IN pred_set$count n' then 3478 (\i. enumerate (IMAGE (neg_part f) (m_space m)) i * 3479 (if (neg_part f t = enumerate (IMAGE (neg_part f) (m_space m)) i) /\ 3480 t IN m_space m then 1 else 0)) x else 0)) = (\x. 0)` 3481 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss [] >> METIS_TAC []) 3482 >> POP_ORW 3483 >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT]) 3484 >> POP_ORW 3485 >> `((\r. r * measure m (PREIMAGE (neg_part f) {r} INTER m_space m)) o 3486 enumerate (IMAGE (neg_part f) (m_space m))) = 3487 (\i. (\i. enumerate (IMAGE (neg_part f) (m_space m)) i) i * 3488 measure m ((\i. 3489 PREIMAGE (neg_part f) 3490 {enumerate (IMAGE (neg_part f) (m_space m)) i} INTER 3491 m_space m) i))` 3492 by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] >> RW_TAC real_ss []) 3493 >> POP_ORW 3494 >> MATCH_MP_TAC psfis_intro 3495 >> ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT] 3496 >> REVERSE CONJ_TAC 3497 >- (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def] 3498 >> METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL]) 3499 >> `(neg_part f) IN borel_measurable (m_space m, measurable_sets m)` 3500 by METIS_TAC [pos_part_neg_part_borel_measurable] 3501 >> REPEAT STRIP_TAC 3502 >> `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (m_space m)) i} INTER m_space m = 3503 {w | w IN m_space m /\ ((neg_part f) w = (\w. enumerate (IMAGE (neg_part f) (m_space m)) i) w)}` 3504 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING] 3505 >> DECIDE_TAC) 3506 >> POP_ORW 3507 >> MATCH_MP_TAC borel_measurable_eq_borel_measurable 3508 >> METIS_TAC [borel_measurable_const, measure_space_def]); 3509 3510val _ = export_theory (); 3511