Examples/brunn_minkowski.ml

   1 (* ========================================================================= *)
   2 (* Brunn-Minkowski theorem and related results.                              *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/realanalysis.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* First, the special case of a box.                                         *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let BRUNN_MINKOWSKI_INTERVAL = prove
  12  (`!a b c d:real^N.
  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;
  24                  VECTOR_ADD_COMPONENT;
  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;
  37                  VECTOR_ADD_COMPONENT;
  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
  50   ANTS_TAC THENL
  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)`;
  54                  DIMINDEX_GE_1; LE_1];
  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
  60   EXISTS_TAC
  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)) +
  64     sum (1..dimindex(:N))
  65         (\i. ((d:real^N)$i - (c:real^N)$i) /
  66              ((b$i + d$i) - (a$i + c$i))) / &(dimindex(:N))` THEN
  67   CONJ_TAC THENL
  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
  70     (ANTS_TAC THENL
  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
  83       `a < b /\ c < d
  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]]);;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Now for a finite union of boxes.                                          *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let BRUNN_MINKOWSKI_ELEMENTARY = prove
  95  (`!s t:real^N->bool.
  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
 101   MAP_EVERY X_GEN_TAC
 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
 118   REWRITE_TAC[MESON[]
 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
 121   DISCH_TAC THEN
 122   MATCH_MP_TAC(MESON[]
 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')
 127                  ==> P d d' s 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];
 136     REPEAT GEN_TAC THEN
 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
 146     SUBGOAL_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
 154     STRIP_TAC THEN
 155     RULE_ASSUM_TAC(REWRITE_RULE[division_of; UNIONS_1; IN_SING]) THEN
 156     REPEAT(FIRST_X_ASSUM
 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
 161     ASM_MESON_TAC[];
 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
 180   SUBGOAL_THEN
 181    `!d1 d2 s t i j k.
 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)`
 191   MP_TAC THENL
 192    [ALL_TAC;
 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]];
 207           DISCH_TAC THEN
 208           SUBGOAL_THEN
 209            `negligible(UNIONS {i | i IN d1 /\ ~(interior i = {})} UNION
 210                        UNIONS {i:real^N->bool | i IN d1 /\ interior i = {}})`
 211           MP_TAC THENL
 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
 227          `c' <= c /\ a' = a
 228           ==> c' >= a' + b ==> c >= a + b`) THEN
 229         CONJ_TAC THENL
 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
 241              `s' SUBSET s
 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[]]];
 247           AP_TERM_TAC THEN
 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
 251           CONJ_TAC THENL
 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
 260              `s' UNION s'' = s
 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
 269       SUBGOAL_THEN
 270        `?d:(real^N->bool)->bool. d SUBSET d1 /\ d HAS_SIZE 2`
 271       MP_TAC THENL
 272        [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP CHOOSE_SUBSET o
 273           MATCH_MP DIVISION_OF_FINITE) THEN ASM_REWRITE_TAC[];
 274         ALL_TAC] THEN
 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
 287       SUBGOAL_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
 299         ==> u < v /\ w < z
 300             ==> u <= a /\ v <= a /\ a <= w /\ a <= z \/
 301                 w <= a /\ z <= a /\ a <= u /\ a <= v`)) THEN
 302       ANTS_TAC THENL
 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
 307         ASM_MESON_TAC[];
 308         ALL_TAC] THEN
 309       STRIP_TAC 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`;
 314           `t:real^N->bool`])
 315       THENL
 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
 326          MATCH_MP_TAC(MESON[]
 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
 334          ASM_MESON_TAC[];
 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
 363          REWRITE_TAC[SET_RULE
 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
 367   SUBGOAL_THEN
 368    `!d1 d2 s t i j k.
 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)`
 381   MP_TAC THENL
 382    [ALL_TAC;
 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];
 388       ALL_TAC] THEN
 389     SUBGOAL_THEN
 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
 393      [SUBGOAL_THEN
 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`
 396       MP_TAC THENL
 397        [ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_MUL_LZERO] THEN
 398         CONJ_TAC THENL
 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
 402            [ALL_TAC;
 403             ASM_MESON_TAC[MEASURABLE_ELEMENTARY];
 404             SET_TAC[]]] THEN
 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`,
 410                  `u:real`)] THEN
 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];
 418         ALL_TAC] THEN
 419       SUBGOAL_THEN
 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
 424        [ASM_REAL_ARITH_TAC;
 425         ALL_TAC;
 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];
 446       ALL_TAC] THEN
 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`;
 450       `s:real^N->bool`;
 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
 457      [CONJ_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
 461         MATCH_MP_TAC(MESON[]
 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;
 465         ALL_TAC] THEN
 466       SUBGOAL_THEN
 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
 472        [CONJ_TAC THEN
 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]);
 480         ALL_TAC] THEN
 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
 498           `(!x. P x \/ Q x)
 499            ==> s INTER {x | P x} UNION s INTER {x | Q x} = s`) THEN
 500          REAL_ARITH_TAC;
 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
 509       REWRITE_TAC[SET_RULE
 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
 513       REWRITE_TAC[SET_RULE
 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];
 523     ALL_TAC] THEN
 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
 538   EXISTS_TAC
 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
 541   CONJ_TAC THENL
 542    [ALL_TAC;
 543     MATCH_MP_TAC REAL_LE_TRANS THEN
 544     EXISTS_TAC
 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
 549     CONJ_TAC THENL
 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
 553         CONJ_TAC THENL
 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]]);
 582       ALL_TAC] THEN
 583     SUBGOAL_THEN
 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})`
 586     MP_TAC THENL
 587      [CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
 588        `(!x. P x \/ Q x)
 589         ==> s = (s INTER {x | P x}) UNION (s INTER {x | Q x})`) THEN
 590       REAL_ARITH_TAC;
 591       DISCH_THEN(fun th ->
 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
 595     ANTS_TAC THENL
 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];
 602         ALL_TAC]) THEN
 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];
 626       SET_TAC[]]] THEN
 627   SUBGOAL_THEN
 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
 633     CONJ_TAC THENL
 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[];
 641     ALL_TAC] THEN
 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
 659       CONJ_TAC THENL
 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[]];
 663         ALL_TAC] THEN
 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
 679       CONJ_TAC THENL
 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]];
 684       DISCH_TAC THEN
 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
 697       CONJ_TAC THENL
 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
 705         ASM SET_TAC[];
 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]]];
 745     ALL_TAC] THEN
 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
 752       CONJ_TAC THENL
 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[]];
 756         ALL_TAC] THEN
 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
 772       CONJ_TAC THENL
 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]];
 777       DISCH_TAC THEN
 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
 790       CONJ_TAC THENL
 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
 798         ASM SET_TAC[];
 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]]];
 838     ALL_TAC] THEN
 839   REWRITE_TAC[real_ge; IMP_IMP] THEN
 840   SUBGOAL_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];
 853     ALL_TAC] THEN
 854   SUBGOAL_THEN
 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
 858   SUBGOAL_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];
 870     ALL_TAC] THEN
 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
 877   SUBGOAL_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)
 883   THENL
 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
 888     CONJ_TAC 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}`]
 907     THENL
 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
 913     SET_TAC[];
 914     ALL_TAC] THEN
 915   SUBGOAL_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
 927    [CONJ_TAC THEN
 928     MATCH_MP_TAC(REAL_FIELD `&0 < s ==> s + t = s * (&1 + t / s)`) THEN
 929     ASM_SIMP_TAC[ROOT_POS_LT; DIMINDEX_NONZERO];
 930     ALL_TAC] THEN
 931   ASM_SIMP_TAC[DIMINDEX_NONZERO; GSYM REAL_ROOT_DIV; MEASURE_POS_LE;
 932     MEASURABLE_INTER_HALFSPACE_LE; MEASURABLE_INTER_HALFSPACE_GE] THEN
 933   SUBGOAL_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
 943     ASM_REWRITE_TAC[];
 944     ALL_TAC] 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
 948   SUBGOAL_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))`
 951   SUBST1_TAC THENL
 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
 956     CONJ_TAC THENL
 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]]);;
 968
 969 (* ------------------------------------------------------------------------- *)
 970 (* Now for open sets.                                                        *)
 971 (* ------------------------------------------------------------------------- *)
 972
 973 let BRUNN_MINKOWSKI_OPEN = prove
 974  (`!s t:real^N->bool.
 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
 982   STRIP_TAC 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
 988     EXISTS_TAC
 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
1013       rand o snd) THEN
1014     ANTS_TAC THENL
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
1018       REAL_ARITH_TAC];
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
1032     ANTS_TAC THENL
1033      [ASM_MESON_TAC[MEASURE_EMPTY; REAL_ARITH `e < s ==> ~(s - e < &0)`];
1034       ALL_TAC] THEN
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
1040     SUBGOAL_THEN
1041      `measurable {x + y :real^N | x IN UNIONS D /\ y IN UNIONS E}`
1042     ASSUME_TAC THENL
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]]);;
1049
1050 (* ------------------------------------------------------------------------- *)
1051 (* Now for convex sets.                                                      *)
1052 (* ------------------------------------------------------------------------- *)
1053
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
1075       ASM SET_TAC[]];
1076     ALL_TAC] 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
1091       ASM SET_TAC[]];
1092     ALL_TAC] 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;
1097                OPEN_INTERIOR] THEN
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]);;
1107
1108 (* ------------------------------------------------------------------------- *)
1109 (* Now for compact sets.                                                     *)
1110 (* ------------------------------------------------------------------------- *)
1111
1112 let INTERS_SUMS_CLOSED_BALL_SEQUENTIAL = prove
1113  (`!s:real^N->bool.
1114         closed s
1115         ==> INTERS {{x + d | x IN s /\ d IN ball(vec 0,inv(&n + &1))} |
1116                     n IN (:num)} = s`,
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
1135       ASM_ARITH_TAC;
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
1140     REAL_ARITH_TAC]);;
1141
1142 let MEASURE_SUMS_COMPACT_EPSILON = prove
1143  (`!s:real^N->bool.
1144         compact s
1145         ==> ((\e. measure {x + d | x IN s /\ d IN ball(vec 0,e)})
1146              ---> measure s)
1147             (atreal (&0) within {e | &0 <= e})`,
1148   REPEAT STRIP_TAC THEN
1149   MP_TAC(ISPEC
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
1153   ANTS_TAC THENL
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
1157      `t' SUBSET t
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
1162     ARITH_TAC;
1163     ALL_TAC] 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]
1181   THENL
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
1186      `t' SUBSET t
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]]);;
1190
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)`,
1196   let lemma1 = prove
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])
1222   and lemma2 = prove
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
1237   EXISTS_TAC
1238    `\e. root (dimindex(:N))
1239              (measure {x + d:real^N | x IN s /\ d IN ball(vec 0,e)}) +
1240         root (dimindex(:N))
1241              (measure {x + d:real^N | x IN t /\ d IN ball(vec 0,e)})` THEN
1242   EXISTS_TAC
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
1265       rand o snd) THEN
1266     ANTS_TAC THENL
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
1270       REAL_ARITH_TAC];
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
1276     ASM SET_TAC[]]);;
1277
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 (* ------------------------------------------------------------------------- *)
1282
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
1303       ASM SET_TAC[]];
1304     ALL_TAC] 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
1317       ASM SET_TAC[]];
1318     ALL_TAC] THEN
1319   SUBGOAL_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];
1324     ALL_TAC] THEN
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
1330     EXISTS_TAC
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
1355       rand o snd) THEN
1356     ANTS_TAC THENL
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
1360       REAL_ARITH_TAC];
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
1373     ANTS_TAC THENL
1374      [ASM_MESON_TAC[MEASURE_EMPTY; REAL_ARITH `e < s ==> ~(s - e < &0)`];
1375       ALL_TAC] THEN
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
1384     ASM SET_TAC[]]);;