1 (* ========================================================================= *)
2 (* Brunn-Minkowski theorem and related results. *)
3 (* ========================================================================= *)
5 needs "Multivariate/realanalysis.ml";;
7 (* ------------------------------------------------------------------------- *)
8 (* First, the special case of a box. *)
9 (* ------------------------------------------------------------------------- *)
11 let BRUNN_MINKOWSKI_INTERVAL = prove
13 ~(interval[a,b] = {}) /\ ~(interval[c,d] = {})
14 ==> root (dimindex(:N))
15 (measure {x + y | x IN interval[a,b] /\ y IN interval[c,d]})
16 >= root (dimindex(:N)) (measure(interval[a,b])) +
17 root (dimindex(:N)) (measure(interval[c,d]))`,
18 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[SUMS_INTERVALS; real_ge] THEN
19 RULE_ASSUM_TAC(REWRITE_RULE[INTERVAL_NE_EMPTY]) THEN
20 ASM_CASES_TAC `measure(interval[a:real^N,b]) = &0` THENL
21 [ASM_SIMP_TAC[ROOT_0; DIMINDEX_GE_1; LE_1; REAL_ADD_LID;
22 ROOT_MONO_LE_EQ; MEASURE_POS_LE; MEASURABLE_INTERVAL] THEN
23 ASM_SIMP_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL;
25 REAL_ARITH `a <= b /\ c <= d ==> a + c <= b + d`] THEN
26 MATCH_MP_TAC PRODUCT_LE_NUMSEG THEN
27 X_GEN_TAC `i:num` THEN DISCH_TAC THEN
28 REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
29 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
30 FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
31 SIMP_TAC[MEASURABLE_MEASURE_EQ_0; MEASURABLE_INTERVAL] THEN
32 REWRITE_TAC[NEGLIGIBLE_INTERVAL; INTERVAL_NE_EMPTY] THEN STRIP_TAC] THEN
33 ASM_CASES_TAC `measure(interval[c:real^N,d]) = &0` THENL
34 [ASM_SIMP_TAC[ROOT_0; DIMINDEX_GE_1; LE_1; REAL_ADD_RID;
35 ROOT_MONO_LE_EQ; MEASURE_POS_LE; MEASURABLE_INTERVAL] THEN
36 ASM_SIMP_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL;
38 REAL_ARITH `a <= b /\ c <= d ==> a + c <= b + d`] THEN
39 MATCH_MP_TAC PRODUCT_LE_NUMSEG THEN
40 X_GEN_TAC `i:num` THEN DISCH_TAC THEN
41 REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
42 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
43 FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
44 SIMP_TAC[MEASURABLE_MEASURE_EQ_0; MEASURABLE_INTERVAL] THEN
45 REWRITE_TAC[NEGLIGIBLE_INTERVAL; INTERVAL_NE_EMPTY] THEN STRIP_TAC] THEN
46 ASM_SIMP_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL; VECTOR_ADD_COMPONENT;
47 REAL_ARITH `a <= b /\ c <= d ==> a + c <= b + d`] THEN
48 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
49 W(MP_TAC o PART_MATCH (rand o rand) REAL_LE_LDIV_EQ o snd) THEN
51 [MATCH_MP_TAC ROOT_POS_LT THEN
52 ASM_SIMP_TAC[GSYM REAL_LE_LDIV_EQ; PRODUCT_POS_LT_NUMSEG; IN_NUMSEG;
53 REAL_ARITH `a < b /\ c < d ==> &0 < (b + d) - (a + c)`;
55 DISCH_THEN(SUBST1_TAC o SYM)] THEN
56 REWRITE_TAC[real_div; REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM real_div] THEN
57 REWRITE_TAC[GSYM REAL_ROOT_DIV] THEN
58 REWRITE_TAC[GSYM PRODUCT_DIV_NUMSEG] THEN
59 MATCH_MP_TAC REAL_LE_TRANS THEN
61 `sum (1..dimindex(:N))
62 (\i. ((b:real^N)$i - (a:real^N)$i) /
63 ((b$i + d$i) - (a$i + c$i))) / &(dimindex(:N)) +
65 (\i. ((d:real^N)$i - (c:real^N)$i) /
66 ((b$i + d$i) - (a$i + c$i))) / &(dimindex(:N))` THEN
68 [MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THEN
69 W(MP_TAC o PART_MATCH (lhand o rand) REAL_ROOT_LE o snd) THEN
71 [SIMP_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_EQ; DIMINDEX_GE_1; LE_1;
72 REAL_LE_RDIV_EQ; REAL_MUL_LZERO] THEN
73 MATCH_MP_TAC SUM_POS_LE_NUMSEG;
74 DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC AGM THEN
75 SIMP_TAC[HAS_SIZE_NUMSEG_1; DIMINDEX_GE_1; LE_1; IN_NUMSEG]]) THEN
76 X_GEN_TAC `i:num` THEN DISCH_TAC THEN REWRITE_TAC[REAL_SUB_LE] THEN
77 MATCH_MP_TAC REAL_LE_DIV THEN
78 REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
79 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
80 REWRITE_TAC[real_div; GSYM REAL_ADD_RDISTRIB] THEN
81 REWRITE_TAC[GSYM SUM_ADD_NUMSEG] THEN
82 ASM_SIMP_TAC[REAL_FIELD
84 ==> (b - a) * inv((b + d) - (a + c)) +
85 (d - c) * inv((b + d) - (a + c)) = &1`] THEN
86 REWRITE_TAC[SUM_CONST_NUMSEG; ADD_SUB] THEN
87 ASM_SIMP_TAC[REAL_MUL_RID; REAL_MUL_RINV; REAL_LE_REFL;
88 REAL_OF_NUM_EQ; DIMINDEX_NONZERO]]);;
90 (* ------------------------------------------------------------------------- *)
91 (* Now for a finite union of boxes. *)
92 (* ------------------------------------------------------------------------- *)
94 let BRUNN_MINKOWSKI_ELEMENTARY = prove
96 (s = {} <=> t = {}) /\ (?d. d division_of s) /\ (?d. d division_of t)
97 ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
98 >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,
99 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
100 REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
102 [`s:real^N->bool`; `t:real^N->bool`;
103 `d1:(real^N->bool)->bool`; `d2:(real^N->bool)->bool`] THEN
104 ASM_CASES_TAC `t:real^N->bool = {}` THENL
105 [ASM_SIMP_TAC[NOT_IN_EMPTY; SET_RULE `{f x y |x,y| F} = {}`] THEN
106 SIMP_TAC[MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO] THEN
107 STRIP_TAC THEN REAL_ARITH_TAC;
108 ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN
109 ONCE_REWRITE_TAC[TAUT `p ==> q /\ r ==> s <=> q /\ p /\ r ==> s`]] THEN
110 X_CHOOSE_THEN `n:num` MP_TAC (ISPEC
111 `CARD(d1:(real^N->bool)->bool) + CARD(d2:(real^N->bool)->bool)`
112 (GSYM EXISTS_REFL)) THEN
113 REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
114 MAP_EVERY (fun t -> SPEC_TAC(t,t))
115 [`t:real^N->bool`; `s:real^N->bool`;
116 `d2:(real^N->bool)->bool`; `d1:(real^N->bool)->bool`; `n:num`] THEN
117 MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
119 `(!m. m < n ==> !a b c d. f a b = m /\ stuff a b c d ==> other a b c d) <=>
120 (!a b c d. f a b:num < n /\ stuff a b c d ==> other a b c d)`] THEN
123 `(!d d' s s'. P d d' s s' ==> P d' d s' s) /\
124 (!d d' s s'. ~(2 <= CARD d) /\ ~(2 <= CARD d') ==> P d d' s s') /\
125 (!d d' s s'. negligible s ==> P d d' s s') /\
126 (!d d' s s'. 2 <= CARD d /\ ~(negligible s) /\ ~(negligible s')
128 ==> !d d' s s'. P d d' s s'`) THEN
129 REPEAT CONJ_TAC THENL
130 [REPEAT GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN
131 CONJ_TAC THENL [REWRITE_TAC[ADD_SYM; CONJ_ACI]; ALL_TAC] THEN
132 MATCH_MP_TAC(REAL_ARITH
133 `x = y ==> x >= a + b ==> y >= b + a`) THEN
134 AP_TERM_TAC THEN AP_TERM_TAC THEN
135 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN MESON_TAC[VECTOR_ADD_SYM];
137 ASM_CASES_TAC `FINITE(d1:(real^N->bool)->bool) /\
138 FINITE(d2:(real^N->bool)->bool)`
139 THENL [ALL_TAC; REWRITE_TAC[division_of] THEN ASM_MESON_TAC[]] THEN
140 ASM_SIMP_TAC[CARD_EQ_0; ARITH_RULE `~(2 <= n) <=> n = 0 \/ n = 1`] THEN
141 ASM_CASES_TAC `d1:(real^N->bool)->bool = {}` THENL
142 [ASM_REWRITE_TAC[EMPTY_DIVISION_OF] THEN MESON_TAC[]; ALL_TAC] THEN
143 ASM_CASES_TAC `d2:(real^N->bool)->bool = {}` THENL
144 [ASM_REWRITE_TAC[EMPTY_DIVISION_OF] THEN MESON_TAC[]; ALL_TAC] THEN
145 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
147 `(d1:(real^N->bool)->bool) HAS_SIZE 1 /\
148 (d2:(real^N->bool)->bool) HAS_SIZE 1`
149 MP_TAC THENL [ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN
150 CONV_TAC(LAND_CONV(BINOP_CONV HAS_SIZE_CONV)) THEN
151 DISCH_THEN(CONJUNCTS_THEN2
152 (X_CHOOSE_THEN `u:real^N->bool` SUBST_ALL_TAC)
153 (X_CHOOSE_THEN `v:real^N->bool` SUBST_ALL_TAC)) THEN
155 RULE_ASSUM_TAC(REWRITE_RULE[division_of; UNIONS_1; IN_SING]) THEN
157 (CONJUNCTS_THEN2 MP_TAC
158 (SUBST_ALL_TAC o SYM o CONJUNCT2) o CONJUNCT2)) THEN
159 REWRITE_TAC[FORALL_UNWIND_THM2] THEN REPEAT STRIP_TAC THEN
160 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC BRUNN_MINKOWSKI_INTERVAL THEN
162 REPEAT STRIP_TAC THEN
163 SUBGOAL_THEN `measure(s:real^N->bool) = &0` SUBST1_TAC THENL
164 [ASM_SIMP_TAC[MEASURE_EQ_0]; ALL_TAC] THEN
165 SIMP_TAC[ROOT_0; DIMINDEX_NONZERO; REAL_ADD_LID; real_ge] THEN
166 MATCH_MP_TAC ROOT_MONO_LE THEN REWRITE_TAC[DIMINDEX_NONZERO] THEN
167 SUBGOAL_THEN `?a:real^N. a IN s` STRIP_ASSUME_TAC THENL
168 [ASM SET_TAC[]; ALL_TAC] THEN
169 MATCH_MP_TAC REAL_LE_TRANS THEN
170 EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) t)` THEN CONJ_TAC THENL
171 [REWRITE_TAC[MEASURE_TRANSLATION; REAL_LE_REFL]; ALL_TAC] THEN
172 MATCH_MP_TAC MEASURE_SUBSET THEN
173 REWRITE_TAC[MEASURABLE_TRANSLATION_EQ] THEN
174 CONJ_TAC THENL [ASM_MESON_TAC[MEASURABLE_ELEMENTARY]; ALL_TAC] THEN
175 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
176 CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
177 MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
178 ASM_MESON_TAC[ELEMENTARY_COMPACT];
179 REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC]] THEN
182 CARD d1 + CARD d2 = n /\
183 1 <= k /\ k <= dimindex(:N) /\ ~(i = j) /\
184 i IN d1 /\ i SUBSET {x:real^N | x$k <= &0} /\
185 j IN d1 /\ j SUBSET {x | x$k >= &0} /\
186 ~(negligible i) /\ ~(negligible j) /\
187 ~(s = {}) /\ ~(t = {}) /\ ~(negligible s) /\ ~(negligible t) /\
188 d1 division_of s /\ d2 division_of t
189 ==> root(dimindex (:N)) (measure {x + y | x IN s /\ y IN t}) >=
190 root(dimindex (:N)) (measure s) + root(dimindex (:N)) (measure t)`
193 POP_ASSUM(LABEL_TAC "*") THEN DISCH_THEN(LABEL_TAC "+") THEN
194 REPEAT STRIP_TAC THEN
195 ASM_CASES_TAC `?i:real^N->bool. i IN d1 /\ interior i = {}` THENL
196 [REMOVE_THEN "+" (K ALL_TAC) THEN REMOVE_THEN "*" MP_TAC THEN
197 DISCH_THEN(MP_TAC o SPECL
198 [`{i:real^N->bool | i IN d1 /\ ~(interior i = {})}`;
199 `d2:(real^N->bool)->bool`;
200 `UNIONS {i:real^N->bool | i IN d1 /\ ~(interior i = {})}`;
201 `t:real^N->bool`]) THEN
202 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
203 [REPEAT CONJ_TAC THENL
204 [EXPAND_TAC "n" THEN REWRITE_TAC[LT_ADD_RCANCEL] THEN
205 MATCH_MP_TAC CARD_PSUBSET THEN CONJ_TAC THENL
206 [ASM SET_TAC[]; ASM_MESON_TAC[DIVISION_OF_FINITE]];
209 `negligible(UNIONS {i | i IN d1 /\ ~(interior i = {})} UNION
210 UNIONS {i:real^N->bool | i IN d1 /\ interior i = {}})`
212 [ASM_REWRITE_TAC[UNION_EMPTY] THEN
213 MATCH_MP_TAC NEGLIGIBLE_UNIONS THEN CONJ_TAC THENL
214 [MATCH_MP_TAC FINITE_RESTRICT THEN
215 ASM_MESON_TAC[DIVISION_OF_FINITE];
216 REWRITE_TAC[IN_ELIM_THM; IMP_CONJ] THEN
217 FIRST_ASSUM(fun th ->
218 GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
219 REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; NEGLIGIBLE_INTERVAL]];
220 REWRITE_TAC[GSYM UNIONS_UNION; SET_RULE
221 `{x | x IN s /\ ~Q x} UNION {x | x IN s /\ Q x} = s`] THEN
222 RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN ASM_REWRITE_TAC[]];
223 MATCH_MP_TAC DIVISION_OF_SUBSET THEN
224 EXISTS_TAC `d1:(real^N->bool)->bool` THEN
225 CONJ_TAC THENL [ASM_MESON_TAC[division_of]; SET_TAC[]]];
226 MATCH_MP_TAC(REAL_ARITH
228 ==> c' >= a' + b ==> c >= a + b`) THEN
230 [MATCH_MP_TAC ROOT_MONO_LE THEN REWRITE_TAC[DIMINDEX_NONZERO] THEN
231 MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
232 [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
233 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[ELEMENTARY_COMPACT]] THEN
234 MATCH_MP_TAC COMPACT_UNIONS THEN
235 RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN
236 ASM_SIMP_TAC[FINITE_RESTRICT; IN_ELIM_THM] THEN
237 ASM_MESON_TAC[COMPACT_INTERVAL];
238 MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
239 ASM_MESON_TAC[ELEMENTARY_COMPACT];
240 MATCH_MP_TAC(SET_RULE
242 ==> {f x y | x IN s' /\ y IN t} SUBSET
243 {f x y | x IN s /\ y IN t}`) THEN
244 SUBGOAL_THEN `s:real^N->bool = UNIONS d1` SUBST1_TAC THENL
245 [ASM_MESON_TAC[division_of];
246 MATCH_MP_TAC SUBSET_UNIONS THEN SET_TAC[]]];
248 MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN
249 MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
250 EXISTS_TAC `UNIONS {i:real^N->bool | i IN d1 /\ interior i = {}}` THEN
252 [MATCH_MP_TAC NEGLIGIBLE_UNIONS THEN CONJ_TAC THENL
253 [MATCH_MP_TAC FINITE_RESTRICT THEN
254 ASM_MESON_TAC[DIVISION_OF_FINITE];
255 REWRITE_TAC[IN_ELIM_THM; IMP_CONJ] THEN
256 FIRST_ASSUM(fun th ->
257 GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
258 REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; NEGLIGIBLE_INTERVAL]];
259 MATCH_MP_TAC(SET_RULE
261 ==> (s' DIFF s) UNION (s DIFF s') SUBSET s''`) THEN
262 REWRITE_TAC[GSYM UNIONS_UNION; SET_RULE
263 `{x | x IN s /\ ~Q x} UNION {x | x IN s /\ Q x} = s`] THEN
264 RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN
265 ASM_REWRITE_TAC[]]]];
266 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
267 REWRITE_TAC[TAUT `~(a /\ b) <=> a ==> ~b`] THEN DISCH_TAC THEN
268 REMOVE_THEN "*" (K ALL_TAC) THEN
270 `?d:(real^N->bool)->bool. d SUBSET d1 /\ d HAS_SIZE 2`
272 [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP CHOOSE_SUBSET o
273 MATCH_MP DIVISION_OF_FINITE) THEN ASM_REWRITE_TAC[];
275 CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV HAS_SIZE_CONV)) THEN
276 REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
277 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
278 DISCH_THEN(X_CHOOSE_THEN `i:real^N->bool` MP_TAC) THEN
279 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
280 DISCH_THEN(X_CHOOSE_THEN `j:real^N->bool` MP_TAC) THEN
281 ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> r /\ p /\ q`] THEN
282 REWRITE_TAC[UNWIND_THM2; INSERT_SUBSET; EMPTY_SUBSET] THEN STRIP_TAC THEN
283 MP_TAC(ASSUME `d1 division_of (s:real^N->bool)`) THEN
284 REWRITE_TAC[division_of] THEN DISCH_THEN(MP_TAC o el 2 o CONJUNCTS) THEN
285 DISCH_THEN(MP_TAC o SPECL [`i:real^N->bool`; `j:real^N->bool`]) THEN
286 ASM_REWRITE_TAC[] THEN
288 `?u v w z. i = interval[u:real^N,v] /\ j = interval[w:real^N,z]`
289 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[DIVISION_OF]; ALL_TAC] THEN
290 ASM_REWRITE_TAC[GSYM INTERIOR_INTER; INTER_INTERVAL] THEN
291 REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; INTERVAL_EQ_EMPTY] THEN
292 DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
293 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
294 SIMP_TAC[LAMBDA_BETA; ASSUME `1 <= k`; ASSUME `k <= dimindex(:N)`] THEN
295 GEN_REWRITE_TAC LAND_CONV [REAL_LE_BETWEEN] THEN
296 DISCH_THEN(X_CHOOSE_THEN `a:real` MP_TAC) THEN
297 DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
298 `min v z <= a /\ a <= max u w
300 ==> u <= a /\ v <= a /\ a <= w /\ a <= z \/
301 w <= a /\ z <= a /\ a <= u /\ a <= v`)) THEN
303 [UNDISCH_TAC `!i:real^N->bool. i IN d1 ==> ~(interior i = {})` THEN
304 DISCH_THEN(fun th -> MP_TAC(ISPEC `interval[u:real^N,v]` th) THEN
305 MP_TAC(ISPEC `interval[w:real^N,z]` th)) THEN
306 REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; INTERVAL_NE_EMPTY] THEN
310 FIRST_X_ASSUM(MP_TAC o SPECL
311 [`IMAGE (IMAGE (\x:real^N. x - a % basis k)) d1`;
312 `d2:(real^N->bool)->bool`;
313 `IMAGE (\x:real^N. x - a % basis k) s`;
316 [DISCH_THEN(MP_TAC o SPECL
317 [`IMAGE (\x:real^N. x - a % basis k) i`;
318 `IMAGE (\x:real^N. x - a % basis k) j`; `k:num`]);
319 DISCH_THEN(MP_TAC o SPECL
320 [`IMAGE (\x:real^N. x - a % basis k) j`;
321 `IMAGE (\x:real^N. x - a % basis k) i`; `k:num`])] THEN
322 (ASM_REWRITE_TAC[] THEN ANTS_TAC THEN REPEAT CONJ_TAC THENL
323 [EXPAND_TAC "n" THEN AP_THM_TAC THEN AP_TERM_TAC THEN
324 MATCH_MP_TAC CARD_IMAGE_INJ THEN
325 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[DIVISION_OF_FINITE]] THEN
327 `(!x y. Q x y ==> R x y)
328 ==> (!x y. P x /\ P y /\ Q x y ==> R x y)`) THEN
329 REWRITE_TAC[INJECTIVE_IMAGE] THEN VECTOR_ARITH_TAC;
330 MATCH_MP_TAC(SET_RULE
331 `(!x y. f x = f y ==> x = y) /\ ~(s = t)
332 ==> ~(IMAGE f s = IMAGE f t)`) THEN
333 REWRITE_TAC[VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN
335 MATCH_MP_TAC FUN_IN_IMAGE THEN ASM_MESON_TAC[];
336 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
337 ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_MUL_COMPONENT;
338 BASIS_COMPONENT; REAL_MUL_RID; REAL_LE_SUB_RADD; REAL_ADD_LID] THEN
339 REWRITE_TAC[IN_INTERVAL] THEN ASM_MESON_TAC[REAL_LE_TRANS];
340 MATCH_MP_TAC FUN_IN_IMAGE THEN ASM_MESON_TAC[];
341 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM; real_ge] THEN
342 ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_MUL_COMPONENT;
343 BASIS_COMPONENT; REAL_MUL_RID; REAL_LE_SUB_LADD; REAL_ADD_LID] THEN
344 REWRITE_TAC[IN_INTERVAL] THEN ASM_MESON_TAC[REAL_LE_TRANS];
345 REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
346 ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ] THEN
347 ASM_MESON_TAC[NEGLIGIBLE_INTERVAL; INTERIOR_CLOSED_INTERVAL];
348 REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
349 ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ] THEN
350 ASM_MESON_TAC[NEGLIGIBLE_INTERVAL; INTERIOR_CLOSED_INTERVAL];
351 ASM_REWRITE_TAC[IMAGE_EQ_EMPTY];
352 REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
353 ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ];
354 REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
355 ASM_REWRITE_TAC[DIVISION_OF_TRANSLATION];
356 MATCH_MP_TAC(REAL_ARITH
357 `a = a' /\ b = b' ==> a >= b + c ==> a' >= b' + c`) THEN
358 REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
359 REWRITE_TAC[MEASURE_TRANSLATION] THEN
360 REWRITE_TAC[GSYM VECTOR_ADD_ASSOC; SET_RULE
361 `{f x y | x IN IMAGE g s /\ y IN t} =
362 {f (g x) y | x IN s /\ y IN t}`] THEN
364 `{a + x + y:real^N | x IN s /\ y IN t} =
365 IMAGE (\z. a + z) {x + y | x IN s /\ y IN t}`] THEN
366 REWRITE_TAC[MEASURE_TRANSLATION]])]] THEN
369 CARD d1 + CARD d2 = n /\
370 1 <= k /\ k <= dimindex(:N) /\ ~(i = j) /\
371 i IN d1 /\ i SUBSET {x:real^N | x$k <= &0} /\ ~(negligible i) /\
372 j IN d1 /\ j SUBSET {x | x$k >= &0} /\ ~(negligible j) /\
373 measure(t INTER {x | x$k <= &0}) / measure t =
374 measure(s INTER {x | x$k <= &0}) / measure s /\
375 measure(t INTER {x | x$k >= &0}) / measure t =
376 measure(s INTER {x | x$k >= &0}) / measure s /\
377 ~(s = {}) /\ ~(t = {}) /\ ~(negligible s) /\ ~(negligible t) /\
378 d1 division_of s /\ d2 division_of t
379 ==> root(dimindex (:N)) (measure {x + y | x IN s /\ y IN t}) >=
380 root(dimindex (:N)) (measure s) + root(dimindex (:N)) (measure t)`
383 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN
384 REPEAT STRIP_TAC THEN
385 SUBGOAL_THEN `&0 < measure(s:real^N->bool) /\ &0 < measure(t:real^N->bool)`
386 STRIP_ASSUME_TAC THENL
387 [ASM_MESON_TAC[MEASURABLE_MEASURE_POS_LT; MEASURABLE_ELEMENTARY];
390 `?a. measure(t INTER {x:real^N | x$k <= a}) / measure t =
391 measure(s INTER {x:real^N | x$k <= &0}) / measure s`
392 STRIP_ASSUME_TAC THENL
394 `&0 <= measure(s INTER {x:real^N | x$k <= &0}) / measure s /\
395 measure(s INTER {x:real^N | x$k <= &0}) / measure s <= &1`
397 [ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_MUL_LZERO] THEN
399 [MATCH_MP_TAC MEASURE_POS_LE;
400 REWRITE_TAC[REAL_MUL_LID] THEN MATCH_MP_TAC MEASURE_SUBSET THEN
401 REPEAT CONJ_TAC THENL
403 ASM_MESON_TAC[MEASURABLE_ELEMENTARY];
405 MATCH_MP_TAC MEASURABLE_COMPACT THEN
406 MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
407 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE] THEN
408 ASM_MESON_TAC[ELEMENTARY_COMPACT];
409 SPEC_TAC(`measure(s INTER {x:real^N | x$k <= &0}) / measure s`,
411 X_GEN_TAC `u:real` THEN STRIP_TAC THEN
412 SUBGOAL_THEN `?b:real. &0 < b /\ !x:real^N. x IN t ==> abs(x$k) <= b`
413 STRIP_ASSUME_TAC THENL
414 [SUBGOAL_THEN `bounded(t:real^N->bool)` MP_TAC THENL
415 [ASM_MESON_TAC[ELEMENTARY_BOUNDED]; REWRITE_TAC[BOUNDED_POS]] THEN
416 MATCH_MP_TAC MONO_EXISTS THEN
417 ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LE_TRANS];
420 `?a. a IN real_interval[--b,b] /\
421 measure (t INTER {x:real^N | x$k <= a}) / measure t = u`
422 (fun th -> MESON_TAC[th]) THEN
423 MATCH_MP_TAC REAL_IVT_INCREASING THEN REPEAT CONJ_TAC THENL
426 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
427 `&0 <= u ==> x = &0 ==> x <= u`)) THEN
428 REWRITE_TAC[real_div; REAL_ENTIRE] THEN DISJ1_TAC THEN
429 MATCH_MP_TAC MEASURE_EQ_0 THEN
430 MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
431 EXISTS_TAC `{x:real^N | x$k = --b}` THEN
432 ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
433 SIMP_TAC[SUBSET; IN_INTER; IN_ELIM_THM; GSYM REAL_LE_ANTISYM] THEN
434 ASM_MESON_TAC[REAL_ARITH `abs x <= b ==> --b <= x`];
435 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
436 `u <= &1 ==> x = &1 ==> u <= x`)) THEN
437 ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_MUL_LID] THEN
438 AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM] THEN
439 ASM_MESON_TAC[REAL_ARITH `abs x <= b ==> x <= b`]] THEN
440 REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
441 REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
442 GEN_TAC THEN DISCH_TAC THEN
443 MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
444 MATCH_MP_TAC REAL_CONTINUOUS_MEASURE_IN_HALFSPACE_LE THEN
445 ASM_MESON_TAC[MEASURABLE_ELEMENTARY];
447 FIRST_X_ASSUM(MP_TAC o SPECL
448 [`d1:(real^N->bool)->bool`;
449 `IMAGE (IMAGE (\x:real^N. x - a % basis k)) d2`;
451 `IMAGE (\x:real^N. x - a % basis k) t`;
452 `i:real^N->bool`; `j:real^N->bool`; `k:num`]) THEN
453 ASM_REWRITE_TAC[] THEN
454 ONCE_REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
455 ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ; DIVISION_OF_TRANSLATION] THEN
456 ASM_REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ANTS_TAC THENL
458 [EXPAND_TAC "n" THEN AP_TERM_TAC THEN
459 MATCH_MP_TAC CARD_IMAGE_INJ THEN
460 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[DIVISION_OF_FINITE]] THEN
462 `(!x y. Q x y ==> R x y)
463 ==> (!x y. P x /\ P y /\ Q x y ==> R x y)`) THEN
464 REWRITE_TAC[INJECTIVE_IMAGE] THEN VECTOR_ARITH_TAC;
467 `IMAGE (\x. --(a % basis k) + x) t INTER {x:real^N | x$k >= &0} =
468 IMAGE (\x. --(a % basis k) + x) (t INTER {x | x$k >= a}) /\
469 IMAGE (\x. --(a % basis k) + x) t INTER {x:real^N | x$k <= &0} =
470 IMAGE (\x. --(a % basis k) + x) (t INTER {x | x$k <= a})`
471 (CONJUNCTS_THEN SUBST1_TAC) THENL
473 MATCH_MP_TAC(SET_RULE
474 `!g. (!x. f(x) IN s' <=> x IN s) /\ (!x. g(f x) = x)
475 ==> IMAGE f t INTER s' = IMAGE f (t INTER s)`) THEN
476 ASM_SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
477 BASIS_COMPONENT; VECTOR_NEG_COMPONENT] THEN
478 EXISTS_TAC `\x:real^N. a % basis k + x` THEN
479 (CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);
481 REWRITE_TAC[MEASURE_TRANSLATION] THEN MATCH_MP_TAC(REAL_FIELD
482 `&0 < s /\ &0 < t /\ t' / t = s' / s /\ s' + s'' = s /\ t' + t'' = t
483 ==> t' / t = s' / s /\ t'' / t = s'' / s`) THEN
484 ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
485 MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNION_EQ THEN
486 (REPEAT CONJ_TAC THENL
487 [MATCH_MP_TAC MEASURABLE_COMPACT THEN
488 MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
489 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
490 CLOSED_HALFSPACE_COMPONENT_GE] THEN
491 ASM_MESON_TAC[ELEMENTARY_COMPACT];
492 MATCH_MP_TAC MEASURABLE_COMPACT THEN
493 MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
494 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
495 CLOSED_HALFSPACE_COMPONENT_GE] THEN
496 ASM_MESON_TAC[ELEMENTARY_COMPACT];
497 MATCH_MP_TAC(SET_RULE
499 ==> s INTER {x | P x} UNION s INTER {x | Q x} = s`) THEN
501 REWRITE_TAC[SET_RULE `(t INTER {x | P x}) INTER (t INTER {x | Q x}) =
502 t INTER {x | P x /\ Q x}`] THEN
503 MATCH_MP_TAC(MESON[NEGLIGIBLE_SUBSET; INTER_SUBSET]
504 `negligible t ==> negligible(s INTER t)`) THEN
505 REWRITE_TAC[REAL_ARITH `x <= a /\ x >= a <=> x = a`] THEN
506 ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE]]);
507 REWRITE_TAC[MEASURE_TRANSLATION] THEN MATCH_MP_TAC(REAL_ARITH
508 `a' = a ==> a' >= b ==> a >= b`) THEN AP_TERM_TAC THEN
510 `{f x y | x IN s /\ y IN IMAGE g t} =
511 {f x (g y) | x IN s /\ y IN t}`] THEN
512 ONCE_REWRITE_TAC[VECTOR_ARITH `x + a + y:real^N = a + x + y`] THEN
514 `{a + x + y:real^N | x IN s /\ y IN t} =
515 IMAGE (\z. a + z) {x + y | x IN s /\ y IN t}`] THEN
516 REWRITE_TAC[MEASURE_TRANSLATION]]] THEN
517 REPEAT STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
518 SUBGOAL_THEN `measurable(s:real^N->bool) /\ measurable(t:real^N->bool)`
519 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[MEASURABLE_ELEMENTARY]; ALL_TAC] THEN
520 SUBGOAL_THEN `measurable {x + y:real^N | x IN s /\ y IN t}` ASSUME_TAC THENL
521 [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
522 ASM_MESON_TAC[ELEMENTARY_COMPACT];
524 SUBGOAL_THEN `&0 < measure(s:real^N->bool) /\ &0 < measure(t:real^N->bool)`
525 STRIP_ASSUME_TAC THENL
526 [ASM_MESON_TAC[MEASURABLE_MEASURE_POS_LT]; ALL_TAC] THEN
527 SUBGOAL_THEN `FINITE(d1:(real^N->bool)->bool) /\
528 FINITE(d2:(real^N->bool)->bool)`
529 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[DIVISION_OF_FINITE]; ALL_TAC] THEN
530 W(MP_TAC o PART_MATCH (lhs o rand) REAL_LE_ROOT o snd) THEN
531 ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; ROOT_POS_LE; REAL_LE_ADD] THEN
532 DISCH_THEN SUBST1_TAC THEN
533 ABBREV_TAC `dl = {l INTER {x:real^N | x$k <= &0} |l|
534 l IN d1 DELETE j /\ ~(l INTER {x | x$k <= &0} = {})}` THEN
535 ABBREV_TAC `dr = {l INTER {x:real^N | x$k >= &0} |l|
536 l IN d1 DELETE i /\ ~(l INTER {x | x$k >= &0} = {})}` THEN
537 MATCH_MP_TAC REAL_LE_TRANS THEN
539 `measure {x + y:real^N | x IN UNIONS dl /\ y IN (t INTER {x | x$k <= &0})} +
540 measure {x + y | x IN UNIONS dr /\ y IN (t INTER {x | x$k >= &0})}` THEN
543 MATCH_MP_TAC REAL_LE_TRANS THEN
545 `measure {x + y:real^N | x IN (s INTER {x | x$k <= &0}) /\
546 y IN (t INTER {x | x$k <= &0})} +
547 measure {x + y:real^N | x IN (s INTER {x | x$k >= &0}) /\
548 y IN (t INTER {x | x$k >= &0})}` THEN
550 [MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THEN
551 (MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
552 [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
554 [MATCH_MP_TAC COMPACT_UNIONS THEN
555 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
556 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
557 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
558 ASM_SIMP_TAC[IN_DELETE; FINITE_DELETE; FINITE_IMAGE;
559 FINITE_RESTRICT; IMP_CONJ] THEN
560 REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
561 FIRST_ASSUM(fun th ->
562 GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
563 ASM_SIMP_TAC[INTERVAL_SPLIT; COMPACT_INTERVAL];
564 MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
565 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
566 CLOSED_HALFSPACE_COMPONENT_GE] THEN
567 ASM_MESON_TAC[ELEMENTARY_COMPACT]];
568 MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
569 CONJ_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
570 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
571 CLOSED_HALFSPACE_COMPONENT_GE] THEN
572 ASM_MESON_TAC[ELEMENTARY_COMPACT];
573 MATCH_MP_TAC(SET_RULE
574 `s SUBSET s' ==> {x + y:real^N | x IN s /\ y IN t} SUBSET
575 {x + y:real^N | x IN s' /\ y IN t}`) THEN
576 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
577 REWRITE_TAC[SUBSET; FORALL_IN_UNIONS] THEN
578 REWRITE_TAC[FORALL_IN_GSPEC; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
579 SIMP_TAC[IN_DELETE; IN_INTER; IN_ELIM_THM] THEN
580 RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN
581 ASM_MESON_TAC[IN_UNIONS]]);
584 `s = (s INTER {x:real^N | x$k <= &0}) UNION (s INTER {x | x$k >= &0}) /\
585 t = (t INTER {x:real^N | x$k <= &0}) UNION (t INTER {x | x$k >= &0})`
587 [CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
589 ==> s = (s INTER {x | P x}) UNION (s INTER {x | Q x})`) THEN
592 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th])] THEN
593 W(MP_TAC o PART_MATCH (rand o rand)
594 MEASURE_NEGLIGIBLE_UNION o lhand o snd) THEN
596 [REPEAT(CONJ_TAC THENL
597 [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
598 CONJ_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
599 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
600 CLOSED_HALFSPACE_COMPONENT_GE] THEN
601 ASM_MESON_TAC[ELEMENTARY_COMPACT];
603 MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
604 EXISTS_TAC `{x:real^N | x$k = &0}` THEN
605 ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
606 REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN MATCH_MP_TAC(SET_RULE
607 `s SUBSET {x | P x} /\ t SUBSET {x | Q x}
608 ==> (s INTER t) SUBSET {x | P x /\ Q x}`) THEN
609 REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN
610 SIMP_TAC[IN_INTER; IN_ELIM_THM; REAL_LE_ADD; VECTOR_ADD_COMPONENT;
611 real_ge; REAL_ARITH `x <= &0 /\ y <= &0 ==> x + y <= &0`];
612 DISCH_THEN(SUBST1_TAC o SYM)] THEN
613 MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
614 [MATCH_MP_TAC MEASURABLE_UNION THEN CONJ_TAC THEN
615 MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
616 CONJ_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
617 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
618 CLOSED_HALFSPACE_COMPONENT_GE] THEN
619 ASM_MESON_TAC[ELEMENTARY_COMPACT];
620 MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
621 CONJ_TAC THEN MATCH_MP_TAC COMPACT_UNION THEN CONJ_TAC THEN
622 MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
623 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
624 CLOSED_HALFSPACE_COMPONENT_GE] THEN
625 ASM_MESON_TAC[ELEMENTARY_COMPACT];
628 `&0 < measure(s INTER {x:real^N | x$k <= &0}) /\
629 &0 < measure(s INTER {x:real^N | x$k >= &0})`
630 STRIP_ASSUME_TAC THENL
631 [ASM_SIMP_TAC[MEASURABLE_MEASURE_POS_LT; MEASURABLE_INTER_HALFSPACE_LE;
632 MEASURABLE_INTER_HALFSPACE_GE] THEN
634 [UNDISCH_TAC `~negligible(i:real^N->bool)`;
635 UNDISCH_TAC `~negligible(j:real^N->bool)`] THEN
636 REWRITE_TAC[CONTRAPOS_THM] THEN MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT]
637 NEGLIGIBLE_SUBSET) THEN
638 ASM_REWRITE_TAC[SUBSET_INTER] THEN
639 UNDISCH_TAC `d1 division_of (s:real^N->bool)` THEN
640 REWRITE_TAC[division_of] THEN ASM SET_TAC[];
642 FIRST_X_ASSUM(fun th ->
643 MP_TAC(SPECL [`dl:(real^N->bool)->bool`;
644 `{l INTER {x:real^N | x$k <= &0} |l|
645 l IN d2 /\ ~(l INTER {x | x$k <= &0} = {})}`;
646 `UNIONS dl :real^N->bool`;
647 `t INTER {x:real^N | x$k <= &0}`] th) THEN
648 MP_TAC(SPECL [`dr:(real^N->bool)->bool`;
649 `{l INTER {x:real^N | x$k >= &0} |l|
650 l IN d2 /\ ~(l INTER {x | x$k >= &0} = {})}`;
651 `UNIONS dr :real^N->bool`;
652 `t INTER {x:real^N | x$k >= &0}`] th)) THEN
653 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
654 [REPEAT CONJ_TAC THENL
655 [EXPAND_TAC "n" THEN MATCH_MP_TAC LTE_ADD2 THEN
656 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
657 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
658 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
660 [MATCH_MP_TAC LET_TRANS THEN
661 EXISTS_TAC `CARD(d1 DELETE (i:real^N->bool))` THEN CONJ_TAC THENL
662 [ALL_TAC; MATCH_MP_TAC CARD_PSUBSET THEN ASM SET_TAC[]];
664 MATCH_MP_TAC(ARITH_RULE
665 `CARD {x | x IN IMAGE f s /\ P x} <= CARD(IMAGE f s) /\
666 CARD(IMAGE f s) <= CARD s
667 ==> CARD {x | x IN IMAGE f s /\ P x} <= CARD s`) THEN
668 ASM_SIMP_TAC[CARD_IMAGE_LE; FINITE_DELETE] THEN
669 MATCH_MP_TAC CARD_SUBSET THEN
670 ASM_SIMP_TAC[FINITE_IMAGE; FINITE_DELETE] THEN SET_TAC[];
671 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_UNIONS] THEN
672 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
673 EXISTS_TAC `j INTER {x:real^N | x$k >= &0}` THEN
674 REWRITE_TAC[RIGHT_EXISTS_AND_THM; MEMBER_NOT_EMPTY] THEN
675 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
676 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
677 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
678 REWRITE_TAC[IN_ELIM_THM; IN_IMAGE; IN_DELETE; GSYM CONJ_ASSOC] THEN
680 [EXISTS_TAC `j:real^N->bool` THEN ASM_REWRITE_TAC[];
681 MATCH_MP_TAC(SET_RULE
682 `~(s = {}) /\ s SUBSET t ==> ~(s INTER t = {})`) THEN
683 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[division_of]];
685 UNDISCH_TAC `measure (t INTER {x:real^N | x$k >= &0}) / measure t =
686 measure (s INTER {x:real^N | x$k >= &0}) / measure s` THEN
687 ASM_SIMP_TAC[MEASURE_EMPTY; REAL_EQ_RDIV_EQ] THEN
688 REWRITE_TAC[real_div; REAL_MUL_LZERO] THEN
689 CONV_TAC(RAND_CONV SYM_CONV) THEN ASM_SIMP_TAC[REAL_LT_IMP_NZ];
690 REWRITE_TAC[division_of] THEN
691 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
692 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
693 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
694 ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
695 REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
696 REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
698 [FIRST_ASSUM(fun th ->
699 GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
700 REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
701 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
702 [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
703 MATCH_MP_TAC(SET_RULE
704 `x IN s ==> x SUBSET UNIONS s`) THEN
706 REPEAT STRIP_TAC THEN
707 MATCH_MP_TAC(SET_RULE
708 `interior(s) INTER interior(s') = {} /\
709 interior(s INTER t) SUBSET interior s /\
710 interior(s' INTER t) SUBSET interior s'
711 ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
712 SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
713 ASM_MESON_TAC[division_of]];
714 REWRITE_TAC[division_of] THEN
715 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
716 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
717 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
718 ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
719 REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
720 REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
721 REPEAT CONJ_TAC THENL
722 [FIRST_ASSUM(fun th ->
723 GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
724 REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
725 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
726 [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
727 MATCH_MP_TAC(SET_RULE
728 `s SUBSET t ==> s INTER u SUBSET t INTER u`) THEN
729 RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN ASM_MESON_TAC[];
730 REPEAT STRIP_TAC THEN
731 MATCH_MP_TAC(SET_RULE
732 `interior(s) INTER interior(s') = {} /\
733 interior(s INTER t) SUBSET interior s /\
734 interior(s' INTER t) SUBSET interior s'
735 ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
736 SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
737 ASM_MESON_TAC[division_of];
738 REWRITE_TAC[SET_RULE `{x | x IN s /\ ~(x = a)} = s DELETE a`] THEN
739 GEN_REWRITE_TAC LAND_CONV [SET_RULE `s = {} UNION s`] THEN
740 REWRITE_TAC[GSYM UNIONS_INSERT] THEN
741 REWRITE_TAC[SET_RULE `x INSERT (s DELETE x) = x INSERT s`] THEN
742 REWRITE_TAC[UNIONS_INSERT; UNION_EMPTY] THEN
743 REWRITE_TAC[GSYM SIMPLE_IMAGE; GSYM INTER_UNIONS] THEN
744 AP_THM_TAC THEN AP_TERM_TAC THEN ASM_MESON_TAC[division_of]]];
746 ONCE_REWRITE_TAC[TAUT `p ==> q ==> r <=> q ==> p ==> r`] THEN ANTS_TAC THENL
747 [REPEAT CONJ_TAC THENL
748 [EXPAND_TAC "n" THEN MATCH_MP_TAC LTE_ADD2 THEN
749 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
750 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
751 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
753 [MATCH_MP_TAC LET_TRANS THEN
754 EXISTS_TAC `CARD(d1 DELETE (j:real^N->bool))` THEN CONJ_TAC THENL
755 [ALL_TAC; MATCH_MP_TAC CARD_PSUBSET THEN ASM SET_TAC[]];
757 MATCH_MP_TAC(ARITH_RULE
758 `CARD {x | x IN IMAGE f s /\ P x} <= CARD(IMAGE f s) /\
759 CARD(IMAGE f s) <= CARD s
760 ==> CARD {x | x IN IMAGE f s /\ P x} <= CARD s`) THEN
761 ASM_SIMP_TAC[CARD_IMAGE_LE; FINITE_DELETE] THEN
762 MATCH_MP_TAC CARD_SUBSET THEN
763 ASM_SIMP_TAC[FINITE_IMAGE; FINITE_DELETE] THEN SET_TAC[];
764 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_UNIONS] THEN
765 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
766 EXISTS_TAC `i INTER {x:real^N | x$k <= &0}` THEN
767 REWRITE_TAC[RIGHT_EXISTS_AND_THM; MEMBER_NOT_EMPTY] THEN
768 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
769 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
770 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
771 REWRITE_TAC[IN_ELIM_THM; IN_IMAGE; IN_DELETE; GSYM CONJ_ASSOC] THEN
773 [EXISTS_TAC `i:real^N->bool` THEN ASM_REWRITE_TAC[];
774 MATCH_MP_TAC(SET_RULE
775 `~(s = {}) /\ s SUBSET t ==> ~(s INTER t = {})`) THEN
776 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[division_of]];
778 UNDISCH_TAC `measure (t INTER {x:real^N | x$k <= &0}) / measure t =
779 measure (s INTER {x:real^N | x$k <= &0}) / measure s` THEN
780 ASM_SIMP_TAC[MEASURE_EMPTY; REAL_EQ_RDIV_EQ] THEN
781 REWRITE_TAC[real_div; REAL_MUL_LZERO] THEN
782 CONV_TAC(RAND_CONV SYM_CONV) THEN ASM_SIMP_TAC[REAL_LT_IMP_NZ];
783 REWRITE_TAC[division_of] THEN
784 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
785 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
786 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
787 ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
788 REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
789 REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
791 [FIRST_ASSUM(fun th ->
792 GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
793 REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
794 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
795 [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
796 MATCH_MP_TAC(SET_RULE
797 `x IN s ==> x SUBSET UNIONS s`) THEN
799 REPEAT STRIP_TAC THEN
800 MATCH_MP_TAC(SET_RULE
801 `interior(s) INTER interior(s') = {} /\
802 interior(s INTER t) SUBSET interior s /\
803 interior(s' INTER t) SUBSET interior s'
804 ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
805 SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
806 ASM_MESON_TAC[division_of]];
807 REWRITE_TAC[division_of] THEN
808 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
809 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
810 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
811 ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
812 REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
813 REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
814 REPEAT CONJ_TAC THENL
815 [FIRST_ASSUM(fun th ->
816 GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
817 REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
818 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
819 [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
820 MATCH_MP_TAC(SET_RULE
821 `s SUBSET t ==> s INTER u SUBSET t INTER u`) THEN
822 RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN ASM_MESON_TAC[];
823 REPEAT STRIP_TAC THEN
824 MATCH_MP_TAC(SET_RULE
825 `interior(s) INTER interior(s') = {} /\
826 interior(s INTER t) SUBSET interior s /\
827 interior(s' INTER t) SUBSET interior s'
828 ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
829 SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
830 ASM_MESON_TAC[division_of];
831 REWRITE_TAC[SET_RULE `{x | x IN s /\ ~(x = a)} = s DELETE a`] THEN
832 GEN_REWRITE_TAC LAND_CONV [SET_RULE `s = {} UNION s`] THEN
833 REWRITE_TAC[GSYM UNIONS_INSERT] THEN
834 REWRITE_TAC[SET_RULE `x INSERT (s DELETE x) = x INSERT s`] THEN
835 REWRITE_TAC[UNIONS_INSERT; UNION_EMPTY] THEN
836 REWRITE_TAC[GSYM SIMPLE_IMAGE; GSYM INTER_UNIONS] THEN
837 AP_THM_TAC THEN AP_TERM_TAC THEN ASM_MESON_TAC[division_of]]];
839 REWRITE_TAC[real_ge; IMP_IMP] THEN
841 `compact(UNIONS dl:real^N->bool) /\ compact(UNIONS dr:real^N->bool)`
842 STRIP_ASSUME_TAC THENL
843 [CONJ_TAC THEN MATCH_MP_TAC COMPACT_UNIONS THEN
844 MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
845 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
846 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
847 ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
848 REWRITE_TAC[IMP_CONJ; IN_ELIM_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
849 REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
850 REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
851 CLOSED_HALFSPACE_COMPONENT_GE] THEN
852 ASM_MESON_TAC[division_of; COMPACT_INTERVAL];
855 `measurable(UNIONS dl:real^N->bool) /\
856 measurable(UNIONS dr:real^N->bool)`
857 STRIP_ASSUME_TAC THENL [ASM_SIMP_TAC[MEASURABLE_COMPACT]; ALL_TAC] THEN
859 `measurable { x + y:real^N |
860 x IN UNIONS dl /\ y IN t INTER {x | x$k <= &0}} /\
861 measurable { x + y:real^N |
862 x IN UNIONS dr /\ y IN t INTER {x | &0 <= x$k}}`
863 STRIP_ASSUME_TAC THENL
864 [CONJ_TAC THEN MATCH_MP_TAC MEASURABLE_COMPACT THEN
865 MATCH_MP_TAC COMPACT_SUMS THEN ASM_REWRITE_TAC[] THEN
866 MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
867 REWRITE_TAC[REAL_ARITH `&0 <= x <=> x >= &0`;
868 CLOSED_HALFSPACE_COMPONENT_LE; CLOSED_HALFSPACE_COMPONENT_GE] THEN
869 ASM_MESON_TAC[ELEMENTARY_COMPACT];
871 ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
872 [REAL_LE_ROOT; DIMINDEX_NONZERO; REAL_LE_ADD; ROOT_POS_LE;
873 MEASURE_POS_LE; MEASURABLE_INTER_HALFSPACE_LE;
874 MEASURABLE_INTER_HALFSPACE_GE; REAL_ARITH `&0 <= x <=> x >= &0`] THEN
875 MATCH_MP_TAC(REAL_ARITH
876 `x <= a' + b' ==> a' <= a /\ b' <= b ==> x <= a + b`) THEN
878 `measure(UNIONS dl :real^N->bool) =
879 measure(s INTER {x:real^N | x$k <= &0}) /\
880 measure(UNIONS dr :real^N->bool) =
881 measure(s INTER {x:real^N | x$k >= &0})`
882 (CONJUNCTS_THEN SUBST1_TAC)
884 [MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
885 ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
886 {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
887 REWRITE_TAC[SET_RULE `{x | x IN s /\ ~(x = a)} = s DELETE a`] THEN
889 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SET_RULE `s = {} UNION s`] THEN
890 REWRITE_TAC[GSYM UNIONS_INSERT] THEN
891 REWRITE_TAC[SET_RULE `x INSERT (s DELETE x) = x INSERT s`] THEN
892 REWRITE_TAC[UNIONS_INSERT; UNION_EMPTY] THEN
893 REWRITE_TAC[GSYM SIMPLE_IMAGE; GSYM INTER_UNIONS] THEN
894 MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN
895 MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
896 EXISTS_TAC `{x:real^N | x$k = &0}` THEN
897 ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
898 MATCH_MP_TAC(SET_RULE
899 `s SUBSET t /\ t DIFF s SUBSET u
900 ==> (s DIFF t UNION t DIFF s) SUBSET u`) THEN
901 REWRITE_TAC[SET_RULE `s INTER u DIFF t INTER u = (s DIFF t) INTER u`] THEN
902 (SUBGOAL_THEN `s:real^N->bool = UNIONS d1` SUBST1_TAC THENL
903 [ASM_MESON_TAC[division_of]; ALL_TAC] THEN
904 CONJ_TAC THENL [SET_TAC[]; ALL_TAC]) THEN
905 REWRITE_TAC[GSYM REAL_LE_ANTISYM; real_ge; SET_RULE
906 `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`]
908 [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> s INTER u SUBSET u INTER t`);
909 MATCH_MP_TAC(SET_RULE `s SUBSET t ==> s INTER u SUBSET t INTER u`)] THEN
910 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN
911 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP
912 (REWRITE_RULE[IMP_CONJ_ALT] SUBSET_TRANS)) THEN
916 `root (dimindex (:N)) (measure (s INTER {x:real^N | x$k <= &0})) +
917 root (dimindex (:N)) (measure (t INTER {x:real^N | x$k <= &0})) =
918 root (dimindex (:N)) (measure (s INTER {x | x$k <= &0})) *
919 (&1 + root (dimindex (:N)) (measure (t INTER {x | x$k <= &0})) /
920 root (dimindex (:N)) (measure (s INTER {x | x$k <= &0}))) /\
921 root (dimindex (:N)) (measure (s INTER {x:real^N | x$k >= &0})) +
922 root (dimindex (:N)) (measure (t INTER {x:real^N | x$k >= &0})) =
923 root (dimindex (:N)) (measure (s INTER {x | x$k >= &0})) *
924 (&1 + root (dimindex (:N)) (measure (t INTER {x | x$k >= &0})) /
925 root (dimindex (:N)) (measure (s INTER {x | x$k >= &0})))`
926 (CONJUNCTS_THEN SUBST1_TAC) THENL
928 MATCH_MP_TAC(REAL_FIELD `&0 < s ==> s + t = s * (&1 + t / s)`) THEN
929 ASM_SIMP_TAC[ROOT_POS_LT; DIMINDEX_NONZERO];
931 ASM_SIMP_TAC[DIMINDEX_NONZERO; GSYM REAL_ROOT_DIV; MEASURE_POS_LE;
932 MEASURABLE_INTER_HALFSPACE_LE; MEASURABLE_INTER_HALFSPACE_GE] THEN
934 `measure(t INTER {x:real^N | x$k <= &0}) /
935 measure(s INTER {x:real^N | x$k <= &0}) = measure t / measure s /\
936 measure(t INTER {x:real^N | x$k >= &0}) /
937 measure(s INTER {x:real^N | x$k >= &0}) = measure t / measure s`
938 (CONJUNCTS_THEN SUBST1_TAC) THENL
939 [MATCH_MP_TAC(REAL_FIELD
940 `tn / t = sn / s /\ tp / t = sp / s /\
941 &0 < sp /\ &0 < sn /\ &0 < s /\ &0 < t
942 ==> tn / sn = t / s /\ tp / sp = t / s`) THEN
945 REWRITE_TAC[GSYM REAL_ADD_RDISTRIB; REAL_POW_MUL] THEN
946 ASM_SIMP_TAC[REAL_POW_ROOT; DIMINDEX_NONZERO; MEASURE_POS_LE;
947 MEASURABLE_INTER_HALFSPACE_LE; MEASURABLE_INTER_HALFSPACE_GE] THEN
949 `measure (s INTER {x | x$k <= &0}) + measure (s INTER {x | x$k >= &0}) =
950 root (dimindex(:N)) (measure(s:real^N->bool)) pow (dimindex(:N))`
952 [ASM_SIMP_TAC[REAL_POW_ROOT; DIMINDEX_NONZERO; REAL_LT_IMP_LE] THEN
953 MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNION_EQ THEN
954 ASM_SIMP_TAC[MEASURABLE_INTER_HALFSPACE_LE;
955 MEASURABLE_INTER_HALFSPACE_GE] THEN
957 [REWRITE_TAC[EXTENSION; IN_UNION; IN_INTER; IN_ELIM_THM] THEN
958 X_GEN_TAC `x:real^N` THEN ASM_CASES_TAC `(x:real^N) IN s` THEN
959 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
960 MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
961 EXISTS_TAC `{x:real^N | x$k = &0}` THEN
962 ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
963 REWRITE_TAC[GSYM REAL_LE_ANTISYM; real_ge] THEN SET_TAC[]];
964 ASM_SIMP_TAC[GSYM REAL_ROOT_MUL; MEASURE_POS_LE; DIMINDEX_NONZERO;
965 REAL_LE_DIV; GSYM REAL_POW_MUL;
966 REAL_ADD_LDISTRIB; REAL_MUL_RID] THEN
967 ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_LE_REFL]]);;
969 (* ------------------------------------------------------------------------- *)
970 (* Now for open sets. *)
971 (* ------------------------------------------------------------------------- *)
973 let BRUNN_MINKOWSKI_OPEN = prove
975 (s = {} <=> t = {}) /\ bounded s /\ open s /\ bounded t /\ open t
976 ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
977 >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,
978 REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
979 ASM_SIMP_TAC[SET_RULE `{x + y:real^N | x IN {} /\ y IN {}} = {}`;
980 REAL_LE_REFL; MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO;
981 real_ge; REAL_ADD_LID] THEN
983 MATCH_MP_TAC(ISPEC `atreal(&0) within {e | &0 <= e}` REALLIM_UBOUND) THEN
984 EXISTS_TAC `\e. root (dimindex(:N)) (measure(s:real^N->bool) - e) +
985 root (dimindex(:N)) (measure(t:real^N->bool) - e)` THEN
986 REPEAT CONJ_TAC THENL
987 [MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
989 `\e. (measure(s:real^N->bool) - e) rpow (inv(&(dimindex(:N)))) +
990 (measure(t:real^N->bool) - e) rpow (inv(&(dimindex(:N))))` THEN
991 REWRITE_TAC[] THEN CONJ_TAC THENL
992 [REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
993 EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
994 ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO;
995 MEASURE_OPEN_POS_LT] THEN
996 REPEAT STRIP_TAC THEN BINOP_TAC THEN CONV_TAC SYM_CONV THEN
997 MATCH_MP_TAC REAL_ROOT_RPOW THEN
998 REWRITE_TAC[DIMINDEX_NONZERO] THEN ASM_REAL_ARITH_TAC;
999 ASM_SIMP_TAC[REAL_ROOT_RPOW; MEASURE_OPEN_POS_LT; DIMINDEX_NONZERO;
1000 REAL_LT_IMP_LE] THEN
1001 MATCH_MP_TAC REALLIM_ADD THEN CONJ_TAC THEN
1002 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
1003 [REAL_ARITH `measure(s:real^N->bool) = measure s - &0`] THEN
1004 REWRITE_TAC[GSYM REAL_CONTINUOUS_WITHINREAL] THEN
1005 REWRITE_TAC[GSYM(REWRITE_CONV [o_DEF]
1006 `(\x. x rpow y) o (\e. s - e)`)] THEN
1007 MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE THEN
1008 ASM_SIMP_TAC[REAL_CONTINUOUS_SUB; REAL_CONTINUOUS_WITHIN_ID;
1009 REAL_CONTINUOUS_CONST] THEN
1010 MATCH_MP_TAC REAL_CONTINUOUS_WITHIN_RPOW THEN
1011 REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS]];
1012 W(MP_TAC o PART_MATCH (lhand o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
1015 [REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN REAL_ARITH_TAC;
1016 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[EXTENSION; IN_SING] THEN
1017 DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
1019 REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
1020 EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
1021 ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO;
1022 MEASURE_OPEN_POS_LT] THEN
1023 X_GEN_TAC `e:real` THEN REWRITE_TAC[real_abs] THEN
1024 ASM_CASES_TAC `&0 <= e` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1025 MAP_EVERY (fun l -> MP_TAC(ISPECL l OPEN_MEASURABLE_INNER_DIVISION))
1026 [[`t:real^N->bool`; `e:real`]; [`s:real^N->bool`; `e:real`]] THEN
1027 ASM_SIMP_TAC[MEASURABLE_OPEN; GSYM REAL_LT_SUB_RADD] THEN
1028 DISCH_THEN(X_CHOOSE_THEN `D:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
1029 DISCH_THEN(X_CHOOSE_THEN `E:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
1030 MP_TAC(ISPECL [`UNIONS D:real^N->bool`; `UNIONS E:real^N->bool`]
1031 BRUNN_MINKOWSKI_ELEMENTARY) THEN
1033 [ASM_MESON_TAC[MEASURE_EMPTY; REAL_ARITH `e < s ==> ~(s - e < &0)`];
1035 MATCH_MP_TAC(REAL_ARITH
1036 `s1 <= r1 /\ s2 <= r2 /\ rs <= s
1037 ==> rs >= r1 + r2 ==> s1 + s2 <= s`) THEN
1038 REPEAT CONJ_TAC THEN MATCH_MP_TAC ROOT_MONO_LE THEN
1039 ASM_SIMP_TAC[DIMINDEX_NONZERO; REAL_SUB_LE; REAL_LT_IMP_LE] THEN
1041 `measurable {x + y :real^N | x IN UNIONS D /\ y IN UNIONS E}`
1043 [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
1044 ASM_MESON_TAC[ELEMENTARY_COMPACT];
1045 MATCH_MP_TAC MEASURE_SUBSET] THEN
1046 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
1047 MATCH_MP_TAC MEASURABLE_OPEN THEN
1048 ASM_SIMP_TAC[BOUNDED_SUMS; OPEN_SUMS]]);;
1050 (* ------------------------------------------------------------------------- *)
1051 (* Now for convex sets. *)
1052 (* ------------------------------------------------------------------------- *)
1054 let BRUNN_MINKOWSKI_CONVEX = prove
1055 (`!s t:real^N->bool.
1056 (s = {} <=> t = {}) /\ bounded s /\ convex s /\ bounded t /\ convex t
1057 ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
1058 >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,
1059 REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
1060 ASM_SIMP_TAC[BRUNN_MINKOWSKI_OPEN; OPEN_EMPTY] THEN STRIP_TAC THEN
1061 ASM_SIMP_TAC[GSYM MEASURE_INTERIOR; NEGLIGIBLE_CONVEX_FRONTIER; real_ge] THEN
1062 ASM_CASES_TAC `interior s:real^N->bool = {}` THENL
1063 [ASM_SIMP_TAC[MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO; REAL_ADD_LID] THEN
1064 MATCH_MP_TAC ROOT_MONO_LE THEN
1065 ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_INTERIOR] THEN
1066 SUBGOAL_THEN `?a:real^N. a IN s` STRIP_ASSUME_TAC THENL
1067 [ASM SET_TAC[]; ALL_TAC] THEN
1068 MATCH_MP_TAC REAL_LE_TRANS THEN
1069 EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) t)` THEN CONJ_TAC THENL
1070 [ASM_SIMP_TAC[MEASURE_TRANSLATION; MEASURE_INTERIOR;
1071 NEGLIGIBLE_CONVEX_FRONTIER; REAL_LE_REFL];
1072 MATCH_MP_TAC MEASURE_SUBSET THEN
1073 ASM_SIMP_TAC[MEASURABLE_TRANSLATION_EQ; MEASURABLE_CONVEX;
1074 CONVEX_SUMS; BOUNDED_SUMS] THEN
1077 ASM_CASES_TAC `interior t:real^N->bool = {}` THENL
1078 [ASM_SIMP_TAC[MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO; REAL_ADD_RID] THEN
1079 MATCH_MP_TAC ROOT_MONO_LE THEN
1080 ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_INTERIOR] THEN
1081 SUBGOAL_THEN `?a:real^N. a IN t` STRIP_ASSUME_TAC THENL
1082 [ASM SET_TAC[]; ALL_TAC] THEN
1083 MATCH_MP_TAC REAL_LE_TRANS THEN
1084 EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) s)` THEN CONJ_TAC THENL
1085 [ASM_SIMP_TAC[MEASURE_TRANSLATION; MEASURE_INTERIOR;
1086 NEGLIGIBLE_CONVEX_FRONTIER; REAL_LE_REFL];
1087 MATCH_MP_TAC MEASURE_SUBSET THEN
1088 ASM_SIMP_TAC[MEASURABLE_TRANSLATION_EQ; MEASURABLE_CONVEX;
1089 CONVEX_SUMS; BOUNDED_SUMS] THEN
1090 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ADD_SYM] THEN
1093 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
1094 `root (dimindex (:N))
1095 (measure {x + y:real^N | x IN interior s /\ y IN interior t})` THEN
1096 ASM_SIMP_TAC[GSYM real_ge; BRUNN_MINKOWSKI_OPEN; BOUNDED_INTERIOR;
1098 REWRITE_TAC[real_ge] THEN MATCH_MP_TAC ROOT_MONO_LE THEN
1099 REWRITE_TAC[DIMINDEX_NONZERO] THEN MATCH_MP_TAC MEASURE_SUBSET THEN
1100 ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; BOUNDED_SUMS;
1101 MEASURABLE_CONVEX; BOUNDED_INTERIOR; CONVEX_SUMS; CONVEX_INTERIOR] THEN
1102 MATCH_MP_TAC(SET_RULE
1103 `s' SUBSET s /\ t' SUBSET t
1104 ==> {x + y:real^N | x IN s' /\ y IN t'} SUBSET
1105 {x + y | x IN s /\ y IN t}`) THEN
1106 REWRITE_TAC[INTERIOR_SUBSET]);;
1108 (* ------------------------------------------------------------------------- *)
1109 (* Now for compact sets. *)
1110 (* ------------------------------------------------------------------------- *)
1112 let INTERS_SUMS_CLOSED_BALL_SEQUENTIAL = prove
1115 ==> INTERS {{x + d | x IN s /\ d IN ball(vec 0,inv(&n + &1))} |
1117 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
1118 REWRITE_TAC[INTERS_GSPEC; IN_ELIM_THM; IN_UNIV] THEN
1119 X_GEN_TAC `x:real^N` THEN EQ_TAC THENL
1120 [ASM_CASES_TAC `(x:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
1121 MP_TAC(ISPECL [`s:real^N->bool`; `x:real^N`] SEPARATE_POINT_CLOSED) THEN
1122 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:real` THEN
1123 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1124 GEN_REWRITE_TAC LAND_CONV [REAL_ARCH_INV] THEN
1125 DISCH_THEN(X_CHOOSE_THEN `n:num` STRIP_ASSUME_TAC) THEN
1126 DISCH_THEN(MP_TAC o SPEC `n:num`) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN
1127 MAP_EVERY X_GEN_TAC [`y:real^N`; `e:real^N`] THEN
1128 REWRITE_TAC[IN_BALL_0] THEN STRIP_TAC THEN
1129 FIRST_X_ASSUM SUBST_ALL_TAC THEN
1130 FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N`) THEN
1131 ASM_REWRITE_TAC[NORM_ARITH `dist(y + e:real^N,y) = norm e`] THEN
1132 SUBGOAL_THEN `inv(&n + &1) <= inv(&n)` MP_TAC THENL
1133 [MATCH_MP_TAC REAL_LE_INV2 THEN
1134 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
1136 ASM_REAL_ARITH_TAC];
1137 DISCH_TAC THEN X_GEN_TAC `n:num` THEN
1138 MAP_EVERY EXISTS_TAC [`x:real^N`; `vec 0:real^N`] THEN
1139 ASM_REWRITE_TAC[CENTRE_IN_BALL; VECTOR_ADD_RID; REAL_LT_INV_EQ] THEN
1142 let MEASURE_SUMS_COMPACT_EPSILON = prove
1145 ==> ((\e. measure {x + d | x IN s /\ d IN ball(vec 0,e)})
1147 (atreal (&0) within {e | &0 <= e})`,
1148 REPEAT STRIP_TAC THEN
1150 `\n. {x + d:real^N | x IN s /\ d IN ball(vec 0,inv(&n + &1))}`
1151 HAS_MEASURE_NESTED_INTERS) THEN
1152 ASM_SIMP_TAC[INTERS_SUMS_CLOSED_BALL_SEQUENTIAL; COMPACT_IMP_CLOSED] THEN
1154 [ASM_SIMP_TAC[MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS;
1155 COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL] THEN
1156 GEN_TAC THEN MATCH_MP_TAC(SET_RULE
1158 ==> {x + y:real^N | x IN s /\ y IN t'} SUBSET
1159 {x + y | x IN s /\ y IN t}`) THEN
1160 MATCH_MP_TAC SUBSET_BALL THEN MATCH_MP_TAC REAL_LE_INV2 THEN
1161 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
1164 REWRITE_TAC[GSYM(REWRITE_RULE[o_DEF] TENDSTO_REAL)] THEN
1165 REWRITE_TAC[REALLIM_SEQUENTIALLY; REALLIM_WITHINREAL] THEN
1166 STRIP_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1167 FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1168 DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `inv(&N + &1)` THEN
1169 ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN
1170 CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
1171 X_GEN_TAC `d:real` THEN REWRITE_TAC[IN_ELIM_THM; REAL_SUB_RZERO] THEN
1172 ASM_CASES_TAC `abs d = d` THENL
1173 [FIRST_X_ASSUM SUBST1_TAC THEN STRIP_TAC; ASM_REAL_ARITH_TAC] THEN
1174 FIRST_X_ASSUM(MP_TAC o SPEC `N:num`) THEN REWRITE_TAC[LE_REFL] THEN
1175 MATCH_MP_TAC(REAL_ARITH
1176 `m <= m1 /\ m1 <= m2
1177 ==> abs(m2 - m) < e ==> abs(m1 - m) < e`) THEN
1178 CONJ_TAC THEN MATCH_MP_TAC MEASURE_SUBSET THEN
1179 ASM_SIMP_TAC[MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS;
1180 COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL]
1182 [REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `x:real^N` THEN
1183 DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`x:real^N`; `vec 0:real^N`] THEN
1184 ASM_REWRITE_TAC[CENTRE_IN_BALL; VECTOR_ADD_RID];
1185 MATCH_MP_TAC(SET_RULE
1187 ==> {x + y:real^N | x IN s /\ y IN t'} SUBSET
1188 {x + y | x IN s /\ y IN t}`) THEN
1189 MATCH_MP_TAC SUBSET_BALL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE]]);;
1191 let BRUNN_MINKOWSKI_COMPACT = prove
1192 (`!s t:real^N->bool.
1193 (s = {} <=> t = {}) /\ compact s /\ compact t
1194 ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
1195 >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,
1197 (`{ x + y:real^N | x IN {x + d | x IN s /\ d IN ball(vec 0,e)} /\
1198 y IN {y + d | y IN t /\ d IN ball(vec 0,e)}} =
1199 { z + d | z IN {x + y | x IN s /\ y IN t} /\ d IN ball(vec 0,&2 * e) }`,
1200 MATCH_MP_TAC SUBSET_ANTISYM THEN
1201 REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN
1202 REWRITE_TAC[IN_ELIM_THM; IN_BALL_0] THEN CONJ_TAC THENL
1203 [X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
1204 X_GEN_TAC `d:real^N` THEN DISCH_TAC THEN
1205 X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
1206 X_GEN_TAC `k:real^N` THEN DISCH_TAC THEN
1207 EXISTS_TAC `x + y:real^N` THEN EXISTS_TAC `d + k:real^N` THEN
1208 CONJ_TAC THENL [ALL_TAC; VECTOR_ARITH_TAC] THEN
1209 ASM_SIMP_TAC[NORM_ARITH
1210 `norm(d:real^N) < e /\ norm(k) < e ==> norm(d + k) < &2 * e`] THEN
1211 EXISTS_TAC `x:real^N` THEN EXISTS_TAC `y:real^N` THEN
1212 ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC;
1213 X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
1214 X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
1215 X_GEN_TAC `d:real^N` THEN DISCH_TAC THEN
1216 EXISTS_TAC `x + inv(&2) % d:real^N` THEN
1217 EXISTS_TAC `y + inv(&2) % d:real^N` THEN
1218 CONJ_TAC THENL [ALL_TAC; VECTOR_ARITH_TAC] THEN CONJ_TAC THENL
1219 [EXISTS_TAC `x:real^N`; EXISTS_TAC `y:real^N`] THEN
1220 EXISTS_TAC `inv(&2) % d:real^N` THEN
1221 ASM_REWRITE_TAC[NORM_MUL] THEN ASM_REAL_ARITH_TAC])
1223 (`(f ---> l) (atreal (&0) within {e | &0 <= e})
1224 ==> ((\e. f(&2 * e)) ---> l) (atreal (&0) within {e | &0 <= e})`,
1225 REWRITE_TAC[REALLIM_WITHINREAL] THEN DISCH_TAC THEN
1226 X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1227 FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1228 REWRITE_TAC[IN_ELIM_THM; REAL_SUB_RZERO] THEN
1229 DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
1230 EXISTS_TAC `d / &2` THEN ASM_REWRITE_TAC[REAL_HALF] THEN
1231 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
1232 ASM_REAL_ARITH_TAC) in
1233 REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
1234 ASM_SIMP_TAC[BRUNN_MINKOWSKI_OPEN; OPEN_EMPTY; BOUNDED_EMPTY] THEN
1235 STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
1236 MATCH_MP_TAC(ISPEC `atreal (&0) within {e | &0 <= e}` REALLIM_LE) THEN
1238 `\e. root (dimindex(:N))
1239 (measure {x + d:real^N | x IN s /\ d IN ball(vec 0,e)}) +
1241 (measure {x + d:real^N | x IN t /\ d IN ball(vec 0,e)})` THEN
1243 `\e. root (dimindex(:N))
1244 (measure { x + y:real^N |
1245 x IN {x + d | x IN s /\ d IN ball(vec 0,e)} /\
1246 y IN {y + d | y IN t /\ d IN ball(vec 0,e)}})` THEN
1247 REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
1248 [ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
1249 [REAL_ROOT_RPOW; DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_COMPACT;
1250 MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS;
1251 COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL] THEN
1252 MATCH_MP_TAC REALLIM_ADD THEN CONJ_TAC THEN MATCH_MP_TAC REALLIM_RPOW THEN
1253 REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
1254 MATCH_MP_TAC MEASURE_SUMS_COMPACT_EPSILON THEN ASM_REWRITE_TAC[];
1255 REWRITE_TAC[lemma1] THEN MATCH_MP_TAC lemma2 THEN
1256 ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 6)
1257 [REAL_ROOT_RPOW; DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_COMPACT;
1258 MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS; COMPACT_SUMS;
1259 COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL] THEN
1260 MATCH_MP_TAC REALLIM_RPOW THEN
1261 REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
1262 MATCH_MP_TAC MEASURE_SUMS_COMPACT_EPSILON THEN
1263 ASM_SIMP_TAC[COMPACT_SUMS];
1264 W(MP_TAC o PART_MATCH (lhand o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
1267 [REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN REAL_ARITH_TAC;
1268 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[EXTENSION; IN_SING] THEN
1269 DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
1271 MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `e:real` THEN
1272 REWRITE_TAC[GSYM real_ge] THEN
1273 MATCH_MP_TAC BRUNN_MINKOWSKI_OPEN THEN
1274 SIMP_TAC[OPEN_SUMS; OPEN_BALL] THEN
1275 ASM_SIMP_TAC[BOUNDED_SUMS; BOUNDED_BALL; COMPACT_IMP_BOUNDED] THEN
1278 (* ------------------------------------------------------------------------- *)
1279 (* Finally, for an arbitrary measurable set. In this general case, the *)
1280 (* measurability of the sum-set is needed as an additional hypothesis. *)
1281 (* ------------------------------------------------------------------------- *)
1283 let BRUNN_MINKOWSKI_MEASURABLE = prove
1284 (`!s t:real^N->bool.
1285 (s = {} <=> t = {}) /\ measurable s /\ measurable t /\
1286 measurable {x + y | x IN s /\ y IN t}
1287 ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
1288 >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,
1289 REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
1290 ASM_SIMP_TAC[BRUNN_MINKOWSKI_OPEN; OPEN_EMPTY; BOUNDED_EMPTY] THEN
1291 STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
1292 ASM_CASES_TAC `measure(s:real^N->bool) = &0` THENL
1293 [ASM_SIMP_TAC[ROOT_0; DIMINDEX_NONZERO; REAL_ADD_LID] THEN
1294 MATCH_MP_TAC ROOT_MONO_LE THEN
1295 ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE] THEN
1296 SUBGOAL_THEN `?a:real^N. a IN s` STRIP_ASSUME_TAC THENL
1297 [ASM SET_TAC[]; ALL_TAC] THEN
1298 MATCH_MP_TAC REAL_LE_TRANS THEN
1299 EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) t)` THEN CONJ_TAC THENL
1300 [ASM_SIMP_TAC[MEASURE_TRANSLATION; REAL_LE_REFL];
1301 MATCH_MP_TAC MEASURE_SUBSET THEN
1302 ASM_REWRITE_TAC[MEASURABLE_TRANSLATION_EQ] THEN
1305 ASM_CASES_TAC `measure(t:real^N->bool) = &0` THENL
1306 [ASM_SIMP_TAC[ROOT_0; DIMINDEX_NONZERO; REAL_ADD_RID] THEN
1307 MATCH_MP_TAC ROOT_MONO_LE THEN
1308 ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE] THEN
1309 SUBGOAL_THEN `?a:real^N. a IN t` STRIP_ASSUME_TAC THENL
1310 [ASM SET_TAC[]; ALL_TAC] THEN
1311 MATCH_MP_TAC REAL_LE_TRANS THEN
1312 EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) s)` THEN CONJ_TAC THENL
1313 [ASM_SIMP_TAC[MEASURE_TRANSLATION; REAL_LE_REFL];
1314 MATCH_MP_TAC MEASURE_SUBSET THEN
1315 ASM_REWRITE_TAC[MEASURABLE_TRANSLATION_EQ] THEN
1316 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ADD_SYM] THEN
1320 `&0 < measure(s:real^N->bool) /\
1321 &0 < measure(t:real^N->bool)`
1322 STRIP_ASSUME_TAC THENL
1323 [ASM_MESON_TAC[MEASURABLE_MEASURE_POS_LT; MEASURABLE_MEASURE_EQ_0];
1325 MATCH_MP_TAC(ISPEC `atreal(&0) within {e | &0 <= e}` REALLIM_UBOUND) THEN
1326 EXISTS_TAC `\e. root (dimindex(:N)) (measure(s:real^N->bool) - e) +
1327 root (dimindex(:N)) (measure(t:real^N->bool) - e)` THEN
1328 REPEAT CONJ_TAC THENL
1329 [MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
1331 `\e. (measure(s:real^N->bool) - e) rpow (inv(&(dimindex(:N)))) +
1332 (measure(t:real^N->bool) - e) rpow (inv(&(dimindex(:N))))` THEN
1333 REWRITE_TAC[] THEN CONJ_TAC THENL
1334 [REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
1335 EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
1336 ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO;
1337 MEASURE_OPEN_POS_LT] THEN
1338 REPEAT STRIP_TAC THEN BINOP_TAC THEN CONV_TAC SYM_CONV THEN
1339 MATCH_MP_TAC REAL_ROOT_RPOW THEN
1340 REWRITE_TAC[DIMINDEX_NONZERO] THEN ASM_REAL_ARITH_TAC;
1341 ASM_SIMP_TAC[REAL_ROOT_RPOW; MEASURE_OPEN_POS_LT; DIMINDEX_NONZERO;
1342 REAL_LT_IMP_LE] THEN
1343 MATCH_MP_TAC REALLIM_ADD THEN CONJ_TAC THEN
1344 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
1345 [REAL_ARITH `measure(s:real^N->bool) = measure s - &0`] THEN
1346 REWRITE_TAC[GSYM REAL_CONTINUOUS_WITHINREAL] THEN
1347 REWRITE_TAC[GSYM(REWRITE_CONV [o_DEF]
1348 `(\x. x rpow y) o (\e. s - e)`)] THEN
1349 MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE THEN
1350 ASM_SIMP_TAC[REAL_CONTINUOUS_SUB; REAL_CONTINUOUS_WITHIN_ID;
1351 REAL_CONTINUOUS_CONST] THEN
1352 MATCH_MP_TAC REAL_CONTINUOUS_WITHIN_RPOW THEN
1353 REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS]];
1354 W(MP_TAC o PART_MATCH (lhand o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
1357 [REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN REAL_ARITH_TAC;
1358 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[EXTENSION; IN_SING] THEN
1359 DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
1361 REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
1362 EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
1363 ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO] THEN
1364 X_GEN_TAC `e:real` THEN REWRITE_TAC[real_abs] THEN
1365 ASM_CASES_TAC `&0 <= e` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1366 MAP_EVERY (fun l -> MP_TAC(ISPECL l MEASURABLE_INNER_COMPACT))
1367 [[`t:real^N->bool`; `e:real`]; [`s:real^N->bool`; `e:real`]] THEN
1368 ASM_SIMP_TAC[MEASURABLE_OPEN; GSYM REAL_LT_SUB_RADD] THEN
1369 DISCH_THEN(X_CHOOSE_THEN `s':real^N->bool` STRIP_ASSUME_TAC) THEN
1370 DISCH_THEN(X_CHOOSE_THEN `t':real^N->bool` STRIP_ASSUME_TAC) THEN
1371 MP_TAC(ISPECL [`s':real^N->bool`; `t':real^N->bool`]
1372 BRUNN_MINKOWSKI_COMPACT) THEN
1374 [ASM_MESON_TAC[MEASURE_EMPTY; REAL_ARITH `e < s ==> ~(s - e < &0)`];
1376 MATCH_MP_TAC(REAL_ARITH
1377 `s1 <= r1 /\ s2 <= r2 /\ rs <= s
1378 ==> rs >= r1 + r2 ==> s1 + s2 <= s`) THEN
1379 REPEAT CONJ_TAC THEN MATCH_MP_TAC ROOT_MONO_LE THEN
1380 ASM_SIMP_TAC[DIMINDEX_NONZERO; REAL_SUB_LE; REAL_LT_IMP_LE] THEN
1381 ASM_SIMP_TAC[MEASURE_POS_LE; COMPACT_SUMS; MEASURABLE_COMPACT] THEN
1382 MATCH_MP_TAC MEASURE_SUBSET THEN
1383 ASM_SIMP_TAC[MEASURE_POS_LE; COMPACT_SUMS; MEASURABLE_COMPACT] THEN