real_borelScript.sml
1(* ------------------------------------------------------------------------- *)
2(* Borel measurable sets defined on reals (from "examples/diningcryptos") *)
3(* Author: Aaron Coble (2010) *)
4(* Cambridge University *)
5(* ------------------------------------------------------------------------- *)
6(* Extended by Chun Tian (2020-2021) using some materials from: *)
7(* *)
8(* Lebesgue Measure Theory (lebesgue_measure_hvgScript.sml) *)
9(* *)
10(* (c) Copyright 2015, *)
11(* Muhammad Qasim, *)
12(* Osman Hasan, *)
13(* Hardware Verification Group, *)
14(* Concordia University *)
15(* *)
16(* Contact: <m_qasi@ece.concordia.ca> *)
17(* *)
18(* Note: This theory is inspired by Isabelle/HOL *)
19(* ------------------------------------------------------------------------- *)
20
21Theory real_borel
22Ancestors
23 arithmetic pred_set num list combin pair real seq real_sigma
24 transc nets metric topology cardinal real_topology iterate derivative
25 real_of_rat sigma_algebra
26Libs
27 metisLib pred_setLib numLib realLib jrhUtils hurdUtils
28
29(* ------------------------------------------------------------------------- *)
30(* Start a new theory called "borel" (renamed to "real_borel") *)
31(* ------------------------------------------------------------------------- *)
32
33val ASM_ARITH_TAC = rpt (POP_ASSUM MP_TAC) THEN ARITH_TAC;
34val ASM_REAL_ARITH_TAC = REAL_ASM_ARITH_TAC;
35val DISC_RW_KILL = DISCH_TAC >> ONCE_ASM_REWRITE_TAC [] >> POP_ASSUM K_TAC;
36fun METIS ths tm = prove(tm,METIS_TAC ths);
37
38val set_ss = std_ss ++ PRED_SET_ss;
39
40val _ = intLib.deprecate_int ();
41val _ = ratLib.deprecate_rat ();
42
43Theorem PREIMAGE_REAL_COMPL1: !c:real. COMPL {x | c < x} = {x | x <= c}
44Proof
45 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION]
46 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lte,SPECIFICATION]
47QED
48
49Theorem PREIMAGE_REAL_COMPL2: !c:real. COMPL {x | c <= x} = {x | x < c}
50Proof
51 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION]
52 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lt,SPECIFICATION]
53QED
54
55Theorem PREIMAGE_REAL_COMPL3: !c:real. COMPL {x | x <= c} = {x | c < x}
56Proof
57 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION]
58 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lt,SPECIFICATION]
59QED
60
61Theorem PREIMAGE_REAL_COMPL4: !c:real. COMPL {x | x < c} = {x | c <= x}
62Proof
63 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION]
64 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lte,SPECIFICATION]
65QED
66
67(* ************************************************************************* *)
68(* Basic Definitions *)
69(* ************************************************************************* *)
70
71(* The new definition is based on open sets.
72
73 See martingaleTheory for 2-dimensional Borel space based on pairTheory
74 (term: ‘borel CROSS borel’).
75
76 See examples/probability/stochastic_processesTheory for n-dimensional Borel
77 spaces based on fcpTheory (term: ‘borel of_dimension(:'N)’).
78
79 See "borel_def" for the old definition.
80 *)
81Definition borel :
82 borel = sigma univ(:real) {s | open s}
83End
84
85Theorem borel_alt_general :
86 borel = general_borel euclidean
87Proof
88 rw [borel, euclidean_open_def, general_borel_def, TOPSPACE_EUCLIDEAN]
89 >> AP_TERM_TAC
90 >> rw [Once EXTENSION, IN_APP]
91QED
92
93(* was: borel_measurable [definition] *)
94Overload borel_measurable = “\a. measurable a borel”
95
96(* The definition of ‘indicator_fn’ is now merged with iterateTheory.indicator *)
97Overload indicator_fn[local] = “indicator”
98Theorem indicator_fn_def[local] = indicator
99
100(* ************************************************************************* *)
101(* Proofs *)
102(* ************************************************************************* *)
103
104Theorem space_borel: space borel = UNIV
105Proof
106 METIS_TAC [borel, sigma_def, space_def]
107QED
108
109Theorem sigma_algebra_borel: sigma_algebra borel
110Proof
111 RW_TAC std_ss [borel]
112 >> MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA
113 >> RW_TAC std_ss [subset_class_def, IN_UNIV, IN_IMAGE, SUBSET_DEF]
114QED
115
116(* NOTE: removed ‘sigma_algebra M’ due to changes of ‘measurable’ *)
117Theorem in_borel_measurable_open :
118 !f M. f IN borel_measurable M <=>
119 (!s. s IN subsets (sigma UNIV {s | open s}) ==>
120 (PREIMAGE f s) INTER (space M) IN subsets M)
121Proof
122 REPEAT GEN_TAC THEN RW_TAC std_ss [measurable_def] THEN
123 SIMP_TAC std_ss [GSPECIFICATION] THEN EQ_TAC THEN REPEAT STRIP_TAC THEN
124 FULL_SIMP_TAC std_ss [] THENL
125 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC std_ss [borel],
126 EVAL_TAC THEN SIMP_TAC std_ss [borel, sigma_def, space_def] THEN
127 SIMP_TAC std_ss [IN_UNIV] THEN SIMP_TAC std_ss [IN_DEF] THEN rw[IN_FUNSET],
128 FIRST_X_ASSUM MATCH_MP_TAC THEN POP_ASSUM MP_TAC THEN
129 SIMP_TAC std_ss [borel, sigma_def, subsets_def, IN_BIGINTER] THEN
130 SIMP_TAC std_ss [GSPECIFICATION] THEN REPEAT STRIP_TAC THEN
131 FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [SUBSET_DEF, sigma_sets_basic] THEN
132 MATCH_MP_TAC sigma_algebra_sigma_sets THEN REWRITE_TAC [POW_DEF] THEN
133 SET_TAC []]
134QED
135
136(* NOTE: removed ‘sigma_algebra M’ due to changes of ‘measurable’ *)
137Theorem in_borel_measurable_borel:
138 !f M. f IN borel_measurable M <=>
139 (!s. s IN subsets borel ==> (PREIMAGE f s) INTER (space M) IN subsets M)
140Proof
141 SIMP_TAC std_ss [in_borel_measurable_open, borel]
142QED
143
144Theorem space_in_borel:
145 UNIV IN subsets borel
146Proof
147 SIMP_TAC std_ss [borel, sigma_def, subsets_def] THEN
148 SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION, SUBSET_DEF] THEN
149 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
150 SIMP_TAC std_ss [OPEN_UNIV]
151QED
152
153Theorem borel_open:
154 !A. open A ==> A IN subsets borel
155Proof
156 SIMP_TAC std_ss [borel, sigma_def, subsets_def] THEN
157 SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION, SUBSET_DEF]
158QED
159
160Theorem borel_closed:
161 !A. closed A ==> A IN subsets borel
162Proof
163 GEN_TAC THEN REWRITE_TAC [closed_def] THEN
164 DISCH_THEN (ASSUME_TAC o MATCH_MP borel_open) THEN
165 FULL_SIMP_TAC std_ss [borel, sigma_def, subsets_def] THEN
166 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION, SUBSET_DEF] THEN
167 GEN_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC ``P:(real->bool)->bool``) THEN
168 REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [sigma_algebra_def, algebra_def] THEN
169 FULL_SIMP_TAC std_ss [subsets_def, space_def] THEN POP_ASSUM K_TAC THEN
170 POP_ASSUM K_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC ``univ(:real) DIFF A``) THEN
171 ASM_SIMP_TAC std_ss [SET_RULE ``UNIV DIFF (UNIV DIFF A) = A``]
172QED
173
174Theorem borel_fsigma :
175 !s. fsigma s ==> s IN subsets borel
176Proof
177 rw [fsigma]
178 >> MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION
179 >> rw [SUBSET_DEF, sigma_algebra_borel]
180 >> MATCH_MP_TAC borel_closed >> simp []
181QED
182
183Theorem borel_gdelta :
184 !s. gdelta s ==> s IN subsets borel
185Proof
186 rw [gdelta]
187 >> Cases_on ‘g = {}’ >- simp [space_in_borel]
188 >> MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_INTER
189 >> rw [SUBSET_DEF, sigma_algebra_borel]
190 >> MATCH_MP_TAC borel_open >> simp []
191QED
192
193Theorem borel_singleton:
194 !A x. A IN subsets borel ==> x INSERT A IN subsets borel
195Proof
196 REPEAT GEN_TAC THEN ASSUME_TAC borel_closed THEN
197 FULL_SIMP_TAC std_ss [borel, sigma_def, subsets_def] THEN
198 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION, SUBSET_DEF] THEN
199 REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
200 FIRST_X_ASSUM (MP_TAC o SPEC ``P:(real->bool)->bool``) THEN
201 FIRST_X_ASSUM (MP_TAC o SPEC ``{x}:real->bool``) THEN
202 SIMP_TAC std_ss [CLOSED_SING] THEN DISCH_TAC THEN
203 FIRST_X_ASSUM (MP_TAC o SPEC ``P:(real->bool)->bool``) THEN
204 REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN
205 FULL_SIMP_TAC std_ss [sigma_algebra_def, algebra_def, subsets_def] THEN
206 REWRITE_TAC [INSERT_DEF] THEN SIMP_TAC std_ss [GSYM IN_SING, GSYM UNION_DEF] THEN
207 FIRST_X_ASSUM MATCH_MP_TAC THEN METIS_TAC []
208QED
209
210Theorem borel_comp:
211 !A. A IN subsets borel ==> (UNIV DIFF A) IN subsets borel
212Proof
213 REPEAT GEN_TAC THEN
214 FULL_SIMP_TAC std_ss [borel, sigma_def, subsets_def] THEN
215 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION, SUBSET_DEF] THEN
216 REPEAT STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC ``P:(real->bool)->bool``) THEN
217FULL_SIMP_TAC std_ss [sigma_algebra_def, algebra_def, subsets_def, space_def]
218QED
219
220Theorem borel_measurable_image:
221 !f M x. f IN borel_measurable M ==>
222 (PREIMAGE f {x}) INTER space M IN subsets M
223Proof
224 REPEAT GEN_TAC THEN SIMP_TAC std_ss [measurable_def] THEN
225 SIMP_TAC std_ss [GSPECIFICATION] THEN REPEAT STRIP_TAC THEN
226 FIRST_X_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC borel_closed THEN
227 SIMP_TAC std_ss [CLOSED_SING]
228QED
229
230Theorem borel_measurable_const:
231 !M c. sigma_algebra M ==> (\x. c) IN borel_measurable M
232Proof
233 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [measurable_def] THEN
234 SIMP_TAC std_ss [GSPECIFICATION] THEN ASM_REWRITE_TAC [sigma_algebra_borel] THEN
235 CONJ_TAC THENL [EVAL_TAC THEN SIMP_TAC std_ss [space_borel, IN_UNIV] THEN
236 SIMP_TAC std_ss[IN_DEF], ALL_TAC] THEN
237 SIMP_TAC std_ss [borel, sigma_def, subsets_def] THEN
238 SIMP_TAC std_ss [IN_BIGINTER, SUBSET_DEF, GSPECIFICATION] THEN
239 REPEAT STRIP_TAC THEN
240 simp[PREIMAGE_def, INTER_DEF, GSPECIFICATION,IN_FUNSET] THEN
241 ASM_CASES_TAC ``(c:real) IN s`` THENL
242 [ASM_SIMP_TAC std_ss [SET_RULE ``{x | x IN s} = s``] THEN
243 MATCH_MP_TAC ALGEBRA_SPACE THEN FULL_SIMP_TAC std_ss [sigma_algebra_def],
244 ALL_TAC] THEN
245 ASM_SIMP_TAC std_ss [GSPEC_F] THEN MATCH_MP_TAC ALGEBRA_EMPTY THEN
246 FULL_SIMP_TAC std_ss [sigma_algebra_def]
247QED
248
249Theorem borel_sigma_sets_subset:
250 !A. A SUBSET subsets borel ==> (sigma_sets UNIV A) SUBSET subsets borel
251Proof
252 RW_TAC std_ss [] THEN MATCH_MP_TAC sigma_sets_subset THEN
253 ASM_SIMP_TAC std_ss [GSYM space_borel, SPACE, sigma_algebra_borel]
254QED
255
256Theorem borel_eq_sigmaI1:
257 !X A f. (borel = sigma UNIV X) /\
258 (!x. x IN X ==> x IN subsets (sigma UNIV (IMAGE f A))) /\
259 (!i. i IN A ==> f i IN subsets borel) ==>
260 (borel = sigma UNIV (IMAGE f A))
261Proof
262 RW_TAC std_ss [borel] THEN SIMP_TAC std_ss [sigma_def] THEN
263 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, GSYM SUBSET_DEF] THEN
264 SIMP_TAC std_ss [EXTENSION, IN_BIGINTER, GSPECIFICATION] THEN
265 GEN_TAC THEN FULL_SIMP_TAC std_ss [GSPECIFICATION] THEN
266 EQ_TAC THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
267 ASM_SET_TAC []
268QED
269
270Theorem borel_eq_sigmaI2:
271 !G f A B. (borel = sigma UNIV (IMAGE (\(i,j). G i j) B)) /\
272 (!i j. (i,j) IN B ==>
273 G i j IN subsets (sigma UNIV (IMAGE (\(i,j). f i j) A))) /\
274 (!i j. (i,j) IN A ==> f i j IN subsets borel) ==>
275 (borel = sigma UNIV (IMAGE (\(i,j). f i j) A))
276Proof
277 REPEAT STRIP_TAC THEN MATCH_MP_TAC borel_eq_sigmaI1 THEN
278 EXISTS_TAC ``(IMAGE (\(i,j). (G:'a->'b->real->bool) i j) B)`` THEN
279 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, borel] THEN
280 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN
281 CONJ_TAC THENL
282 [RW_TAC std_ss [IN_IMAGE] THEN MP_TAC (ISPEC ``x':'a#'b`` ABS_PAIR_THM) THEN
283 STRIP_TAC THEN FULL_SIMP_TAC std_ss [], ALL_TAC] THEN
284 RW_TAC std_ss [] THEN MP_TAC (ISPEC ``i:'c#'d`` ABS_PAIR_THM) THEN
285 STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN ASM_SET_TAC []
286QED
287
288Theorem borel_eq_sigmaI3:
289 !f A X. (borel = sigma UNIV X) /\
290 (!x. x IN X ==> x IN subsets (sigma UNIV (IMAGE (\(i,j). f i j) A))) /\
291 (!i j. (i,j) IN A ==> f i j IN subsets borel) ==>
292 (borel = sigma UNIV (IMAGE (\(i,j). f i j) A))
293Proof
294 REPEAT STRIP_TAC THEN MATCH_MP_TAC borel_eq_sigmaI1 THEN
295 EXISTS_TAC ``X:(real->bool)->bool`` THEN
296 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, borel] THEN
297 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN
298 RW_TAC std_ss [] THEN MP_TAC (ISPEC ``i:'a#'b`` ABS_PAIR_THM) THEN
299 STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN ASM_SET_TAC []
300QED
301
302Theorem borel_eq_sigmaI4:
303 !G f A. (borel = sigma UNIV (IMAGE (\(i,j). G i j) A)) /\
304 (!i j. (i,j) IN A ==>
305 G i j IN subsets (sigma UNIV (IMAGE f UNIV))) /\
306 (!i. f i IN subsets borel) ==>
307 (borel = sigma UNIV (IMAGE f UNIV))
308Proof
309 REPEAT STRIP_TAC THEN MATCH_MP_TAC borel_eq_sigmaI1 THEN
310 EXISTS_TAC ``(IMAGE (\(i,j). (G:'a->'b->real->bool) i j) A)`` THEN
311 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, borel] THEN
312 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN
313 CONJ_TAC THENL
314 [RW_TAC std_ss [IN_IMAGE] THEN MP_TAC (ISPEC ``x':'a#'b`` ABS_PAIR_THM) THEN
315 STRIP_TAC THEN FULL_SIMP_TAC std_ss [], ALL_TAC] THEN
316 RW_TAC std_ss [IN_UNIV] THEN ASM_SET_TAC []
317QED
318
319Theorem borel_eq_sigmaI5:
320 !G f. (borel = sigma UNIV (IMAGE G UNIV)) /\
321 (!i. G i IN subsets (sigma UNIV (IMAGE (\(i,j). f i j) UNIV))) /\
322 (!i j. f i j IN subsets borel) ==>
323 (borel = sigma UNIV (IMAGE (\(i,j). f i j) UNIV))
324Proof
325 REPEAT STRIP_TAC THEN MATCH_MP_TAC borel_eq_sigmaI1 THEN
326 EXISTS_TAC ``(IMAGE (G:'a->real->bool) UNIV)`` THEN
327 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, borel] THEN
328 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN
329 CONJ_TAC THENL
330 [RW_TAC std_ss [IN_IMAGE] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
331 ASM_SIMP_TAC std_ss [], ALL_TAC] THEN
332 RW_TAC std_ss [IN_UNIV] THEN
333 MP_TAC (ISPEC ``i:'b#'c`` ABS_PAIR_THM) THEN STRIP_TAC THEN
334 ASM_SIMP_TAC std_ss [] THEN ASM_SET_TAC []
335QED
336
337Theorem BIGUNION_IMAGE_QSET:
338 !a f: real -> 'a -> bool. sigma_algebra a /\ f IN (q_set -> subsets a)
339 ==> BIGUNION (IMAGE f q_set) IN subsets a
340Proof
341 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_UNIV, SUBSET_DEF] THEN
342 FIRST_X_ASSUM MATCH_MP_TAC THEN RW_TAC std_ss [IN_IMAGE] THEN
343 ASM_SIMP_TAC std_ss [] THEN MATCH_MP_TAC image_countable THEN
344 SIMP_TAC std_ss [QSET_COUNTABLE]
345QED
346
347Definition box : (* `OPEN_interval (a,b)` *)
348 box a b = {x:real | a < x /\ x < b}
349End
350
351Theorem box_alt :
352 !a b. box a b = OPEN_interval (a,b)
353Proof
354 RW_TAC std_ss [box, OPEN_interval]
355QED
356
357Theorem rational_boxes:
358 !x e. 0 < e ==> ?a b. a IN q_set /\ b IN q_set /\ x IN box a b /\
359 box a b SUBSET ball (x,e)
360Proof
361 RW_TAC std_ss [] THEN
362 `0:real < e / 2` by FULL_SIMP_TAC real_ss [] THEN
363 KNOW_TAC ``?y. y IN q_set /\ y < x /\ x - y < e / 2`` THENL
364 [MP_TAC (ISPECL [``x - e / 2:real``,``x:real``] Q_DENSE_IN_REAL) THEN
365 DISCH_TAC THEN
366 REWRITE_TAC [REAL_ARITH ``y < x /\ x - y < e:real <=> x - e < y /\ y < x``] THEN
367 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC, STRIP_TAC] THEN
368 KNOW_TAC ``?y. y IN q_set /\ x < y /\ y - x < e / 2`` THENL
369 [MP_TAC (ISPECL [``x:real``,``x + e / 2:real``] Q_DENSE_IN_REAL) THEN
370 DISCH_TAC THEN
371 REWRITE_TAC [REAL_ARITH ``x < y /\ y - x < e:real <=> x < y /\ y < x + e``] THEN
372 FIRST_X_ASSUM MATCH_MP_TAC THEN METIS_TAC [REAL_LT_ADDR], STRIP_TAC] THEN
373 EXISTS_TAC ``y:real`` THEN EXISTS_TAC ``y':real`` THEN
374 FULL_SIMP_TAC std_ss [box, GSPECIFICATION, IN_BALL, SUBSET_DEF, dist] THEN
375 RW_TAC real_ss [] THEN GEN_REWR_TAC RAND_CONV [GSYM REAL_HALF_DOUBLE] THEN
376 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ``(x - y) + (y' - x):real`` THEN
377 CONJ_TAC THENL [ALL_TAC, METIS_TAC [REAL_LT_ADD2]] THEN
378 ASM_REAL_ARITH_TAC
379QED
380
381Theorem open_UNION_box:
382 !M. open M ==> (M = BIGUNION {box a b | box a b SUBSET M})
383Proof
384 RW_TAC std_ss [OPEN_CONTAINS_BALL] THEN
385 SIMP_TAC std_ss [EXTENSION, IN_BIGUNION, GSPECIFICATION, EXISTS_PROD] THEN
386 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
387 [FIRST_X_ASSUM (MP_TAC o SPEC ``x:real``) THEN ASM_REWRITE_TAC [] THEN
388 STRIP_TAC THEN
389 FIRST_X_ASSUM (MP_TAC o SPEC ``x:real`` o MATCH_MP rational_boxes) THEN
390 STRIP_TAC THEN METIS_TAC [SUBSET_DEF], ALL_TAC] THEN
391 FULL_SIMP_TAC std_ss [SUBSET_DEF]
392QED
393
394Theorem open_union_box[local]:
395 !M. open M ==>
396 (M = BIGUNION
397 {box (FST f) (SND f) | f IN {f | box (FST f) (SND f) SUBSET M}})
398Proof
399 RW_TAC std_ss [OPEN_CONTAINS_BALL] THEN
400 SIMP_TAC std_ss [EXTENSION, IN_BIGUNION, GSPECIFICATION, EXISTS_PROD] THEN
401 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
402 [FIRST_X_ASSUM (MP_TAC o SPEC ``x:real``) THEN ASM_REWRITE_TAC [] THEN
403 STRIP_TAC THEN
404 FIRST_ASSUM (MP_TAC o SPEC ``x:real`` o MATCH_MP rational_boxes) THEN
405 STRIP_TAC THEN METIS_TAC [SUBSET_DEF], ALL_TAC] THEN
406 FULL_SIMP_TAC std_ss [SUBSET_DEF]
407QED
408
409Theorem open_UNION_rational_box :
410 !M. open M ==> (M = BIGUNION {box a b | a IN q_set /\ b IN q_set /\
411 box a b SUBSET M})
412Proof
413 RW_TAC std_ss [OPEN_CONTAINS_BALL] THEN
414 SIMP_TAC std_ss [EXTENSION, IN_BIGUNION, GSPECIFICATION, EXISTS_PROD] THEN
415 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
416 [FIRST_X_ASSUM (MP_TAC o SPEC ``x:real``) THEN ASM_REWRITE_TAC [] THEN
417 STRIP_TAC THEN
418 FIRST_X_ASSUM (MP_TAC o SPEC ``x:real`` o MATCH_MP rational_boxes) THEN
419 STRIP_TAC THEN METIS_TAC [SUBSET_DEF], ALL_TAC] THEN
420 FULL_SIMP_TAC std_ss [SUBSET_DEF]
421QED
422
423Theorem open_union_rational_box[local]:
424 !M. open M ==>
425 (M = BIGUNION
426 {box (FST f) (SND f) | f IN {f | (FST f) IN q_set /\ (SND f) IN q_set /\
427 box (FST f) (SND f) SUBSET M}})
428Proof
429 RW_TAC std_ss [OPEN_CONTAINS_BALL] THEN
430 SIMP_TAC std_ss [EXTENSION, IN_BIGUNION, GSPECIFICATION, EXISTS_PROD] THEN
431 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
432 [FIRST_X_ASSUM (MP_TAC o SPEC ``x:real``) THEN ASM_REWRITE_TAC [] THEN
433 STRIP_TAC THEN
434 FIRST_ASSUM (MP_TAC o SPEC ``x:real`` o MATCH_MP rational_boxes) THEN
435 STRIP_TAC THEN METIS_TAC [SUBSET_DEF], ALL_TAC] THEN
436 FULL_SIMP_TAC std_ss [SUBSET_DEF]
437QED
438
439(* key lemma for alternative definitions of ``borel`` *)
440Theorem borel_eq_box :
441 borel = sigma UNIV (IMAGE (\(a,b). box a b) UNIV)
442Proof
443 SIMP_TAC std_ss [box] THEN MATCH_MP_TAC borel_eq_sigmaI1
444 >> Q.EXISTS_TAC `{s | open s}` >> SIMP_TAC std_ss [borel]
445 >> reverse CONJ_TAC
446 >- (FULL_SIMP_TAC std_ss [sigma_def, subsets_def] \\
447 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] \\
448 RW_TAC std_ss [] \\
449 FULL_SIMP_TAC std_ss [SUBSET_DEF] \\
450 FIRST_X_ASSUM MATCH_MP_TAC \\
451 SIMP_TAC std_ss [GSPECIFICATION] \\
452 MP_TAC (ISPEC ``i:real#real`` ABS_PAIR_THM) >> STRIP_TAC \\
453 FULL_SIMP_TAC std_ss [GSYM interval, OPEN_INTERVAL])
454 >> RW_TAC std_ss [GSPECIFICATION]
455 >> FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP open_union_rational_box)
456 >> ONCE_ASM_REWRITE_TAC []
457 >> ONCE_REWRITE_TAC
458 [METIS [] ``box (FST f) (SND f) = (\f. box (FST f) (SND f)) f``]
459 >> MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UN'
460 >> Q.EXISTS_TAC `univ(:real)`
461 >> RW_TAC std_ss [] >> fs [GSPECIFICATION]
462 >- (Suff `sigma_algebra
463 (space (sigma univ(:real)
464 (IMAGE (\(a,b). {x | a < x /\ x < b}) univ(:real # real))),
465 subsets (sigma univ(:real)
466 (IMAGE (\(a,b). {x | a < x /\ x < b}) univ(:real # real))))`
467 >- METIS_TAC [SPACE_SIGMA] \\
468 SIMP_TAC std_ss [SPACE] \\
469 MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA \\
470 SIMP_TAC std_ss [subset_class_def] \\
471 SIMP_TAC std_ss [SUBSET_UNIV])
472 >- (RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, subsets_def, sigma_def, GSPECIFICATION] \\
473 RW_TAC std_ss [IN_BIGINTER, GSPECIFICATION, IN_UNIV] \\
474 FIRST_X_ASSUM MATCH_MP_TAC \\
475 rename1 `FST f' IN q_set` \\
476 Cases_on `f'` >> Q.EXISTS_TAC `(q, r)` \\
477 RW_TAC std_ss [box])
478 (* COUNTABLE {f | box (FST f) (SND f) SUBSET x} *)
479 >> MATCH_MP_TAC COUNTABLE_SUBSET
480 >> EXISTS_TAC ``{f | (?q r. (f = (q,r)) /\ q IN q_set /\ r IN q_set)}``
481 >> reverse CONJ_TAC
482 >- (ONCE_REWRITE_TAC [SET_RULE ``{f | ?q r. (f = (q,r)) /\ q IN q_set /\ r IN q_set} =
483 {f | FST f IN q_set /\ SND f IN q_set}``] THEN
484 SIMP_TAC std_ss [GSYM CROSS_DEF] THEN
485 MATCH_MP_TAC cross_countable THEN
486 SIMP_TAC std_ss [QSET_COUNTABLE])
487 >> SET_TAC []
488QED
489
490Theorem borel_eq_gr_less : (* was: borel_eq_greaterThanLessThan *)
491 borel = sigma UNIV (IMAGE (\(a,b). {x | a < x /\ x < b}) UNIV)
492Proof
493 SIMP_TAC std_ss [borel_eq_box, box]
494QED
495
496Theorem halfspace_gt_in_halfspace[local]:
497 !a. {x | x < a} IN
498 subsets (sigma univ(:real) (IMAGE (\(a,i). {x | x < a}) UNIV))
499Proof
500 RW_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER, GSPECIFICATION,
501 SUBSET_DEF] THEN ASM_SET_TAC []
502QED
503
504Theorem borel_eq_less : (* was: borel_eq_halfspace_less *)
505 borel = sigma UNIV (IMAGE (\a. {x | x < a}) UNIV)
506Proof
507 ONCE_REWRITE_TAC [SET_RULE
508 ``(IMAGE (\a. {x | x < a}) univ(:real)) =
509 (IMAGE (\(a:real,i:num). (\a i. {x | x < a}) a i) UNIV)``]
510 >> Suff `(borel = sigma univ(:real) (IMAGE (\(i,j). box i j) UNIV)) /\
511 (!i j. (i,j) IN UNIV ==>
512 box i j IN subsets (sigma univ(:real)
513 (IMAGE (\(i,j). (\a i. {x | x < a}) i j)
514 univ(:real # num)))) /\
515 !i j. (i,j) IN univ(:real # num) ==>
516 (\a i. {x | x < a}) i j IN subsets borel`
517 >- (DISCH_THEN (MP_TAC o MATCH_MP borel_eq_sigmaI2) \\
518 SIMP_TAC std_ss [])
519 >> SIMP_TAC std_ss [borel_eq_box]
520 >> SIMP_TAC std_ss [GSYM borel_eq_box, IN_UNIV]
521 >> KNOW_TAC ``!a b. box a b =
522 {x | x IN space (sigma UNIV (IMAGE (\a. {x | x < a}) UNIV)) /\
523 (\x. a < x) x /\ (\x. x < b) x}`` THENL
524 [SIMP_TAC std_ss [SPACE_SIGMA, box, EXTENSION, GSPECIFICATION, IN_UNIV],
525 DISCH_TAC] THEN CONJ_TAC THENL
526 [ONCE_ASM_REWRITE_TAC [] THEN
527 REPEAT GEN_TAC THEN MATCH_MP_TAC SEMIRING_SETS_COLLECT THEN CONJ_TAC THENL
528 [RW_TAC std_ss [semiring_alt] THENL
529 [SIMP_TAC std_ss [subset_class_def, SPACE_SIGMA, SUBSET_UNIV],
530 RW_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER,
531 GSPECIFICATION, SUBSET_DEF] THEN
532 FULL_SIMP_TAC std_ss [sigma_algebra_alt_pow],
533 RW_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER,
534 GSPECIFICATION, SUBSET_DEF] THEN
535 ONCE_REWRITE_TAC [METIS [subsets_def] ``P = subsets (univ(:real), P)``] THEN
536 MATCH_MP_TAC ALGEBRA_INTER THEN
537 ASM_SIMP_TAC std_ss [SIGMA_ALGEBRA_ALGEBRA] THEN
538 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER,
539 GSPECIFICATION, SUBSET_DEF],
540 ALL_TAC] THEN Q.EXISTS_TAC `{s DIFF t}` THEN
541 SIMP_TAC std_ss [BIGUNION_SING, FINITE_SING, disjoint_sing] THEN
542 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER,
543 GSPECIFICATION, SUBSET_DEF] THEN
544 RW_TAC std_ss [IN_SING] THEN
545 ONCE_REWRITE_TAC [METIS [subsets_def] ``P = subsets (univ(:real), P)``] THEN
546 MATCH_MP_TAC ALGEBRA_DIFF THEN ASM_SIMP_TAC std_ss [SIGMA_ALGEBRA_ALGEBRA] THEN
547 FULL_SIMP_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER,
548 GSPECIFICATION, SUBSET_DEF],
549 ALL_TAC] THEN CONJ_TAC THENL
550 [ALL_TAC, SIMP_TAC std_ss [SPACE_SIGMA, halfspace_gt_in_halfspace, IN_UNIV]] THEN
551 SIMP_TAC std_ss [SPACE_SIGMA, IN_UNIV] THEN POP_ASSUM K_TAC THEN
552 KNOW_TAC ``!a. {x | a < x} = UNIV DIFF {x:real | x <= a}`` THENL
553 [RW_TAC std_ss [GSPECIFICATION, EXTENSION, IN_UNIV, IN_DIFF] THEN
554 REAL_ARITH_TAC, DISC_RW_KILL] THEN MATCH_MP_TAC ALGEBRA_DIFF THEN
555 RW_TAC std_ss [] THENL
556 [RW_TAC std_ss [algebra_def, sigma_def, subsets_def, space_def] THENL
557 [SIMP_TAC std_ss [subset_class_def, SUBSET_UNIV],
558 SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN
559 FULL_SIMP_TAC std_ss [sigma_algebra_alt_pow],
560 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN
561 RW_TAC std_ss [] THEN FULL_SIMP_TAC std_ss [sigma_algebra_alt_pow],
562 FULL_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN RW_TAC std_ss [] THEN
563 ONCE_REWRITE_TAC [METIS [subsets_def] ``P = subsets (univ(:real), P)``] THEN
564 MATCH_MP_TAC ALGEBRA_UNION THEN
565 FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA_ALGEBRA] THEN
566 FULL_SIMP_TAC std_ss [subsets_def]],
567 RW_TAC std_ss [algebra_def, sigma_def, subsets_def, space_def] THEN
568 SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN RW_TAC std_ss [] THEN
569 FULL_SIMP_TAC std_ss [sigma_algebra_alt_pow] THEN
570 FIRST_X_ASSUM (MP_TAC o SPEC ``{}:real->bool``) THEN ASM_REWRITE_TAC [] THEN
571 SIMP_TAC std_ss [DIFF_EMPTY],
572 ALL_TAC] THEN
573 RW_TAC std_ss [] THEN
574 KNOW_TAC ``!c. {x:real | x <= c} =
575 BIGINTER (IMAGE (\n:num. {x | x < (c + (1/2) pow n)}) UNIV)`` THENL
576 [RW_TAC std_ss [EXTENSION, IN_BIGINTER_IMAGE, IN_UNIV,IN_INTER] THEN EQ_TAC THENL
577 [RW_TAC std_ss [GSPECIFICATION] THEN
578 `0:real < (1/2) pow n` by RW_TAC real_ss [REAL_POW_LT] THEN
579 `0:real < ((1 / 2) pow n)` by METIS_TAC [POW_HALF_POS] THEN
580 ASM_REAL_ARITH_TAC, ALL_TAC] THEN
581 RW_TAC std_ss [GSPECIFICATION] THEN
582 `!n. x:real < (c + (1 / 2) pow n)` by METIS_TAC [] THEN
583 `(\n. c + (1 / 2) pow n) = (\n. (\n. c) n + (\n. (1 / 2) pow n) n) `
584 by RW_TAC real_ss [FUN_EQ_THM] THEN
585 ASSUME_TAC (ISPEC ``c:real`` SEQ_CONST) THEN
586 MP_TAC (ISPEC ``1 / (2:real)`` SEQ_POWER) THEN
587 KNOW_TAC ``abs (1 / 2) < 1:real`` THENL
588 [REWRITE_TAC [abs] THEN COND_CASES_TAC THEN
589 SIMP_TAC std_ss [REAL_HALF_BETWEEN] THEN
590 REWRITE_TAC [real_div, REAL_NEG_LMUL] THEN SIMP_TAC std_ss [GSYM real_div] THEN
591 SIMP_TAC real_ss [REAL_LT_LDIV_EQ], DISCH_TAC THEN ASM_REWRITE_TAC [] THEN
592 POP_ASSUM K_TAC THEN DISCH_TAC] THEN
593 MP_TAC (Q.SPECL [`(\n. c)`,`c`,`(\n. (1/2) pow n)`,`0`] SEQ_ADD) THEN
594 ASM_REWRITE_TAC [] THEN BETA_TAC THEN SIMP_TAC std_ss [REAL_ADD_RID] THEN
595 DISCH_TAC THEN METIS_TAC [REAL_LT_IMP_LE,
596 Q.SPECL [`r`,`c`,`(\n. c + (1 / 2) pow n)`] LE_SEQ_IMP_LE_LIM], ALL_TAC] THEN
597 FULL_SIMP_TAC std_ss [] THEN DISCH_TAC THEN
598 KNOW_TAC ``sigma_algebra (sigma univ(:real)
599 (IMAGE (\(i',j). {x | x < i'}) univ(:real # num)))`` THENL
600 [MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA THEN
601 SIMP_TAC std_ss [subset_class_def, SUBSET_UNIV],
602 DISCH_TAC] THEN
603 (MP_TAC o UNDISCH o Q.SPEC `(sigma univ(:real) (IMAGE (\(i',j). {x | x < i'})
604 univ(:real # num)))`)
605 (INST_TYPE [alpha |-> ``:real``] SIGMA_ALGEBRA_FN_BIGINTER) THEN
606 RW_TAC std_ss [] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
607 RW_TAC std_ss [IN_FUNSET, IN_UNIV] THEN MATCH_MP_TAC IN_SIGMA THEN
608 SIMP_TAC std_ss [IN_IMAGE, IN_UNIV] THEN
609 Q.EXISTS_TAC `(i + (1 / 2) pow n, 1)` THEN
610 SIMP_TAC std_ss [], ALL_TAC] THEN
611 METIS_TAC [OPEN_HALFSPACE_COMPONENT_LT, borel_open]
612QED
613val borel_eq_halfspace_less = borel_eq_less;
614
615Theorem borel_eq_le : (* was: borel_eq_halfspace_le *)
616 borel = sigma UNIV (IMAGE (\a. {x | x <= a}) UNIV)
617Proof
618 ONCE_REWRITE_TAC [SET_RULE
619 `` (IMAGE (\a. {x | x <= a}) univ(:real)) =
620 (IMAGE (\(a:real,i:num). (\a i. {x | x <= a}) a i) UNIV)``] THEN
621 KNOW_TAC `` (borel = sigma univ(:real)
622 (IMAGE (\(i:real,j:num). (\a i. {x | x < a}) i j) UNIV)) /\
623 (!i j. (i:real,j:num) IN UNIV ==>
624 (\a i. {x | x < a}) i j IN
625 subsets (sigma univ(:real)
626 (IMAGE (\(i,j). (\a i. {x | x <= a}) i j)
627 univ(:real # num)))) /\
628 !i j. (i,j) IN univ(:real # num) ==>
629 (\a i. {x | x <= a}) i j IN subsets borel`` THENL
630 [ALL_TAC, DISCH_THEN (MP_TAC o MATCH_MP borel_eq_sigmaI2) THEN
631 SIMP_TAC std_ss []] THEN
632 ONCE_REWRITE_TAC [SET_RULE
633 ``(IMAGE (\(i:real,j:num). (\a i. {x | x < a}) i j) UNIV) =
634 (IMAGE (\a. {x | x < a}) univ(:real))``] THEN
635 SIMP_TAC std_ss [borel_eq_less, IN_UNIV] THEN
636 KNOW_TAC ``!a:real. {x | x < a} =
637 BIGUNION {{x | x <= a - 1 / &(SUC n)} | n IN UNIV}`` THENL
638 [RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION, IN_UNIV] THEN
639 ASM_CASES_TAC ``x < a:real`` THENL
640 [ASM_REWRITE_TAC [] THEN MP_TAC (ISPEC ``a - x:real`` REAL_ARCH_INV_SUC) THEN
641 ASM_REWRITE_TAC [REAL_SUB_LT] THEN STRIP_TAC THEN
642 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [REAL_ARITH
643 ``a < b - c <=> c < b - a:real``]) THEN
644 Q.EXISTS_TAC `{x:real | x <= a - inv (&SUC n)}` THEN
645 ASM_SIMP_TAC std_ss [GSPECIFICATION] THEN
646 GEN_REWR_TAC LAND_CONV [REAL_LE_LT] THEN ASM_SIMP_TAC real_ss [real_div] THEN
647 METIS_TAC [], ALL_TAC] THEN
648 ASM_SIMP_TAC std_ss [] THEN RW_TAC std_ss [] THEN
649 ASM_CASES_TAC ``(x:real) NOTIN s`` THEN
650 ASM_SIMP_TAC std_ss [] THEN GEN_TAC THEN FULL_SIMP_TAC std_ss [REAL_NOT_LT] THEN
651 EXISTS_TAC ``x:real`` THEN ASM_SIMP_TAC std_ss [REAL_NOT_LE] THEN
652 KNOW_TAC ``0:real < 1 / &SUC n`` THENL [ALL_TAC, ASM_REAL_ARITH_TAC] THEN
653 SIMP_TAC real_ss [REAL_LT_RDIV_EQ], DISCH_TAC] THEN
654 ASM_REWRITE_TAC [] THEN CONJ_TAC THENL
655 [RW_TAC std_ss [subsets_def, sigma_def, IN_BIGINTER,
656 GSPECIFICATION, SUBSET_DEF] THEN
657 FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subsets_def] THEN
658 FIRST_X_ASSUM MATCH_MP_TAC THEN
659 CONJ_TAC THENL
660 [SIMP_TAC std_ss [GSYM IMAGE_DEF] THEN
661 MATCH_MP_TAC image_countable THEN
662 SIMP_TAC std_ss [pred_setTheory.COUNTABLE_NUM], ALL_TAC] THEN
663 RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
664 SET_TAC [], ALL_TAC] THEN
665 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN ASM_REWRITE_TAC [] THEN
666 SIMP_TAC std_ss [GSYM borel_eq_less] THEN GEN_TAC THEN
667 MATCH_MP_TAC borel_closed THEN SIMP_TAC std_ss [CLOSED_HALFSPACE_COMPONENT_LE]
668QED
669val borel_eq_halfspace_le = borel_eq_le;
670
671Theorem borel_eq_gr : (* borel_eq_greaterThan *)
672 borel = sigma UNIV (IMAGE (\a. {x | a < x}) UNIV)
673Proof
674 KNOW_TAC ``(borel = sigma univ(:real)
675 (IMAGE (\(i,j). (\a i. {x | x <= a}) i j) univ(:real#num))) /\
676 (!i j.
677 (i:real,j:num) IN UNIV ==>
678 (\a i. {x | x <= a}) i j IN
679 subsets
680 (sigma univ(:real) (IMAGE (\a. {x | a < x}) univ(:real)))) /\
681 !i. (\a. {x | a < x}) i IN subsets borel`` THENL
682 [ALL_TAC, DISCH_THEN (MP_TAC o MATCH_MP borel_eq_sigmaI4) THEN
683 SIMP_TAC std_ss []] THEN SIMP_TAC std_ss [borel_eq_le] THEN
684 ONCE_REWRITE_TAC [SET_RULE
685 `` (IMAGE (\a. {x | x <= a}) univ(:real)) =
686 (IMAGE (\(a:real,i:num). (\a i. {x | x <= a}) a i) UNIV)``] THEN
687 SIMP_TAC std_ss [IN_UNIV] THEN CONJ_TAC THENL
688 [ALL_TAC,
689 ONCE_REWRITE_TAC [SET_RULE ``(IMAGE (\(a:real,i:num). {x | x <= a}) UNIV) =
690 (IMAGE (\a. {x | x <= a}) univ(:real))``] THEN
691 SIMP_TAC std_ss [GSYM borel_eq_le] THEN GEN_TAC THEN
692 MATCH_MP_TAC borel_open THEN SIMP_TAC std_ss [OPEN_INTERVAL_RIGHT]] THEN
693 KNOW_TAC ``!a:real. {x | x <= a} = UNIV DIFF {x | a < x}`` THENL
694 [RW_TAC std_ss [EXTENSION, IN_DIFF, GSPECIFICATION, IN_UNIV] THEN
695 REAL_ARITH_TAC, DISCH_TAC] THEN
696 RW_TAC std_ss [sigma_def, subsets_def, IN_BIGINTER, GSPECIFICATION,
697 IN_UNIV, SUBSET_DEF] THEN
698 ONCE_REWRITE_TAC [METIS [subsets_def] ``P = subsets (univ(:real), P)``] THEN
699 MATCH_MP_TAC ALGEBRA_DIFF THEN ASM_SIMP_TAC std_ss [SIGMA_ALGEBRA_ALGEBRA] THEN
700 CONJ_TAC THENL
701 [FULL_SIMP_TAC std_ss [sigma_algebra_alt_pow, subsets_def] THEN
702 ONCE_REWRITE_TAC [SET_RULE ``UNIV = UNIV DIFF {}``] THEN
703 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC [],
704 ALL_TAC] THEN
705 SIMP_TAC std_ss [subsets_def] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
706 SIMP_TAC std_ss [IN_IMAGE, IN_UNIV] THEN METIS_TAC []
707QED
708val borel_eq_greaterThan = borel_eq_gr;
709
710Theorem borel_eq_ge_le : (* borel_eq_atLeastAtMost *)
711 borel = sigma UNIV (IMAGE (\(a,b). {x | a <= x /\ x <= b}) UNIV)
712Proof
713 ONCE_REWRITE_TAC [METIS [] ``{x | a <= x /\ x <= b} =
714 (\a b. {x:real | a <= x /\ x <= b}) a b``] THEN
715 KNOW_TAC ``(borel = sigma univ(:real) (IMAGE (\a. {x | x <= a}) univ(:real))) /\
716 (!i.
717 (\a. {x | x <= a}) i IN
718 subsets
719 (sigma univ(:real)
720 (IMAGE (\(i,j). (\a b. {x | a <= x /\ x <= b}) i j)
721 univ(:real # real)))) /\
722 !i j. (\a b. {x | a <= x /\ x <= b}) i j IN subsets borel`` THENL
723 [ALL_TAC,
724 DISCH_THEN (MP_TAC o MATCH_MP borel_eq_sigmaI5) THEN SIMP_TAC std_ss []] THEN
725 SIMP_TAC std_ss [borel_eq_le] THEN
726 KNOW_TAC ``!a. {x | x <= a} =
727 BIGUNION {{x:real | -&n <= x /\ x <= a} | n IN UNIV}`` THENL
728 [RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION, IN_UNIV] THEN
729 EQ_TAC THENL
730 [ALL_TAC, STRIP_TAC THEN POP_ASSUM (MP_TAC o SPEC ``x:real``) THEN
731 ASM_REWRITE_TAC [] THEN REAL_ARITH_TAC] THEN
732 DISCH_TAC THEN MP_TAC (ISPEC ``-x:real`` SIMP_REAL_ARCH) THEN STRIP_TAC THEN
733 POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [GSYM REAL_LE_NEG]) THEN
734 RW_TAC std_ss [REAL_NEG_NEG] THEN Q.EXISTS_TAC `{x | -&n <= x /\ x <= a}` THEN
735 ASM_SIMP_TAC std_ss [GSPECIFICATION] THEN METIS_TAC [], DISCH_TAC] THEN
736 CONJ_TAC THENL
737 [ALL_TAC, SIMP_TAC std_ss [GSYM borel_eq_le] THEN
738 REPEAT GEN_TAC THEN MATCH_MP_TAC borel_closed THEN
739 SIMP_TAC std_ss [GSYM interval, CLOSED_INTERVAL]] THEN
740 RW_TAC std_ss [subsets_def, sigma_def, IN_BIGINTER,
741 GSPECIFICATION, SUBSET_DEF] THEN
742 ONCE_REWRITE_TAC [METIS [] ``{x | -&n <= x /\ x <= i} =
743 (\n. {x:real | -&n <= x /\ x <= i}) n``] THEN
744 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UN THEN EXISTS_TAC ``univ(:real)`` THEN
745 ASM_SIMP_TAC std_ss [COUNTABLE_NUM] THEN
746 RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
747 SET_TAC []
748QED
749val borel_eq_atLeastAtMost = borel_eq_ge_le;
750
751(* this is the original definition *)
752Theorem borel_def = borel_eq_le;
753
754Theorem borel_eq_gr_le :
755 borel = sigma UNIV (IMAGE (\(a,b). {x | a < x /\ x <= b}) UNIV)
756Proof
757 ONCE_REWRITE_TAC [METIS [] ``{x | a < x /\ x <= b} =
758 (\a b. {x:real | a < x /\ x <= b}) a b``]
759 >> Suff `(borel = sigma univ(:real) (IMAGE (\a. {x | x <= a}) univ(:real))) /\
760 (!i. (\a. {x | x <= a}) i IN
761 subsets (sigma univ(:real)
762 (IMAGE (\(i,j). (\a b. {x | a < x /\ x <= b}) i j)
763 univ(:real # real)))) /\
764 !i j. (\a b. {x | a < x /\ x <= b}) i j IN subsets borel`
765 >- (DISCH_THEN (MP_TAC o MATCH_MP borel_eq_sigmaI5) >> SIMP_TAC std_ss [])
766 >> SIMP_TAC std_ss [borel_eq_le]
767 >> Know `!a. {x | x <= a} =
768 BIGUNION {{x:real | -&n < x /\ x <= a} | n IN UNIV}`
769 >- (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION, IN_UNIV] \\
770 reverse EQ_TAC
771 >- (STRIP_TAC >> POP_ASSUM (MP_TAC o SPEC ``x:real``) \\
772 ASM_REWRITE_TAC [] >> REAL_ARITH_TAC) \\
773 DISCH_TAC \\
774 MP_TAC (ISPEC ``x:real`` SIMP_REAL_ARCH_NEG) >> STRIP_TAC \\
775 Q.EXISTS_TAC `{x | -&SUC n < x /\ x <= a}` \\
776 ASM_SIMP_TAC std_ss [GSPECIFICATION] \\
777 CONJ_TAC >- (MATCH_MP_TAC REAL_LTE_TRANS \\
778 Q.EXISTS_TAC ‘-&n’ >> rw []) \\
779 Q.EXISTS_TAC ‘SUC n’ >> rw [])
780 >> DISCH_TAC
781 >> CONJ_TAC
782 >- (RW_TAC std_ss [subsets_def, sigma_def, IN_BIGINTER,
783 GSPECIFICATION, SUBSET_DEF] \\
784 ONCE_REWRITE_TAC [METIS [] ``{x | -&n < x /\ x <= i} =
785 (\n. {x:real | -&n < x /\ x <= i}) n``] \\
786 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UN >> EXISTS_TAC ``univ(:real)`` \\
787 ASM_SIMP_TAC std_ss [COUNTABLE_NUM] \\
788 RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV] >> FIRST_X_ASSUM MATCH_MP_TAC \\
789 SET_TAC [])
790 (* below are new steps by Chun Tian *)
791 >> rpt GEN_TAC
792 >> Know ‘{x | i < x /\ x <= j} = {x | x <= j} DIFF {x | x <= i}’
793 >- (rw [Once EXTENSION] >> METIS_TAC [real_lt]) >> Rewr'
794 >> MATCH_MP_TAC SIGMA_ALGEBRA_DIFF
795 >> STRONG_CONJ_TAC
796 >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> rw [subset_class_def])
797 >> DISCH_TAC
798 >> CONJ_TAC
799 >| [ (* goal 1 (of 2) *)
800 Suff ‘{x | x <= j} IN (IMAGE (\a. {x | x <= a}) univ(:real))’
801 >- METIS_TAC [SUBSET_DEF, SIGMA_SUBSET_SUBSETS] \\
802 rw [] >> Q.EXISTS_TAC ‘j’ >> REWRITE_TAC [],
803 (* goal 2 (of 2) *)
804 Suff ‘{x | x <= i} IN (IMAGE (\a. {x | x <= a}) univ(:real))’
805 >- METIS_TAC [SUBSET_DEF, SIGMA_SUBSET_SUBSETS] \\
806 rw [] >> Q.EXISTS_TAC ‘i’ >> REWRITE_TAC [] ]
807QED
808
809(* NOTE: removed ‘sigma_algebra s’ due to changes in ‘measurable’ *)
810Theorem in_borel_measurable:
811 !f s. f IN borel_measurable s <=>
812 (!s'. s' IN subsets (sigma UNIV (IMAGE (\a. {x | x <= a}) UNIV)) ==>
813 PREIMAGE f s' INTER space s IN subsets s)
814Proof
815 RW_TAC std_ss [IN_MEASURABLE, borel_def,
816 SPACE_SIGMA, IN_FUNSET, IN_UNIV]
817 >> `sigma_algebra (sigma UNIV (IMAGE (\a. {x | x <= a}) UNIV))`
818 by (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA
819 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, IN_UNIV])
820 >> ASM_REWRITE_TAC []
821QED
822
823Theorem in_borel_measurable_I :
824 (\x. x) IN measurable borel borel
825Proof
826 ‘(\x :real. x) = I’ by METIS_TAC [I_THM]
827 >> POP_ORW
828 >> MATCH_MP_TAC MEASURABLE_I
829 >> REWRITE_TAC [sigma_algebra_borel]
830QED
831
832Theorem borel_measurable_indicator:
833 !s a. sigma_algebra s /\ a IN subsets s ==>
834 indicator_fn a IN borel_measurable s
835Proof
836 RW_TAC std_ss [indicator_fn_def, in_borel_measurable]
837 >> Cases_on `1 IN s'`
838 >- (Cases_on `0 IN s'`
839 >- (`PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = space s`
840 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE]
841 >> METIS_TAC [])
842 >> POP_ORW
843 >> MATCH_MP_TAC ALGEBRA_SPACE >> MATCH_MP_TAC SIGMA_ALGEBRA_ALGEBRA
844 >> ASM_REWRITE_TAC [])
845 >> `PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = a`
846 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE]
847 >> METIS_TAC [SIGMA_ALGEBRA, algebra_def, subset_class_def, SUBSET_DEF])
848 >> ASM_REWRITE_TAC [])
849 >> Cases_on `0 IN s'`
850 >- (`PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = space s DIFF a`
851 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, IN_DIFF]
852 >> METIS_TAC [SIGMA_ALGEBRA, algebra_def, subset_class_def, SUBSET_DEF])
853 >> METIS_TAC [SIGMA_ALGEBRA, algebra_def])
854 >> `PREIMAGE (\x. (if x IN a then 1 else 0)) s' INTER space s = {}`
855 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, NOT_IN_EMPTY] >> METIS_TAC [])
856 >> POP_ORW >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, algebra_def]
857QED
858
859(* NOTE: moved ‘sigma_algebra m’ to antecedents due to changes of ‘measurable’
860
861 cf. IN_MEASURABLE_BOREL_RC in borelTheory
862 *)
863Theorem in_borel_measurable_le :
864 !f m. sigma_algebra m ==>
865 (f IN borel_measurable m <=>
866 f IN (space m -> UNIV) /\
867 !a. {w | w IN space m /\ f w <= a} IN subsets m)
868Proof
869 rpt STRIP_TAC >> EQ_TAC
870 >- (RW_TAC std_ss [in_borel_measurable, subsets_def, space_def,
871 IN_FUNSET, IN_UNIV]
872 >> POP_ASSUM (MP_TAC o REWRITE_RULE [PREIMAGE_def] o Q.SPEC `{b | b <= a}`)
873 >> RW_TAC std_ss [GSPECIFICATION]
874 >> `{x | f x <= a} INTER space m =
875 {w | w IN space m /\ f w <= a}`
876 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, GSPECIFICATION]
877 >> DECIDE_TAC)
878 >> FULL_SIMP_TAC std_ss [] >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM MATCH_MP_TAC
879 >> MATCH_MP_TAC IN_SIGMA
880 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV, Once EXTENSION, GSPECIFICATION]
881 >> Q.EXISTS_TAC `a` >> SIMP_TAC std_ss [])
882 >> RW_TAC std_ss [borel_def]
883 >> MATCH_MP_TAC MEASURABLE_SIGMA
884 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, subset_class_def, space_def, subsets_def, SUBSET_UNIV,
885 IN_IMAGE]
886 >> `PREIMAGE f {x | x <= a} INTER space m =
887 {w | w IN space m /\ f w <= a}`
888 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, GSPECIFICATION, IN_PREIMAGE]
889 >> DECIDE_TAC)
890 >> RW_TAC std_ss []
891QED
892
893(* cf. IN_MEASURABLE_BOREL_IMP in borelTheory *)
894Theorem sigma_le_less:
895 !f A. sigma_algebra A /\ (!(a:real). {w | w IN space A /\ f w <= a} IN subsets A) ==>
896 !a. {w | w IN space A /\ f w < a} IN subsets A
897Proof
898 rpt STRIP_TAC
899 >> `BIGUNION (IMAGE (\n. {w | w IN space A /\ f w <= a - inv(&(SUC n))}) (UNIV:num->bool)) =
900 {w | w IN space A /\ f w < a}`
901 by (ONCE_REWRITE_TAC [EXTENSION]
902 >> RW_TAC std_ss [GSPECIFICATION, IN_BIGUNION, IN_IMAGE, IN_UNIV]
903 >> `(?s. x IN s /\ ?n. s = {w | w IN space A /\ f w <= a - inv (&SUC n)}) =
904 (?n. x IN {w | w IN space A /\ f w <= a - inv (& (SUC n))})`
905 by METIS_TAC [GSYM EXTENSION]
906 >> POP_ORW
907 >> RW_TAC std_ss [GSPECIFICATION]
908 >> EQ_TAC
909 >- (RW_TAC std_ss [] >- METIS_TAC []
910 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `a - inv (& (SUC n))`
911 >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_INV_EQ]
912 >> METIS_TAC [])
913 >> RW_TAC std_ss []
914 >> `(\n. inv (($& o SUC) n)) --> 0`
915 by (MATCH_MP_TAC SEQ_INV0
916 >> RW_TAC std_ss [o_DEF]
917 >> Q.EXISTS_TAC `clg y`
918 >> RW_TAC std_ss [GREATER_EQ, real_gt]
919 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `&(clg y)`
920 >> RW_TAC std_ss [REAL_LT, LE_NUM_CEILING]
921 >> MATCH_MP_TAC LESS_EQ_LESS_TRANS >> Q.EXISTS_TAC `n`
922 >> RW_TAC arith_ss [])
923 >> FULL_SIMP_TAC real_ss [SEQ, o_DEF]
924 >> POP_ASSUM (MP_TAC o REWRITE_RULE [REAL_LT_SUB_LADD] o Q.SPEC `a - f x`)
925 >> RW_TAC real_ss [ABS_INV, ABS_N, REAL_LE_SUB_LADD]
926 >> Q.EXISTS_TAC `N` >> MATCH_MP_TAC REAL_LT_IMP_LE
927 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> POP_ASSUM MATCH_MP_TAC >> RW_TAC std_ss [])
928 >> POP_ASSUM (MP_TAC o GSYM) >> RW_TAC std_ss []
929 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA]
930 >> Q.PAT_ASSUM `!c. P c ==> BIGUNION c IN subsets A` MATCH_MP_TAC
931 >> RW_TAC std_ss [COUNTABLE_NUM, image_countable, SUBSET_DEF, IN_IMAGE, IN_UNIV]
932 >> METIS_TAC []
933QED
934
935Theorem sigma_less_ge:
936 !f A. sigma_algebra A /\ (!(a:real). {w | w IN space A /\ f w < a} IN subsets A) ==>
937 !a. {w | w IN space A /\ a <= f w} IN subsets A
938Proof
939 rpt STRIP_TAC
940 >> `{w | w IN space A /\ a <= f w} =
941 space A DIFF {w | w IN space A /\ f w < a}`
942 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt]
943 >> DECIDE_TAC)
944 >> POP_ORW
945 >> METIS_TAC [SIGMA_ALGEBRA]
946QED
947
948Theorem sigma_ge_gr:
949 !f A. sigma_algebra A /\ (!(a:real). {w | w IN space A /\ a <= f w} IN subsets A) ==>
950 !a. {w | w IN space A /\ a < f w} IN subsets A
951Proof
952 rpt STRIP_TAC
953 >> `BIGUNION (IMAGE (\n. {w | w IN space A /\ a <= f w - inv(&(SUC n))}) (UNIV:num->bool)) =
954 {w | w IN space A /\ a < f w}`
955 by (ONCE_REWRITE_TAC [EXTENSION]
956 >> RW_TAC std_ss [GSPECIFICATION, IN_BIGUNION, IN_IMAGE, IN_UNIV]
957 >> `(?s. x IN s /\ ?n. s = {w | w IN space A /\ a <= f w - inv (& (SUC n))}) =
958 (?n. x IN {w | w IN space A /\ a <= f w - inv (& (SUC n))})`
959 by METIS_TAC []
960 >> POP_ORW
961 >> RW_TAC std_ss [GSPECIFICATION]
962 >> EQ_TAC
963 >- (RW_TAC std_ss [] >- ASM_REWRITE_TAC []
964 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f x - inv (& (SUC n))`
965 >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_INV_EQ])
966 >> RW_TAC std_ss []
967 >> `(\n. inv (($& o SUC) n)) --> 0`
968 by (MATCH_MP_TAC SEQ_INV0
969 >> RW_TAC std_ss [o_DEF]
970 >> Q.EXISTS_TAC `clg y`
971 >> RW_TAC std_ss [GREATER_EQ, real_gt]
972 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `&(clg y)`
973 >> RW_TAC std_ss [REAL_LT, LE_NUM_CEILING]
974 >> MATCH_MP_TAC LESS_EQ_LESS_TRANS >> Q.EXISTS_TAC `n`
975 >> RW_TAC arith_ss [])
976 >> FULL_SIMP_TAC real_ss [SEQ, o_DEF]
977 >> POP_ASSUM (MP_TAC o REWRITE_RULE [REAL_LT_SUB_LADD] o Q.SPEC `f x - a`)
978 >> RW_TAC real_ss [ABS_INV, ABS_N, REAL_LE_SUB_LADD]
979 >> Q.EXISTS_TAC `N` >> MATCH_MP_TAC REAL_LT_IMP_LE
980 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> POP_ASSUM MATCH_MP_TAC >> RW_TAC std_ss [])
981 >> POP_ASSUM (MP_TAC o GSYM) >> RW_TAC std_ss []
982 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA]
983 >> Q.PAT_X_ASSUM `!c. P c ==> BIGUNION c IN subsets A` MATCH_MP_TAC
984 >> RW_TAC std_ss [COUNTABLE_NUM, image_countable, SUBSET_DEF, IN_IMAGE, IN_UNIV, REAL_LE_SUB_LADD]
985 >> METIS_TAC []
986QED
987
988Theorem sigma_gr_le:
989 !f A. sigma_algebra A /\
990 (!(a:real). {w | w IN space A /\ a < f w} IN subsets A) ==>
991 !a. {w | w IN space A /\ f w <= a} IN subsets A
992Proof
993 rpt STRIP_TAC
994 >> `{w | w IN space A /\ f w <= a} =
995 space A DIFF {w | w IN space A /\ a < f w}`
996 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt]
997 >> DECIDE_TAC)
998 >> POP_ORW
999 >> METIS_TAC [SIGMA_ALGEBRA]
1000QED
1001
1002(* NOTE: moved ‘sigma_algebra m’ to antecedents due to changes of ‘measurable’ *)
1003Theorem in_borel_measurable_gr :
1004 !f m. sigma_algebra m ==>
1005 (f IN borel_measurable m <=>
1006 f IN (space m -> UNIV) /\
1007 !a. {w | w IN space m /\ a < f w} IN subsets m)
1008Proof
1009 RW_TAC std_ss [in_borel_measurable_le]
1010 >> EQ_TAC
1011 >- (RW_TAC std_ss [IN_FUNSET, IN_UNIV]
1012 >> `{w | w IN space m /\ a < f w} =
1013 space m DIFF {w | w IN space m /\ f w <= a}`
1014 by (ONCE_REWRITE_TAC [EXTENSION]
1015 >> RW_TAC std_ss [IN_DIFF, GSPECIFICATION, real_lt]
1016 >> DECIDE_TAC)
1017 >> POP_ORW
1018 >> METIS_TAC [SIGMA_ALGEBRA, space_def, subsets_def])
1019 >> METIS_TAC [sigma_gr_le, SPACE, subsets_def, space_def]
1020QED
1021
1022(* NOTE: moved ‘sigma_algebra m’ to antecedents due to changes of ‘measurable’ *)
1023Theorem in_borel_measurable_less :
1024 !f m. sigma_algebra m ==>
1025 (f IN borel_measurable m <=>
1026 f IN (space m -> UNIV) /\
1027 !a. {w | w IN space m /\ f w < a} IN subsets m)
1028Proof
1029 RW_TAC std_ss [in_borel_measurable_le, IN_FUNSET, IN_UNIV]
1030 >> EQ_TAC
1031 >- (RW_TAC std_ss [] \\
1032 METIS_TAC [sigma_le_less, SPACE, subsets_def, space_def])
1033 >> RW_TAC std_ss []
1034 >> `BIGUNION (IMAGE (\n. {w | w IN space m /\ a <= f w - inv(&(SUC n))}) (UNIV:num->bool)) =
1035 {w | w IN space m /\ a < f w}`
1036 by (ONCE_REWRITE_TAC [EXTENSION]
1037 >> RW_TAC std_ss [GSPECIFICATION, IN_BIGUNION, IN_IMAGE, IN_UNIV]
1038 >> `(?s. x IN s /\ ?n. s = {w | w IN space m /\ a <= f w - inv (& (SUC n))}) =
1039 (?n. x IN {w | w IN space m /\ a <= f w - inv (& (SUC n))})`
1040 by METIS_TAC []
1041 >> POP_ORW
1042 >> RW_TAC std_ss [GSPECIFICATION]
1043 >> EQ_TAC
1044 >- (RW_TAC std_ss [] >- ASM_REWRITE_TAC [] \\
1045 MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f x - inv (&(SUC n))` \\
1046 RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_INV_EQ])
1047 >> RW_TAC std_ss []
1048 >> `(\n. inv (($& o SUC) n)) --> 0`
1049 by (MATCH_MP_TAC SEQ_INV0
1050 >> RW_TAC std_ss [o_DEF]
1051 >> Q.EXISTS_TAC `clg y`
1052 >> RW_TAC std_ss [GREATER_EQ, real_gt]
1053 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `&(clg y)`
1054 >> RW_TAC std_ss [REAL_LT, LE_NUM_CEILING]
1055 >> MATCH_MP_TAC LESS_EQ_LESS_TRANS >> Q.EXISTS_TAC `n`
1056 >> RW_TAC arith_ss [])
1057 >> FULL_SIMP_TAC real_ss [SEQ, o_DEF]
1058 >> POP_ASSUM (MP_TAC o REWRITE_RULE [REAL_LT_SUB_LADD] o Q.SPEC `f x - a`)
1059 >> RW_TAC real_ss [ABS_INV, ABS_N, REAL_LE_SUB_LADD]
1060 >> Q.EXISTS_TAC `N` >> MATCH_MP_TAC REAL_LT_IMP_LE
1061 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> POP_ASSUM MATCH_MP_TAC >> RW_TAC std_ss [])
1062 >> `{w | w IN space m /\ f w <= a} =
1063 space m DIFF {w | w IN space m /\ a < f w}`
1064 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt]
1065 >> DECIDE_TAC)
1066 >> POP_ORW
1067 >> Suff `{w | w IN space m /\ a < f w} IN subsets m`
1068 >- METIS_TAC [SPACE, subsets_def, space_def, SIGMA_ALGEBRA]
1069 >> POP_ASSUM (MP_TAC o GSYM) >> RW_TAC std_ss []
1070 >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subsets_def]
1071 >> Q.PAT_X_ASSUM `!c. P c ==> BIGUNION c IN subsets m` MATCH_MP_TAC
1072 >> RW_TAC std_ss [COUNTABLE_NUM, image_countable, SUBSET_DEF, IN_IMAGE, IN_UNIV, REAL_LE_SUB_LADD]
1073 >> `{w | w IN space m /\ a + inv (& (SUC n)) <= f w} =
1074 space m DIFF {w | w IN space m /\ f w < a + inv (& (SUC n))}`
1075 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt]
1076 >> DECIDE_TAC)
1077 >> POP_ORW
1078 >> Suff `{w | w IN space m /\ f w < a + inv (& (SUC n))} IN subsets m`
1079 >- METIS_TAC [SPACE, subsets_def, space_def, SIGMA_ALGEBRA]
1080 >> METIS_TAC []
1081QED
1082
1083(* NOTE: moved ‘sigma_algebra m’ to antecedents due to changes of ‘measurable’ *)
1084Theorem in_borel_measurable_ge :
1085 !f m. sigma_algebra m ==>
1086 (f IN borel_measurable m <=>
1087 f IN (space m -> UNIV) /\
1088 !a. {w | w IN space m /\ a <= f w} IN subsets m)
1089Proof
1090 RW_TAC std_ss [in_borel_measurable_less, IN_FUNSET, IN_UNIV]
1091 >> EQ_TAC
1092 >- (RW_TAC std_ss []
1093 >> `{w | w IN space m /\ a <= f w} =
1094 space m DIFF {w | w IN space m /\ f w < a}`
1095 by (RW_TAC std_ss [Once EXTENSION, IN_DIFF, GSPECIFICATION, real_lt]
1096 >> DECIDE_TAC)
1097 >> POP_ORW
1098 >> METIS_TAC [SIGMA_ALGEBRA, space_def, subsets_def])
1099 >> METIS_TAC [sigma_ge_gr, sigma_gr_le, sigma_le_less, SPACE, subsets_def, space_def]
1100QED
1101
1102Theorem in_borel_measurable_ge_lt_imp :
1103 !A f a b. sigma_algebra A /\ f IN borel_measurable A ==>
1104 {x | x IN space A /\ a <= f x /\ f x < b} IN subsets A
1105Proof
1106 rpt STRIP_TAC
1107 >> ‘{x | x IN space A /\ a <= f x /\ f x < b} =
1108 {x | x IN space A /\ a <= f x} INTER {x | x IN space A /\ f x < b}’
1109 by SET_TAC [] >> POP_ORW
1110 >> MATCH_MP_TAC SIGMA_ALGEBRA_INTER >> rw [] (* 2 subgoals *)
1111 >| [ (* goal 1 (of 2) *)
1112 MP_TAC (Q.SPECL [‘f’, ‘A’] (iffLR in_borel_measurable_ge)) \\
1113 rw [IN_FUNSET],
1114 (* goal 2 (of 2) *)
1115 MP_TAC (Q.SPECL [‘f’, ‘A’] (iffLR in_borel_measurable_less)) \\
1116 rw [IN_FUNSET] ]
1117QED
1118
1119Theorem borel_measurable_sets_le :
1120 !a. {x | x <= a} IN subsets borel
1121Proof
1122 ASSUME_TAC
1123 (REWRITE_RULE [space_borel, sigma_algebra_borel, IN_FUNSET, IN_UNIV, I_THM]
1124 (Q.SPECL [`I`, `borel`]
1125 (INST_TYPE [``:'a`` |-> ``:real``] in_borel_measurable_le)))
1126 >> POP_ASSUM (REWRITE_TAC o wrap o SYM)
1127 >> MATCH_MP_TAC MEASURABLE_I
1128 >> ACCEPT_TAC sigma_algebra_borel
1129QED
1130
1131Theorem borel_measurable_sets_less :
1132 !a. {x | x < a} IN subsets borel
1133Proof
1134 MATCH_MP_TAC
1135 (REWRITE_RULE [space_borel, sigma_algebra_borel, IN_UNIV, I_THM]
1136 (Q.SPECL [`I`, `borel`]
1137 (INST_TYPE [``:'a`` |-> ``:real``] sigma_le_less)))
1138 >> REWRITE_TAC [borel_measurable_sets_le]
1139QED
1140
1141Theorem borel_measurable_sets_ge :
1142 !a. {x | a <= x} IN subsets borel
1143Proof
1144 MATCH_MP_TAC
1145 (REWRITE_RULE [space_borel, sigma_algebra_borel, IN_UNIV, I_THM]
1146 (Q.SPECL [`I`, `borel`]
1147 (INST_TYPE [``:'a`` |-> ``:real``] sigma_less_ge)))
1148 >> REWRITE_TAC [borel_measurable_sets_less]
1149QED
1150
1151Theorem borel_measurable_sets_gr :
1152 !a. {x | a < x} IN subsets borel
1153Proof
1154 MATCH_MP_TAC
1155 (REWRITE_RULE [space_borel, sigma_algebra_borel, IN_UNIV, I_THM]
1156 (Q.SPECL [`I`, `borel`]
1157 (INST_TYPE [``:'a`` |-> ``:real``] sigma_ge_gr)))
1158 >> REWRITE_TAC [borel_measurable_sets_ge]
1159QED
1160
1161Theorem borel_measurable_sets_gr_less :
1162 !a b. {x | a < x /\ x < b} IN subsets borel
1163Proof
1164 rpt GEN_TAC
1165 >> `{x | a < x /\ x < b} = {x | a < x} INTER {x | x < b}`
1166 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER]
1167 >> POP_ORW
1168 >> MATCH_MP_TAC ALGEBRA_INTER
1169 >> rw [borel_measurable_sets_gr, borel_measurable_sets_less]
1170 >> METIS_TAC [SIGMA_ALGEBRA_ALGEBRA, sigma_algebra_borel]
1171QED
1172
1173Theorem borel_measurable_sets_gr_le :
1174 !a b. {x | a < x /\ x <= b} IN subsets borel
1175Proof
1176 rpt GEN_TAC
1177 >> `{x | a < x /\ x <= b} = {x | a < x} INTER {x | x <= b}`
1178 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER]
1179 >> POP_ORW
1180 >> MATCH_MP_TAC ALGEBRA_INTER
1181 >> rw [borel_measurable_sets_gr, borel_measurable_sets_le]
1182 >> METIS_TAC [SIGMA_ALGEBRA_ALGEBRA, sigma_algebra_borel]
1183QED
1184
1185Theorem borel_measurable_sets_ge_less :
1186 !a b. {x | a <= x /\ x < b} IN subsets borel
1187Proof
1188 rpt GEN_TAC
1189 >> `{x | a <= x /\ x < b} = {x | a <= x} INTER {x | x < b}`
1190 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER]
1191 >> POP_ORW
1192 >> MATCH_MP_TAC ALGEBRA_INTER
1193 >> rw [borel_measurable_sets_ge, borel_measurable_sets_less]
1194 >> METIS_TAC [SIGMA_ALGEBRA_ALGEBRA, sigma_algebra_borel]
1195QED
1196
1197Theorem borel_measurable_sets_ge_le :
1198 !a b. {x | a <= x /\ x <= b} IN subsets borel
1199Proof
1200 rpt GEN_TAC
1201 >> `{x | a <= x /\ x <= b} = {x | a <= x} INTER {x | x <= b}`
1202 by RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER]
1203 >> POP_ORW
1204 >> MATCH_MP_TAC ALGEBRA_INTER
1205 >> rw [borel_measurable_sets_ge, borel_measurable_sets_le]
1206 >> METIS_TAC [SIGMA_ALGEBRA_ALGEBRA, sigma_algebra_borel]
1207QED
1208
1209(* also used in borelTheory.lambda_point_eq_zero *)
1210Theorem REAL_SING_BIGINTER :
1211 !(c :real). {c} = BIGINTER (IMAGE (\n. {x | c - ((1/2) pow n) <= x /\
1212 x < c + ((1/2) pow n)}) UNIV)
1213Proof
1214 RW_TAC std_ss [EXTENSION, IN_BIGINTER_IMAGE, IN_UNIV, IN_SING, IN_INTER]
1215 >> EQ_TAC >- RW_TAC set_ss [REAL_POW_LT, REAL_LT_IMP_LE, REAL_LT_ADDR, REAL_LT_DIV,
1216 HALF_POS, REAL_LT_ADDNEG2, real_sub, IN_INTER]
1217 >> RW_TAC std_ss [GSPECIFICATION]
1218 >> `!n. c - (1/2) pow n <= x` by FULL_SIMP_TAC real_ss [real_sub]
1219 >> `!n. x <= c + (1/2) pow n` by FULL_SIMP_TAC real_ss [REAL_LT_IMP_LE]
1220 >> `(\n. c - (1/2) pow n) = (\n. (\n. c) n - (\n. (1/2) pow n) n)`
1221 by RW_TAC real_ss [FUN_EQ_THM]
1222 >> `(\n. c + (1/2) pow n) = (\n. (\n. c) n + (\n. (1/2) pow n) n)`
1223 by RW_TAC real_ss [FUN_EQ_THM]
1224 >> `(\n. c) --> c` by RW_TAC std_ss [SEQ_CONST]
1225 >> `(\n. (1/2) pow n) --> 0` by RW_TAC real_ss [SEQ_POWER]
1226 >> `(\n. c - (1/2) pow n) --> c`
1227 by METIS_TAC [Q.SPECL [`(\n. c)`, `c`, `(\n. (1/2) pow n)`, `0`] SEQ_SUB, REAL_SUB_RZERO]
1228 >> `(\n. c + (1/2) pow n) --> c`
1229 by METIS_TAC [Q.SPECL [`(\n. c)`, `c`, `(\n. (1/2) pow n)`, `0`] SEQ_ADD, REAL_ADD_RID]
1230 >> `c <= x` by METIS_TAC [Q.SPECL [`x`, `c`, `(\n. c - (1/2) pow n)`] SEQ_LE_IMP_LIM_LE]
1231 >> `x <= c` by METIS_TAC [Q.SPECL [`x`, `c`, `(\n. c + (1/2) pow n)`] LE_SEQ_IMP_LE_LIM]
1232 >> METIS_TAC [REAL_LE_ANTISYM]
1233QED
1234
1235Theorem borel_measurable_sets_sing :
1236 !c. {c} IN subsets borel
1237Proof
1238 GEN_TAC >> REWRITE_TAC [REAL_SING_BIGINTER]
1239 >> ASSUME_TAC sigma_algebra_borel
1240 >> (MP_TAC o UNDISCH o Q.SPEC `borel` o (INST_TYPE [alpha |-> ``:real``]))
1241 SIGMA_ALGEBRA_FN_BIGINTER
1242 >> RW_TAC std_ss []
1243 >> Q.PAT_X_ASSUM `!f. P f ==> Q f`
1244 (MP_TAC o
1245 Q.SPEC `(\n. {x | c - ((1/2) pow n) <= x /\ x < c + ((1/2) pow n)})`)
1246 >> ‘(\n. {x | c - ((1/2) pow n) <= x /\ x < c + ((1/2) pow n)}) IN
1247 (UNIV -> subsets borel)’
1248 by RW_TAC std_ss [IN_FUNSET, borel_measurable_sets_ge_less]
1249 >> METIS_TAC []
1250QED
1251
1252Theorem borel_measurable_sets_not_sing :
1253 !c. {x | x <> c} IN subsets borel
1254Proof
1255 RW_TAC std_ss []
1256 >> `{x | x <> c} = (space borel) DIFF ({c})`
1257 by RW_TAC std_ss [space_borel, EXTENSION, IN_DIFF, IN_SING, GSPECIFICATION, IN_UNIV]
1258 >> POP_ORW
1259 >> METIS_TAC [sigma_algebra_borel, borel_measurable_sets_sing,
1260 sigma_algebra_def, algebra_def]
1261QED
1262
1263(* A summary of all borel-measurable sets *)
1264Theorem borel_measurable_sets :
1265 (!a. {x | x < a} IN subsets borel) /\
1266 (!a. {x | x <= a} IN subsets borel) /\
1267 (!a. {x | a < x} IN subsets borel) /\
1268 (!a. {x | a <= x} IN subsets borel) /\
1269 (!a b. {x | a < x /\ x < b} IN subsets borel) /\
1270 (!a b. {x | a < x /\ x <= b} IN subsets borel) /\
1271 (!a b. {x | a <= x /\ x < b} IN subsets borel) /\
1272 (!a b. {x | a <= x /\ x <= b} IN subsets borel) /\
1273 (!c. {c} IN subsets borel) /\
1274 (!c. {x | x <> c} IN subsets borel)
1275Proof
1276 RW_TAC std_ss [borel_measurable_sets_less,
1277 borel_measurable_sets_le,
1278 borel_measurable_sets_gr,
1279 borel_measurable_sets_ge,
1280 borel_measurable_sets_gr_less,
1281 borel_measurable_sets_gr_le,
1282 borel_measurable_sets_ge_less,
1283 borel_measurable_sets_ge_le,
1284 borel_measurable_sets_sing,
1285 borel_measurable_sets_not_sing]
1286QED
1287
1288Theorem finite_imp_borel_measurable :
1289 !c. FINITE c ==> c IN subsets borel
1290Proof
1291 HO_MATCH_MP_TAC FINITE_INDUCT
1292 >> ASSUME_TAC sigma_algebra_borel
1293 >> rw [SIGMA_ALGEBRA_EMPTY]
1294 >> ‘e INSERT c = c UNION {e}’ by ASM_SET_TAC [] >> POP_ORW
1295 >> MATCH_MP_TAC SIGMA_ALGEBRA_UNION
1296 >> rw [borel_measurable_sets_sing]
1297QED
1298
1299Theorem countable_imp_borel_measurable :
1300 !c. countable c ==> c IN subsets borel
1301Proof
1302 ASSUME_TAC sigma_algebra_borel
1303 >> rw [COUNTABLE_ENUM]
1304 >- rw [SIGMA_ALGEBRA_EMPTY]
1305 >> ASSUME_TAC sigma_algebra_borel
1306 >> qabbrev_tac ‘g = \x. {f x}’
1307 >> Know ‘IMAGE f UNIV = BIGUNION (IMAGE g UNIV)’
1308 >- rw [Once EXTENSION, IN_BIGUNION_IMAGE, Abbr ‘g’]
1309 >> Rewr'
1310 >> fs [SIGMA_ALGEBRA_FN]
1311 >> FIRST_X_ASSUM MATCH_MP_TAC
1312 >> rw [Abbr ‘g’, IN_FUNSET, borel_measurable_sets_sing]
1313QED
1314
1315(* borel_measurable_plus_borel_measurable *)
1316Theorem in_borel_measurable_add :
1317 !a f g h. sigma_algebra a /\ f IN measurable a borel /\ g IN measurable a borel /\
1318 (!x. x IN space a ==> (h x = f x + g x)) ==> h IN measurable a borel
1319Proof
1320 rpt STRIP_TAC
1321 >> RW_TAC std_ss [in_borel_measurable_less, IN_FUNSET, IN_UNIV]
1322 >> Know ‘!c. {w | w IN space a /\ h w < c} =
1323 BIGUNION
1324 (IMAGE (\r. {x | x IN space a /\ f x < r /\ r < c - g x}) q_set)’
1325 >- (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION_IMAGE, IN_UNIV,
1326 IN_INTER] \\
1327 EQ_TAC >- (RW_TAC std_ss [] \\
1328 MATCH_MP_TAC Q_DENSE_IN_REAL \\
1329 METIS_TAC [REAL_LT_SUB_LADD]) \\
1330 RW_TAC std_ss [] >- art [] \\
1331 ‘h x = f x + g x’ by PROVE_TAC [] >> POP_ORW \\
1332 ‘f x < c - g x’ by PROVE_TAC [REAL_LT_TRANS] \\
1333 METIS_TAC [REAL_LT_SUB_LADD])
1334 >> DISCH_TAC
1335 >> FULL_SIMP_TAC std_ss []
1336 >> MATCH_MP_TAC BIGUNION_IMAGE_QSET
1337 >> RW_TAC std_ss [IN_FUNSET]
1338 >> rename1 ‘{x | x IN space a /\ f x < r /\ r < c - g x} IN subsets a’
1339 >> `{x | x IN space a /\ f x < r /\ r < c - g x} =
1340 {x | x IN space a /\ f x < r} INTER {x | x IN space a /\ r < c - g x}`
1341 by SET_TAC [] >> POP_ORW
1342 >> MATCH_MP_TAC SIGMA_ALGEBRA_INTER >> art []
1343 >> CONJ_TAC
1344 >- (MP_TAC (REWRITE_RULE [IN_FUNSET, IN_UNIV]
1345 (Q.SPECL [‘f’, ‘a’] in_borel_measurable_less)) \\
1346 RW_TAC std_ss [])
1347 >> Know `!x. x IN space a ==> (r < c - g x <=> g x < c - r)`
1348 >- (rpt STRIP_TAC \\
1349 METIS_TAC [REAL_LT_SUB_LADD, REAL_ADD_COMM])
1350 >> DISCH_TAC
1351 >> ‘{x | x IN space a /\ r < c - g x} =
1352 {x | x IN space a /\ g x < c - r}’ by ASM_SET_TAC [] >> POP_ORW
1353 >> MP_TAC (REWRITE_RULE [IN_FUNSET, IN_UNIV]
1354 (Q.SPECL [‘g’, ‘a’] in_borel_measurable_less))
1355 >> RW_TAC std_ss []
1356QED
1357
1358Theorem borel_2d_measurable_add :
1359 (\(x,y). x + y) IN borel_measurable (borel CROSS borel)
1360Proof
1361 rpt STRIP_TAC
1362 >> ASSUME_TAC sigma_algebra_borel
1363 >> ‘sigma_algebra (borel CROSS borel)’ by PROVE_TAC [SIGMA_ALGEBRA_PROD_SIGMA_WEAK]
1364 >> MATCH_MP_TAC in_borel_measurable_add
1365 >> qexistsl_tac [‘FST’, ‘SND’]
1366 >> simp [MEASURABLE_FST, MEASURABLE_SND]
1367 >> simp [FORALL_PROD]
1368QED
1369
1370Theorem in_borel_measurable_const :
1371 !a k f. sigma_algebra a /\ (!x. x IN space a ==> (f x = k)) ==>
1372 f IN measurable a borel
1373Proof
1374 RW_TAC std_ss [in_borel_measurable_less, IN_FUNSET, IN_UNIV]
1375 >> rename1 ‘{w | w IN space a /\ f w < c} IN subsets a’
1376 >> Cases_on `c <= k`
1377 >- (`{x | x IN space a /\ f x < c} = {}` by ASM_SET_TAC [real_lt] >> POP_ORW \\
1378 MATCH_MP_TAC SIGMA_ALGEBRA_EMPTY >> art [])
1379 >> `{x | x IN space a /\ f x < c} = space a` by ASM_SET_TAC [real_lt]
1380 >> POP_ORW
1381 >> MATCH_MP_TAC SIGMA_ALGEBRA_SPACE >> art []
1382QED
1383
1384Theorem in_borel_measurable_cmul :
1385 !a f g z. sigma_algebra a /\ f IN measurable a borel /\
1386 (!x. x IN space a ==> (g x = z * f x)) ==> g IN measurable a borel
1387Proof
1388 RW_TAC std_ss []
1389 >> Cases_on `z = 0`
1390 >- METIS_TAC [in_borel_measurable_const, REAL_MUL_LZERO]
1391 >> Cases_on `0 < z`
1392 >- (RW_TAC real_ss [in_borel_measurable_less, IN_FUNSET, IN_UNIV] \\
1393 Know `!c. {x | x IN space a /\ g x < c} = {x | x IN space a /\ f x < c / z}`
1394 >- (rw [Once EXTENSION] \\
1395 METIS_TAC [REAL_LT_RDIV_EQ, REAL_MUL_COMM]) >> Rewr' \\
1396 MP_TAC (REWRITE_RULE [IN_FUNSET, IN_UNIV]
1397 (Q.SPECL [‘f’, ‘a’] in_borel_measurable_less)) \\
1398 RW_TAC std_ss [])
1399 >> `z < 0` by METIS_TAC [REAL_LT_LE, GSYM real_lte]
1400 >> RW_TAC real_ss [in_borel_measurable_less, IN_FUNSET, IN_UNIV]
1401 >> Know `!c. {x | x IN space a /\ g x < c} = {x | x IN space a /\ c / z < f x}`
1402 >- (rw [Once EXTENSION] \\
1403 METIS_TAC [REAL_LT_RDIV_EQ_NEG, REAL_MUL_COMM]) >> Rewr'
1404 >> MP_TAC (REWRITE_RULE [IN_FUNSET, IN_UNIV]
1405 (Q.SPECL [‘f’, ‘a’] in_borel_measurable_gr))
1406 >> RW_TAC std_ss []
1407QED
1408
1409Theorem in_borel_measurable_ainv :
1410 !a f. sigma_algebra a /\ f IN measurable a borel ==>
1411 (\x. -f x) IN measurable a borel
1412Proof
1413 rpt STRIP_TAC
1414 >> ‘(\x. -f x) = (\x. -1 * f x)’ by rw [Once REAL_NEG_MINUS1, FUN_EQ_THM]
1415 >> POP_ORW
1416 >> MATCH_MP_TAC in_borel_measurable_cmul
1417 >> qexistsl_tac [‘f’, ‘-1’] >> rw []
1418QED
1419
1420(* cf. borel_measurable_sub_borel_measurable (real_measureTheory) *)
1421Theorem in_borel_measurable_sub :
1422 !a f g h. sigma_algebra a /\ f IN measurable a borel /\ g IN measurable a borel /\
1423 (!x. x IN space a ==> (h x = f x - g x)) ==> h IN measurable a borel
1424Proof
1425 RW_TAC std_ss []
1426 >> MATCH_MP_TAC in_borel_measurable_add
1427 >> qexistsl_tac [`f`, `\x. - g x`]
1428 >> RW_TAC std_ss []
1429 >| [ (* goal 1 (of 2) *)
1430 MATCH_MP_TAC in_borel_measurable_cmul \\
1431 qexistsl_tac [‘g’, ‘-1’] \\
1432 RW_TAC real_ss [],
1433 (* goal 2 (of 2) *)
1434 REWRITE_TAC [real_sub] ]
1435QED
1436
1437Theorem borel_2d_measurable_sub :
1438 (\(x,y). x - y) IN borel_measurable (borel CROSS borel)
1439Proof
1440 rpt STRIP_TAC
1441 >> ASSUME_TAC sigma_algebra_borel
1442 >> ‘sigma_algebra (borel CROSS borel)’ by PROVE_TAC [SIGMA_ALGEBRA_PROD_SIGMA_WEAK]
1443 >> MATCH_MP_TAC in_borel_measurable_sub
1444 >> qexistsl_tac [‘FST’, ‘SND’]
1445 >> simp [MEASURABLE_FST, MEASURABLE_SND]
1446 >> simp [FORALL_PROD]
1447QED
1448
1449Theorem in_borel_measurable_pow2 : (* was: in_borel_measurable_sqr *)
1450 !a f g. sigma_algebra a /\ f IN measurable a borel /\
1451 (!x. x IN space a ==> (g x = (f x) pow 2)) ==> g IN measurable a borel
1452Proof
1453 rpt STRIP_TAC
1454 >> Know `!c. {x | f x <= c} INTER space a IN subsets a`
1455 >- (GEN_TAC >> rfs [in_borel_measurable_le, IN_FUNSET, IN_UNIV] \\
1456 ‘{x | f x <= c} INTER space a = {x | x IN space a /\ f x <= c}’ by SET_TAC [] \\
1457 POP_ORW >> art [])
1458 >> DISCH_TAC
1459 >> Know `!c. {x | c <= f x} INTER space a IN subsets a`
1460 >- (GEN_TAC >> rfs [in_borel_measurable_ge, IN_FUNSET, IN_UNIV] \\
1461 ‘{x | c <= f x} INTER space a = {x | x IN space a /\ c <= f x}’ by SET_TAC [] \\
1462 POP_ORW >> art [])
1463 >> DISCH_TAC
1464 >> simp [IN_FUNSET, in_borel_measurable_le]
1465 >> Q.X_GEN_TAC ‘c’
1466 >> ‘{w | w IN space a /\ g w <= c} = {x | g x <= c} INTER space a’ by SET_TAC []
1467 >> POP_ORW
1468 >> Cases_on `c < 0`
1469 >- (Know `{x | g x <= c} INTER space a = {}`
1470 >- (rw [Once EXTENSION, NOT_IN_EMPTY, GSYM real_lt] \\
1471 ONCE_REWRITE_TAC [DISJ_COMM] >> STRONG_DISJ_TAC \\
1472 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC ‘0’ >> art [] \\
1473 METIS_TAC [REAL_LE_POW2]) >> Rewr' \\
1474 MATCH_MP_TAC SIGMA_ALGEBRA_EMPTY >> art [])
1475 >> FULL_SIMP_TAC real_ss [real_lt]
1476 >> Suff `{x | g x <= c} INTER space a =
1477 ({x | f x <= sqrt c} INTER space a) INTER
1478 ({x | - (sqrt c) <= f x} INTER space a)`
1479 >- (Rewr' >> MATCH_MP_TAC SIGMA_ALGEBRA_INTER >> art [])
1480 >> rw [Once EXTENSION]
1481 >> EQ_TAC
1482 >- (RW_TAC real_ss []
1483 >- (Cases_on `f x < 0` >- METIS_TAC [REAL_LTE_TRANS, REAL_LT_IMP_LE, SQRT_POS_LE] \\
1484 FULL_SIMP_TAC real_ss [real_lt] \\
1485 Know ‘sqrt (g x) <= sqrt c’
1486 >- (MATCH_MP_TAC SQRT_MONO_LE >> art [] \\
1487 METIS_TAC [REAL_LE_POW2]) >> DISCH_TAC \\
1488 Suff ‘sqrt (g x) = f x’ >- PROVE_TAC [] \\
1489 MATCH_MP_TAC SQRT_POS_UNIQ >> METIS_TAC [REAL_LE_POW2]) \\
1490 SPOSE_NOT_THEN ASSUME_TAC \\
1491 FULL_SIMP_TAC real_ss [GSYM real_lt] \\
1492 `sqrt c < -(f x)` by METIS_TAC [REAL_LT_NEG, REAL_NEG_NEG] \\
1493 Know `(sqrt c) pow 2 < (- (f x)) pow 2`
1494 >- (MATCH_MP_TAC REAL_POW_LT2 >> rw [SQRT_POS_LE]) >> DISCH_TAC \\
1495 `(sqrt c) pow 2 = c` by METIS_TAC [SQRT_POW2] \\
1496 `(-1) pow 2 = (1 :real)` by METIS_TAC [POW_MINUS1, MULT_RIGHT_1] \\
1497 `(- (f x)) pow 2 = (f x) pow 2`
1498 by RW_TAC std_ss [Once REAL_NEG_MINUS1, POW_MUL, REAL_MUL_LID] \\
1499 METIS_TAC [real_lt])
1500 >> RW_TAC std_ss []
1501 >> Cases_on `0 <= f x` >- METIS_TAC [POW_LE, SQRT_POW2]
1502 >> FULL_SIMP_TAC real_ss [GSYM real_lt]
1503 >> `- (f x) <= sqrt c` by METIS_TAC [REAL_LE_NEG, REAL_NEG_NEG]
1504 >> `(- (f x)) pow 2 <= (sqrt c) pow 2`
1505 by METIS_TAC [POW_LE, SQRT_POS_LE, REAL_LT_NEG, REAL_NEG_NEG, REAL_NEG_0, REAL_LT_IMP_LE]
1506 >> `(sqrt c) pow 2 = c` by METIS_TAC [SQRT_POW2]
1507 >> `(-1) pow 2 = (1 :real)` by METIS_TAC [POW_MINUS1, MULT_RIGHT_1]
1508 >> `(- (f x)) pow 2 = (f x) pow 2`
1509 by RW_TAC std_ss [Once REAL_NEG_MINUS1, POW_MUL, REAL_MUL_LID]
1510 >> METIS_TAC []
1511QED
1512
1513Theorem in_borel_measurable_mul :
1514 !a f g h. sigma_algebra a /\ f IN measurable a borel /\ g IN measurable a borel /\
1515 (!x. x IN space a ==> (h x = f x * g x)) ==> h IN measurable a borel
1516Proof
1517 RW_TAC std_ss []
1518 >> Know `!x. x IN space a ==>
1519 (f x * g x = 1 / 2 * ((f x + g x) pow 2 - f x pow 2 - g x pow 2))`
1520 >- (rpt STRIP_TAC \\
1521 (MP_TAC o Q.SPECL [`f x`, `g x`]) ADD_POW_2 >> Rewr' \\
1522 simp [] >> REAL_ARITH_TAC)
1523 >> DISCH_TAC
1524 >> MATCH_MP_TAC in_borel_measurable_cmul
1525 >> Q.EXISTS_TAC `(\x. (f x + g x) pow 2 - f x pow 2 - g x pow 2)`
1526 >> Q.EXISTS_TAC `1 / 2`
1527 >> RW_TAC real_ss []
1528 >> MATCH_MP_TAC in_borel_measurable_sub
1529 >> Q.EXISTS_TAC `(\x. (f x + g x) pow 2 - f x pow 2)`
1530 >> Q.EXISTS_TAC `(\x. g x pow 2)`
1531 >> RW_TAC std_ss []
1532 >| [ (* goal 1 (of 2) *)
1533 MATCH_MP_TAC in_borel_measurable_sub \\
1534 Q.EXISTS_TAC `(\x. (f x + g x) pow 2)` \\
1535 Q.EXISTS_TAC `(\x. f x pow 2)` \\
1536 RW_TAC std_ss [] >| (* 2 subgoals *)
1537 [ (* goal 1.1 (of 2) *)
1538 MATCH_MP_TAC in_borel_measurable_pow2 \\
1539 Q.EXISTS_TAC `(\x. f x + g x)` \\
1540 RW_TAC std_ss [] \\
1541 MATCH_MP_TAC in_borel_measurable_add \\
1542 qexistsl_tac [`f`, `g`] \\
1543 RW_TAC std_ss [],
1544 (* goal 1.2 (of 2) *)
1545 MATCH_MP_TAC in_borel_measurable_pow2 >> METIS_TAC [] ],
1546 (* goal 2 (of 2) *)
1547 MATCH_MP_TAC in_borel_measurable_pow2 >> METIS_TAC [] ]
1548QED
1549
1550(* NOTE: added ‘sigma_algebra a’ due to changes in ‘measurable’
1551
1552 cf. borelTheory.IN_MEASURABLE_BOREL_MAX
1553 *)
1554Theorem in_borel_measurable_max :
1555 !a f g. sigma_algebra a /\ f IN measurable a borel /\ g IN measurable a borel
1556 ==> (\x. max (f x) (g x)) IN measurable a borel
1557Proof
1558 RW_TAC std_ss [in_borel_measurable_less, max_def, IN_FUNSET, IN_UNIV]
1559 >> rfs [in_borel_measurable_less]
1560 >> `!c. {x | x IN space a /\ (if f x <= g x then g x else f x) < c} =
1561 {x | x IN space a /\ f x < c} INTER
1562 {x | x IN space a /\ g x < c}`
1563 by (rw [Once EXTENSION] \\
1564 EQ_TAC >> rw [] >- METIS_TAC [REAL_LET_TRANS] \\
1565 METIS_TAC [real_lte, REAL_LT_TRANS])
1566 >> POP_ORW
1567 >> MATCH_MP_TAC SIGMA_ALGEBRA_INTER >> art []
1568QED
1569
1570(* NOTE: added ‘sigma_algebra a’ due to changes in ‘measurable’
1571
1572 cf. borelTheory.IN_MEASURABLE_BOREL_MIN
1573 *)
1574Theorem in_borel_measurable_min :
1575 !a f g. sigma_algebra a /\ f IN measurable a borel /\ g IN measurable a borel
1576 ==> (\x. min (f x) (g x)) IN measurable a borel
1577Proof
1578 RW_TAC std_ss [in_borel_measurable_less, min_def, IN_FUNSET, IN_UNIV]
1579 >> rfs [in_borel_measurable_less]
1580 >> `!c. {x | x IN space a /\ (if f x <= g x then f x else g x) < c} =
1581 {x | x IN space a /\ f x < c} UNION
1582 {x | x IN space a /\ g x < c}`
1583 by (rw [Once EXTENSION] \\
1584 EQ_TAC >> rw [] >> rw [] >- METIS_TAC [REAL_LET_TRANS] \\
1585 METIS_TAC [real_lte, REAL_LT_TRANS])
1586 >> POP_ORW
1587 >> MATCH_MP_TAC SIGMA_ALGEBRA_UNION >> art []
1588QED
1589
1590(* NOTE: added ‘sigma_algebra a’ due to changes in ‘measurable’
1591
1592 cf. borelTheory.IN_MEASURABLE_BOREL_LT
1593 *)
1594Theorem in_borel_measurable_lt2 :
1595 !a f g. sigma_algebra a /\ f IN measurable a borel /\ g IN measurable a borel ==>
1596 {x | x IN space a /\ f x < g x} IN subsets a
1597Proof
1598 RW_TAC std_ss []
1599 >> `{x | x IN space a /\ f x < g x} =
1600 BIGUNION (IMAGE (\r. {x | f x < r /\ r < g x} INTER space a) q_set)`
1601 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION_IMAGE, IN_INTER] \\
1602 EQ_TAC >- RW_TAC std_ss [Q_DENSE_IN_REAL] \\
1603 METIS_TAC [REAL_LT_TRANS])
1604 >> POP_ORW
1605 >> MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION >> art []
1606 >> CONJ_TAC >- (MATCH_MP_TAC image_countable \\
1607 REWRITE_TAC [QSET_COUNTABLE])
1608 >> rw [SUBSET_DEF]
1609 >> `{x | f x < r /\ r < g x} INTER space a =
1610 {x | x IN space a /\ f x < r} INTER {x | x IN space a /\ r < g x}` by SET_TAC []
1611 >> POP_ORW
1612 >> MATCH_MP_TAC SIGMA_ALGEBRA_INTER >> art []
1613 >> CONJ_TAC
1614 >| [ (* goal 1 (of 2) *)
1615 Q.PAT_X_ASSUM ‘f IN borel_measurable a’ MP_TAC \\
1616 rw [in_borel_measurable_less, IN_FUNSET],
1617 (* goal 2 (of 2) *)
1618 Q.PAT_X_ASSUM ‘g IN borel_measurable a’ MP_TAC \\
1619 rw [in_borel_measurable_gr, IN_FUNSET] ]
1620QED
1621
1622(* NOTE: added ‘sigma_algebra a’ due to changes in ‘measurable’
1623
1624 cf. borelTheory.IN_MEASURABLE_BOREL_LE
1625 *)
1626Theorem in_borel_measurable_le2 :
1627 !a f g. sigma_algebra a /\ f IN measurable a borel /\ g IN measurable a borel ==>
1628 {x | x IN space a /\ f x <= g x} IN subsets a
1629Proof
1630 RW_TAC std_ss []
1631 >> `{x | x IN space a /\ f x <= g x} = space a DIFF {x | x IN space a /\ g x < f x}`
1632 by (RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER, IN_DIFF] \\
1633 METIS_TAC [real_lte])
1634 >> POP_ORW
1635 >> MATCH_MP_TAC SIGMA_ALGEBRA_COMPL
1636 >> rw [in_borel_measurable_lt2]
1637 >> fs [in_borel_measurable]
1638QED
1639
1640(* NOTE: added ‘sigma_algebra a’ due to changes in ‘measurable’
1641
1642 cf. borelTheory.IN_MEASURABLE_BOREL_MUL_INDICATOR
1643 *)
1644Theorem in_borel_measurable_mul_indicator :
1645 !a f s. sigma_algebra a /\ f IN measurable a borel /\ s IN subsets a ==>
1646 (\x. f x * indicator_fn s x) IN measurable a borel
1647Proof
1648 rpt STRIP_TAC
1649 >> rfs [in_borel_measurable_le, IN_FUNSET]
1650 >> Q.X_GEN_TAC ‘c’
1651 >> Cases_on `0 <= c`
1652 >- (`{x | x IN space a /\ f x * indicator_fn s x <= c} =
1653 ({x | x IN space a /\ f x <= c} INTER s) UNION (space a DIFF s)`
1654 by (RW_TAC std_ss [indicator_fn_def, EXTENSION, GSPECIFICATION, IN_INTER,
1655 IN_UNION, IN_DIFF] \\
1656 Cases_on `x IN s` >> RW_TAC real_ss []) >> POP_ORW \\
1657 MATCH_MP_TAC SIGMA_ALGEBRA_UNION >> art [] \\
1658 reverse CONJ_TAC >- (MATCH_MP_TAC SIGMA_ALGEBRA_COMPL >> art []) \\
1659 MATCH_MP_TAC SIGMA_ALGEBRA_INTER >> art [])
1660 >> `{x | x IN space a /\ f x * indicator_fn s x <= c} =
1661 {x | x IN space a /\ f x <= c} INTER s`
1662 by (RW_TAC std_ss [indicator_fn_def, EXTENSION, GSPECIFICATION, IN_INTER] \\
1663 Cases_on `x IN s` >> RW_TAC real_ss []) >> POP_ORW
1664 >> MATCH_MP_TAC SIGMA_ALGEBRA_INTER >> art []
1665QED
1666
1667(* cf. borelTheory.in_measurable_sigma_pow for measure_space version *)
1668Theorem in_measurable_sigma_pow' :
1669 !a sp N f. sigma_algebra a /\
1670 N SUBSET POW sp /\ f IN (space a -> sp) /\
1671 (!y. y IN N ==> (PREIMAGE f y) INTER space a IN subsets a) ==>
1672 f IN measurable a (sigma sp N)
1673Proof
1674 RW_TAC std_ss []
1675 >> MATCH_MP_TAC MEASURABLE_SIGMA
1676 >> rw [subset_class_def]
1677 >> fs [SUBSET_DEF, IN_POW]
1678 >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
1679QED
1680
1681(* cf. borelTheory.in_borel_measurable_imp' for measure_space version
1682
1683 NOTE: theorem renamed due to name conflicts with HVG's work.
1684 *)
1685Theorem in_borel_measurable_open_imp : (* was: in_borel_measurable_open *)
1686 !a f. sigma_algebra a /\
1687 (!s. open s ==> (PREIMAGE f s) INTER space a IN subsets a) ==>
1688 f IN measurable a borel
1689Proof
1690 RW_TAC std_ss [borel]
1691 >> MATCH_MP_TAC in_measurable_sigma_pow'
1692 >> ASM_SIMP_TAC std_ss [IN_FUNSET, IN_UNIV]
1693 >> CONJ_TAC >- SET_TAC [POW_DEF]
1694 >> ASM_SET_TAC []
1695QED
1696
1697Theorem in_borel_measurable_continuous_on : (* was: borel_measurable_continuous_on1 *)
1698 !f. f continuous_on UNIV ==> f IN measurable borel borel
1699Proof
1700 rpt STRIP_TAC
1701 >> MATCH_MP_TAC in_borel_measurable_open_imp
1702 >> rw [sigma_algebra_borel]
1703 >> Know `open {x | x IN UNIV /\ f x IN s}`
1704 >- (MATCH_MP_TAC CONTINUOUS_OPEN_PREIMAGE (* key lemma *) \\
1705 ASM_SIMP_TAC std_ss [OPEN_UNIV])
1706 >> DISCH_TAC
1707 >> SIMP_TAC std_ss [PREIMAGE_def, space_borel, INTER_UNIV]
1708 >> MATCH_MP_TAC borel_open >> fs []
1709QED
1710
1711Definition real_fn_plus_def :
1712 real_fn_plus f x = max (0 :real) (f x)
1713End
1714
1715Definition real_fn_minus_def :
1716 real_fn_minus f x = -min (0 :real) (f x)
1717End
1718
1719Overload TC = “real_fn_plus”
1720Overload fn_plus[inferior] = “real_fn_plus”
1721Overload fn_minus = “real_fn_minus”
1722
1723Theorem real_fn_plus :
1724 !f. real_fn_plus f = \x. max 0 (f x)
1725Proof
1726 rw [FUN_EQ_THM, real_fn_plus_def]
1727QED
1728
1729Theorem real_fn_minus :
1730 real_fn_minus f = \x. -min 0 (f x)
1731Proof
1732 rw [FUN_EQ_THM, real_fn_minus_def]
1733QED
1734
1735Theorem real_fn_plus_pos :
1736 !f x. 0 <= real_fn_plus f x
1737Proof
1738 rw [real_fn_plus_def, REAL_LE_MAX]
1739QED
1740
1741Theorem real_fn_minus_pos :
1742 !f x. 0 <= real_fn_minus f x
1743Proof
1744 rw [real_fn_minus_def, REAL_MIN_LE]
1745QED
1746
1747(* cf. extrealTheory.FN_DECOMP *)
1748Theorem fn_decompose :
1749 !(f :'a -> real) x. f x = fn_plus f x - fn_minus f x
1750Proof
1751 RW_TAC real_ss [real_fn_plus_def, real_fn_minus_def]
1752 >> Cases_on ‘0 <= f x’
1753 >- simp [REAL_MAX_REDUCE, REAL_MIN_REDUCE]
1754 >> fs [REAL_NOT_LE]
1755 >> simp [REAL_MAX_REDUCE, REAL_MIN_REDUCE]
1756QED
1757
1758Theorem fn_abs_decompose :
1759 !(f :'a -> real) x. abs (f x) = fn_plus f x + fn_minus f x
1760Proof
1761 RW_TAC real_ss [real_fn_plus_def, real_fn_minus_def]
1762 >> Cases_on ‘0 <= f x’
1763 >- simp [ABS_REDUCE, REAL_MAX_REDUCE, REAL_MIN_REDUCE]
1764 >> fs [REAL_NOT_LE]
1765 >> simp [ABS_EQ_NEG, REAL_MAX_REDUCE, REAL_MIN_REDUCE]
1766QED
1767
1768Theorem fn_abs :
1769 !(f :'a -> real). abs o f = \x. fn_plus f x + fn_minus f x
1770Proof
1771 rw [FUN_EQ_THM, fn_abs_decompose]
1772QED
1773
1774Theorem in_borel_measurable_fn_plus :
1775 !a f. sigma_algebra a /\ f IN borel_measurable a ==>
1776 real_fn_plus f IN borel_measurable a
1777Proof
1778 rw [real_fn_plus]
1779 >> HO_MATCH_MP_TAC in_borel_measurable_max >> art []
1780 >> MATCH_MP_TAC in_borel_measurable_const
1781 >> Q.EXISTS_TAC ‘0’ >> rw []
1782QED
1783
1784Theorem in_borel_measurable_fn_minus :
1785 !a f. sigma_algebra a /\ f IN borel_measurable a ==>
1786 real_fn_minus f IN borel_measurable a
1787Proof
1788 rw [real_fn_minus]
1789 >> HO_MATCH_MP_TAC in_borel_measurable_ainv >> art []
1790 >> HO_MATCH_MP_TAC in_borel_measurable_min >> art []
1791 >> MATCH_MP_TAC in_borel_measurable_const
1792 >> Q.EXISTS_TAC ‘0’ >> rw []
1793QED
1794
1795Theorem in_borel_measurable_abs' :
1796 !a f. sigma_algebra a /\ f IN borel_measurable a ==>
1797 abs o f IN borel_measurable a
1798Proof
1799 rw [fn_abs]
1800 >> MATCH_MP_TAC in_borel_measurable_add
1801 >> qexistsl_tac [‘fn_plus f’, ‘fn_minus f’]
1802 >> rw [in_borel_measurable_fn_plus, in_borel_measurable_fn_minus]
1803QED
1804
1805Theorem in_borel_measurable_borel_abs :
1806 abs IN borel_measurable borel
1807Proof
1808 MP_TAC (ISPECL [“borel”, “\x. (x :real)”] in_borel_measurable_abs')
1809 >> simp [o_DEF, in_borel_measurable_I, sigma_algebra_borel]
1810 >> SIMP_TAC (std_ss ++ ETA_ss) []
1811QED
1812
1813(************************************************************)
1814(* right-open (left-closed) intervals [a, b) in R *)
1815(************************************************************)
1816
1817(* cf. `open_interval` (extrealTheory), `box` (real_borelTheory),
1818 `OPEN_interval` and `CLOSE_interval` (real_topologyTheory)
1819
1820 The name "right_open_interval" is from MML (Mizar Math Library)
1821 *)
1822Definition right_open_interval :
1823 right_open_interval a b = {(x :real) | a <= x /\ x < b}
1824End
1825
1826Theorem in_right_open_interval :
1827 !a b x. x IN right_open_interval a b <=> a <= x /\ x < b
1828Proof
1829 SIMP_TAC std_ss [right_open_interval, GSPECIFICATION]
1830QED
1831
1832Theorem right_open_interval_interior :
1833 !a b. a < b ==> a IN (right_open_interval a b)
1834Proof
1835 RW_TAC std_ss [right_open_interval, GSPECIFICATION, REAL_LE_REFL]
1836QED
1837
1838Theorem right_open_interval_frontier :
1839 !a b. a < b ==> frontier (right_open_interval a b) = {a; b}
1840Proof
1841 rw [right_open_interval, FRONTIER_CLOSURES]
1842 >> Know ‘UNIV DIFF {x | a <= x /\ x < b} = {x | x < a} UNION {x | b <= x}’
1843 >- rw [Once EXTENSION, REAL_NOT_LT, REAL_NOT_LE]
1844 >> Rewr'
1845 >> Know ‘{x | a <= x /\ x < b} = {a} UNION interval (a,b)’
1846 >- (rw [Once EXTENSION, REAL_LE_LT, IN_INTERVAL] \\
1847 METIS_TAC [])
1848 >> Rewr'
1849 >> ‘interval (a,b) <> {}’ by PROVE_TAC [INTERVAL_NE_EMPTY]
1850 >> simp [CLOSURE_UNION, CLOSURE_INTERVAL, CLOSURE_SING,
1851 CLOSURE_HALFSPACE_COMPONENT_LT]
1852 >> ASSUME_TAC
1853 (REWRITE_RULE [real_ge] (Q.SPEC ‘b’ CLOSED_HALFSPACE_COMPONENT_GE))
1854 >> simp [CLOSURE_CLOSED]
1855 >> rw [Once EXTENSION, IN_INTERVAL]
1856 >> METIS_TAC [REAL_LE_ANTISYM, REAL_LE_REFL, REAL_LT_IMP_LE]
1857QED
1858
1859Theorem borel_frontier :
1860 !s. frontier s IN subsets borel
1861Proof
1862 rw [FRONTIER_CLOSURES]
1863 >> MATCH_MP_TAC SIGMA_ALGEBRA_INTER
1864 >> rw [sigma_algebra_borel]
1865 >> MATCH_MP_TAC borel_closed
1866 >> REWRITE_TAC [CLOSED_CLOSURE]
1867QED
1868
1869(* cf. `open_intervals_set` in extrealTheory *)
1870Definition right_open_intervals :
1871 right_open_intervals = (univ(:real), {right_open_interval a b | T})
1872End
1873
1874Theorem in_right_open_intervals :
1875 !s. s IN subsets right_open_intervals <=> ?a b. (s = right_open_interval a b)
1876Proof
1877 RW_TAC std_ss [subsets_def, right_open_intervals,
1878 right_open_interval, GSPECIFICATION]
1879 >> EQ_TAC >> rpt STRIP_TAC
1880 >- (Cases_on `x` >> fs [] >> qexistsl_tac [`q`, `r`] >> rw [])
1881 >> Q.EXISTS_TAC `(a,b)` >> rw []
1882QED
1883
1884Theorem right_open_interval_in_intervals :
1885 !a b. (right_open_interval a b) IN subsets right_open_intervals
1886Proof
1887 RW_TAC std_ss [in_right_open_intervals]
1888 >> qexistsl_tac [`a`, `b`] >> REWRITE_TAC []
1889QED
1890
1891Theorem right_open_interval_empty :
1892 !a b. (right_open_interval a b = {}) <=> ~(a < b)
1893Proof
1894 RW_TAC real_ss [right_open_interval, EXTENSION, GSPECIFICATION,
1895 NOT_IN_EMPTY, GSYM real_lte]
1896 >> EQ_TAC >> rpt STRIP_TAC
1897 >- POP_ASSUM (ACCEPT_TAC o (REWRITE_RULE [REAL_LE_REFL]) o (Q.SPEC `a`))
1898 >> STRONG_DISJ_TAC
1899 >> PROVE_TAC [REAL_LE_TRANS]
1900QED
1901
1902Theorem in_right_open_intervals_nonempty :
1903 !s. s <> {} /\ s IN subsets right_open_intervals <=>
1904 ?a b. a < b /\ s = right_open_interval a b
1905Proof
1906 RW_TAC std_ss [subsets_def, right_open_intervals, GSPECIFICATION]
1907 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *)
1908 >| [ (* goal 1 (of 3) *)
1909 Cases_on `x` >> fs [right_open_interval_empty] \\
1910 qexistsl_tac [`q`, `r`] >> art [],
1911 (* goal 2 (of 3) *)
1912 METIS_TAC [right_open_interval_empty],
1913 (* goal 3 (of 3) *)
1914 Q.EXISTS_TAC `(a,b)` >> ASM_SIMP_TAC std_ss [] ]
1915QED
1916
1917(* [c [a b) d) *)
1918Theorem right_open_interval_SUBSET_EQ :
1919 !a b c d. a < b /\ c < d ==>
1920 (right_open_interval a b SUBSET right_open_interval c d <=>
1921 c <= a /\ b <= d)
1922Proof
1923 rpt STRIP_TAC
1924 >> EQ_TAC >> rw [SUBSET_DEF, in_right_open_interval] (* 3 subgoals *)
1925 >| [ (* goal 1 (of 3) *)
1926 CCONTR_TAC >> fs [GSYM real_lt] \\
1927 MP_TAC (Q.SPECL [‘max a d’, ‘b’] REAL_MEAN) \\
1928 PURE_REWRITE_TAC [REAL_MAX_LT] \\
1929 impl_tac >- art [] >> STRIP_TAC \\
1930 ‘a <= z’ by simp [REAL_LT_IMP_LE] \\
1931 ‘c <= z /\ z < d’ by PROVE_TAC [] \\
1932 METIS_TAC [REAL_LT_ANTISYM],
1933 (* goal 2 (of 3) *)
1934 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘a’ >> art [],
1935 (* goal 3 (of 3) *)
1936 Q_TAC (TRANS_TAC REAL_LTE_TRANS) ‘b’ >> art [] ]
1937QED
1938
1939(* [c [a, b) d) *)
1940Theorem right_open_interval_SUBSET :
1941 !a b c d. a < b /\ c < d /\
1942 right_open_interval a b SUBSET right_open_interval c d ==>
1943 b - a <= d - c
1944Proof
1945 rpt STRIP_TAC
1946 >> gs [right_open_interval_SUBSET_EQ]
1947 >> REAL_ASM_ARITH_TAC
1948QED
1949
1950Theorem right_open_interval_shift_lemma :
1951 !s c. s SUBSET right_open_interval 0 1 ==>
1952 IMAGE (\x. x + c) s SUBSET right_open_interval c (c + 1)
1953Proof
1954 rw [SUBSET_DEF, in_right_open_interval]
1955 >> rename1 ‘y IN s’
1956 >- (Suff ‘0 <= y’ >- REAL_ARITH_TAC >> simp [])
1957 >> Suff ‘y < 1’ >- REAL_ARITH_TAC
1958 >> simp []
1959QED
1960
1961Theorem right_open_interval_shift :
1962 !c. IMAGE (\x. x + c) (right_open_interval a b) =
1963 right_open_interval (a + c) (b + c)
1964Proof
1965 rw [Once EXTENSION, in_right_open_interval]
1966 >> EQ_TAC >> rw []
1967 >- REAL_ASM_ARITH_TAC
1968 >- REAL_ASM_ARITH_TAC
1969 >> Q.EXISTS_TAC ‘x - c’
1970 >> REAL_ASM_ARITH_TAC
1971QED
1972
1973Theorem right_open_interval_11 :
1974 !a b c d. a < b /\ c < d ==>
1975 (right_open_interval a b = right_open_interval c d <=> a = c /\ b = d)
1976Proof
1977 RW_TAC std_ss [GSYM SUBSET_ANTISYM_EQ, right_open_interval_SUBSET_EQ]
1978 >> METIS_TAC [REAL_LE_ANTISYM]
1979QED
1980
1981Theorem right_open_interval_empty_eq :
1982 !a b. (a = b) ==> (right_open_interval a b = {})
1983Proof
1984 RW_TAC std_ss [right_open_interval_empty, REAL_LT_REFL]
1985QED
1986
1987Theorem right_open_interval_DISJOINT :
1988 !a b c d. a <= b /\ b <= c /\ c <= d ==>
1989 DISJOINT (right_open_interval a b) (right_open_interval c d)
1990Proof
1991 RW_TAC std_ss [DISJOINT_DEF, INTER_DEF, right_open_interval,
1992 EXTENSION, GSPECIFICATION, NOT_IN_EMPTY]
1993 >> Suff `x < b ==> ~(c <= x)` >- METIS_TAC []
1994 >> DISCH_TAC >> REWRITE_TAC [real_lte]
1995 >> MATCH_MP_TAC REAL_LTE_TRANS
1996 >> Q.EXISTS_TAC `b` >> art []
1997QED
1998
1999Theorem right_open_interval_disjoint :
2000 !a b c d. a <= b /\ b <= c /\ c <= d ==>
2001 disjoint {right_open_interval a b; right_open_interval c d}
2002Proof
2003 rpt STRIP_TAC
2004 >> Cases_on `right_open_interval a b = right_open_interval c d`
2005 >- PROVE_TAC [disjoint_same]
2006 >> MATCH_MP_TAC disjoint_two >> art []
2007 >> MATCH_MP_TAC right_open_interval_DISJOINT >> art []
2008QED
2009
2010Theorem right_open_interval_inter :
2011 !a b c d. right_open_interval a b INTER right_open_interval c d =
2012 right_open_interval (max a c) (min b d)
2013Proof
2014 rpt GEN_TAC
2015 >> `min b d <= b /\ min b d <= d` by PROVE_TAC [REAL_MIN_LE1, REAL_MIN_LE2]
2016 >> `a <= max a c /\ c <= max a c` by PROVE_TAC [REAL_LE_MAX1, REAL_LE_MAX2]
2017 >> Cases_on `~(a < b)`
2018 >- (`right_open_interval a b = {}` by PROVE_TAC [right_open_interval_empty] \\
2019 fs [GSYM real_lte] \\
2020 `min b d <= max a c` by PROVE_TAC [REAL_LE_TRANS] \\
2021 PROVE_TAC [right_open_interval_empty, real_lte])
2022 >> Cases_on `~(c < d)`
2023 >- (`right_open_interval c d = {}` by PROVE_TAC [right_open_interval_empty] \\
2024 fs [GSYM real_lte] \\
2025 `min b d <= max a c` by PROVE_TAC [REAL_LE_TRANS] \\
2026 PROVE_TAC [right_open_interval_empty, real_lte])
2027 >> fs []
2028 (* now we have assumeed that `a < b /\ c < d`, then there're 4 major cases:
2029 ______
2030 ____________ / \
2031 ----/------------\-----/--------\------> (case 1: b <= c)
2032 a b c d
2033 ________
2034 ______/_____ \ ___
2035 ----/-----/------\---\----\------------> (case 2: c < b /\ a <= c)
2036 a c b d b'
2037 ________ _____
2038 / __\___________ \
2039 ----------/------/---\----------\--\---> (case 3: c < b /\ c < a /\ a <= d)
2040 c a d b d'
2041 _______
2042 / \ ______________
2043 ---/---------\---/--------------\------> (case 4: c < b /\ c < a /\ d < a)
2044 c d a b
2045 *)
2046 >> Cases_on `b <= c` (* case 1 *)
2047 >- (`min b d <= max a c` by PROVE_TAC [REAL_LE_TRANS] \\
2048 `right_open_interval (max a c) (min b d) = {}`
2049 by PROVE_TAC [right_open_interval_empty, real_lte] >> POP_ORW \\
2050 RW_TAC std_ss [right_open_interval, INTER_DEF, EXTENSION,
2051 GSPECIFICATION, NOT_IN_EMPTY] \\
2052 Suff `x < b ==> ~(c <= x)` >- METIS_TAC [] \\
2053 RW_TAC std_ss [real_lte] \\
2054 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `b` >> art [])
2055 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2056 >> Cases_on `a <= c` (* case 2 *)
2057 >- (Cases_on `b <= d`
2058 >- (`(max a c = c) /\ (min b d = b)`
2059 by PROVE_TAC [REAL_MAX_REDUCE, REAL_MIN_REDUCE] \\
2060 RW_TAC std_ss [right_open_interval, INTER_DEF, EXTENSION, GSPECIFICATION] \\
2061 EQ_TAC >> RW_TAC std_ss [] >|
2062 [ MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `c` >> art [],
2063 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `b` >> art [] ]) \\
2064 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
2065 `(max a c = c) /\ (min b d = d)`
2066 by PROVE_TAC [REAL_MAX_REDUCE, REAL_MIN_REDUCE] \\
2067 RW_TAC std_ss [right_open_interval, INTER_DEF, EXTENSION, GSPECIFICATION] \\
2068 EQ_TAC >> RW_TAC std_ss [] >|
2069 [ MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `c` >> art [],
2070 MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC `d` >> art [] ])
2071 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2072 >> Cases_on `a <= d` (* case 3 *)
2073 >- (Cases_on `d <= b`
2074 >- (`(max a c = a) /\ (min b d = d)`
2075 by PROVE_TAC [REAL_MAX_REDUCE, REAL_MIN_REDUCE] \\
2076 RW_TAC std_ss [right_open_interval, INTER_DEF, EXTENSION, GSPECIFICATION] \\
2077 EQ_TAC >> RW_TAC std_ss [] >|
2078 [ MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `d` >> art [],
2079 MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `a` >> art [] \\
2080 MATCH_MP_TAC REAL_LT_IMP_LE >> art [] ]) \\
2081 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
2082 `(max a c = a) /\ (min b d = b)`
2083 by PROVE_TAC [REAL_MAX_REDUCE, REAL_MIN_REDUCE] \\
2084 RW_TAC std_ss [right_open_interval, INTER_DEF, EXTENSION, GSPECIFICATION] \\
2085 EQ_TAC >> RW_TAC std_ss [] >|
2086 [ MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `a` >> art [] \\
2087 MATCH_MP_TAC REAL_LT_IMP_LE >> art [],
2088 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `b` >> art [] \\
2089 MATCH_MP_TAC REAL_LT_IMP_LE >> art [] ])
2090 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2091 >> `min b d < max a c` by PROVE_TAC [REAL_LET_TRANS, REAL_LT_TRANS, REAL_LTE_TRANS]
2092 >> `right_open_interval (max a c) (min b d) = {}`
2093 by PROVE_TAC [right_open_interval_empty, REAL_LT_IMP_LE, real_lte]
2094 >> RW_TAC std_ss [right_open_interval, INTER_DEF, EXTENSION,
2095 GSPECIFICATION, NOT_IN_EMPTY]
2096 >> Suff `a <= x ==> ~(x < d)` >- METIS_TAC []
2097 >> RW_TAC std_ss [GSYM real_lte]
2098 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `a` >> art []
2099 >> MATCH_MP_TAC REAL_LT_IMP_LE >> art []
2100QED
2101
2102(* or, they must have non-empty intersections *)
2103Theorem right_open_interval_union_imp :
2104 !a b c d. a < b /\ c < d /\
2105 (right_open_interval a b) UNION (right_open_interval c d)
2106 IN subsets right_open_intervals ==> a <= d /\ c <= b
2107Proof
2108 RW_TAC std_ss [right_open_intervals, right_open_interval, subsets_def,
2109 GSPECIFICATION, UNION_DEF, EXTENSION]
2110 >> Cases_on `x` >> fs [EXTENSION, GSPECIFICATION] (* 2 subgoals *)
2111 >| [ (* goal 1 (of 2) *)
2112 CCONTR_TAC \\
2113 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
2114 `q <= a /\ a < r` by PROVE_TAC [REAL_LE_REFL] \\
2115 `q <= c /\ c < r` by PROVE_TAC [REAL_LE_REFL] \\
2116 STRIP_ASSUME_TAC (MATCH_MP REAL_MEAN (ASSUME ``d < a :real``)) \\
2117
2118 `c < z` by PROVE_TAC [REAL_LT_TRANS] \\
2119 `q <= z` by PROVE_TAC [REAL_LET_TRANS, REAL_LT_IMP_LE] \\
2120 `z < r` by PROVE_TAC [REAL_LT_TRANS] \\
2121 `a <= z /\ z < b \/ c <= z /\ z < d` by PROVE_TAC []
2122 >| [ PROVE_TAC [REAL_LET_ANTISYM],
2123 PROVE_TAC [REAL_LT_ANTISYM] ],
2124 (* goal 2 (of 2) *)
2125 CCONTR_TAC \\
2126 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
2127 `q <= a /\ a < r` by PROVE_TAC [REAL_LE_REFL] \\
2128 `q <= c /\ c < r` by PROVE_TAC [REAL_LE_REFL] \\
2129 STRIP_ASSUME_TAC (MATCH_MP REAL_MEAN (ASSUME ``b < c :real``)) \\
2130 `a < z` by PROVE_TAC [REAL_LT_TRANS] \\
2131 `q <= z` by PROVE_TAC [REAL_LT_IMP_LE, REAL_LET_TRANS] \\
2132 `z < r` by PROVE_TAC [REAL_LT_TRANS] \\
2133 `a <= z /\ z < b \/ c <= z /\ z < d` by PROVE_TAC []
2134 >| [ PROVE_TAC [REAL_LT_ANTISYM],
2135 PROVE_TAC [REAL_LET_ANTISYM] ] ]
2136QED
2137
2138Theorem right_open_interval_union :
2139 !a b c d. a < b /\ c < d /\ a <= d /\ c <= b ==>
2140 (right_open_interval a b UNION right_open_interval c d =
2141 right_open_interval (min a c) (max b d))
2142Proof
2143 rpt STRIP_TAC
2144 >> `min a c <= a /\ min a c <= c` by PROVE_TAC [REAL_MIN_LE1, REAL_MIN_LE2]
2145 >> `b <= max b d /\ d <= max b d` by PROVE_TAC [REAL_LE_MAX1, REAL_LE_MAX2]
2146 >> RW_TAC std_ss [right_open_interval, EXTENSION, GSPECIFICATION, IN_UNION]
2147 >> EQ_TAC >> rpt STRIP_TAC (* 5 subgoals, first 4 are easy *)
2148 >- (MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `a` >> art [])
2149 >- (MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `b` >> art [])
2150 >- (MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `c` >> art [])
2151 >- (MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `d` >> art [])
2152 >> Cases_on `a <= c` (* 2 subgoals *)
2153 >| [ (* goal 5.1 (of 2) *)
2154 `min a c = a` by PROVE_TAC [REAL_MIN_REDUCE] >> fs [] \\
2155 Cases_on `x < c`
2156 >- (DISJ1_TAC \\
2157 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `c` >> art []) \\
2158 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM real_lte])) \\
2159 Cases_on `x < b` >- (DISJ1_TAC >> art []) \\
2160 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM real_lte])) \\
2161 DISJ2_TAC >> art [] \\
2162 MATCH_MP_TAC REAL_LT_MAX_BETWEEN >> Q.EXISTS_TAC `b` >> art [],
2163 (* goal 5.2 (of 2) *)
2164 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
2165 Cases_on `x < a`
2166 >- (DISJ2_TAC \\
2167 CONJ_TAC
2168 >- (MATCH_MP_TAC REAL_MIN_LE_BETWEEN >> Q.EXISTS_TAC `a` >> art []) \\
2169 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `a` >> art []) \\
2170 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM real_lte])) \\
2171 Cases_on `x < b` >- (DISJ1_TAC >> art []) \\
2172 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM real_lte])) \\
2173 `c <= x` by PROVE_TAC [REAL_LTE_TRANS, REAL_LT_IMP_LE] \\
2174 DISJ2_TAC >> art [] \\
2175 MATCH_MP_TAC REAL_LT_MAX_BETWEEN >> Q.EXISTS_TAC `b` >> art [] ]
2176QED
2177
2178Theorem right_open_interval_DISJOINT_imp :
2179 !a b c d. a < b /\ c < d /\
2180 DISJOINT (right_open_interval a b) (right_open_interval c d) ==>
2181 b <= c \/ d <= a
2182Proof
2183 RW_TAC std_ss [DISJOINT_DEF, INTER_DEF, right_open_interval, EXTENSION,
2184 GSPECIFICATION, NOT_IN_EMPTY]
2185 >> Suff `a < d ==> b <= c` >- METIS_TAC [real_lte]
2186 >> DISCH_TAC
2187 >> CCONTR_TAC
2188 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2189 >> Cases_on `c <= a`
2190 >- (Q.PAT_X_ASSUM `!x. P` (STRIP_ASSUME_TAC o (Q.SPEC `a`)) \\
2191 fs [REAL_LE_REFL])
2192 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2193 >> Cases_on `d < b`
2194 >- (Q.PAT_X_ASSUM `!x. P` (STRIP_ASSUME_TAC o (Q.SPEC `c`)) >| (* 2 subgoals *)
2195 [ (* goal 1 (of 2) *)
2196 `c < a` by PROVE_TAC [real_lte] >> PROVE_TAC [REAL_LT_ANTISYM],
2197 (* goal 2 (of 2) *)
2198 PROVE_TAC [REAL_LE_ANTISYM] ])
2199 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM real_lte]))
2200 >> STRIP_ASSUME_TAC (MATCH_MP REAL_MEAN (ASSUME ``c < b :real``))
2201 >> Q.PAT_X_ASSUM `!x. P` (STRIP_ASSUME_TAC o (Q.SPEC `z`)) (* 3 subgoals *)
2202 >| [ (* goal 1 (of 3) *)
2203 `a < z` by PROVE_TAC [REAL_LT_TRANS] \\
2204 `z < a` by PROVE_TAC [real_lte] \\
2205 PROVE_TAC [REAL_LT_ANTISYM],
2206 (* goal 2 (of 3) *)
2207 `z < c` by PROVE_TAC [real_lte] \\
2208 PROVE_TAC [REAL_LT_ANTISYM],
2209 (* goal 3 (of 3) *)
2210 `z < d` by PROVE_TAC [REAL_LTE_TRANS] ]
2211QED
2212
2213Theorem right_open_interval_DISJOINT_EQ :
2214 !a b c d. a < b /\ c < d ==>
2215 (DISJOINT (right_open_interval a b) (right_open_interval c d) <=>
2216 b <= c \/ d <= a)
2217Proof
2218 rpt STRIP_TAC
2219 >> EQ_TAC
2220 >- (DISCH_TAC >> MATCH_MP_TAC right_open_interval_DISJOINT_imp >> art [])
2221 >> STRIP_TAC
2222 >- (MATCH_MP_TAC right_open_interval_DISJOINT >> rw [REAL_LT_IMP_LE])
2223 >> ONCE_REWRITE_TAC [DISJOINT_SYM]
2224 >> MATCH_MP_TAC right_open_interval_DISJOINT >> rw [REAL_LT_IMP_LE]
2225QED
2226
2227Theorem right_open_intervals_semiring :
2228 semiring right_open_intervals
2229Proof
2230 RW_TAC std_ss [semiring_def, right_open_intervals, space_def, subsets_def,
2231 subset_class_def, SUBSET_UNIV] (* 3 subgoals *)
2232 >- (SIMP_TAC std_ss [GSPECIFICATION, IN_UNIV] \\
2233 Q.EXISTS_TAC `(0,0)` >> SIMP_TAC std_ss [right_open_interval_empty_eq])
2234 >- (fs [GSPECIFICATION, IN_UNIV] \\
2235 Cases_on `x` >> Cases_on `x'` >> fs [] \\
2236 rename1 `s = right_open_interval a b` \\
2237 rename1 `t = right_open_interval c d` \\
2238 Q.EXISTS_TAC `(max a c,min b d)` >> SIMP_TAC std_ss [] \\
2239 REWRITE_TAC [right_open_interval_inter])
2240 >> fs [GSPECIFICATION, IN_UNIV]
2241 >> Cases_on `x` >> Cases_on `x'` >> fs []
2242 >> rename1 `s = right_open_interval a b`
2243 >> rename1 `t = right_open_interval c d`
2244 >> Cases_on `~(a < b)`
2245 >- (fs [GSYM right_open_interval_empty] \\
2246 Q.EXISTS_TAC `{}` \\
2247 ASM_SIMP_TAC std_ss [EMPTY_SUBSET, FINITE_EMPTY, disjoint_empty])
2248 >> Cases_on `~(c < d)`
2249 >- (fs [GSYM right_open_interval_empty] \\
2250 Q.EXISTS_TAC `{right_open_interval a b}` \\
2251 ASM_SIMP_TAC std_ss [BIGUNION_SING, disjoint_sing, FINITE_SING, SUBSET_DEF,
2252 IN_SING, GSPECIFICATION] \\
2253 Q.EXISTS_TAC `(a,b)` >> SIMP_TAC std_ss [])
2254 >> fs []
2255 (* now we have assumeed that `a < b /\ c < d`, then there're 4 major cases:
2256 ______
2257 ____________ / \
2258 ----/------------\-----/--------\------> (case 1: b <= c)
2259 a b c d
2260 ________
2261 ______/_____ \ ___
2262 ----/-----/------\---\----\------------> (case 2: c < b /\ a <= c)
2263 a c b d b'
2264 ________ _____
2265 / __\___________ \
2266 ----------/------/---\----------\--\---> (case 3: c < b /\ c < a /\ a <= d)
2267 c a d b d'
2268 _______
2269 / \ ______________
2270 ---/---------\---/--------------\------> (case 4: c < b /\ c < a /\ d < a)
2271 c d a b
2272 *)
2273 >> Cases_on `b <= c` (* case 1 *)
2274 >- (Q.EXISTS_TAC `{right_open_interval a b}` \\
2275 rw [FINITE_SING, disjoint_sing] >- (qexistsl_tac [`a`, `b`] >> rw []) \\
2276 RW_TAC std_ss [right_open_interval, EXTENSION, IN_DIFF,
2277 GSPECIFICATION, NOT_IN_EMPTY, SUBSET_DEF, IN_BIGUNION] \\
2278 Suff `x < b ==> ~(c <= x)` >- METIS_TAC [] \\
2279 RW_TAC std_ss [real_lte] \\
2280 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `b` >> art [])
2281 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2282 >> Cases_on `a <= c` (* case 2 *)
2283 >- (Cases_on `b <= d`
2284 >- (Q.EXISTS_TAC `{right_open_interval a c}` \\
2285 rw [FINITE_SING, disjoint_sing] >- (qexistsl_tac [`a`, `c`] >> rw []) \\
2286 RW_TAC std_ss [right_open_interval, IN_DIFF, EXTENSION, GSPECIFICATION] \\
2287 EQ_TAC >> RW_TAC std_ss [real_lte] >|
2288 [ PROVE_TAC [REAL_LT_REFL, REAL_LTE_TRANS],
2289 MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC `c` >> art [] ]) \\
2290 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
2291 Q.EXISTS_TAC `{right_open_interval a c; right_open_interval d b}` \\
2292 rw [FINITE_TWO]
2293 >- (qexistsl_tac [`a`, `c`] >> rw [])
2294 >- (qexistsl_tac [`d`, `b`] >> rw [])
2295 >- (MATCH_MP_TAC right_open_interval_disjoint >> PROVE_TAC [REAL_LT_IMP_LE]) \\
2296 RW_TAC std_ss [right_open_interval, IN_DIFF, IN_UNION, EXTENSION, GSPECIFICATION] \\
2297 EQ_TAC >> RW_TAC real_ss [real_lte] >> fs [] >|
2298 [ MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC `c` >> art [],
2299 fs [GSYM real_lte] >> MATCH_MP_TAC REAL_LT_IMP_LE \\
2300 PROVE_TAC [REAL_LET_TRANS, REAL_LTE_TRANS] ])
2301 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2302 >> Cases_on `a <= d` (* case 3 *)
2303 >- (Cases_on `d <= b`
2304 >- (Q.EXISTS_TAC `{right_open_interval d b}` \\
2305 rw [FINITE_SING, disjoint_sing] >- (qexistsl_tac [`d`, `b`] >> rw []) \\
2306 RW_TAC std_ss [right_open_interval, IN_DIFF, EXTENSION, GSPECIFICATION] \\
2307 EQ_TAC >> RW_TAC std_ss [real_lte] >> fs [GSYM real_lte] >|
2308 [ PROVE_TAC [REAL_LTE_ANTISYM, REAL_LT_TRANS],
2309 MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `d` >> art [] ]) \\
2310 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
2311 Q.EXISTS_TAC `{}` \\
2312 RW_TAC std_ss [right_open_interval, EXTENSION, IN_DIFF, disjoint_empty,
2313 GSPECIFICATION, NOT_IN_EMPTY, SUBSET_DEF, IN_BIGUNION,
2314 FINITE_EMPTY] \\
2315 Suff `a <= x /\ x < b ==> c <= x /\ x < d ` >- METIS_TAC [] \\
2316 RW_TAC std_ss [] >|
2317 [ MATCH_MP_TAC REAL_LT_IMP_LE \\
2318 MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `a` >> art [],
2319 MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC `b` >> art [] ])
2320 (* case 4 *)
2321 >> POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [real_lte]))
2322 >> Q.EXISTS_TAC `{right_open_interval a b}`
2323 >> rw [FINITE_SING, disjoint_sing] >- (qexistsl_tac [`a`, `b`] >> rw [])
2324 >> RW_TAC std_ss [right_open_interval, IN_DIFF, EXTENSION, GSPECIFICATION]
2325 >> EQ_TAC >> RW_TAC real_ss [real_lte] >> fs [GSYM real_lte]
2326 >> DISJ2_TAC
2327 >> MATCH_MP_TAC REAL_LT_IMP_LE
2328 >> MATCH_MP_TAC REAL_LTE_TRANS >> Q.EXISTS_TAC `a` >> art []
2329QED
2330
2331Theorem right_open_intervals_sigma_borel :
2332 sigma (space right_open_intervals) (subsets right_open_intervals) = borel
2333Proof
2334 ASSUME_TAC space_borel
2335 >> ASSUME_TAC sigma_algebra_borel
2336 >> `space (sigma (space right_open_intervals)
2337 (subsets right_open_intervals)) = UNIV`
2338 by PROVE_TAC [SPACE_SIGMA, right_open_intervals, space_def]
2339 >> Suff `subsets (sigma (space right_open_intervals)
2340 (subsets right_open_intervals)) =
2341 subsets borel` >- PROVE_TAC [SPACE]
2342 >> MATCH_MP_TAC SUBSET_ANTISYM
2343 >> CONJ_TAC
2344 >- (`space right_open_intervals = space borel`
2345 by PROVE_TAC [right_open_intervals, space_def] >> POP_ORW \\
2346 MATCH_MP_TAC SIGMA_SUBSET >> art [] \\
2347 RW_TAC std_ss [SUBSET_DEF, right_open_intervals, subsets_def,
2348 GSPECIFICATION, IN_UNIV] \\
2349 Cases_on `x'` >> fs [right_open_interval] \\
2350 REWRITE_TAC [borel_measurable_sets_ge_less])
2351 >> REWRITE_TAC [borel_eq_less]
2352 >> MATCH_MP_TAC SIGMA_PROPERTY (* this lemma is so useful! *)
2353 >> STRONG_CONJ_TAC
2354 >- REWRITE_TAC [subset_class_def, SUBSET_UNIV] >> DISCH_TAC
2355 >> STRONG_CONJ_TAC
2356 >- (Suff `{} IN (subsets right_open_intervals)`
2357 >- PROVE_TAC [SUBSET_DEF, SIGMA_SUBSET_SUBSETS] \\
2358 RW_TAC std_ss [right_open_intervals, subsets_def, GSPECIFICATION, IN_UNIV] \\
2359 Q.EXISTS_TAC `(0,0)` >> SIMP_TAC std_ss [right_open_interval_empty_eq])
2360 >> DISCH_TAC
2361 >> Know `sigma_algebra (sigma (space right_open_intervals)
2362 (subsets right_open_intervals))`
2363 >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA \\
2364 RW_TAC std_ss [subset_class_def, space_def, subsets_def, right_open_intervals,
2365 SUBSET_UNIV]) >> DISCH_TAC
2366 >> STRONG_CONJ_TAC
2367 >- (RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV, GSPECIFICATION] \\
2368 Know `{x | x < a} =
2369 BIGUNION (IMAGE (\n. right_open_interval (a - &n) a) univ(:num))`
2370 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION_IMAGE, IN_UNIV, GSPECIFICATION,
2371 right_open_interval] \\
2372 EQ_TAC >> rw [] \\
2373 STRIP_ASSUME_TAC (Q.SPEC `a - x` SIMP_REAL_ARCH) \\
2374 Q.EXISTS_TAC `n` \\
2375 NTAC 2 (POP_ASSUM MP_TAC) >> REAL_ARITH_TAC) >> Rewr' \\
2376 MATCH_MP_TAC SIGMA_ALGEBRA_ENUM >> rw [IN_FUNSET, IN_UNIV] \\
2377 ASSUME_TAC (Q.ISPECL [`space right_open_intervals`,
2378 `subsets right_open_intervals`] SIGMA_SUBSET_SUBSETS) \\
2379 Suff `right_open_interval (a - &n) a IN (subsets right_open_intervals)`
2380 >- ASM_SET_TAC [] \\
2381 rw [right_open_intervals, subsets_def, GSPECIFICATION] \\
2382 Q.EXISTS_TAC `(a - &n, a)` >> rw []) >> DISCH_TAC
2383 >> CONJ_TAC
2384 >- (RW_TAC std_ss [IN_INTER] \\
2385 Q.PAT_X_ASSUM `space (sigma (space right_open_intervals)
2386 (subsets right_open_intervals)) = UNIV`
2387 (ONCE_REWRITE_TAC o wrap o (MATCH_MP EQ_SYM)) \\
2388 MATCH_MP_TAC ALGEBRA_COMPL >> fs [sigma_algebra_def])
2389 >> fs [sigma_algebra_def]
2390QED
2391
2392Theorem right_open_intervals_subset_borel :
2393 (subsets right_open_intervals) SUBSET subsets borel
2394Proof
2395 REWRITE_TAC [SYM right_open_intervals_sigma_borel]
2396 >> PROVE_TAC [SIGMA_SUBSET_SUBSETS]
2397QED
2398
2399(* another equivalent definition of `borel` *)
2400Theorem borel_eq_ge_less :
2401 borel = sigma UNIV (IMAGE (\(a,b). {x | a <= x /\ x < b}) UNIV)
2402Proof
2403 ASSUME_TAC (REWRITE_RULE [space_borel, space_def, subsets_def,
2404 right_open_interval, right_open_intervals]
2405 (SYM right_open_intervals_sigma_borel))
2406 >> Suff `IMAGE (\(a,b). {x | a <= x /\ x < b}) univ(:real # real) =
2407 {{x:real | a <= x /\ x < b} | T}` >- rw []
2408 >> KILL_TAC
2409 >> RW_TAC std_ss [Once EXTENSION, IN_IMAGE, IN_UNIV, GSPECIFICATION]
2410 >> EQ_TAC >> rpt STRIP_TAC
2411 >> Cases_on `x'` >> fs []
2412 >> Q.EXISTS_TAC `(q,r)` >> rw []
2413QED
2414
2415(* cf. integrationTheory.INTERVAL_UPPERBOUND for open/closed intervals *)
2416Theorem right_open_interval_upperbound :
2417 !a b. a < b ==> interval_upperbound (right_open_interval a b) = b
2418Proof
2419 RW_TAC std_ss [interval_upperbound]
2420 >- (fs [EXTENSION, GSPECIFICATION, in_right_open_interval] \\
2421 METIS_TAC [REAL_LE_REFL])
2422 >> RW_TAC std_ss [right_open_interval, GSPECIFICATION,
2423 GSYM REAL_LE_ANTISYM]
2424 >- (MATCH_MP_TAC REAL_IMP_SUP_LE >> rw []
2425 >- (Q.EXISTS_TAC `a` >> rw [REAL_LE_REFL]) \\
2426 MATCH_MP_TAC REAL_LT_IMP_LE >> art [])
2427 >> MATCH_MP_TAC REAL_LE_EPSILON
2428 >> rpt STRIP_TAC
2429 >> Q.ABBREV_TAC `y = sup {x | a <= x /\ x < b}`
2430 >> `b <= y + e <=> b - e <= y` by REAL_ARITH_TAC >> POP_ORW
2431 >> Q.UNABBREV_TAC `y`
2432 >> MATCH_MP_TAC REAL_IMP_LE_SUP >> rw []
2433 >- (Q.EXISTS_TAC `b` >> rw [] \\
2434 MATCH_MP_TAC REAL_LT_IMP_LE >> art [])
2435 >> Cases_on `a <= b - e`
2436 >- (Q.EXISTS_TAC `b - e` >> rw [REAL_LE_TRANS] \\
2437 Q.PAT_X_ASSUM `0 < e` MP_TAC >> REAL_ARITH_TAC)
2438 >> Q.EXISTS_TAC `a` >> rw [REAL_LE_REFL]
2439 >> MATCH_MP_TAC REAL_LT_IMP_LE >> fs [real_lte]
2440QED
2441
2442Theorem right_open_interval_lowerbound :
2443 !a b. a < b ==> interval_lowerbound (right_open_interval a b) = a
2444Proof
2445 RW_TAC std_ss [interval_lowerbound]
2446 >- (fs [EXTENSION, GSPECIFICATION, in_right_open_interval] \\
2447 METIS_TAC [REAL_LE_REFL])
2448 >> RW_TAC std_ss [right_open_interval, GSPECIFICATION]
2449 >> MATCH_MP_TAC REAL_INF_MIN >> rw []
2450QED
2451
2452Theorem right_open_interval_two_bounds :
2453 !a b. interval_lowerbound (right_open_interval a b) <=
2454 interval_upperbound (right_open_interval a b)
2455Proof
2456 rpt GEN_TAC
2457 >> Cases_on `a < b`
2458 >- (rw [right_open_interval_upperbound, right_open_interval_lowerbound] \\
2459 IMP_RES_TAC REAL_LT_IMP_LE)
2460 >> fs [GSYM right_open_interval_empty]
2461 >> rw [interval_lowerbound, interval_upperbound]
2462QED
2463
2464Theorem right_open_interval_between_bounds :
2465 !x a b. x IN right_open_interval a b <=>
2466 interval_lowerbound (right_open_interval a b) <= x /\
2467 x < interval_upperbound (right_open_interval a b)
2468Proof
2469 rpt GEN_TAC
2470 >> reverse (Cases_on `a < b`)
2471 >- (FULL_SIMP_TAC std_ss [GSYM right_open_interval_empty] \\
2472 rw [NOT_IN_EMPTY, INTERVAL_BOUNDS_EMPTY] \\
2473 REAL_ARITH_TAC)
2474 >> rw [in_right_open_interval]
2475 >> EQ_TAC >> rpt STRIP_TAC (* 4 subgoals *)
2476 >| [ (* goal 1 (of 4) *)
2477 fs [right_open_interval_lowerbound],
2478 (* goal 2 (of 4) *)
2479 fs [right_open_interval_upperbound],
2480 (* goal 3 (of 4) *)
2481 rfs [right_open_interval_lowerbound, right_open_interval_upperbound],
2482 (* goal 4 (of 4) *)
2483 rfs [right_open_interval_lowerbound, right_open_interval_upperbound] ]
2484QED
2485
2486(* ------------------------------------------------------------------------- *)
2487(* Standard Cubes *)
2488(* ------------------------------------------------------------------------- *)
2489
2490val _ = hide "line"; (* for satefy purposes only *)
2491
2492Definition line :
2493 line n = {x:real | -&n <= x /\ x <= &n}
2494End
2495
2496Theorem IN_LINE :
2497 !x n. x IN line n <=> -&n <= x /\ x <= &n
2498Proof
2499 rw [line]
2500QED
2501
2502Theorem line_def :
2503 !n. line n = interval [-&n,&n]
2504Proof
2505 rw [interval, line]
2506QED
2507
2508Theorem borel_line: !n. line n IN subsets borel
2509Proof
2510 RW_TAC std_ss [line]
2511 >> MATCH_MP_TAC borel_closed
2512 >> SIMP_TAC std_ss [GSYM interval, CLOSED_INTERVAL]
2513QED
2514
2515Theorem line_closed: !n. closed (line n)
2516Proof
2517 RW_TAC std_ss [GSYM interval, line, CLOSED_INTERVAL]
2518QED
2519
2520Theorem LINE_MONO : (* was: line_subset *)
2521 !n N. n <= N ==> line n SUBSET line N
2522Proof
2523 FULL_SIMP_TAC std_ss [line, SUBSET_DEF, GSPECIFICATION] THEN
2524 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THENL
2525 [EXISTS_TAC ``-&n:real`` THEN ASM_SIMP_TAC real_ss [],
2526 EXISTS_TAC ``&n:real`` THEN ASM_SIMP_TAC real_ss []]
2527QED
2528
2529Theorem LINE_MONO_EQ : (* was: line_subset_iff *)
2530 !n N. line n SUBSET line N <=> n <= N
2531Proof
2532 REPEAT GEN_TAC THEN EQ_TAC THENL
2533 [ALL_TAC, REWRITE_TAC [LINE_MONO]] THEN
2534 SIMP_TAC std_ss [line, SUBSET_DEF, GSPECIFICATION] THEN
2535 DISCH_THEN (MP_TAC o SPEC ``&n:real``) THEN
2536 KNOW_TAC ``-&n <= &n:real /\ &n <= &n:real`` THENL
2537 [SIMP_TAC std_ss [REAL_LE_REFL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
2538 EXISTS_TAC ``0:real`` THEN
2539 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_NEG_0] THEN
2540 SIMP_TAC std_ss [REAL_LE_NEG, REAL_POS], ALL_TAC] THEN
2541 DISC_RW_KILL THEN SIMP_TAC real_ss []
2542QED
2543
2544Theorem BALL_IN_LINE : (* was: ball_subset_line *)
2545 !n. ball (0,&n) SUBSET line n
2546Proof
2547 GEN_TAC THEN SIMP_TAC std_ss [ball, line, SUBSET_DEF, GSPECIFICATION] THEN
2548 GEN_TAC THEN SIMP_TAC std_ss [DIST_0] THEN REAL_ARITH_TAC
2549QED
2550
2551Theorem REAL_IN_LINE : (* was: mem_big_line *)
2552 !x. ?n. x IN line n
2553Proof
2554 GEN_TAC THEN MP_TAC (ISPEC ``x:real`` SIMP_REAL_ARCH) THEN
2555 STRIP_TAC THEN SIMP_TAC std_ss [line, GSPECIFICATION] THEN
2556 ASM_CASES_TAC ``0 <= x:real`` THENL
2557 [EXISTS_TAC ``n:num`` THEN ASM_REAL_ARITH_TAC, ALL_TAC] THEN
2558 MP_TAC (ISPEC ``-x:real`` SIMP_REAL_ARCH) THEN STRIP_TAC THEN
2559 EXISTS_TAC ``n':num`` THEN ASM_REAL_ARITH_TAC
2560QED
2561
2562Theorem LINE_MONO_SUC : (* was: line_subset_Suc *)
2563 !n. line n SUBSET line (SUC n)
2564Proof
2565 GEN_TAC THEN MATCH_MP_TAC LINE_MONO THEN ARITH_TAC
2566QED
2567
2568(* [-n [a, b] n] *)
2569Theorem LINE_EXISTS :
2570 !a b. ?n. interval [a,b] SUBSET line n
2571Proof
2572 rpt STRIP_TAC
2573 >> STRIP_ASSUME_TAC (Q.SPEC ‘max (abs a) (abs b)’ SIMP_REAL_ARCH)
2574 >> fs [REAL_MAX_LE, ABS_BOUNDS]
2575 >> Q.EXISTS_TAC ‘n’
2576 >> rw [SUBSET_DEF, line_def, IN_INTERVAL]
2577 >| [ Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘a’ >> art [],
2578 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘b’ >> art [] ]
2579QED
2580
2581Theorem BOUNDED_LINE_EXISTS :
2582 !s. bounded s ==> ?n. s SUBSET line n
2583Proof
2584 rw [bounded_def, ABS_BOUNDS]
2585 >> MP_TAC (Q.SPECL [‘-a’, ‘a’] LINE_EXISTS) >> rw []
2586 >> Q.EXISTS_TAC ‘n’
2587 >> Q_TAC (TRANS_TAC SUBSET_TRANS) ‘interval [-a,a]’ >> art []
2588 >> rw [SUBSET_DEF, IN_INTERVAL]
2589QED
2590
2591(* cf. right_open_interval_11 *)
2592Theorem closed_interval_11 :
2593 !a b c d. a < b /\ c < d ==>
2594 (interval [a,b] = interval [c,d] <=> a = c /\ b = d)
2595Proof
2596 rw [EQ_INTERVAL, GSYM INTERVAL_EQ_EMPTY]
2597 >> REAL_ASM_ARITH_TAC
2598QED
2599
2600(* cf. right_open_interval_SUBSET_EQ, ordering: [c [a, b] d] *)
2601Theorem closed_interval_subset_eq :
2602 !a b c d. a < b /\ c < d ==>
2603 (interval [a,b] SUBSET interval [c,d] <=> c <= a /\ b <= d)
2604Proof
2605 rpt STRIP_TAC
2606 >> EQ_TAC >> rw [SUBSET_DEF, IN_INTERVAL] (* 4 subgoals *)
2607 >| [ (* goal 1 (of 4) *)
2608 CCONTR_TAC >> fs [GSYM real_lt] \\
2609 (* a < z < b,c < d *)
2610 MP_TAC (Q.SPECL [‘a’, ‘min b c’] REAL_MEAN) \\
2611 ASM_REWRITE_TAC [REAL_LT_MIN] \\
2612 CCONTR_TAC >> fs [] \\
2613 ‘a <= z /\ z <= b’ by simp [REAL_LT_IMP_LE] \\
2614 ‘c <= z’ by PROVE_TAC [] \\
2615 METIS_TAC [REAL_LTE_ANTISYM],
2616 (* goal 2 (of 4) *)
2617 CCONTR_TAC >> fs [GSYM real_lt] \\
2618 (* c < d,a < z < b *)
2619 MP_TAC (Q.SPECL [‘max d a’, ‘b’] REAL_MEAN) \\
2620 ASM_REWRITE_TAC [REAL_MAX_LT] \\
2621 CCONTR_TAC >> fs [] \\
2622 ‘a <= z /\ z <= b’ by simp [REAL_LT_IMP_LE] \\
2623 ‘z <= d’ by PROVE_TAC [] \\
2624 METIS_TAC [REAL_LTE_ANTISYM],
2625 (* goal 3 (of 4) *)
2626 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘a’ >> art [],
2627 (* goal 3 (of 3) *)
2628 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘b’ >> art [] ]
2629QED
2630
2631(* cf. right_open_interval_SUBSET *)
2632Theorem closed_interval_subset :
2633 !a b c d. a < b /\ c < d /\ interval [a,b] SUBSET interval [c,d] ==>
2634 b - a <= d - c
2635Proof
2636 rpt STRIP_TAC
2637 >> POP_ASSUM MP_TAC
2638 >> simp [closed_interval_subset_eq]
2639 >> REAL_ASM_ARITH_TAC
2640QED
2641
2642(* cf. right_open_interval_DISJOINT_EQ *)
2643Theorem closed_interval_disjoint_eq :
2644 !a b c d. a < b /\ c < d ==>
2645 (DISJOINT (interval (a,b)) (interval (c,d)) <=> b <= c \/ d <= a)
2646Proof
2647 rw [DISJOINT_ALT, IN_INTERVAL]
2648 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *)
2649 >| [ (* goal 1 (of 3) *)
2650 CCONTR_TAC >> fs [REAL_NOT_LE, REAL_NOT_LT] \\
2651 (* a < c < b < d *)
2652 MP_TAC (Q.SPECL [‘max a c’, ‘min b d’] REAL_MEAN) \\
2653 rw [REAL_MAX_LT, REAL_LT_MIN] \\
2654 CCONTR_TAC >> fs [] (* a < c < z < b < d *) \\
2655 METIS_TAC [REAL_LET_ANTISYM],
2656 (* goal 2 (of 3) *)
2657 CCONTR_TAC >> fs [] \\
2658 ‘x < c’ by PROVE_TAC [REAL_LTE_TRANS] \\
2659 METIS_TAC [REAL_LT_ANTISYM],
2660 (* goal 3 (of 3) *)
2661 CCONTR_TAC >> fs [] \\
2662 ‘d < x’ by PROVE_TAC [REAL_LET_TRANS] \\
2663 METIS_TAC [REAL_LT_ANTISYM] ]
2664QED
2665
2666(* ------------------------------------------------------------------------- *)
2667(* Two-dimensional Borel sigma-algebra (real version), author: Chun Tian *)
2668(* ------------------------------------------------------------------------- *)
2669
2670(* Theorem 3.8 [1,p.19]: borel_2d can be also generated by open rectangles
2671 having rational endpoints.
2672
2673 see open_UNION_rational_box for one-dimension case.
2674 *)
2675Theorem borel_2d_lemma1[local] :
2676 !U. open_in (mtop mr2) U ==>
2677 U = BIGUNION
2678 {J | ?a b c d. a IN q_set /\ b IN q_set /\ c IN q_set /\ d IN q_set /\
2679 J = OPEN_interval (a,b) CROSS OPEN_interval (c,d) /\
2680 J SUBSET U}
2681Proof
2682 rpt STRIP_TAC
2683 >> MATCH_MP_TAC SUBSET_ANTISYM
2684 >> reverse CONJ_TAC
2685 >- (rw [SUBSET_DEF, IN_BIGUNION] \\
2686 POP_ASSUM MATCH_MP_TAC >> art [])
2687 (* now the hard part, fix ‘x IN U’ *)
2688 >> rw [Once SUBSET_DEF]
2689 >> fs [MTOP_OPEN]
2690 >> Q.PAT_X_ASSUM ‘!x. U x ==> _’ (MP_TAC o (Q.SPEC ‘x’))
2691 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [IN_APP]))
2692 >> RW_TAC std_ss []
2693 >> Cases_on ‘x’ >> rename1 ‘U (x1,x2)’
2694 >> MP_TAC (Q.SPECL [‘x2’, ‘e / 2’] rational_boxes)
2695 >> MP_TAC (Q.SPECL [‘x1’, ‘e / 2’] rational_boxes)
2696 >> Know ‘0 < e / 2’
2697 >- (MATCH_MP_TAC REAL_LT_DIV >> rw [])
2698 >> RW_TAC std_ss []
2699 >> rename1 ‘x2 IN box c d’
2700 >> fs [box_alt, ball, dist]
2701 >> Q.EXISTS_TAC ‘OPEN_interval (a,b) CROSS OPEN_interval (c,d)’
2702 >> rw [IN_CROSS]
2703 >> qexistsl_tac [‘a’, ‘b’, ‘c’, ‘d’]
2704 >> rw [SUBSET_DEF, IN_CROSS]
2705 >> REWRITE_TAC [IN_APP]
2706 >> FIRST_X_ASSUM MATCH_MP_TAC
2707 >> Cases_on ‘x’ >> fs []
2708 (* stage work *)
2709 >> MATCH_MP_TAC REAL_LET_TRANS
2710 >> Q.EXISTS_TAC ‘dist mr2 ((x1,x2),(q,x2)) + dist mr2 ((q,x2),(q,r))’
2711 >> REWRITE_TAC [METRIC_TRIANGLE]
2712 >> rw [MR2_DEF]
2713 >> Know ‘(x1 - q) pow 2 = (abs (x1 - q)) pow 2’
2714 >- (rw [POW_ABS, ABS_POW2]) >> Rewr'
2715 >> Know ‘(x2 - r) pow 2 = (abs (x2 - r)) pow 2’
2716 >- (rw [POW_ABS, ABS_POW2]) >> Rewr'
2717 >> Know ‘sqrt (abs (x1 - q) pow 2) = abs (x1 - q)’
2718 >- (MATCH_MP_TAC POW_2_SQRT \\
2719 REWRITE_TAC [ABS_POS]) >> Rewr'
2720 >> Know ‘sqrt (abs (x2 - r) pow 2) = abs (x2 - r)’
2721 >- (MATCH_MP_TAC POW_2_SQRT \\
2722 REWRITE_TAC [ABS_POS]) >> Rewr'
2723 >> ‘e = e / 2 + e / 2’ by REWRITE_TAC [REAL_HALF_DOUBLE] >> POP_ORW
2724 >> MATCH_MP_TAC REAL_LT_ADD2
2725 >> CONJ_TAC (* 2 subgoals *)
2726 >| [ (* goal 1 (of 2) *)
2727 Q.PAT_X_ASSUM ‘interval (a,b) SUBSET _’ MP_TAC \\
2728 Q.PAT_X_ASSUM ‘q IN interval (a,b)’ MP_TAC,
2729 (* goal 2 (of 2) *)
2730 Q.PAT_X_ASSUM ‘interval (c,d) SUBSET _’ MP_TAC \\
2731 Q.PAT_X_ASSUM ‘r IN interval (c,d)’ MP_TAC ]
2732 >> rw [SUBSET_DEF, IN_INTERVAL]
2733QED
2734
2735Theorem IMAGE_FST_CROSS_INTERVAL :
2736 !a b c d. c < d ==>
2737 IMAGE FST (interval (a,b) CROSS interval (c,d)) = interval (a,b)
2738Proof
2739 rw [Once EXTENSION, IN_INTERVAL]
2740 >> EQ_TAC >> rw [] >> art []
2741 >> MP_TAC (Q.SPECL [‘c’, ‘d’] REAL_MEAN)
2742 >> RW_TAC std_ss []
2743 >> Q.EXISTS_TAC ‘(x,z)’
2744 >> RW_TAC std_ss []
2745QED
2746
2747Theorem IMAGE_SND_CROSS_INTERVAL :
2748 !a b c d. a < b ==>
2749 IMAGE SND (interval (a,b) CROSS interval (c,d)) = interval (c,d)
2750Proof
2751 rw [Once EXTENSION, IN_INTERVAL]
2752 >> EQ_TAC >> rw [] >> art []
2753 >> MP_TAC (Q.SPECL [‘a’, ‘b’] REAL_MEAN)
2754 >> RW_TAC std_ss []
2755 >> Q.EXISTS_TAC ‘(z,x)’
2756 >> RW_TAC std_ss []
2757QED
2758
2759(* This proof needs advanced results from cardinalTheory *)
2760Theorem borel_2d_lemma2[local] :
2761 !U. COUNTABLE
2762 {J | ?a b c d. a IN q_set /\ b IN q_set /\ c IN q_set /\ d IN q_set /\
2763 J = OPEN_interval (a,b) CROSS OPEN_interval (c,d) /\
2764 J SUBSET U}
2765Proof
2766 GEN_TAC
2767 >> MATCH_MP_TAC (INST_TYPE [“:'b” |-> “:real # real # real # real”]
2768 CARD_LE_COUNTABLE)
2769 >> Q.EXISTS_TAC ‘q_set CROSS (q_set CROSS (q_set CROSS q_set))’
2770 >> CONJ_TAC >- PROVE_TAC [COUNTABLE_CROSS, QSET_COUNTABLE]
2771 >> rw [cardleq_def]
2772 >> Q.EXISTS_TAC ‘\s. if s = {} then (0,0,0,0)
2773 else (interval_lowerbound (IMAGE FST s),
2774 interval_upperbound (IMAGE FST s),
2775 interval_lowerbound (IMAGE SND s),
2776 interval_upperbound (IMAGE SND s))’
2777 >> rw [INJ_DEF] (* 5 subgoals *)
2778 >| [ (* goal 1 (of 5) *)
2779 reverse (Cases_on ‘a < b’)
2780 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2781 rw [real_of_num, NUM_IN_QSET]) \\
2782 reverse (Cases_on ‘c < d’)
2783 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2784 rw [real_of_num, NUM_IN_QSET]) \\
2785 ‘interval (a,b) <> {} /\ interval (c,d) <> {}’
2786 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2787 Know ‘interval (a,b) CROSS interval (c,d) <> {}’
2788 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2789 RW_TAC std_ss [] \\
2790 Know ‘IMAGE FST (interval (a,b) CROSS interval (c,d)) = interval (a,b)’
2791 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) >> Rewr' \\
2792 Suff ‘interval_lowerbound (interval (a,b)) = a’ >- rw [] \\
2793 MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art [],
2794 (* goal 2 (of 5) *)
2795 reverse (Cases_on ‘a < b’)
2796 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2797 rw [real_of_num, NUM_IN_QSET]) \\
2798 reverse (Cases_on ‘c < d’)
2799 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2800 rw [real_of_num, NUM_IN_QSET]) \\
2801 ‘interval (a,b) <> {} /\ interval (c,d) <> {}’
2802 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2803 Know ‘interval (a,b) CROSS interval (c,d) <> {}’
2804 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2805 RW_TAC std_ss [] \\
2806 Know ‘IMAGE FST (interval (a,b) CROSS interval (c,d)) = interval (a,b)’
2807 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) >> Rewr' \\
2808 Suff ‘interval_upperbound (interval (a,b)) = b’ >- rw [] \\
2809 MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art [],
2810 (* goal 3 (of 5) *)
2811 reverse (Cases_on ‘a < b’)
2812 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2813 rw [real_of_num, NUM_IN_QSET]) \\
2814 reverse (Cases_on ‘c < d’)
2815 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2816 rw [real_of_num, NUM_IN_QSET]) \\
2817 ‘interval (a,b) <> {} /\ interval (c,d) <> {}’
2818 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2819 Know ‘interval (a,b) CROSS interval (c,d) <> {}’
2820 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2821 RW_TAC std_ss [] \\
2822 Know ‘IMAGE SND (interval (a,b) CROSS interval (c,d)) = interval (c,d)’
2823 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) >> Rewr' \\
2824 Suff ‘interval_lowerbound (interval (c,d)) = c’ >- rw [] \\
2825 MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art [],
2826 (* goal 4 (of 5) *)
2827 reverse (Cases_on ‘a < b’)
2828 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2829 rw [real_of_num, NUM_IN_QSET]) \\
2830 reverse (Cases_on ‘c < d’)
2831 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2832 rw [real_of_num, NUM_IN_QSET]) \\
2833 ‘interval (a,b) <> {} /\ interval (c,d) <> {}’
2834 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2835 Know ‘interval (a,b) CROSS interval (c,d) <> {}’
2836 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2837 RW_TAC std_ss [] \\
2838 Know ‘IMAGE SND (interval (a,b) CROSS interval (c,d)) = interval (c,d)’
2839 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) >> Rewr' \\
2840 Suff ‘interval_upperbound (interval (c,d)) = d’ >- rw [] \\
2841 MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art [],
2842 (* goal 5 (of 5) *)
2843 reverse (Cases_on ‘a < b’)
2844 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2845 reverse (Cases_on ‘a' < b'’)
2846 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY]) \\
2847 reverse (Cases_on ‘c' < d'’)
2848 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY]) \\
2849 ‘interval (a',b') <> {} /\ interval (c',d') <> {}’
2850 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2851 Know ‘interval (a',b') CROSS interval (c',d') <> {}’
2852 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2853 DISCH_THEN (fs o wrap) \\
2854 Know ‘IMAGE FST (interval (a',b') CROSS interval (c',d')) = interval (a',b')’
2855 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) \\
2856 DISCH_THEN (fs o wrap) \\
2857 Know ‘IMAGE SND (interval (a',b') CROSS interval (c',d')) = interval (c',d')’
2858 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) \\
2859 DISCH_THEN (fs o wrap) \\
2860 Know ‘interval_lowerbound (interval (a',b')) = a'’
2861 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2862 DISCH_THEN (fs o wrap) \\
2863 Know ‘interval_upperbound (interval (a',b')) = b'’
2864 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2865 DISCH_THEN (fs o wrap) \\
2866 rfs [REAL_LT_REFL]) \\
2867 reverse (Cases_on ‘c < d’)
2868 >- (fs [GSYM real_lte] \\
2869 ‘interval (c,d) = {}’ by PROVE_TAC [INTERVAL_EQ_EMPTY] >> fs [] \\
2870 reverse (Cases_on ‘a' < b'’)
2871 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY]) \\
2872 reverse (Cases_on ‘c' < d'’)
2873 >- (fs [GSYM real_lte, INTERVAL_EQ_EMPTY]) \\
2874 ‘interval (a',b') <> {} /\ interval (c',d') <> {}’
2875 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2876 Know ‘interval (a',b') CROSS interval (c',d') <> {}’
2877 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2878 DISCH_THEN (fs o wrap) \\
2879 Know ‘IMAGE FST (interval (a',b') CROSS interval (c',d')) = interval (a',b')’
2880 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) \\
2881 DISCH_THEN (fs o wrap) \\
2882 Know ‘IMAGE SND (interval (a',b') CROSS interval (c',d')) = interval (c',d')’
2883 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) \\
2884 DISCH_THEN (fs o wrap) \\
2885 Know ‘interval_lowerbound (interval (a',b')) = a'’
2886 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2887 DISCH_THEN (fs o wrap) \\
2888 Know ‘interval_upperbound (interval (a',b')) = b'’
2889 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2890 DISCH_THEN (fs o wrap) \\
2891 rfs [REAL_LT_REFL]) \\
2892 ‘interval (a,b) <> {} /\ interval (c,d) <> {}’
2893 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2894 Know ‘interval (a,b) CROSS interval (c,d) <> {}’
2895 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2896 DISCH_THEN (fs o wrap) \\
2897 reverse (Cases_on ‘a' < b'’)
2898 >- (fs [GSYM real_lte] \\
2899 ‘interval (a',b') = {}’ by PROVE_TAC [INTERVAL_EQ_EMPTY] >> fs [] \\
2900 Know ‘IMAGE FST (interval (a,b) CROSS interval (c,d)) = interval (a,b)’
2901 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) \\
2902 DISCH_THEN (fs o wrap) \\
2903 Know ‘IMAGE SND (interval (a,b) CROSS interval (c,d)) = interval (c,d)’
2904 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) \\
2905 DISCH_THEN (fs o wrap) \\
2906 Know ‘interval_lowerbound (interval (a,b)) = a’
2907 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2908 DISCH_THEN (fs o wrap) \\
2909 Know ‘interval_upperbound (interval (a,b)) = b’
2910 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2911 DISCH_THEN (fs o wrap) \\
2912 rfs [REAL_LT_REFL]) \\
2913 reverse (Cases_on ‘c' < d'’)
2914 >- (fs [GSYM real_lte] \\
2915 ‘interval (c',d') = {}’ by PROVE_TAC [INTERVAL_EQ_EMPTY] >> fs [] \\
2916 Know ‘IMAGE FST (interval (a,b) CROSS interval (c,d)) = interval (a,b)’
2917 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) \\
2918 DISCH_THEN (fs o wrap) \\
2919 Know ‘IMAGE SND (interval (a,b) CROSS interval (c,d)) = interval (c,d)’
2920 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) \\
2921 DISCH_THEN (fs o wrap) \\
2922 Know ‘interval_lowerbound (interval (a,b)) = a’
2923 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2924 DISCH_THEN (fs o wrap) \\
2925 Know ‘interval_upperbound (interval (a,b)) = b’
2926 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2927 DISCH_THEN (fs o wrap) \\
2928 rfs [REAL_LT_REFL]) \\
2929 ‘interval (a',b') <> {} /\ interval (c',d') <> {}’
2930 by PROVE_TAC [GSYM real_lte, INTERVAL_EQ_EMPTY] \\
2931 Know ‘interval (a',b') CROSS interval (c',d') <> {}’
2932 >- (CCONTR_TAC >> rfs [CROSS_EMPTY_EQN]) \\
2933 DISCH_THEN (fs o wrap) \\
2934 Know ‘IMAGE FST (interval (a,b) CROSS interval (c,d)) = interval (a,b)’
2935 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) \\
2936 DISCH_THEN (fs o wrap) \\
2937 Know ‘IMAGE SND (interval (a,b) CROSS interval (c,d)) = interval (c,d)’
2938 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) \\
2939 DISCH_THEN (fs o wrap) \\
2940 Know ‘IMAGE FST (interval (a',b') CROSS interval (c',d')) = interval (a',b')’
2941 >- (MATCH_MP_TAC IMAGE_FST_CROSS_INTERVAL >> art []) \\
2942 DISCH_THEN (fs o wrap) \\
2943 Know ‘IMAGE SND (interval (a',b') CROSS interval (c',d')) = interval (c',d')’
2944 >- (MATCH_MP_TAC IMAGE_SND_CROSS_INTERVAL >> art []) \\
2945 DISCH_THEN (fs o wrap) \\
2946 Know ‘interval_lowerbound (interval (a,b)) = a’
2947 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2948 DISCH_THEN (fs o wrap) \\
2949 Know ‘interval_upperbound (interval (a,b)) = b’
2950 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2951 DISCH_THEN (fs o wrap) \\
2952 Know ‘interval_lowerbound (interval (a',b')) = a'’
2953 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2954 DISCH_THEN (fs o wrap) \\
2955 Know ‘interval_upperbound (interval (a',b')) = b'’
2956 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2957 DISCH_THEN (fs o wrap) \\
2958 Know ‘interval_lowerbound (interval (c,d)) = c’
2959 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2960 DISCH_THEN (fs o wrap) \\
2961 Know ‘interval_upperbound (interval (c,d)) = d’
2962 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2963 DISCH_THEN (fs o wrap) \\
2964 Know ‘interval_lowerbound (interval (c',d')) = c'’
2965 >- (MATCH_MP_TAC OPEN_INTERVAL_LOWERBOUND >> art []) \\
2966 DISCH_THEN (fs o wrap) \\
2967 Know ‘interval_upperbound (interval (c',d')) = d'’
2968 >- (MATCH_MP_TAC OPEN_INTERVAL_UPPERBOUND >> art []) \\
2969 DISCH_THEN (fs o wrap) ]
2970QED
2971
2972Theorem POW_2_SUB[local] :
2973 !x y. (x - y) pow 2 = (y - x) pow 2
2974Proof
2975 rpt GEN_TAC
2976 >> ‘(x - y) pow 2 = (abs (x - y)) pow 2’ by PROVE_TAC [REAL_POW2_ABS] >> POP_ORW
2977 >> ‘(y - x) pow 2 = (abs (y - x)) pow 2’ by PROVE_TAC [REAL_POW2_ABS] >> POP_ORW
2978 >> REWRITE_TAC [Once ABS_SUB]
2979QED
2980
2981Theorem box_open_in_mr2 :
2982 !a b c d. open_in (mtop mr2) (interval (a,b) CROSS interval (c,d))
2983Proof
2984 rw [MTOP_OPEN]
2985 >> Cases_on ‘x’ >> fs []
2986 (* open_in (mtop mr2) (interval (a,b) CROSS interval (c,d)) *)
2987 >> reverse (Cases_on ‘a < b’)
2988 >- (‘interval (a,b) = {}’ by METIS_TAC [real_lte, INTERVAL_EQ_EMPTY] \\
2989 FULL_SIMP_TAC std_ss [NOT_IN_EMPTY])
2990 >> reverse (Cases_on ‘c < d’)
2991 >- (‘interval (c,d) = {}’ by METIS_TAC [real_lte, INTERVAL_EQ_EMPTY] \\
2992 FULL_SIMP_TAC std_ss [NOT_IN_EMPTY])
2993 (* stage work *)
2994 >> Q.ABBREV_TAC ‘dx = min (q - a) (b - q)’
2995 >> Q.ABBREV_TAC ‘dy = min (r - c) (d - r)’
2996 >> Q.EXISTS_TAC ‘min dx dy’
2997 >> STRONG_CONJ_TAC
2998 >- (rw [Abbr ‘dx’, Abbr ‘dy’, REAL_LT_MIN, REAL_SUB_LT] \\
2999 fs [IN_INTERVAL])
3000 >> DISCH_TAC
3001 >> GEN_TAC
3002 >> Cases_on ‘y’
3003 >> rw [REAL_LT_MIN, IN_INTERVAL] (* 4 subgoals *)
3004 >> rename1 ‘dist mr2 ((x0,y0),(x1,y1)) < dx’
3005 >| [ (* goal 1 (of 4) *)
3006 CCONTR_TAC >> fs [GSYM real_lte] \\
3007 Know ‘dist mr2 ((x0,y0),(x1,y0)) <= dist mr2 ((x0,y0),(x1,y1))’
3008 >- (rw [MR2_DEF] \\
3009 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3010 Know ‘dist mr2 ((x0,y0),(x1,y0)) < dx’
3011 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3012 Q.EXISTS_TAC ‘dist mr2 ((x0,y0),(x1,y1))’ >> art []) \\
3013 rw [Abbr ‘dx’, REAL_LT_MIN, MR2_DEF] \\
3014 DISJ1_TAC >> rw [GSYM real_lte] \\
3015 Cases_on ‘0 <= x0 - x1’
3016 >- (Know ‘sqrt ((x0 - x1) pow 2) = x0 - x1’
3017 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> Rewr' \\
3018 Q.PAT_X_ASSUM ‘x1 <= a’ MP_TAC \\
3019 REAL_ARITH_TAC) \\
3020 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3021 Know ‘x0 < 0 + x1’
3022 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3023 Know ‘x0 < a’
3024 >- (MATCH_MP_TAC REAL_LTE_TRANS \\
3025 Q.EXISTS_TAC ‘x1’ >> art []) >> DISCH_TAC \\
3026 Q.PAT_X_ASSUM ‘x0 IN interval (a,b)’
3027 (STRIP_ASSUME_TAC o (REWRITE_RULE [IN_INTERVAL])) \\
3028 PROVE_TAC [REAL_LT_ANTISYM],
3029 (* goal 2 (of 4) *)
3030 CCONTR_TAC >> fs [GSYM real_lte] \\
3031 Know ‘dist mr2 ((x0,y0),(x1,y0)) <= dist mr2 ((x0,y0),(x1,y1))’
3032 >- (rw [MR2_DEF] \\
3033 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3034 Know ‘dist mr2 ((x0,y0),(x1,y0)) < dx’
3035 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3036 Q.EXISTS_TAC ‘dist mr2 ((x0,y0),(x1,y1))’ >> art []) \\
3037 rw [Abbr ‘dx’, REAL_LT_MIN, MR2_DEF] \\
3038 DISJ2_TAC >> rw [GSYM real_lte] \\
3039 ONCE_REWRITE_TAC [POW_2_SUB] \\
3040 Cases_on ‘0 <= x1 - x0’
3041 >- (Know ‘sqrt ((x1 - x0) pow 2) = x1 - x0’
3042 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> Rewr' \\
3043 ASM_REWRITE_TAC [REAL_LE_SUB_CANCEL2]) \\
3044 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3045 Know ‘x1 < 0 + x0’
3046 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3047 Know ‘b < x0’
3048 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3049 Q.EXISTS_TAC ‘x1’ >> art []) >> DISCH_TAC \\
3050 Q.PAT_X_ASSUM ‘x0 IN interval (a,b)’
3051 (STRIP_ASSUME_TAC o (REWRITE_RULE [IN_INTERVAL])) \\
3052 PROVE_TAC [REAL_LT_ANTISYM],
3053 (* goal 3 (of 4) *)
3054 CCONTR_TAC >> fs [GSYM real_lte] \\
3055 Know ‘dist mr2 ((x0,y0),(x0,y1)) <= dist mr2 ((x0,y0),(x1,y1))’
3056 >- (rw [MR2_DEF] \\
3057 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3058 Know ‘dist mr2 ((x0,y0),(x0,y1)) < dy’
3059 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3060 Q.EXISTS_TAC ‘dist mr2 ((x0,y0),(x1,y1))’ >> art []) \\
3061 rw [Abbr ‘dy’, REAL_LT_MIN, MR2_DEF] \\
3062 DISJ1_TAC >> rw [GSYM real_lte] \\
3063 Cases_on ‘0 <= y0 - y1’
3064 >- (Know ‘sqrt ((y0 - y1) pow 2) = y0 - y1’
3065 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> Rewr' \\
3066 Q.PAT_X_ASSUM ‘y1 <= c’ MP_TAC \\
3067 REAL_ARITH_TAC) \\
3068 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3069 Know ‘y0 < 0 + y1’
3070 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3071 Know ‘y0 < c’
3072 >- (MATCH_MP_TAC REAL_LTE_TRANS \\
3073 Q.EXISTS_TAC ‘y1’ >> art []) >> DISCH_TAC \\
3074 Q.PAT_X_ASSUM ‘y0 IN interval (c,d)’
3075 (STRIP_ASSUME_TAC o (REWRITE_RULE [IN_INTERVAL])) \\
3076 PROVE_TAC [REAL_LT_ANTISYM],
3077 (* goal 4 (of 4) *)
3078 CCONTR_TAC >> fs [GSYM real_lte] \\
3079 Know ‘dist mr2 ((x0,y0),(x0,y1)) <= dist mr2 ((x0,y0),(x1,y1))’
3080 >- (rw [MR2_DEF] \\
3081 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3082 Know ‘dist mr2 ((x0,y0),(x0,y1)) < dy’
3083 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3084 Q.EXISTS_TAC ‘dist mr2 ((x0,y0),(x1,y1))’ >> art []) \\
3085 rw [Abbr ‘dy’, REAL_LT_MIN, MR2_DEF] \\
3086 DISJ2_TAC >> rw [GSYM real_lte] \\
3087 ONCE_REWRITE_TAC [POW_2_SUB] \\
3088 Cases_on ‘0 <= y1 - y0’
3089 >- (Know ‘sqrt ((y1 - y0) pow 2) = y1 - y0’
3090 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> Rewr' \\
3091 ASM_REWRITE_TAC [REAL_LE_SUB_CANCEL2]) \\
3092 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3093 Know ‘y1 < 0 + y0’
3094 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3095 Know ‘d < y0’
3096 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3097 Q.EXISTS_TAC ‘y1’ >> art []) >> DISCH_TAC \\
3098 Q.PAT_X_ASSUM ‘y0 IN interval (c,d)’
3099 (STRIP_ASSUME_TAC o (REWRITE_RULE [IN_INTERVAL])) \\
3100 PROVE_TAC [REAL_LT_ANTISYM] ]
3101QED
3102
3103Theorem borel_2d_lemma3[local] :
3104 sigma UNIV {s | open_in (mtop mr2) s} =
3105 sigma UNIV {J | ?a b c d. a IN q_set /\ b IN q_set /\ c IN q_set /\ d IN q_set /\
3106 J = OPEN_interval (a,b) CROSS OPEN_interval (c,d)}
3107Proof
3108 Q.ABBREV_TAC ‘S1 = sigma UNIV {s | open_in (mtop mr2) s}’
3109 >> Q.ABBREV_TAC
3110 ‘S3 = sigma UNIV
3111 {J | ?a b c d. a IN q_set /\ b IN q_set /\ c IN q_set /\ d IN q_set /\
3112 J = OPEN_interval (a,b) CROSS OPEN_interval (c,d)}’
3113 >> Suff ‘subsets S1 = subsets S3’ >- METIS_TAC [SIGMA_CONG]
3114 >> MATCH_MP_TAC SUBSET_ANTISYM
3115 >> reverse CONJ_TAC
3116 >- (qunabbrevl_tac [‘S1’, ‘S3’] \\
3117 MATCH_MP_TAC SIGMA_MONOTONE \\
3118 rw [Once SUBSET_DEF] \\
3119 REWRITE_TAC [box_open_in_mr2])
3120 (* subsets S1 SUBSET subsets S3 *)
3121 >> Q.UNABBREV_TAC ‘S1’
3122 >> ‘univ(:real # real) = space S3’ by METIS_TAC [SPACE_SIGMA] >> POP_ORW
3123 >> MATCH_MP_TAC SIGMA_SUBSET
3124 >> Know ‘sigma_algebra S3’
3125 >- (Q.UNABBREV_TAC ‘S3’ \\
3126 MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> rw [subset_class_def])
3127 >> rw [SUBSET_DEF]
3128 >> POP_ASSUM (ONCE_REWRITE_TAC o wrap o (MATCH_MP borel_2d_lemma1))
3129 >> MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION >> art [borel_2d_lemma2]
3130 >> MATCH_MP_TAC SUBSET_TRANS
3131 >> Q.EXISTS_TAC
3132 ‘{J | ?a b c d. a IN q_set /\ b IN q_set /\ c IN q_set /\ d IN q_set /\
3133 J = OPEN_interval (a,b) CROSS OPEN_interval (c,d)}’
3134 >> reverse CONJ_TAC >- rw [Abbr ‘S3’, SIGMA_SUBSET_SUBSETS]
3135 >> rw [SUBSET_DEF]
3136 >> qexistsl_tac [‘a’, ‘b’, ‘c’, ‘d’] >> rw []
3137QED
3138
3139(* now rationals are all removed *)
3140Theorem borel_2d_lemma4[local] :
3141 sigma UNIV {s | open_in (mtop mr2) s} =
3142 sigma UNIV {J | ?a b c d. J = OPEN_interval (a,b) CROSS OPEN_interval (c,d)}
3143Proof
3144 Q.ABBREV_TAC ‘S1 = sigma UNIV {s | open_in (mtop mr2) s}’
3145 >> Q.ABBREV_TAC
3146 ‘S2 = sigma UNIV {J | ?a b c d. J = OPEN_interval (a,b) CROSS OPEN_interval (c,d)}’
3147 >> Q.ABBREV_TAC
3148 ‘S3 = sigma UNIV
3149 {J | ?a b c d. a IN q_set /\ b IN q_set /\ c IN q_set /\ d IN q_set /\
3150 J = OPEN_interval (a,b) CROSS OPEN_interval (c,d)}’
3151 >> Suff ‘subsets S1 = subsets S2’ >- METIS_TAC [SIGMA_CONG]
3152 >> MATCH_MP_TAC SUBSET_ANTISYM
3153 >> reverse CONJ_TAC
3154 >- (qunabbrevl_tac [‘S1’, ‘S2’] \\
3155 MATCH_MP_TAC SIGMA_MONOTONE \\
3156 rw [Once SUBSET_DEF] \\
3157 REWRITE_TAC [box_open_in_mr2])
3158 >> MATCH_MP_TAC SUBSET_TRANS
3159 >> Q.EXISTS_TAC ‘subsets S3’
3160 >> reverse CONJ_TAC
3161 >- (qunabbrevl_tac [‘S2’, ‘S3’] \\
3162 MATCH_MP_TAC SIGMA_MONOTONE \\
3163 rw [Once SUBSET_DEF] \\
3164 qexistsl_tac [‘a’, ‘b’, ‘c’, ‘d’] >> REWRITE_TAC [])
3165 >> ‘S1 = S3’ by METIS_TAC [borel_2d_lemma3] >> POP_ORW
3166 >> qunabbrevl_tac [‘S2’, ‘S3’]
3167 >> MATCH_MP_TAC SIGMA_MONOTONE
3168 >> rw [Once SUBSET_DEF]
3169 >> qexistsl_tac [‘a’, ‘b’, ‘c’, ‘d’] >> REWRITE_TAC []
3170QED
3171
3172Theorem sigma_algebra_borel_2d :
3173 sigma_algebra (borel CROSS borel)
3174Proof
3175 MATCH_MP_TAC SIGMA_ALGEBRA_PROD_SIGMA
3176 >> rw [subset_class_def, space_borel]
3177QED
3178
3179(* 2D borel sets can be also generated by open sets in MR2 *)
3180Theorem borel_2d :
3181 borel CROSS borel = sigma UNIV {s | open_in (mtop mr2) s}
3182Proof
3183 Suff ‘subsets (borel CROSS borel) =
3184 subsets (sigma UNIV {s | open_in (mtop mr2) s})’
3185 >- (rw [prod_sigma_def, SPACE_SIGMA, GSYM CROSS_UNIV, space_borel] \\
3186 MATCH_MP_TAC SIGMA_CONG >> art [])
3187 >> MATCH_MP_TAC SUBSET_ANTISYM
3188 >> reverse CONJ_TAC
3189 >- (rw [borel_2d_lemma4] \\
3190 Know ‘univ(:real # real) = space (borel CROSS borel)’
3191 >- (rw [SPACE_PROD_SIGMA, CROSS_UNIV, space_borel]) >> Rewr' \\
3192 MATCH_MP_TAC SIGMA_SUBSET \\
3193 REWRITE_TAC [sigma_algebra_borel_2d, prod_sigma_def] \\
3194 MATCH_MP_TAC SUBSET_TRANS \\
3195 Q.EXISTS_TAC ‘prod_sets (subsets borel) (subsets borel)’ \\
3196 REWRITE_TAC [SIGMA_SUBSET_SUBSETS] \\
3197 rw [SUBSET_DEF, IN_PROD_SETS] \\
3198 qexistsl_tac [‘interval (a,b)’, ‘interval (c,d)’] \\
3199 rw [OPEN_interval, borel_measurable_sets_gr_less])
3200 (* applying prod_sigma_alt_sigma_functions *)
3201 >> Know ‘borel CROSS borel =
3202 sigma (space borel CROSS space borel)
3203 (binary borel borel) (binary FST SND) {0; 1}’
3204 >- (MATCH_MP_TAC prod_sigma_alt_sigma_functions \\
3205 REWRITE_TAC [sigma_algebra_borel])
3206 >> Rewr'
3207 >> rw [sigma_functions_def, binary_def, space_borel, GSYM CROSS_UNIV]
3208 >> Q.ABBREV_TAC ‘B = sigma univ(:real # real) {s | open_in (mtop mr2) s}’
3209 >> ‘univ(:real # real) = space B’ by PROVE_TAC [SPACE_SIGMA] >> POP_ORW
3210 >> MATCH_MP_TAC SIGMA_SUBSET
3211 >> Q.UNABBREV_TAC ‘B’
3212 >> CONJ_TAC
3213 >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA \\
3214 rw [subset_class_def])
3215 >> rw [SUBSET_DEF] >> rename1 ‘s IN subsets borel’
3216 >| [ (* goal 1 (of 2) *)
3217 Suff ‘IMAGE (\s. PREIMAGE FST s) (subsets borel) SUBSET
3218 subsets (sigma univ(:real # real) {s | open_in (mtop mr2) s})’
3219 >- (rw [SUBSET_DEF] >> POP_ASSUM MATCH_MP_TAC \\
3220 Q.EXISTS_TAC ‘s’ >> art []) \\
3221 KILL_TAC \\
3222 REWRITE_TAC [borel_eq_gr_less] \\
3223 Q.ABBREV_TAC ‘sts = IMAGE (\(a,b). {x | a < x /\ x < b}) univ(:real # real)’ \\
3224 Q.ABBREV_TAC ‘Z = univ(:real # real)’ \\
3225 Know ‘IMAGE (\s. PREIMAGE FST s INTER Z) (subsets (sigma UNIV sts)) =
3226 subsets (sigma Z (IMAGE (\s. PREIMAGE FST s INTER Z) sts))’
3227 >- (MATCH_MP_TAC PREIMAGE_SIGMA >> rw [subset_class_def, IN_FUNSET]) \\
3228 simp [Abbr ‘Z’] >> Rewr' \\
3229 Q.ABBREV_TAC ‘B = sigma univ(:real # real) {s | open_in (mtop mr2) s}’ \\
3230 ‘univ(:real # real) = space B’ by PROVE_TAC [SPACE_SIGMA] >> POP_ORW \\
3231 MATCH_MP_TAC SIGMA_SUBSET \\
3232 Q.UNABBREV_TAC ‘B’ \\
3233 CONJ_TAC >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> rw [subset_class_def]) \\
3234 MATCH_MP_TAC SUBSET_TRANS \\
3235 Q.EXISTS_TAC ‘{s | open_in (mtop mr2) s}’ >> rw [SIGMA_SUBSET_SUBSETS] \\
3236 simp [Abbr ‘sts’, SUBSET_DEF] \\
3237 Q.X_GEN_TAC ‘y’ >> rw [] \\
3238 Cases_on ‘x’ >> simp [] \\
3239 Know ‘PREIMAGE FST {x | q < x /\ x < r} = {x | q < x /\ x < r} CROSS univ(:real)’
3240 >- (rw [Once EXTENSION, IN_PREIMAGE, IN_CROSS]) >> Rewr' \\
3241 rw [MTOP_OPEN] \\
3242 Cases_on ‘x’ >> rename1 ‘q < FST (x,y)’ >> fs [] \\
3243 Q.ABBREV_TAC ‘dx = min (x - q) (r - x)’ \\
3244 Q.EXISTS_TAC ‘dx’ \\
3245 CONJ_TAC >- (rw [Abbr ‘dx’, REAL_LT_MIN, REAL_SUB_LT]) \\
3246 Q.X_GEN_TAC ‘z’ >> Cases_on ‘z’ >> simp [] \\
3247 DISCH_TAC >> rename1 ‘dist mr2 ((x0,y0),(x1,y1)) < dx’ \\
3248 Know ‘dist mr2 ((x0,y0),(x1,y0)) <= dist mr2 ((x0,y0),(x1,y1))’
3249 >- (rw [MR2_DEF] \\
3250 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3251 Know ‘dist mr2 ((x0,y0),(x1,y0)) < dx’
3252 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3253 Q.EXISTS_TAC ‘dist mr2 ((x0,y0),(x1,y1))’ >> art []) \\
3254 rw [Abbr ‘dx’, REAL_LT_MIN, MR2_DEF] >| (* 2 subgoals *)
3255 [ (* goal 1.1 (of 2) *)
3256 Cases_on ‘0 <= x0 - x1’
3257 >- (Know ‘sqrt ((x0 - x1) pow 2) = x0 - x1’
3258 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> DISCH_THEN (fs o wrap) \\
3259 Q.PAT_X_ASSUM ‘x0 - x1 < x0 - q’ MP_TAC \\
3260 REAL_ARITH_TAC) \\
3261 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3262 Know ‘x0 < 0 + x1’
3263 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3264 MATCH_MP_TAC REAL_LT_TRANS \\
3265 Q.EXISTS_TAC ‘x0’ >> art [],
3266 (* goal 1.2 (of 2) *)
3267 ‘sqrt ((x1 - x0) pow 2) < r - x0’ by PROVE_TAC [POW_2_SUB] \\
3268 Cases_on ‘0 <= x1 - x0’
3269 >- (Know ‘sqrt ((x1 - x0) pow 2) = x1 - x0’
3270 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> DISCH_THEN (fs o wrap) \\
3271 Q.PAT_X_ASSUM ‘x1 - x0 < r - x0’ MP_TAC \\
3272 REAL_ARITH_TAC) \\
3273 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3274 Know ‘x1 < 0 + x0’
3275 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3276 MATCH_MP_TAC REAL_LT_TRANS \\
3277 Q.EXISTS_TAC ‘x0’ >> art [] ],
3278 (* goal 2 (of 2) *)
3279 Suff ‘IMAGE (\s. PREIMAGE SND s) (subsets borel) SUBSET
3280 subsets (sigma univ(:real # real) {s | open_in (mtop mr2) s})’
3281 >- (rw [SUBSET_DEF] >> POP_ASSUM MATCH_MP_TAC \\
3282 Q.EXISTS_TAC ‘s’ >> art []) \\
3283 KILL_TAC \\
3284 REWRITE_TAC [borel_eq_gr_less] \\
3285 Q.ABBREV_TAC ‘sts = IMAGE (\(a,b). {x | a < x /\ x < b}) univ(:real # real)’ \\
3286 Q.ABBREV_TAC ‘Z = univ(:real # real)’ \\
3287 Know ‘IMAGE (\s. PREIMAGE SND s INTER Z) (subsets (sigma UNIV sts)) =
3288 subsets (sigma Z (IMAGE (\s. PREIMAGE SND s INTER Z) sts))’
3289 >- (MATCH_MP_TAC PREIMAGE_SIGMA >> rw [subset_class_def, IN_FUNSET]) \\
3290 simp [Abbr ‘Z’] >> Rewr' \\
3291 Q.ABBREV_TAC ‘B = sigma univ(:real # real) {s | open_in (mtop mr2) s}’ \\
3292 ‘univ(:real # real) = space B’ by PROVE_TAC [SPACE_SIGMA] >> POP_ORW \\
3293 MATCH_MP_TAC SIGMA_SUBSET \\
3294 Q.UNABBREV_TAC ‘B’ \\
3295 CONJ_TAC >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> rw [subset_class_def]) \\
3296 MATCH_MP_TAC SUBSET_TRANS \\
3297 Q.EXISTS_TAC ‘{s | open_in (mtop mr2) s}’ >> rw [SIGMA_SUBSET_SUBSETS] \\
3298 simp [Abbr ‘sts’, SUBSET_DEF] \\
3299 Q.X_GEN_TAC ‘y’ >> rw [] \\
3300 Cases_on ‘x’ >> simp [] \\
3301 Know ‘PREIMAGE SND {x | q < x /\ x < r} =
3302 univ(:real) CROSS {x | q < x /\ x < r}’
3303 >- (rw [Once EXTENSION, IN_PREIMAGE, IN_CROSS]) >> Rewr' \\
3304 rw [MTOP_OPEN] \\
3305 Cases_on ‘x’ >> rename1 ‘q < SND (x,y)’ >> fs [] \\
3306 Q.ABBREV_TAC ‘dy = min (y - q) (r - y)’ \\
3307 Q.EXISTS_TAC ‘dy’ \\
3308 CONJ_TAC >- (rw [Abbr ‘dy’, REAL_LT_MIN, REAL_SUB_LT]) \\
3309 Q.X_GEN_TAC ‘z’ >> Cases_on ‘z’ >> simp [] \\
3310 DISCH_TAC >> rename1 ‘dist mr2 ((x0,y0),(x1,y1)) < dy’ \\
3311 Know ‘dist mr2 ((x0,y0),(x0,y1)) <= dist mr2 ((x0,y0),(x1,y1))’
3312 >- (rw [MR2_DEF] \\
3313 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3314 Know ‘dist mr2 ((x0,y0),(x0,y1)) < dy’
3315 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3316 Q.EXISTS_TAC ‘dist mr2 ((x0,y0),(x1,y1))’ >> art []) \\
3317 rw [Abbr ‘dy’, REAL_LT_MIN, MR2_DEF] >| (* 2 subgoals *)
3318 [ (* goal 2.1 (of 2) *)
3319 Cases_on ‘0 <= y0 - y1’
3320 >- (Know ‘sqrt ((y0 - y1) pow 2) = y0 - y1’
3321 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> DISCH_THEN (fs o wrap) \\
3322 Q.PAT_X_ASSUM ‘y0 - y1 < y0 - q’ MP_TAC \\
3323 REAL_ARITH_TAC) \\
3324 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3325 Know ‘y0 < 0 + y1’
3326 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3327 MATCH_MP_TAC REAL_LT_TRANS \\
3328 Q.EXISTS_TAC ‘y0’ >> art [],
3329 (* goal 2.2 (of 2) *)
3330 ‘sqrt ((y1 - y0) pow 2) < r - y0’ by PROVE_TAC [POW_2_SUB] \\
3331 Cases_on ‘0 <= y1 - y0’
3332 >- (Know ‘sqrt ((y1 - y0) pow 2) = y1 - y0’
3333 >- (MATCH_MP_TAC POW_2_SQRT >> art []) >> DISCH_THEN (fs o wrap) \\
3334 Q.PAT_X_ASSUM ‘y1 - y0 < r - y0’ MP_TAC \\
3335 REAL_ARITH_TAC) \\
3336 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [real_lte])) \\
3337 Know ‘y1 < 0 + y0’
3338 >- (rw [GSYM REAL_LT_SUB_RADD]) >> rw [] \\
3339 MATCH_MP_TAC REAL_LT_TRANS \\
3340 Q.EXISTS_TAC ‘y0’ >> art [] ] ]
3341QED
3342
3343Theorem borel_2d_alt_box :
3344 borel CROSS borel = sigma UNIV {(box a b) CROSS (box c d) | T}
3345Proof
3346 REWRITE_TAC [borel_2d, borel_2d_lemma4]
3347 >> Suff ‘{J | (?a b c d. J = interval (a,b) CROSS interval (c,d))} =
3348 {box a b CROSS box c d | T}’ >- Rewr
3349 >> rw [Once EXTENSION, box_alt]
3350QED
3351
3352Theorem space_borel_2d :
3353 space (borel CROSS borel) = UNIV
3354Proof
3355 REWRITE_TAC [borel_2d_alt_box, SPACE_SIGMA]
3356QED
3357
3358(* Hyperbola area is a open set, needed by IN_MEASURABLE_BOREL_2D_MUL *)
3359Theorem hyperbola_lemma1[local] :
3360 !q r. 0 < q /\ 0 < r ==>
3361 ?e. 0 < e /\
3362 !y. dist mr2 ((q,r),y) < e ==>
3363 ?x. (y,T) = (\(x,y). ((x,y),0 < x * y)) x
3364Proof
3365 rpt STRIP_TAC
3366 >> Q.EXISTS_TAC ‘min q r’
3367 >> simp [REAL_LT_MIN]
3368 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’ >> rw [MR2_DEF]
3369 >> Q.EXISTS_TAC ‘(q',r')’ >> simp []
3370 >> MATCH_MP_TAC REAL_LT_MUL
3371 >> CCONTR_TAC >> fs [GSYM real_lte] (* 2 subgoals *)
3372 >| [ (* goal 1 (of 2) *)
3373 Know ‘q <= q - q'’
3374 >- (REWRITE_TAC [REAL_LE_SUB_LADD] \\
3375 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites
3376 [GSYM REAL_ADD_RID] \\
3377 ASM_REWRITE_TAC [REAL_LE_LADD]) >> DISCH_TAC \\
3378 Know ‘q pow 2 <= (q - q') pow 2’
3379 >- (MATCH_MP_TAC POW_LE >> art [] \\
3380 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3381 Know ‘q pow 2 <= (q - q') pow 2 + (r - r') pow 2’
3382 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3383 Q.EXISTS_TAC ‘(q - q') pow 2’ >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3384 Know ‘sqrt (q pow 2) <= sqrt ((q - q') pow 2 + (r - r') pow 2)’
3385 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3386 Know ‘sqrt (q pow 2) = q’
3387 >- (MATCH_MP_TAC POW_2_SQRT \\
3388 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3389 DISCH_THEN (PURE_ASM_REWRITE_TAC o wrap) >> DISCH_TAC \\
3390 METIS_TAC [REAL_LTE_ANTISYM],
3391 (* goal 2 (of 2) *)
3392 Know ‘r <= r - r'’
3393 >- (REWRITE_TAC [REAL_LE_SUB_LADD] \\
3394 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites
3395 [GSYM REAL_ADD_RID] \\
3396 ASM_REWRITE_TAC [REAL_LE_LADD]) >> DISCH_TAC \\
3397 Know ‘r pow 2 <= (r - r') pow 2’
3398 >- (MATCH_MP_TAC POW_LE >> art [] \\
3399 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3400 Know ‘r pow 2 <= (q - q') pow 2 + (r - r') pow 2’
3401 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3402 Q.EXISTS_TAC ‘(r - r') pow 2’ >> rw [REAL_LE_POW2]) >> DISCH_TAC \\
3403 Know ‘sqrt (r pow 2) <= sqrt ((q - q') pow 2 + (r - r') pow 2)’
3404 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3405 Know ‘sqrt (r pow 2) = r’
3406 >- (MATCH_MP_TAC POW_2_SQRT \\
3407 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3408 DISCH_THEN (PURE_ASM_REWRITE_TAC o wrap) >> DISCH_TAC \\
3409 METIS_TAC [REAL_LTE_ANTISYM] ]
3410QED
3411
3412Theorem hyperbola_lemma2[local] :
3413 !q r. q < 0 /\ r < 0 ==>
3414 ?e. 0 < e /\
3415 !y. dist mr2 ((q,r),y) < e ==>
3416 ?x. (y,T) = (\(x,y). ((x,y),0 < x * y)) x
3417Proof
3418 rpt STRIP_TAC
3419 >> MP_TAC (Q.SPECL [‘-q’, ‘-r’] hyperbola_lemma1)
3420 >> ‘0 < -q /\ 0 < -r’ by METIS_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG]
3421 >> RW_TAC std_ss []
3422 >> Q.EXISTS_TAC ‘e’ >> art []
3423 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’
3424 >> STRIP_TAC
3425 >> rename1 ‘dist mr2 ((x0,y0),(x1,y1)) < e’
3426 >> Q.PAT_X_ASSUM ‘!y. P ==> Q’ (MP_TAC o (Q.SPEC ‘(-x1,-y1)’))
3427 >> rw [MR2_MIRROR]
3428 >> Cases_on ‘x’ >> fs []
3429 >> Q.EXISTS_TAC ‘(x1,y1)’ >> rw []
3430 >> fs [REAL_NEG_MUL2]
3431QED
3432
3433Theorem hyperbola_lemma3[local] :
3434 !a q r. a < q * r /\ 0 < a /\ 0 < q /\ 0 < r ==>
3435 ?e. 0 < e /\
3436 !y. dist mr2 ((q,r),y) < e ==>
3437 ?x. (y,T) = (\(x,y). ((x,y),a < x * y)) x
3438Proof
3439 qx_genl_tac [‘R’, ‘X’, ‘Y’] >> STRIP_TAC
3440 >> ‘R <> 0 /\ X <> 0 /\ Y <> 0’ by PROVE_TAC [REAL_LT_IMP_NE]
3441 >> Q.ABBREV_TAC ‘A = X - R / Y’ (* horizontal distance to the curve *)
3442 >> Q.ABBREV_TAC ‘B = Y - R / X’ (* vertical distance to the curve *)
3443 >> ‘0 < A /\ 0 < B’ by rw [REAL_LT_SUB_LADD, Abbr ‘A’, Abbr ‘B’]
3444 (* applying jensen_pos_convex_SIGMA and pos_convex_inv *)
3445 >> MP_TAC (ISPEC “{(0 :num);1}” jensen_pos_convex_SIGMA)
3446 >> rw [FINITE_TWO]
3447 >> POP_ASSUM (MP_TAC o (Q.SPECL [‘inv’,
3448 ‘binary (1 / 2) (1 / 2)’,
3449 ‘binary X (R / Y)’]))
3450 >> simp [binary_def, pos_convex_inv]
3451 >> ‘{1:num} DELETE 0 = {1}’ by rw [GSYM DELETE_NON_ELEMENT]
3452 >> DISCH_TAC
3453 >> Know ‘inv (SIGMA (\(x :num). 1 / 2 * if x = 0 then X else R / Y) {0; 1}) <=
3454 SIGMA (\(x :num). 1 / 2 * inv (if x = 0 then X else R / Y)) {0; 1}’
3455 >- (POP_ASSUM MATCH_MP_TAC \\
3456 rw [REAL_SUM_IMAGE_THM])
3457 >> POP_ASSUM K_TAC
3458 >> rw [REAL_SUM_IMAGE_THM]
3459 >> Q.PAT_X_ASSUM ‘{1} DELETE 0 = {1}’ K_TAC
3460 (* stage work *)
3461 >> Q.ABBREV_TAC ‘cx = 1 / 2 * X + 1 / 2 * (R * inv Y)’
3462 >> Q.ABBREV_TAC ‘cy = 1 / 2 * Y + 1 / 2 * (R * inv X)’
3463 >> Know ‘0 < cx /\ 0 < cy’
3464 >- (CONJ_TAC >> qunabbrevl_tac [‘cx’, ‘cy’] \\
3465 MATCH_MP_TAC REAL_LT_ADD \\
3466 CONJ_TAC >> MATCH_MP_TAC REAL_LT_MUL >> rw [])
3467 >> STRIP_TAC
3468 >> Know ‘R <= cx * cy’
3469 >- (Know ‘R <= cx * cy <=> R / cx <= cy’
3470 >- (REWRITE_TAC [Once REAL_MUL_COMM, Once EQ_SYM_EQ] \\
3471 MATCH_MP_TAC REAL_LE_LDIV_EQ >> art []) >> Rewr' \\
3472 REWRITE_TAC [real_div] \\
3473 Know ‘R * inv cx <= R * (1 / 2 * inv X + 1 / 2 * inv (R / Y))’
3474 >- (MATCH_MP_TAC REAL_LE_LMUL_IMP >> art [] \\
3475 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3476 Suff ‘cy = R * (1 / 2 * inv X + 1 / 2 * inv (R / Y))’
3477 >- (Rewr' >> art []) \\
3478 Q.UNABBREV_TAC ‘cy’ \\
3479 REWRITE_TAC [real_div, REAL_ADD_LDISTRIB, REAL_MUL_LID] \\
3480 rw [REAL_INV_MUL, REAL_INV_INV, Once REAL_ADD_COMM])
3481 >> DISCH_TAC
3482 (* now estimate e *)
3483 >> Q.EXISTS_TAC ‘min (A / 2) (B / 2)’
3484 >> CONJ_TAC >- rw [Abbr ‘A’, Abbr ‘B’, REAL_LT_MIN, REAL_SUB_LT]
3485 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’
3486 >> RW_TAC std_ss [REAL_LT_MIN, MR2_DEF]
3487 >> Q.EXISTS_TAC ‘(q,r)’ >> rw []
3488 >> Know ‘X - A / 2 < q’
3489 >- (REWRITE_TAC [REAL_LT_SUB_RADD, Once REAL_ADD_COMM] \\
3490 REWRITE_TAC [GSYM REAL_LT_SUB_RADD] \\
3491 Cases_on ‘X - q <= 0’ >- (MATCH_MP_TAC REAL_LET_TRANS \\
3492 Q.EXISTS_TAC ‘0’ >> rw []) \\
3493 FULL_SIMP_TAC std_ss [GSYM real_lt] \\
3494 CCONTR_TAC >> FULL_SIMP_TAC std_ss [GSYM real_lte] \\
3495 Suff ‘A / 2 <= sqrt ((X - q) pow 2 + (Y - r) pow 2)’
3496 >- METIS_TAC [REAL_LET_ANTISYM] \\
3497 MATCH_MP_TAC REAL_LE_TRANS \\
3498 Q.EXISTS_TAC ‘sqrt ((X - q) pow 2)’ \\
3499 CONJ_TAC >- (Suff ‘sqrt ((X - q) pow 2) = X - q’ >- (Rewr' >> art []) \\
3500 MATCH_MP_TAC POW_2_SQRT \\
3501 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3502 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2])
3503 >> DISCH_TAC
3504 >> Know ‘X - A / 2 < q’
3505 >- (REWRITE_TAC [REAL_LT_SUB_RADD, Once REAL_ADD_COMM] \\
3506 REWRITE_TAC [GSYM REAL_LT_SUB_RADD] \\
3507 Cases_on ‘X - q <= 0’ >- (MATCH_MP_TAC REAL_LET_TRANS \\
3508 Q.EXISTS_TAC ‘0’ >> rw []) \\
3509 FULL_SIMP_TAC std_ss [GSYM real_lt] \\
3510 CCONTR_TAC >> FULL_SIMP_TAC std_ss [GSYM real_lte] \\
3511 Suff ‘A / 2 <= sqrt ((X - q) pow 2 + (Y - r) pow 2)’
3512 >- METIS_TAC [REAL_LET_ANTISYM] \\
3513 MATCH_MP_TAC REAL_LE_TRANS \\
3514 Q.EXISTS_TAC ‘sqrt ((X - q) pow 2)’ \\
3515 CONJ_TAC >- (Suff ‘sqrt ((X - q) pow 2) = X - q’ >- (Rewr' >> art []) \\
3516 MATCH_MP_TAC POW_2_SQRT \\
3517 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3518 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2])
3519 >> DISCH_TAC
3520 >> Know ‘Y - B / 2 < r’
3521 >- (REWRITE_TAC [REAL_LT_SUB_RADD, Once REAL_ADD_COMM] \\
3522 REWRITE_TAC [GSYM REAL_LT_SUB_RADD] \\
3523 Cases_on ‘Y - r <= 0’ >- (MATCH_MP_TAC REAL_LET_TRANS \\
3524 Q.EXISTS_TAC ‘0’ >> rw []) \\
3525 FULL_SIMP_TAC std_ss [GSYM real_lt] \\
3526 CCONTR_TAC >> FULL_SIMP_TAC std_ss [GSYM real_lte] \\
3527 Suff ‘B / 2 <= sqrt ((X - q) pow 2 + (Y - r) pow 2)’
3528 >- METIS_TAC [REAL_LET_ANTISYM] \\
3529 MATCH_MP_TAC REAL_LE_TRANS \\
3530 Q.EXISTS_TAC ‘sqrt ((Y - r) pow 2)’ \\
3531 CONJ_TAC >- (Suff ‘sqrt ((Y - r) pow 2) = Y - r’ >- (Rewr' >> art []) \\
3532 MATCH_MP_TAC POW_2_SQRT \\
3533 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3534 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2])
3535 >> DISCH_TAC
3536 >> Q.PAT_X_ASSUM ‘sqrt _ < A / 2’ K_TAC
3537 >> Q.PAT_X_ASSUM ‘sqrt _ < B / 2’ K_TAC
3538 (* stage work *)
3539 >> Know ‘X - A / 2 = cx’
3540 >- (qunabbrevl_tac [‘cx’, ‘A’] \\
3541 SIMP_TAC real_ss [real_div, REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB, REAL_MUL_LID,
3542 REAL_ARITH “x - (y - z) = x - y + z”] \\
3543 Q.ABBREV_TAC ‘c = R * inv Y’ \\
3544 rw [REAL_SUB_LDISTRIB] >> REAL_ARITH_TAC)
3545 >> DISCH_THEN ((FULL_SIMP_TAC std_ss) o wrap)
3546 >> Know ‘Y - B / 2 = cy’
3547 >- (qunabbrevl_tac [‘cy’, ‘B’] \\
3548 SIMP_TAC real_ss [real_div, REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB, REAL_MUL_LID,
3549 REAL_ARITH “x - (y - z) = x - y + z”] \\
3550 Q.ABBREV_TAC ‘c = R * inv X’ \\
3551 rw [REAL_SUB_LDISTRIB] >> REAL_ARITH_TAC)
3552 >> DISCH_THEN ((FULL_SIMP_TAC std_ss) o wrap)
3553 >> MATCH_MP_TAC REAL_LET_TRANS
3554 >> Q.EXISTS_TAC ‘cx * cy’ >> art []
3555 >> MATCH_MP_TAC REAL_LT_MUL2 >> art []
3556 >> CONJ_TAC >> MATCH_MP_TAC REAL_LT_IMP_LE >> art []
3557QED
3558
3559Theorem hyperbola_lemma4[local] :
3560 !a q r. a < q * r /\ 0 < a /\ q < 0 /\ r < 0 ==>
3561 ?e. 0 < e /\
3562 !y. dist mr2 ((q,r),y) < e ==>
3563 ?x. (y,T) = (\(x,y). ((x,y),a < x * y)) x
3564Proof
3565 rpt STRIP_TAC
3566 >> MP_TAC (Q.SPECL [‘a’, ‘-q’, ‘-r’] hyperbola_lemma3)
3567 >> ‘0 < -q /\ 0 < -r’ by METIS_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG]
3568 >> RW_TAC std_ss [REAL_NEG_MUL2]
3569 >> Q.EXISTS_TAC ‘e’ >> art []
3570 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’
3571 >> STRIP_TAC
3572 >> rename1 ‘dist mr2 ((x0,y0),(x1,y1)) < e’
3573 >> Q.PAT_X_ASSUM ‘!y. P ==> Q’ (MP_TAC o (Q.SPEC ‘(-x1,-y1)’))
3574 >> rw [MR2_MIRROR]
3575 >> Cases_on ‘x’ >> fs []
3576 >> Q.EXISTS_TAC ‘(x1,y1)’ >> rw []
3577 >> fs [REAL_NEG_MUL2]
3578QED
3579
3580Theorem hyperbola_lemma5[local] :
3581 !a. a < 0 ==> ?e. 0 < e /\
3582 !y. dist mr2 ((0,0),y) < e ==>
3583 ?x. (y,T) = (\(x,y). ((x,y),a < x * y)) x
3584Proof
3585 rpt STRIP_TAC
3586 >> Q.EXISTS_TAC ‘sqrt (-(2 * a))’
3587 >> STRONG_CONJ_TAC
3588 >- (MATCH_MP_TAC SQRT_POS_LT >> art [GSYM REAL_NEG_LT0, REAL_NEG_NEG] \\
3589 ‘0 = 2 * 0’ by PROVE_TAC [REAL_MUL_RZERO] >> POP_ORW \\
3590 MATCH_MP_TAC REAL_LT_LMUL_IMP >> rw [])
3591 >> DISCH_TAC
3592 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’
3593 >> rename1 ‘dist mr2 ((0,0),(x,y)) < sqrt (-(2 * a))’
3594 >> rw [MR2_DEF]
3595 >> Q.EXISTS_TAC ‘(x,y)’ >> rw []
3596 >> Know ‘sqrt (x pow 2 + y pow 2) pow 2 < sqrt (-(2 * a)) pow 2’
3597 >- (MATCH_MP_TAC REAL_POW_LT2 >> rw [] \\
3598 MATCH_MP_TAC SQRT_POS_LE \\
3599 MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
3600 >> Know ‘sqrt (x pow 2 + y pow 2) pow 2 = x pow 2 + y pow 2’
3601 >- (MATCH_MP_TAC SQRT_POW_2 \\
3602 MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2]) >> Rewr'
3603 >> Know ‘sqrt (-(2 * a)) pow 2 = -(2 * a)’
3604 >- (MATCH_MP_TAC SQRT_POW_2 >> rw [REAL_NEG_GE0] \\
3605 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> Rewr'
3606 >> DISCH_TAC
3607 >> Know ‘0 <= (x + y) pow 2’ >- REWRITE_TAC [REAL_LE_POW2]
3608 >> REWRITE_TAC [ADD_POW_2, REAL_SUB_LZERO, Once (GSYM REAL_LE_SUB_RADD)]
3609 >> DISCH_TAC
3610 >> Know ‘-(2 * x * y) < -(2 * a)’ >- PROVE_TAC [REAL_LET_TRANS]
3611 >> rw []
3612QED
3613
3614Theorem REAL_LE_SUBR[local] :
3615 !x y. x <= x - y <=> y <= 0
3616Proof
3617 rw [REWRITE_RULE [GSYM real_sub] (Q.SPECL [‘r’, ‘-y1’] REAL_LE_ADDR)]
3618QED
3619
3620Theorem hyperbola_lemma6[local] :
3621 !a r. a < 0 /\ 0 < r (* q = 0 *) ==>
3622 ?e. 0 < e /\ !y. dist mr2 ((0,r),y) < e ==>
3623 ?x. (y,T) = (\(x,y). ((x,y),a < x * y)) x
3624Proof
3625 rpt STRIP_TAC
3626 >> ‘r <> 0’ by PROVE_TAC [REAL_LT_IMP_NE]
3627 >> ‘0 < -a’ by METIS_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG]
3628 >> Q.EXISTS_TAC ‘min ((1 / 2) * (-a / r)) r’
3629 >> CONJ_TAC >- rw [REAL_LT_MIN]
3630 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’
3631 >> rw [REAL_LT_MIN, MR2_DEF]
3632 >> rename1 ‘sqrt (x1 pow 2 + (r - y1) pow 2) < r’
3633 >> Q.EXISTS_TAC ‘(x1,y1)’ >> rw []
3634 >> STRIP_ASSUME_TAC (Q.SPECL [‘x1’, ‘0’] REAL_LT_TOTAL) (* 3 subgoals *)
3635 >| [ (* goal 1 (of 3): trivial *)
3636 rw [],
3637 (* goal 2 (of 3): hard *)
3638 Know ‘0 < y1’
3639 >- (CCONTR_TAC >> fs [GSYM real_lte] \\
3640 ‘r <= r - y1’ by PROVE_TAC [REAL_LE_SUBR] \\
3641 Know ‘r pow 2 <= x1 pow 2 + (r - y1) pow 2’
3642 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3643 Q.EXISTS_TAC ‘(r - y1) pow 2’ \\
3644 reverse CONJ_TAC >- rw [] \\
3645 MATCH_MP_TAC POW_LE >> rw [REAL_LE_SUBR] \\
3646 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3647 Know ‘sqrt (r pow 2) <= sqrt (x1 pow 2 + (r - y1) pow 2)’
3648 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3649 Know ‘sqrt (r pow 2) = r’
3650 >- (MATCH_MP_TAC POW_2_SQRT \\
3651 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3652 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3653 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM]) >> DISCH_TAC \\
3654 Suff ‘(1 / 2) * (a / r) < x1 /\ y1 < 2 * r’
3655 >- (STRIP_TAC \\
3656 ‘a < x1 * y1 <=> (~x1) * y1 < -a’ by rw [GSYM REAL_NEG_LMUL] >> POP_ORW \\
3657 ‘~a = (1 / 2 * (~a / r)) * (2 * r)’ by rw [] >> POP_ORW \\
3658 MATCH_MP_TAC REAL_LT_MUL2 >> rw [] >| (* 3 subgoals *)
3659 [ MATCH_MP_TAC REAL_LT_IMP_LE >> art [],
3660 MATCH_MP_TAC REAL_LT_IMP_LE >> art [],
3661 fs [GSYM REAL_NEG_LMUL] \\
3662 Know ‘a < 2 * (r * x1) <=> a * inv r < 2 * (r * x1) * inv r’
3663 >- (MATCH_MP_TAC (GSYM REAL_LT_RMUL) \\
3664 rw [REAL_LT_INV_EQ]) >> Rewr' \\
3665 Know ‘2 * (r * x1) * inv r = 2 * x1’ >- rw [] \\
3666 Rewr' >> art [] ]) \\
3667 CCONTR_TAC >> fs [GSYM real_lte] >| (* 2 subgoals *)
3668 [ (* goal 1 (of 2) *)
3669 Know ‘2 * r * ~x1 < -a’
3670 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3671 Q.EXISTS_TAC ‘2 * (r * sqrt (x1 pow 2 + (r - y1) pow 2))’ >> rw [] \\
3672 Know ‘-x1 = sqrt (-x1 pow 2)’
3673 >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
3674 MATCH_MP_TAC POW_2_SQRT \\
3675 REWRITE_TAC [GSYM REAL_NEG_LE0, REAL_NEG_NEG] \\
3676 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> Rewr' \\
3677 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3678 PURE_REWRITE_TAC [GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL, REAL_LT_NEG] \\
3679 Know ‘a < 2 * r * x1 <=> a * inv r < 2 * r * x1 * inv r’
3680 >- (MATCH_MP_TAC (GSYM REAL_LT_RMUL) >> rw [REAL_LT_INV_EQ]) \\
3681 DISCH_THEN (PURE_REWRITE_TAC o wrap) \\
3682 ‘2 * r * x1 * inv r = 2 * x1’ by rw [] \\
3683 POP_ASSUM (PURE_REWRITE_TAC o wrap) \\
3684 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM],
3685 (* goal 2 (of 2) *)
3686 ‘r <= y1 - r’ by rw [REAL_LE_SUB_LADD, REAL_DOUBLE] \\
3687 Know ‘r pow 2 <= (y1 - r) pow 2’
3688 >- (MATCH_MP_TAC POW_LE >> art [] \\
3689 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3690 Know ‘(y1 - r) pow 2 = (r - y1) pow 2’
3691 >- (‘y1 - r = -(r - y1)’ by REAL_ARITH_TAC >> POP_ORW \\
3692 rw []) \\
3693 DISCH_THEN (PURE_REWRITE_TAC o wrap) >> DISCH_TAC \\
3694 Know ‘r pow 2 <= x1 pow 2 + (r - y1) pow 2’
3695 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3696 Q.EXISTS_TAC ‘(r - y1) pow 2’ >> art [] \\
3697 rw [REAL_LE_ADDL, REAL_LE_POW2]) >> DISCH_TAC \\
3698 Know ‘sqrt (r pow 2) <= sqrt (x1 pow 2 + (r - y1) pow 2)’
3699 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3700 Know ‘sqrt (r pow 2) = r’
3701 >- (MATCH_MP_TAC POW_2_SQRT \\
3702 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3703 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3704 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM] ],
3705 (* goal 2 (of 3): easy *)
3706 Know ‘0 < y1’
3707 >- (CCONTR_TAC >> fs [GSYM real_lte] \\
3708 ‘r <= r - y1’ by PROVE_TAC [REAL_LE_SUBR] \\
3709 Know ‘r pow 2 <= x1 pow 2 + (r - y1) pow 2’
3710 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3711 Q.EXISTS_TAC ‘(r - y1) pow 2’ \\
3712 reverse CONJ_TAC >- rw [] \\
3713 MATCH_MP_TAC POW_LE >> rw [REAL_LE_SUBR] \\
3714 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3715 Know ‘sqrt (r pow 2) <= sqrt (x1 pow 2 + (r - y1) pow 2)’
3716 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3717 Know ‘sqrt (r pow 2) = r’
3718 >- (MATCH_MP_TAC POW_2_SQRT \\
3719 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3720 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3721 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM]) >> DISCH_TAC \\
3722 MATCH_MP_TAC REAL_LT_TRANS \\
3723 Q.EXISTS_TAC ‘0’ >> art [] \\
3724 MATCH_MP_TAC REAL_LT_MUL >> art [] ]
3725QED
3726
3727Theorem hyperbola_lemma7[local] :
3728 !a q. a < 0 /\ 0 < q (* r = 0 *) ==>
3729 ?e. 0 < e /\ !y. dist mr2 ((q,0),y) < e ==>
3730 ?x. (y,T) = (\(x,y). ((x,y),a < x * y)) x
3731Proof
3732 rpt STRIP_TAC
3733 >> ‘q <> 0’ by PROVE_TAC [REAL_LT_IMP_NE]
3734 >> ‘0 < -a’ by METIS_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG]
3735 >> Q.EXISTS_TAC ‘min ((1 / 2) * (-a / q)) q’
3736 >> CONJ_TAC >- rw [REAL_LT_MIN]
3737 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’
3738 >> rw [REAL_LT_MIN, MR2_DEF]
3739 >> rename1 ‘sqrt ((q - x1) pow 2 + y1 pow 2) < q’
3740 >> Q.EXISTS_TAC ‘(x1,y1)’ >> rw []
3741 >> STRIP_ASSUME_TAC (Q.SPECL [‘y1’, ‘0’] REAL_LT_TOTAL) (* 3 subgoals *)
3742 >| [ (* goal 1 (of 3): trivial *)
3743 rw [],
3744 (* goal 2 (of 3): hard *)
3745 Know ‘0 < x1’
3746 >- (CCONTR_TAC >> fs [GSYM real_lte] \\
3747 ‘q <= q - x1’ by PROVE_TAC [REAL_LE_SUBR] \\
3748 Know ‘q pow 2 <= (q - x1) pow 2 + y1 pow 2’
3749 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3750 Q.EXISTS_TAC ‘(q - x1) pow 2’ \\
3751 reverse CONJ_TAC >- rw [] \\
3752 MATCH_MP_TAC POW_LE >> rw [REAL_LE_SUBR] \\
3753 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3754 Know ‘sqrt (q pow 2) <= sqrt ((q - x1) pow 2 + y1 pow 2)’
3755 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3756 Know ‘sqrt (q pow 2) = q’
3757 >- (MATCH_MP_TAC POW_2_SQRT \\
3758 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3759 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3760 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM]) >> DISCH_TAC \\
3761 Suff ‘(1 / 2) * (a / q) < y1 /\ x1 < 2 * q’
3762 >- (STRIP_TAC \\
3763 ‘a < x1 * y1 <=> x1 * ~y1 < -a’ by rw [GSYM REAL_NEG_LMUL] >> POP_ORW \\
3764 ‘~a = (2 * q) * (1 / 2 * (~a / q))’ by rw [] >> POP_ORW \\
3765 MATCH_MP_TAC REAL_LT_MUL2 >> rw [] >| (* 3 subgoals *)
3766 [ MATCH_MP_TAC REAL_LT_IMP_LE >> art [],
3767 MATCH_MP_TAC REAL_LT_IMP_LE >> art [],
3768 fs [GSYM REAL_NEG_LMUL, REAL_LT_NEG] \\
3769 Know ‘a < 2 * (q * y1) <=> a * inv q < 2 * (q * y1) * inv q’
3770 >- (MATCH_MP_TAC (GSYM REAL_LT_RMUL) \\
3771 rw [REAL_LT_INV_EQ]) >> Rewr' \\
3772 Know ‘2 * (q * y1) * inv q = 2 * y1’ >- rw [] \\
3773 Rewr' >> art [] ]) \\
3774 CCONTR_TAC >> fs [GSYM real_lte] >| (* 2 subgoals *)
3775 [ (* goal 1 (of 2) *)
3776 Know ‘2 * q * ~y1 < -a’
3777 >- (MATCH_MP_TAC REAL_LET_TRANS \\
3778 Q.EXISTS_TAC ‘2 * (q * sqrt ((q - x1) pow 2 + y1 pow 2))’ >> rw [] \\
3779 Know ‘-y1 = sqrt (-y1 pow 2)’
3780 >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
3781 MATCH_MP_TAC POW_2_SQRT \\
3782 REWRITE_TAC [GSYM REAL_NEG_LE0, REAL_NEG_NEG] \\
3783 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> Rewr' \\
3784 MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3785 PURE_REWRITE_TAC [GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL, REAL_LT_NEG] \\
3786 Know ‘a < 2 * q * y1 <=> a * inv q < 2 * q * y1 * inv q’
3787 >- (MATCH_MP_TAC (GSYM REAL_LT_RMUL) \\
3788 rw [REAL_LT_INV_EQ]) \\
3789 DISCH_THEN (PURE_REWRITE_TAC o wrap) \\
3790 ‘2 * q * y1 * inv q = 2 * y1’ by rw [] \\
3791 POP_ASSUM (PURE_REWRITE_TAC o wrap) \\
3792 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM],
3793 (* goal 2 (of 2) *)
3794 ‘q <= x1 - q’ by rw [REAL_LE_SUB_LADD, REAL_DOUBLE] \\
3795 Know ‘q pow 2 <= (x1 - q) pow 2’
3796 >- (MATCH_MP_TAC POW_LE >> art [] \\
3797 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3798 Know ‘(x1 - q) pow 2 = (q - x1) pow 2’
3799 >- (‘x1 - q = -(q - x1)’ by REAL_ARITH_TAC >> POP_ORW \\
3800 rw []) \\
3801 DISCH_THEN (PURE_REWRITE_TAC o wrap) >> DISCH_TAC \\
3802 Know ‘q pow 2 <= (q - x1) pow 2 + y1 pow 2’
3803 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3804 Q.EXISTS_TAC ‘(q - x1) pow 2’ >> art [] \\
3805 rw [REAL_LE_ADDR, REAL_LE_POW2]) >> DISCH_TAC \\
3806 Know ‘sqrt (q pow 2) <= sqrt ((q - x1) pow 2 + y1 pow 2)’
3807 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3808 Know ‘sqrt (q pow 2) = q’
3809 >- (MATCH_MP_TAC POW_2_SQRT \\
3810 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3811 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3812 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM] ],
3813 (* goal 2 (of 3): easy *)
3814 Know ‘0 < x1’
3815 >- (CCONTR_TAC >> fs [GSYM real_lte] \\
3816 ‘q <= q - x1’ by PROVE_TAC [REAL_LE_SUBR] \\
3817 Know ‘q pow 2 <= (q - x1) pow 2 + y1 pow 2’
3818 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3819 Q.EXISTS_TAC ‘(q - x1) pow 2’ \\
3820 reverse CONJ_TAC >- rw [] \\
3821 MATCH_MP_TAC POW_LE >> rw [REAL_LE_SUBR] \\
3822 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3823 Know ‘sqrt (q pow 2) <= sqrt ((q - x1) pow 2 + y1 pow 2)’
3824 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3825 Know ‘sqrt (q pow 2) = q’
3826 >- (MATCH_MP_TAC POW_2_SQRT \\
3827 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3828 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3829 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM]) >> DISCH_TAC \\
3830 MATCH_MP_TAC REAL_LT_TRANS \\
3831 Q.EXISTS_TAC ‘0’ >> art [] \\
3832 MATCH_MP_TAC REAL_LT_MUL >> art [] ]
3833QED
3834
3835Theorem hyperbola_lemma8[local] :
3836 !a q r. a < 0 /\ a < q * r /\ q < 0 /\ 0 < r ==>
3837 ?e. 0 < e /\
3838 !y. dist mr2 ((q,r),y) < e ==>
3839 ?x. (y,T) = (\(x,y). ((x,y),a < x * y)) x
3840Proof
3841 rpt STRIP_TAC
3842 >> ‘q <> 0 /\ r <> 0’ by PROVE_TAC [REAL_LT_IMP_NE]
3843 >> ‘0 < -a’ by METIS_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG]
3844 >> Know ‘a / r < q’
3845 >- (Know ‘a / r < q <=> a / r * r < q * r’
3846 >- (MATCH_MP_TAC (GSYM REAL_LT_RMUL) >> art []) >> Rewr' \\
3847 Suff ‘a / r * r = a’ >- rw [] \\
3848 MATCH_MP_TAC REAL_DIV_RMUL >> art [])
3849 >> DISCH_TAC
3850 >> MP_TAC (Q.SPECL [‘a / r’, ‘q’] REAL_MEAN)
3851 >> RW_TAC std_ss []
3852 >> ‘z < 0’ by PROVE_TAC [REAL_LT_TRANS]
3853 >> ‘z <> 0’ by PROVE_TAC [REAL_LT_IMP_NE]
3854 >> Q.EXISTS_TAC ‘min (min (q - z) (a / z - r)) (min (-q) r)’
3855 >> simp [REAL_LT_MIN, REAL_SUB_LT]
3856 >> STRONG_CONJ_TAC (* a < r * z *)
3857 >- (Know ‘a / r * r < z * r’
3858 >- (MATCH_MP_TAC REAL_LT_RMUL_IMP >> art []) \\
3859 Know ‘a / r * r = a’ >- (MATCH_MP_TAC REAL_DIV_RMUL >> art []) \\
3860 Rewr' >> DISCH_TAC >> art [Once REAL_MUL_COMM])
3861 >> DISCH_TAC
3862 >> Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’ >> rw [MR2_DEF]
3863 >> rename1 ‘sqrt ((q - x) pow 2 + (r - y) pow 2) < q - z’
3864 >> Q.EXISTS_TAC ‘(x,y)’ >> rw []
3865 >> Know ‘x < 0’
3866 >- (CCONTR_TAC >> fs [GSYM real_lte] \\
3867 ‘-q <= -q + x’ by PROVE_TAC [REAL_LE_ADDR] \\
3868 Know ‘(-q) pow 2 <= (-q + x) pow 2 + (r - y) pow 2’
3869 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3870 Q.EXISTS_TAC ‘(-q + x) pow 2’ >> rw [REAL_LE_ADDR, REAL_LE_POW2] \\
3871 ‘q pow 2 = (-q) pow 2’ by rw [] >> POP_ORW \\
3872 MATCH_MP_TAC POW_LE >> rw [REAL_LE_ADDR, GSYM REAL_NEG_LE0, REAL_NEG_NEG] \\
3873 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3874 ‘-q + x = -(q - x)’ by REAL_ARITH_TAC \\
3875 POP_ASSUM (PURE_ONCE_REWRITE_TAC o wrap) \\
3876 ‘-(q - x) pow 2 = (q - x) pow 2’ by PROVE_TAC [NEGATED_POW] \\
3877 POP_ASSUM (PURE_ONCE_REWRITE_TAC o wrap) \\
3878 DISCH_TAC \\
3879 Know ‘sqrt (-q pow 2) <= sqrt ((q - x) pow 2 + (r - y) pow 2)’
3880 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_ADDR]) \\
3881 Know ‘sqrt (-q pow 2) = -q’
3882 >- (MATCH_MP_TAC POW_2_SQRT >> rw [GSYM REAL_NEG_LE0, REAL_NEG_NEG] \\
3883 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3884 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3885 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM]) >> DISCH_TAC
3886 >> Know ‘0 < y’
3887 >- (CCONTR_TAC >> fs [GSYM real_lte] \\
3888 ‘r <= r - y’ by rw [REAL_LE_SUBR] \\
3889 Know ‘r pow 2 <= (q - x) pow 2 + (r - y) pow 2’
3890 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3891 Q.EXISTS_TAC ‘(r - y) pow 2’ >> rw [REAL_LE_ADDL, REAL_LE_POW2] \\
3892 MATCH_MP_TAC POW_LE >> rw [REAL_LE_SUBR] \\
3893 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3894 Know ‘sqrt (r pow 2) <= sqrt ((q - x) pow 2 + (r - y) pow 2)’
3895 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw [REAL_LE_POW2]) \\
3896 Know ‘sqrt (r pow 2) = r’
3897 >- (MATCH_MP_TAC POW_2_SQRT \\
3898 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3899 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3900 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM]) >> DISCH_TAC
3901 >> Suff ‘z < x /\ y < a / z’
3902 >- (STRIP_TAC \\
3903 ‘a < x * y <=> ~x * y < -a’ by rw [GSYM REAL_NEG_LMUL] >> POP_ORW \\
3904 ‘~a = -z * (a / z)’ by rw [] >> POP_ORW \\
3905 MATCH_MP_TAC REAL_LT_MUL2 >> rw [] \\
3906 MATCH_MP_TAC REAL_LT_IMP_LE >> art [])
3907 (* stage work *)
3908 >> CCONTR_TAC
3909 >> fs [GSYM real_lte]
3910 >| [ (* goal 1 (of 2) *)
3911 ‘q - z <= q - x’ by rw [REAL_LE_SUB_CANCEL1] \\
3912 Know ‘(q - z) pow 2 <= (q - x) pow 2 + (r - y) pow 2’
3913 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3914 Q.EXISTS_TAC ‘(q - x) pow 2’ >> rw [REAL_LE_ADDR] \\
3915 MATCH_MP_TAC POW_LE >> rw [REAL_SUB_LE] \\
3916 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3917 Know ‘sqrt ((q - z) pow 2) <= sqrt ((q - x) pow 2 + (r - y) pow 2)’
3918 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw []) \\
3919 Know ‘sqrt ((q - z) pow 2) = q - z’
3920 >- (MATCH_MP_TAC POW_2_SQRT >> rw [REAL_SUB_LE] \\
3921 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3922 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3923 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM],
3924 (* goal 2 (of 2) *)
3925 ‘a / z - r <= y - r’ by rw [REAL_LE_SUB_CANCEL2] \\
3926 Know ‘(a / z - r) pow 2 <= (q - x) pow 2 + (y - r) pow 2’
3927 >- (MATCH_MP_TAC REAL_LE_TRANS \\
3928 Q.EXISTS_TAC ‘(y - r) pow 2’ >> rw [] \\
3929 MATCH_MP_TAC POW_LE >> rw [REAL_SUB_LE] \\
3930 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) >> DISCH_TAC \\
3931 Know ‘sqrt ((a / z - r) pow 2) <= sqrt ((q - x) pow 2 + (y - r) pow 2)’
3932 >- (MATCH_MP_TAC SQRT_MONO_LE >> rw []) \\
3933 Know ‘sqrt ((a / z - r) pow 2) = a / z - r’
3934 >- (MATCH_MP_TAC POW_2_SQRT >> rw [REAL_SUB_LE] \\
3935 MATCH_MP_TAC REAL_LT_IMP_LE >> art []) \\
3936 DISCH_THEN (PURE_ONCE_REWRITE_TAC o wrap) \\
3937 ‘y - r = -(r - y)’ by REAL_ARITH_TAC \\
3938 POP_ASSUM (PURE_ONCE_REWRITE_TAC o wrap) \\
3939 PURE_ONCE_REWRITE_TAC [NEGATED_POW] \\
3940 DISCH_TAC >> PROVE_TAC [REAL_LET_ANTISYM] ]
3941QED
3942
3943Theorem hyperbola_open_in_mr2 :
3944 !a. {(x,y) | a < x * y} IN {s | open_in (mtop mr2) s}
3945Proof
3946 rw [MTOP_OPEN]
3947 >> rename1 ‘(x,T) = (\(x,y). ((x,y),a < x * y)) z’
3948 >> Cases_on ‘z’ >> fs []
3949 >> Q.PAT_X_ASSUM ‘x = (q,r)’ K_TAC (* cleanup *)
3950 >> STRIP_ASSUME_TAC (Q.SPECL [‘a’, ‘0’] REAL_LT_TOTAL) (* 3 subgoals *)
3951 >| [ (* goal 1 (of 3): a = 0 *)
3952 POP_ASSUM (fs o wrap) \\
3953 Know ‘(0 < q /\ 0 < r) \/ (q < 0 /\ r < 0)’
3954 >- (Cases_on ‘0 < q’ >- (DISJ1_TAC >> art [] \\
3955 PROVE_TAC [REAL_LT_LMUL_0]) \\
3956 reverse (fs [GSYM real_lte, REAL_LE_LT]) >- fs [] \\
3957 DISJ2_TAC >> CCONTR_TAC \\
3958 reverse (fs [GSYM real_lte, REAL_LE_LT]) >- fs [] \\
3959 METIS_TAC [REAL_MUL_COMM, REAL_LT_LMUL_0, REAL_LT_ANTISYM]) \\
3960 Q.PAT_X_ASSUM ‘0 < q * r’ K_TAC \\
3961 STRIP_TAC >| (* 2 subgoals *)
3962 [ MATCH_MP_TAC hyperbola_lemma1 >> art [],
3963 MATCH_MP_TAC hyperbola_lemma2 >> art [] ],
3964 (* goal 2 (of 3): a < 0 *)
3965 Cases_on ‘0 < q /\ 0 < r’
3966 >- (MP_TAC (Q.SPECL [‘q’, ‘r’] hyperbola_lemma1) \\
3967 RW_TAC std_ss [] \\
3968 Q.EXISTS_TAC ‘e’ >> RW_TAC std_ss [] \\
3969 Q.PAT_X_ASSUM ‘!y. dist mr2 ((q,r),y) < e ==> P’ (MP_TAC o (Q.SPEC ‘y’)) \\
3970 Cases_on ‘y’ >> RW_TAC std_ss [] \\
3971 Cases_on ‘x’ >> rfs [] >> rename1 ‘0 < x * y’ \\
3972 Q.EXISTS_TAC ‘(x,y)’ >> rw [] \\
3973 MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC ‘0’ >> art []) \\
3974 Cases_on ‘q < 0 /\ r < 0’
3975 >- (MP_TAC (Q.SPECL [‘q’, ‘r’] hyperbola_lemma2) \\
3976 RW_TAC std_ss [] \\
3977 Q.EXISTS_TAC ‘e’ >> RW_TAC std_ss [] \\
3978 Q.PAT_X_ASSUM ‘!y. dist mr2 ((q,r),y) < e ==> P’ (MP_TAC o (Q.SPEC ‘y’)) \\
3979 Cases_on ‘y’ >> RW_TAC std_ss [] \\
3980 Cases_on ‘x’ >> rfs [] >> rename1 ‘0 < x * y’ \\
3981 Q.EXISTS_TAC ‘(x,y)’ >> rw [] \\
3982 MATCH_MP_TAC REAL_LT_TRANS >> Q.EXISTS_TAC ‘0’ >> art []) \\
3983 fs [GSYM real_lte] >| (* 4 subgoals *)
3984 [ (* goal 2.1 (of 4) *)
3985 ‘q = 0’ by PROVE_TAC [REAL_LE_ANTISYM] >> fs [] \\
3986 STRIP_ASSUME_TAC (Q.SPECL [‘r’, ‘0’] REAL_LT_TOTAL) >| (* 3 subgoals *)
3987 [ (* goal 2.1.1 (of 3) *)
3988 Q.PAT_X_ASSUM ‘r = 0’ (REWRITE_TAC o wrap) \\
3989 MATCH_MP_TAC hyperbola_lemma5 >> art [],
3990 (* goal 2.1.2 (of 3) *)
3991 MP_TAC (Q.SPECL [‘a’, ‘-r’] hyperbola_lemma6) \\
3992 ‘0 < -r’ by PROVE_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG] >> rw [] \\
3993 Q.EXISTS_TAC ‘e’ >> art [] \\
3994 Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’ >> DISCH_TAC \\
3995 rename1 ‘dist mr2 ((0,r),(x0,y0)) < e’ \\
3996 Q.EXISTS_TAC ‘(x0,y0)’ >> rw [] \\
3997 Q.PAT_X_ASSUM ‘!y. dist mr2 ((0,-r),y) < e ==> P’
3998 (MP_TAC o (Q.SPEC ‘(-x0,-y0)’)) \\
3999 ‘0 = -0’ by PROVE_TAC [REAL_NEG_0] >> POP_ORW \\
4000 RW_TAC std_ss [MR2_MIRROR] \\
4001 Cases_on ‘x’ >> fs [] \\
4002 rename1 ‘-x0 = x1’ >> rename1 ‘-y0 = y1’ \\
4003 Q.PAT_X_ASSUM ‘-x0 = x1’ (fs o wrap o SYM) \\
4004 Q.PAT_X_ASSUM ‘-y0 = y1’ (fs o wrap o SYM),
4005 (* goal 2.1.3 (of 3) *)
4006 MATCH_MP_TAC hyperbola_lemma6 >> art [] ],
4007 (* goal 2.2 (of 4) *)
4008 fs [REAL_LE_LT] >| (* 4 subgoals *)
4009 [ (* goal 2.2.1 (of 4) *)
4010 MATCH_MP_TAC hyperbola_lemma8 >> art [],
4011 (* goal 2.2.2 (of 4) *)
4012 MP_TAC (Q.SPECL [‘a’, ‘-q’] hyperbola_lemma7) \\
4013 ‘0 < -q’ by PROVE_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG] >> rw [] \\
4014 Q.EXISTS_TAC ‘e’ >> art [] \\
4015 Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’ >> DISCH_TAC \\
4016 rename1 ‘dist mr2 ((q,0),(x0,y0)) < e’ \\
4017 Q.EXISTS_TAC ‘(x0,y0)’ >> rw [] \\
4018 Q.PAT_X_ASSUM ‘!y. dist mr2 ((-q,0),y) < e ==> P’
4019 (MP_TAC o (Q.SPEC ‘(-x0,-y0)’)) \\
4020 ‘0 = -0’ by PROVE_TAC [REAL_NEG_0] >> POP_ORW \\
4021 RW_TAC std_ss [MR2_MIRROR] \\
4022 Cases_on ‘x’ >> fs [] \\
4023 rename1 ‘-x0 = x1’ >> rename1 ‘-y0 = y1’ \\
4024 Q.PAT_X_ASSUM ‘-x0 = x1’ (fs o wrap o SYM) \\
4025 Q.PAT_X_ASSUM ‘-y0 = y1’ (fs o wrap o SYM),
4026 (* goal 2.2.3 (of 4) *)
4027 MATCH_MP_TAC hyperbola_lemma6 >> art [],
4028 (* goal 2.2.4 (of 4) *)
4029 MATCH_MP_TAC hyperbola_lemma5 >> art [] ],
4030 (* goal 2.3 (of 4) *)
4031 fs [REAL_LE_LT] >| (* 4 subgoals *)
4032 [ (* goal 2.3.1 (of 4) *)
4033 MP_TAC (Q.SPECL [‘a’, ‘-q’, ‘-r’] hyperbola_lemma8) \\
4034 rw [REAL_NEG_MUL2, REAL_NEG_LE0] \\
4035 Q.EXISTS_TAC ‘e’ >> art [] \\
4036 Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’ >> DISCH_TAC \\
4037 rename1 ‘dist mr2 ((x0,y0),(x1,y1)) < e’ \\
4038 Q.EXISTS_TAC ‘(x1,y1)’ >> rw [] \\
4039 Q.PAT_X_ASSUM ‘!y. dist mr2 ((-x0,-y0),y) < e ==> P’
4040 (MP_TAC o (Q.SPEC ‘(-x1,-y1)’)) \\
4041 rw [MR2_MIRROR] \\
4042 Cases_on ‘x’ >> fs [] \\
4043 Q.PAT_X_ASSUM ‘-x1 = x2’ (fs o wrap o SYM) \\
4044 Q.PAT_X_ASSUM ‘-y1 = y2’ (fs o wrap o SYM),
4045 (* goal 2.3.2 (of 4) *)
4046 MP_TAC (Q.SPECL [‘a’, ‘-r’] hyperbola_lemma6) \\
4047 ‘0 < -r’ by PROVE_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG] >> rw [] \\
4048 Q.EXISTS_TAC ‘e’ >> art [] \\
4049 Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’ >> DISCH_TAC \\
4050 rename1 ‘dist mr2 ((0,r),(x0,y0)) < e’ \\
4051 Q.EXISTS_TAC ‘(x0,y0)’ >> rw [] \\
4052 Q.PAT_X_ASSUM ‘!y. dist mr2 ((0,-r),y) < e ==> P’
4053 (MP_TAC o (Q.SPEC ‘(-x0,-y0)’)) \\
4054 ‘0 = -0’ by PROVE_TAC [REAL_NEG_0] >> POP_ORW \\
4055 RW_TAC std_ss [MR2_MIRROR] \\
4056 Cases_on ‘x’ >> fs [] \\
4057 rename1 ‘-x0 = x1’ >> rename1 ‘-y0 = y1’ \\
4058 Q.PAT_X_ASSUM ‘-x0 = x1’ (fs o wrap o SYM) \\
4059 Q.PAT_X_ASSUM ‘-y0 = y1’ (fs o wrap o SYM),
4060 (* goal 2.3.3 (of 4) *)
4061 MATCH_MP_TAC hyperbola_lemma7 >> art [],
4062 (* goal 2.3.4 (of 4) *)
4063 MATCH_MP_TAC hyperbola_lemma5 >> art [] ],
4064 (* goal 2.4 (of 4) *)
4065 ‘r = 0’ by PROVE_TAC [REAL_LE_ANTISYM] >> fs [] \\
4066 STRIP_ASSUME_TAC (Q.SPECL [‘q’, ‘0’] REAL_LT_TOTAL) >| (* 3 subgoals *)
4067 [ (* goal 2.1.1 (of 3) *)
4068 Q.PAT_X_ASSUM ‘q = 0’ (REWRITE_TAC o wrap) \\
4069 MATCH_MP_TAC hyperbola_lemma5 >> art [],
4070 (* goal 2.1.2 (of 3) *)
4071 MP_TAC (Q.SPECL [‘a’, ‘-q’] hyperbola_lemma7) \\
4072 ‘0 < -q’ by PROVE_TAC [GSYM REAL_NEG_LT0, REAL_NEG_NEG] >> rw [] \\
4073 Q.EXISTS_TAC ‘e’ >> art [] \\
4074 Q.X_GEN_TAC ‘y’ >> Cases_on ‘y’ >> DISCH_TAC \\
4075 rename1 ‘dist mr2 ((q,0),(x0,y0)) < e’ \\
4076 Q.EXISTS_TAC ‘(x0,y0)’ >> rw [] \\
4077 Q.PAT_X_ASSUM ‘!y. dist mr2 ((-q,0),y) < e ==> P’
4078 (MP_TAC o (Q.SPEC ‘(-x0,-y0)’)) \\
4079 ‘0 = -0’ by PROVE_TAC [REAL_NEG_0] >> POP_ORW \\
4080 RW_TAC std_ss [MR2_MIRROR] \\
4081 Cases_on ‘x’ >> fs [] \\
4082 rename1 ‘-x0 = x1’ >> rename1 ‘-y0 = y1’ \\
4083 Q.PAT_X_ASSUM ‘-x0 = x1’ (fs o wrap o SYM) \\
4084 Q.PAT_X_ASSUM ‘-y0 = y1’ (fs o wrap o SYM),
4085 (* goal 2.1.3 (of 3) *)
4086 MATCH_MP_TAC hyperbola_lemma7 >> art [] ] ],
4087 (* goal 3 (of 3): 0 < a *)
4088 ‘0 < q * r’ by PROVE_TAC [REAL_LT_TRANS] \\
4089 Know ‘(0 < q /\ 0 < r) \/ (q < 0 /\ r < 0)’
4090 >- (Cases_on ‘0 < q’ >- (DISJ1_TAC >> art [] \\
4091 PROVE_TAC [REAL_LT_LMUL_0]) \\
4092 reverse (fs [GSYM real_lte, REAL_LE_LT]) >- fs [] \\
4093 DISJ2_TAC >> CCONTR_TAC \\
4094 reverse (fs [GSYM real_lte, REAL_LE_LT]) >- fs [] \\
4095 METIS_TAC [REAL_MUL_COMM, REAL_LT_LMUL_0, REAL_LT_ANTISYM]) \\
4096 Q.PAT_X_ASSUM ‘0 < q * r’ K_TAC \\
4097 STRIP_TAC >| (* 2 subgoals *)
4098 [ MATCH_MP_TAC hyperbola_lemma3 >> art [],
4099 MATCH_MP_TAC hyperbola_lemma4 >> art [] ] ]
4100QED
4101
4102(* ------------------------------------------------------------------------- *)
4103(* More Measurability Results *)
4104(* ------------------------------------------------------------------------- *)
4105
4106(*
4107These are the results from my own accumulated library for borel measurable functions
4108that I believe stand on their own as something useful for future users.
4109- Jared Yeager
4110*)
4111
4112(* This first batch of results has to do with sets derived from borel measurable
4113 functions being measurable sets
4114*)
4115
4116Theorem in_borel_measurable_ge_imp:
4117 ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
4118 ∀c. {x | c ≤ f x} ∩ space a ∈ subsets a
4119Proof
4120 rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_ge >>
4121 rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
4122 qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
4123 simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
4124QED
4125
4126Theorem in_borel_measurable_gt_imp:
4127 ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
4128 ∀c. {x | c < f x} ∩ space a ∈ subsets a
4129Proof
4130 rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_gr >>
4131 rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
4132 qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
4133 simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
4134QED
4135
4136Theorem in_borel_measurable_le_imp:
4137 ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
4138 ∀c. {x | f x ≤ c} ∩ space a ∈ subsets a
4139Proof
4140 rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_le >>
4141 rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
4142 qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
4143 simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
4144QED
4145
4146Theorem in_borel_measurable_lt_imp:
4147 ∀a f. sigma_algebra a ∧ f ∈ borel_measurable a ⇒
4148 ∀c. {x | f x < c} ∩ space a ∈ subsets a
4149Proof
4150 rw[] >> drule_all_then mp_tac $ cj 2 $ SRULE [AND_IMP_INTRO] $ iffLR in_borel_measurable_less >>
4151 rw[INTER_DEF] >> pop_assum $ qspec_then ‘c’ mp_tac >>
4152 qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
4153 simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
4154QED
4155
4156Theorem in_borel_measurable_le2_imp:
4157 ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
4158 {x | f x ≤ g x} ∩ space a ∈ subsets a
4159Proof
4160 rw[] >> qspecl_then [‘a’,‘f’,‘g’] mp_tac in_borel_measurable_le2 >> simp[INTER_DEF] >>
4161 qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
4162 simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
4163QED
4164
4165Theorem in_borel_measurable_lt2_imp:
4166 ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ⇒
4167 {x | f x < g x} ∩ space a ∈ subsets a
4168Proof
4169 rw[] >> qspecl_then [‘a’,‘f’,‘g’] mp_tac in_borel_measurable_lt2 >> simp[INTER_DEF] >>
4170 qmatch_goalsub_abbrev_tac ‘s ∈ _ ⇒ t ∈ _’ >> ‘s = t’ suffices_by simp[] >>
4171 simp[EXTENSION,Abbr ‘s’,Abbr ‘t’] >> metis_tac[]
4172QED
4173
4174(* This second batch of results has to do with functions being borel measurable *)
4175
4176(* name conflict *)
4177Theorem in_borel_measurable_ainv':
4178 ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧
4179 (∀x. x ∈ space a ⇒ g x = -f x) ⇒ g ∈ borel_measurable a
4180Proof
4181 rw[] >> irule $ INST_TYPE [“:β”|->“:γ”] IN_MEASURABLE_COMP >>
4182 qexistsl [‘borel’,‘f’,‘λx. -x’] >> simp[] >>
4183 irule in_borel_measurable_mul >> simp[sigma_algebra_borel,space_borel] >>
4184 qexistsl [‘λx. -1r’,‘I’] >>
4185 simp[sigma_algebra_borel,MEASURABLE_I,borel_measurable_sets,borel_measurable_const]
4186QED
4187
4188Theorem in_borel_measurable_abs:
4189 ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧
4190 (∀x. x ∈ space a ⇒ g x = abs (f x)) ⇒ g ∈ borel_measurable a
4191Proof
4192 rw[] >> irule $ INST_TYPE [“:β”|->“:γ”] IN_MEASURABLE_COMP >>
4193 qexistsl [‘borel’,‘f’,‘abs’] >> simp[] >>
4194 ‘abs = λr:real. max (I r) ((λrr. -rr) r)’ by (
4195 simp[FUN_EQ_THM,abs,max_def] >> strip_tac >> Cases_on ‘0 ≤ r’ >> simp[]
4196 >- (Cases_on ‘r = 0’ >> simp[] >> ‘0 < r’ by simp[REAL_LT_LE] >>
4197 ‘¬(r ≤ -r)’ suffices_by simp[] >> simp[REAL_NOT_LE])
4198 >- (‘r ≤ -r’ suffices_by simp[] >> gs[REAL_NOT_LE])) >>
4199 pop_assum SUBST1_TAC >> irule in_borel_measurable_max >>
4200 simp[sigma_algebra_borel,MEASURABLE_I] >>
4201 irule in_borel_measurable_ainv' >> simp[sigma_algebra_borel] >>
4202 qexists ‘I’ >> simp[sigma_algebra_borel,MEASURABLE_I]
4203QED
4204
4205Theorem in_borel_measurable_sum:
4206 ∀a f g s. FINITE s ∧ sigma_algebra a ∧ (∀i. i ∈ s ⇒ f i ∈ borel_measurable a) ∧
4207 (∀x. x ∈ space a ⇒ g x = REAL_SUM_IMAGE (λi. f i x) s) ⇒ g ∈ borel_measurable a
4208Proof
4209 simp[Once $ GSYM AND_IMP_INTRO] >> rpt gen_tac >> map_every qid_spec_tac [‘f’,‘g’] >>
4210 simp[RIGHT_FORALL_IMP_THM] >> Induct_on ‘s’ >> rw[]
4211 >- (irule in_borel_measurable_const >> simp[] >> qexists ‘0’ >> simp[]) >>
4212 gs[REAL_SUM_IMAGE_THM] >> irule in_borel_measurable_add >> simp[] >>
4213 qexistsl [‘f e’,‘λx. REAL_SUM_IMAGE (λi. f i x) (s DELETE e)’] >> simp[] >>
4214 last_x_assum irule >> qexists ‘f’ >> simp[DELETE_NON_ELEMENT_RWT]
4215QED
4216
4217Theorem in_borel_measurable_inv:
4218 ∀a f g. sigma_algebra a ∧ f ∈ borel_measurable a ∧
4219 (∀x. x ∈ space a ⇒ g x = (f x)⁻¹) ⇒ g ∈ borel_measurable a
4220Proof
4221 rw[] >> irule $ INST_TYPE [“:β”|->“:γ”] IN_MEASURABLE_COMP >>
4222 qexistsl [‘borel’,‘f’,‘λx. x⁻¹’] >> simp[] >>
4223 simp[sigma_algebra_borel,in_borel_measurable_le,FUNSET,space_borel] >>
4224 qx_gen_tac ‘c’ >> Cases_on ‘c < 0’
4225 >- (‘{x | x⁻¹ ≤ c} = {x | c⁻¹ ≤ x ∧ x < 0}’ suffices_by
4226 simp[borel_measurable_sets,Excl "RMUL_LEQNORM"] >>
4227 rw[EXTENSION] >> Cases_on ‘x < 0’ >> simp[REAL_NEG_NZ,nonzerop_EQ1_I] >>
4228 gs[REAL_NOT_LT,REAL_NOT_LE] >> irule REAL_LTE_TRANS >>
4229 qexists ‘0’ >> simp[]) >>
4230 reverse $ gs[REAL_NOT_LT,Once REAL_LE_LT]
4231 >- (‘{x | x⁻¹ ≤ 0r} = {x | x ≤ 0}’ suffices_by simp[borel_measurable_sets] >>
4232 rw[EXTENSION,REAL_LE_LT]) >>
4233 ‘{x | x⁻¹ ≤ c} = {x | x ≤ 0} ∪ {x | c⁻¹ ≤ x}’ suffices_by (
4234 disch_then SUBST1_TAC >> irule SIGMA_ALGEBRA_UNION >>
4235 simp[sigma_algebra_borel,borel_measurable_sets,Excl "RMUL_LEQNORM"]) >>
4236 rw[EXTENSION] >> Cases_on ‘x ≤ 0’ >> simp[]
4237 >- (irule REAL_LE_TRANS >> qexists ‘0’ >> gs[REAL_LE_LT]) >>
4238 gs[REAL_NOT_LE] >> simp[REAL_POS_NZ,nonzerop_EQ1_I]
4239QED
4240
4241Theorem in_borel_measurable_div:
4242 ∀a f g h. sigma_algebra a ∧ f ∈ borel_measurable a ∧ g ∈ borel_measurable a ∧
4243 (∀x. x ∈ space a ⇒ h x = f x / g x) ⇒ h ∈ borel_measurable a
4244Proof
4245 rw[] >> irule in_borel_measurable_mul >> simp[real_div] >>
4246 qexistsl [‘f’,‘λx. (g x)⁻¹’] >> simp[] >>
4247 irule in_borel_measurable_inv >> simp[] >> qexists ‘g’ >> simp[]
4248QED
4249
4250Theorem in_borel_measurable_pow:
4251 ∀a n f g.
4252 sigma_algebra a ∧ f ∈ borel_measurable a ∧
4253 (∀x. x ∈ space a ⇒ g x = (f x) pow n) ⇒
4254 g ∈ borel_measurable a
4255Proof
4256 Induct_on ‘n’ >> rw[pow] >- (metis_tac[in_borel_measurable_const]) >>
4257 irule in_borel_measurable_mul >> simp[] >> qexistsl [‘f’,‘λx. f x pow n’] >>
4258 simp[] >> last_x_assum $ irule_at Any >> simp[] >> qexists ‘f’ >> simp[]
4259QED
4260
4261Theorem in_measurable_borel_borel_abs :
4262 abs IN borel_measurable borel
4263Proof
4264 MATCH_MP_TAC in_borel_measurable_continuous_on
4265 >> rw [continuous_on_def, CONTINUOUS_AT_ABS, WITHIN_UNIV]
4266QED
4267
4268Theorem in_measurable_borel_borel_ainv :
4269 numeric_negate IN borel_measurable borel
4270Proof
4271 Know ‘$real_neg = \x. -1 * x’
4272 >- (rw [FUN_EQ_THM, Once REAL_NEG_MINUS1])
4273 >> Rewr'
4274 >> MATCH_MP_TAC in_borel_measurable_cmul
4275 >> qexistsl_tac [‘\x. x’, ‘-1’]
4276 >> rw [sigma_algebra_borel, in_borel_measurable_I, space_borel]
4277QED
4278
4279Theorem in_measurable_borel_not_sing :
4280 !f a. sigma_algebra a /\ f IN measurable a borel ==>
4281 !c. ({x | f x <> c} INTER space a) IN subsets a
4282Proof
4283 rpt STRIP_TAC
4284 >> MP_TAC (Q.SPECL [‘f’, ‘a’] in_borel_measurable_borel) >> rw []
4285 >> POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘{x | x <> (c :real)}’)
4286 >> fs [borel_measurable_sets_not_sing, PREIMAGE_def]
4287QED
4288
4289Theorem in_measurable_borel_eq :
4290 !a f g.
4291 (!x. x IN space a ==> f x = g x) /\ g IN borel_measurable a ==>
4292 f IN borel_measurable a
4293Proof
4294 rw [measurable_def, IN_FUNSET]
4295 >> Know ‘PREIMAGE f s INTER space a = PREIMAGE g s INTER space a’
4296 >- (rw [Once EXTENSION, PREIMAGE_def] \\
4297 METIS_TAC [])
4298 >> Rewr'
4299 >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
4300QED
4301
4302Theorem in_measurable_borel_comp_borel :
4303 !a f g h.
4304 f IN borel_measurable borel /\ g IN borel_measurable a /\
4305 (!x. x IN space a ==> h x = f (g x)) ==>
4306 h IN borel_measurable a
4307Proof
4308 rw[] >> dxrule_all_then assume_tac MEASURABLE_COMP
4309 >> irule in_measurable_borel_eq >> qexists_tac ‘f o g’ >> simp[]
4310QED
4311
4312Theorem in_measurable_borel_borel_exp :
4313 exp IN borel_measurable borel
4314Proof
4315 MATCH_MP_TAC in_borel_measurable_continuous_on
4316 >> REWRITE_TAC [CONTINUOUS_ON_EXP]
4317QED
4318
4319(* References:
4320
4321 [1] Schilling, R.L.: Measures, Integrals and Martingales (Second Edition).
4322 Cambridge University Press (2017).
4323 *)