(* ========================================================================= *)
(* Brunn-Minkowski theorem and related results.                              *)
(* ========================================================================= *)

needs "Multivariate/realanalysis.ml";;
needs "Library/agm.ml";;

(* ------------------------------------------------------------------------- *)
(* First, the special case of a box.                                         *)
(* ------------------------------------------------------------------------- *)

let BRUNN_MINKOWSKI_INTERVAL = 
prove
 (`!a b c d:real^N.
    ~(interval[a,b] = {}) /\ ~(interval[c,d] = {})
    ==> root (dimindex(:N))
             (measure {x + y | x IN interval[a,b] /\ y IN interval[c,d]})
        >= root (dimindex(:N)) (measure(interval[a,b])) +
           root (dimindex(:N)) (measure(interval[c,d]))`,

  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[SUMS_INTERVALS; real_ge] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[INTERVAL_NE_EMPTY]) THEN
  ASM_CASES_TAC `measure(interval[a:real^N,b]) = &0` THENL
   [ASM_SIMP_TAC[ROOT_0; DIMINDEX_GE_1; LE_1; REAL_ADD_LID;
                 ROOT_MONO_LE_EQ; MEASURE_POS_LE; MEASURABLE_INTERVAL] THEN
    ASM_SIMP_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL;
                 VECTOR_ADD_COMPONENT;
                 REAL_ARITH `a <= b /\ c <= d ==> a + c <= b + d`] THEN
    MATCH_MP_TAC PRODUCT_LE_NUMSEG THEN
    X_GEN_TAC `i:num` THEN DISCH_TAC THEN
    REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
    ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
    FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
    SIMP_TAC[MEASURABLE_MEASURE_EQ_0; MEASURABLE_INTERVAL] THEN
    REWRITE_TAC[NEGLIGIBLE_INTERVAL; INTERVAL_NE_EMPTY] THEN STRIP_TAC] THEN
  ASM_CASES_TAC `measure(interval[c:real^N,d]) = &0` THENL
   [ASM_SIMP_TAC[ROOT_0; DIMINDEX_GE_1; LE_1; REAL_ADD_RID;
                 ROOT_MONO_LE_EQ; MEASURE_POS_LE; MEASURABLE_INTERVAL] THEN
    ASM_SIMP_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL;
                 VECTOR_ADD_COMPONENT;
                 REAL_ARITH `a <= b /\ c <= d ==> a + c <= b + d`] THEN
    MATCH_MP_TAC PRODUCT_LE_NUMSEG THEN
    X_GEN_TAC `i:num` THEN DISCH_TAC THEN
    REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
    ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
    FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
    SIMP_TAC[MEASURABLE_MEASURE_EQ_0; MEASURABLE_INTERVAL] THEN
    REWRITE_TAC[NEGLIGIBLE_INTERVAL; INTERVAL_NE_EMPTY] THEN STRIP_TAC] THEN
  ASM_SIMP_TAC[MEASURE_INTERVAL; CONTENT_CLOSED_INTERVAL; VECTOR_ADD_COMPONENT;
               REAL_ARITH `a <= b /\ c <= d ==> a + c <= b + d`] THEN
  GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
  W(MP_TAC o PART_MATCH (rand o rand) REAL_LE_LDIV_EQ o snd) THEN
  ANTS_TAC THENL
   [MATCH_MP_TAC ROOT_POS_LT THEN
    ASM_SIMP_TAC[GSYM REAL_LE_LDIV_EQ; PRODUCT_POS_LT_NUMSEG; IN_NUMSEG;
                 REAL_ARITH `a < b /\ c < d ==> &0 < (b + d) - (a + c)`;
                 DIMINDEX_GE_1; LE_1];
    DISCH_THEN(SUBST1_TAC o SYM)] THEN
  REWRITE_TAC[real_div; REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM real_div] THEN
  W(MP_TAC o PART_MATCH (lhand o rand) (GSYM REAL_ROOT_DIV) o
    lhand o lhand o snd) THEN
  W(MP_TAC o PART_MATCH (lhand o rand) (GSYM REAL_ROOT_DIV) o
    rand o lhand o rand o snd) THEN
  ASM_SIMP_TAC[DIMINDEX_NONZERO; PRODUCT_POS_LE_NUMSEG;
               IN_NUMSEG; REAL_SUB_LE;
               REAL_ARITH `a < b /\ c < d ==> a + c <= b + d`] THEN
  REPEAT(DISCH_THEN(K ALL_TAC)) THEN
  REWRITE_TAC[GSYM PRODUCT_DIV_NUMSEG] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC
   `sum (1..dimindex(:N))
        (\i. ((b:real^N)$i - (a:real^N)$i) /
             ((b$i + d$i) - (a$i + c$i))) / &(dimindex(:N)) +
    sum (1..dimindex(:N))
        (\i. ((d:real^N)$i - (c:real^N)$i) /
             ((b$i + d$i) - (a$i + c$i))) / &(dimindex(:N))` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THEN
    W(MP_TAC o PART_MATCH (lhand o rand) REAL_ROOT_LE o snd) THEN
    (ANTS_TAC THENL
      [REWRITE_TAC[DIMINDEX_NONZERO] THEN CONJ_TAC THENL
        [MATCH_MP_TAC PRODUCT_POS_LE_NUMSEG;
         MATCH_MP_TAC REAL_LE_DIV THEN REWRITE_TAC[REAL_POS] THEN
         MATCH_MP_TAC SUM_POS_LE_NUMSEG];
       DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC AGM THEN
       REWRITE_TAC[DIMINDEX_GE_1]] THEN
     X_GEN_TAC `i:num` THEN DISCH_TAC THEN REWRITE_TAC[REAL_SUB_LE] THEN
     MATCH_MP_TAC REAL_LE_DIV THEN
     REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
     ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
     REWRITE_TAC[real_div; GSYM REAL_ADD_RDISTRIB] THEN
     REWRITE_TAC[GSYM SUM_ADD_NUMSEG] THEN
     ASM_SIMP_TAC[REAL_FIELD
      `a < b /\ c < d
       ==> (b - a) * inv((b + d) - (a + c)) +
           (d - c) * inv((b + d) - (a + c)) = &1`] THEN
     REWRITE_TAC[SUM_CONST_NUMSEG; ADD_SUB] THEN
     ASM_SIMP_TAC[REAL_MUL_RID; REAL_MUL_RINV; REAL_LE_REFL;
                  REAL_OF_NUM_EQ; DIMINDEX_NONZERO]]);;
(* ------------------------------------------------------------------------- *)
(* Now for a finite union of boxes.                                          *)
(* ------------------------------------------------------------------------- *)

let BRUNN_MINKOWSKI_ELEMENTARY = 
prove
 (`!s t:real^N->bool.
    (s = {} <=> t = {}) /\ (?d. d division_of s) /\ (?d. d division_of t)
    ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
        >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,

  REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
  REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC
   [`s:real^N->bool`; `t:real^N->bool`;
    `d1:(real^N->bool)->bool`; `d2:(real^N->bool)->bool`] THEN
  ASM_CASES_TAC `t:real^N->bool = {}` THENL
   [ASM_SIMP_TAC[NOT_IN_EMPTY; SET_RULE `{f x y |x,y| F} = {}`] THEN
    SIMP_TAC[MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO] THEN
    STRIP_TAC THEN REAL_ARITH_TAC;
    ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN
    ONCE_REWRITE_TAC[TAUT `p ==> q /\ r ==> s <=> q /\ p /\ r ==> s`]] THEN
  X_CHOOSE_THEN `n:num` MP_TAC (ISPEC
   `CARD(d1:(real^N->bool)->bool) + CARD(d2:(real^N->bool)->bool)`
   (GSYM EXISTS_REFL)) THEN
  REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
  MAP_EVERY (fun t -> SPEC_TAC(t,t))
   [`t:real^N->bool`; `s:real^N->bool`;
    `d2:(real^N->bool)->bool`; `d1:(real^N->bool)->bool`; `n:num`] THEN
  MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
  REWRITE_TAC[MESON[]
   `(!m. m < n ==> !a b c d. f a b = m /\ stuff a b c d ==> other a b c d) <=>
    (!a b c d. f a b:num < n /\ stuff a b c d ==> other a b c d)`] THEN
  DISCH_TAC THEN
  MATCH_MP_TAC(MESON[]
   `(!d d' s s'. P d d' s s' ==> P d' d s' s) /\
    (!d d' s s'. ~(2 <= CARD d) /\ ~(2 <= CARD d') ==> P d d' s s') /\
    (!d d' s s'. negligible s ==>  P d d' s s') /\
    (!d d' s s'. 2 <= CARD d /\ ~(negligible s) /\ ~(negligible s')
                 ==> P d d' s s')
    ==> !d d' s s'.  P d d' s s'`) THEN
  REPEAT CONJ_TAC THENL
   [REPEAT GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN
    CONJ_TAC THENL [REWRITE_TAC[ADD_SYM; CONJ_ACI]; ALL_TAC] THEN
    MATCH_MP_TAC(REAL_ARITH
     `x = y ==> x >= a + b ==> y >= b + a`) THEN
    AP_TERM_TAC THEN AP_TERM_TAC THEN
    REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN MESON_TAC[VECTOR_ADD_SYM];
    REPEAT GEN_TAC THEN
    ASM_CASES_TAC `FINITE(d1:(real^N->bool)->bool) /\
                   FINITE(d2:(real^N->bool)->bool)`
    THENL [ALL_TAC; REWRITE_TAC[division_of] THEN ASM_MESON_TAC[]] THEN
    ASM_SIMP_TAC[CARD_EQ_0; ARITH_RULE `~(2 <= n) <=> n = 0 \/ n = 1`] THEN
    ASM_CASES_TAC `d1:(real^N->bool)->bool = {}` THENL
     [ASM_REWRITE_TAC[EMPTY_DIVISION_OF] THEN MESON_TAC[]; ALL_TAC] THEN
    ASM_CASES_TAC `d2:(real^N->bool)->bool = {}` THENL
     [ASM_REWRITE_TAC[EMPTY_DIVISION_OF] THEN MESON_TAC[]; ALL_TAC] THEN
    ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
    SUBGOAL_THEN
     `(d1:(real^N->bool)->bool) HAS_SIZE 1 /\
      (d2:(real^N->bool)->bool) HAS_SIZE 1`
    MP_TAC THENL [ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN
    CONV_TAC(LAND_CONV(BINOP_CONV HAS_SIZE_CONV)) THEN
    DISCH_THEN(CONJUNCTS_THEN2
     (X_CHOOSE_THEN `u:real^N->bool` SUBST_ALL_TAC)
     (X_CHOOSE_THEN `v:real^N->bool` SUBST_ALL_TAC)) THEN
    STRIP_TAC THEN
    RULE_ASSUM_TAC(REWRITE_RULE[division_of; UNIONS_1; IN_SING]) THEN
    REPEAT(FIRST_X_ASSUM
     (CONJUNCTS_THEN2 MP_TAC
       (SUBST_ALL_TAC o SYM o CONJUNCT2) o CONJUNCT2)) THEN
    REWRITE_TAC[FORALL_UNWIND_THM2] THEN REPEAT STRIP_TAC THEN
    ASM_REWRITE_TAC[] THEN MATCH_MP_TAC BRUNN_MINKOWSKI_INTERVAL THEN
    ASM_MESON_TAC[];
    REPEAT STRIP_TAC THEN
    SUBGOAL_THEN `measure(s:real^N->bool) = &0` SUBST1_TAC THENL
     [ASM_SIMP_TAC[MEASURE_EQ_0]; ALL_TAC] THEN
    SIMP_TAC[ROOT_0; DIMINDEX_NONZERO; REAL_ADD_LID; real_ge] THEN
    MATCH_MP_TAC ROOT_MONO_LE THEN REWRITE_TAC[DIMINDEX_NONZERO] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC MEASURE_POS_LE THEN ASM_MESON_TAC[MEASURABLE_ELEMENTARY];
      ALL_TAC] THEN
    SUBGOAL_THEN `?a:real^N. a IN s` STRIP_ASSUME_TAC THENL
     [ASM SET_TAC[]; ALL_TAC] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) t)` THEN CONJ_TAC THENL
     [REWRITE_TAC[MEASURE_TRANSLATION; REAL_LE_REFL]; ALL_TAC] THEN
    MATCH_MP_TAC MEASURE_SUBSET THEN
    REWRITE_TAC[MEASURABLE_TRANSLATION_EQ] THEN
    CONJ_TAC THENL [ASM_MESON_TAC[MEASURABLE_ELEMENTARY]; ALL_TAC] THEN
    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
    CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
    MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
    ASM_MESON_TAC[ELEMENTARY_COMPACT];
    REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC]] THEN
  SUBGOAL_THEN
   `!d1 d2 s t i j k.
        CARD d1 + CARD d2 = n /\
        1 <= k /\ k <= dimindex(:N) /\ ~(i = j) /\
        i IN d1 /\ i SUBSET {x:real^N | x$k <= &0} /\
        j IN d1 /\ j SUBSET {x | x$k >= &0} /\
        ~(negligible i) /\ ~(negligible j) /\
        ~(s = {}) /\ ~(t = {}) /\ ~(negligible s) /\ ~(negligible t) /\
        d1 division_of s /\ d2 division_of t
        ==> root(dimindex (:N)) (measure {x + y | x IN s /\ y IN t}) >=
            root(dimindex (:N)) (measure s) + root(dimindex (:N)) (measure t)`
  MP_TAC THENL
   [ALL_TAC;
    POP_ASSUM(LABEL_TAC "*") THEN DISCH_THEN(LABEL_TAC "+") THEN
    REPEAT STRIP_TAC THEN
    ASM_CASES_TAC `?i:real^N->bool. i IN d1 /\ interior i = {}` THENL
     [REMOVE_THEN "+" (K ALL_TAC) THEN REMOVE_THEN "*" MP_TAC THEN
      DISCH_THEN(MP_TAC o SPECL
       [`{i:real^N->bool | i IN d1 /\ ~(interior i = {})}`;
        `d2:(real^N->bool)->bool`;
        `UNIONS {i:real^N->bool | i IN d1 /\ ~(interior i = {})}`;
        `t:real^N->bool`]) THEN
      ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
       [REPEAT CONJ_TAC THENL
         [EXPAND_TAC "n" THEN REWRITE_TAC[LT_ADD_RCANCEL] THEN
          MATCH_MP_TAC CARD_PSUBSET THEN CONJ_TAC THENL
           [ASM SET_TAC[]; ASM_MESON_TAC[DIVISION_OF_FINITE]];
          DISCH_TAC THEN
          SUBGOAL_THEN
           `negligible(UNIONS {i | i IN d1 /\ ~(interior i = {})} UNION
                       UNIONS {i:real^N->bool | i IN d1 /\ interior i = {}})`
          MP_TAC THENL
           [ASM_REWRITE_TAC[UNION_EMPTY] THEN
            MATCH_MP_TAC NEGLIGIBLE_UNIONS THEN CONJ_TAC THENL
             [MATCH_MP_TAC FINITE_RESTRICT THEN
              ASM_MESON_TAC[DIVISION_OF_FINITE];
              REWRITE_TAC[IN_ELIM_THM; IMP_CONJ] THEN
              FIRST_ASSUM(fun th ->
                GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
              REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; NEGLIGIBLE_INTERVAL]];
            REWRITE_TAC[GSYM UNIONS_UNION; SET_RULE
              `{x | x IN s /\ ~Q x} UNION {x | x IN s /\ Q x} = s`] THEN
            RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN ASM_REWRITE_TAC[]];
          MATCH_MP_TAC DIVISION_OF_SUBSET THEN
          EXISTS_TAC `d1:(real^N->bool)->bool` THEN
          CONJ_TAC THENL [ASM_MESON_TAC[division_of]; SET_TAC[]]];
        MATCH_MP_TAC(REAL_ARITH
         `c' <= c /\ a' = a
          ==> c' >= a' + b ==> c >= a + b`) THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC ROOT_MONO_LE THEN REWRITE_TAC[DIMINDEX_NONZERO] THEN
          CONJ_TAC THENL
           [MATCH_MP_TAC MEASURE_POS_LE THEN
            MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
            CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[ELEMENTARY_COMPACT]] THEN
            MATCH_MP_TAC COMPACT_UNIONS THEN
            RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN
            ASM_SIMP_TAC[FINITE_RESTRICT; IN_ELIM_THM] THEN
            ASM_MESON_TAC[COMPACT_INTERVAL];
            ALL_TAC] THEN
          MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
           [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
            CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[ELEMENTARY_COMPACT]] THEN
            MATCH_MP_TAC COMPACT_UNIONS THEN
            RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN
            ASM_SIMP_TAC[FINITE_RESTRICT; IN_ELIM_THM] THEN
            ASM_MESON_TAC[COMPACT_INTERVAL];
            MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
            ASM_MESON_TAC[ELEMENTARY_COMPACT];
            MATCH_MP_TAC(SET_RULE
             `s' SUBSET s
              ==> {f x y | x IN s' /\ y IN t} SUBSET
                  {f x y | x IN s /\ y IN t}`) THEN
            SUBGOAL_THEN `s:real^N->bool = UNIONS d1` SUBST1_TAC THENL
             [ASM_MESON_TAC[division_of];
              MATCH_MP_TAC SUBSET_UNIONS THEN SET_TAC[]]];
          AP_TERM_TAC THEN
          MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN
          MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
          EXISTS_TAC `UNIONS {i:real^N->bool | i IN d1 /\ interior i = {}}` THEN
          CONJ_TAC THENL
           [MATCH_MP_TAC NEGLIGIBLE_UNIONS THEN CONJ_TAC THENL
             [MATCH_MP_TAC FINITE_RESTRICT THEN
              ASM_MESON_TAC[DIVISION_OF_FINITE];
              REWRITE_TAC[IN_ELIM_THM; IMP_CONJ] THEN
              FIRST_ASSUM(fun th ->
                GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
              REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; NEGLIGIBLE_INTERVAL]];
            MATCH_MP_TAC(SET_RULE
             `s' UNION s'' = s
              ==> (s' DIFF s) UNION (s DIFF s') SUBSET s''`) THEN
            REWRITE_TAC[GSYM UNIONS_UNION; SET_RULE
              `{x | x IN s /\ ~Q x} UNION {x | x IN s /\ Q x} = s`] THEN
            RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN
            ASM_REWRITE_TAC[]]]];
      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
      REWRITE_TAC[TAUT `~(a /\ b) <=> a ==> ~b`] THEN DISCH_TAC THEN
      REMOVE_THEN "*" (K ALL_TAC) THEN
      SUBGOAL_THEN
       `?d:(real^N->bool)->bool. d SUBSET d1 /\ d HAS_SIZE 2`
      MP_TAC THENL
       [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP CHOOSE_SUBSET o
          MATCH_MP DIVISION_OF_FINITE) THEN ASM_REWRITE_TAC[];
        ALL_TAC] THEN
      CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV HAS_SIZE_CONV)) THEN
      REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
      ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
      DISCH_THEN(X_CHOOSE_THEN `i:real^N->bool` MP_TAC) THEN
      ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
      DISCH_THEN(X_CHOOSE_THEN `j:real^N->bool` MP_TAC) THEN
      ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> r /\ p /\ q`] THEN
      REWRITE_TAC[UNWIND_THM2; INSERT_SUBSET; EMPTY_SUBSET] THEN STRIP_TAC THEN
      MP_TAC(ASSUME `d1 division_of (s:real^N->bool)`) THEN
      REWRITE_TAC[division_of] THEN DISCH_THEN(MP_TAC o el 2 o CONJUNCTS) THEN
      DISCH_THEN(MP_TAC o SPECL [`i:real^N->bool`; `j:real^N->bool`]) THEN
      ASM_REWRITE_TAC[] THEN
      SUBGOAL_THEN
       `?u v w z. i = interval[u:real^N,v] /\ j = interval[w:real^N,z]`
      STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[DIVISION_OF]; ALL_TAC] THEN
      ASM_REWRITE_TAC[GSYM INTERIOR_INTER; INTER_INTERVAL] THEN
      REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; INTERVAL_EQ_EMPTY] THEN
      DISCH_THEN(X_CHOOSE_THEN `k:num` MP_TAC) THEN
      REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
      SIMP_TAC[LAMBDA_BETA; ASSUME `1 <= k`; ASSUME `k <= dimindex(:N)`] THEN
      GEN_REWRITE_TAC LAND_CONV [REAL_LE_BETWEEN] THEN
      DISCH_THEN(X_CHOOSE_THEN `a:real` MP_TAC) THEN
      DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
       `min v z <= a /\ a <= max u w
        ==> u < v /\ w < z
            ==> u <= a /\ v <= a /\ a <= w /\ a <= z \/
                w <= a /\ z <= a /\ a <= u /\ a <= v`)) THEN
      ANTS_TAC THENL
       [UNDISCH_TAC `!i:real^N->bool. i IN d1 ==> ~(interior i = {})` THEN
        DISCH_THEN(fun th -> MP_TAC(ISPEC `interval[u:real^N,v]` th) THEN
                             MP_TAC(ISPEC `interval[w:real^N,z]` th)) THEN
        REWRITE_TAC[INTERIOR_CLOSED_INTERVAL; INTERVAL_NE_EMPTY] THEN
        ASM_MESON_TAC[];
        ALL_TAC] THEN
      STRIP_TAC THEN
      FIRST_X_ASSUM(MP_TAC o SPECL
         [`IMAGE (IMAGE (\x:real^N. x - a % basis k)) d1`;
          `d2:(real^N->bool)->bool`;
          `IMAGE (\x:real^N. x - a % basis k) s`;
          `t:real^N->bool`])
      THENL
       [DISCH_THEN(MP_TAC o SPECL
         [`IMAGE (\x:real^N. x - a % basis k) i`;
          `IMAGE (\x:real^N. x - a % basis k) j`; `k:num`]);
        DISCH_THEN(MP_TAC o SPECL
         [`IMAGE (\x:real^N. x - a % basis k) j`;
          `IMAGE (\x:real^N. x - a % basis k) i`; `k:num`])] THEN
      (ASM_REWRITE_TAC[] THEN ANTS_TAC THEN REPEAT CONJ_TAC THENL
        [EXPAND_TAC "n" THEN AP_THM_TAC THEN AP_TERM_TAC THEN
         MATCH_MP_TAC CARD_IMAGE_INJ THEN
         CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[DIVISION_OF_FINITE]] THEN
         MATCH_MP_TAC(MESON[]
          `(!x y. Q x y ==> R x y)
           ==> (!x y. P x /\ P y /\ Q x y ==> R x y)`) THEN
         REWRITE_TAC[INJECTIVE_IMAGE] THEN VECTOR_ARITH_TAC;
         MATCH_MP_TAC(SET_RULE
          `(!x y. f x = f y ==> x = y) /\ ~(s = t)
           ==> ~(IMAGE f s = IMAGE f t)`) THEN
         REWRITE_TAC[VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN
         ASM_MESON_TAC[];
         MATCH_MP_TAC FUN_IN_IMAGE THEN ASM_MESON_TAC[];
         REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
         ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_MUL_COMPONENT;
          BASIS_COMPONENT; REAL_MUL_RID; REAL_LE_SUB_RADD; REAL_ADD_LID] THEN
         REWRITE_TAC[IN_INTERVAL] THEN ASM_MESON_TAC[REAL_LE_TRANS];
         MATCH_MP_TAC FUN_IN_IMAGE THEN ASM_MESON_TAC[];
         REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM; real_ge] THEN
         ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_MUL_COMPONENT;
          BASIS_COMPONENT; REAL_MUL_RID; REAL_LE_SUB_LADD; REAL_ADD_LID] THEN
         REWRITE_TAC[IN_INTERVAL] THEN ASM_MESON_TAC[REAL_LE_TRANS];
         REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
         ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ] THEN
         ASM_MESON_TAC[NEGLIGIBLE_INTERVAL; INTERIOR_CLOSED_INTERVAL];
         REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
         ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ] THEN
         ASM_MESON_TAC[NEGLIGIBLE_INTERVAL; INTERIOR_CLOSED_INTERVAL];
         ASM_REWRITE_TAC[IMAGE_EQ_EMPTY];
         REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
         ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ];
         REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
         ASM_REWRITE_TAC[DIVISION_OF_TRANSLATION];
         MATCH_MP_TAC(REAL_ARITH
          `a = a' /\ b = b' ==> a >= b + c ==> a' >= b' + c`) THEN
         REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
         REWRITE_TAC[MEASURE_TRANSLATION] THEN
         REWRITE_TAC[GSYM VECTOR_ADD_ASSOC; SET_RULE
          `{f x y | x IN IMAGE g s /\ y IN t} =
           {f (g x) y | x IN s /\ y IN t}`] THEN
         REWRITE_TAC[SET_RULE
          `{a + x + y:real^N | x IN s /\ y IN t} =
           IMAGE (\z. a + z) {x + y | x IN s /\ y IN t}`] THEN
         REWRITE_TAC[MEASURE_TRANSLATION]])]] THEN
  SUBGOAL_THEN
   `!d1 d2 s t i j k.
        CARD d1 + CARD d2 = n /\
        1 <= k /\ k <= dimindex(:N) /\ ~(i = j) /\
        i IN d1 /\ i SUBSET {x:real^N | x$k <= &0} /\ ~(negligible i) /\
        j IN d1 /\ j SUBSET {x | x$k >= &0} /\ ~(negligible j) /\
        measure(t INTER {x | x$k <= &0}) / measure t =
        measure(s INTER {x | x$k <= &0}) / measure s /\
        measure(t INTER {x | x$k >= &0}) / measure t =
        measure(s INTER {x | x$k >= &0}) / measure s /\
        ~(s = {}) /\ ~(t = {}) /\ ~(negligible s) /\ ~(negligible t) /\
        d1 division_of s /\ d2 division_of t
        ==> root(dimindex (:N)) (measure {x + y | x IN s /\ y IN t}) >=
            root(dimindex (:N)) (measure s) + root(dimindex (:N)) (measure t)`
  MP_TAC THENL
   [ALL_TAC;
    POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN
    REPEAT STRIP_TAC THEN
    SUBGOAL_THEN `&0 < measure(s:real^N->bool) /\ &0 < measure(t:real^N->bool)`
    STRIP_ASSUME_TAC THENL
     [ASM_MESON_TAC[MEASURABLE_MEASURE_POS_LT; MEASURABLE_ELEMENTARY];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `?a. measure(t INTER {x:real^N | x$k <= a}) / measure t =
          measure(s INTER {x:real^N | x$k <= &0}) / measure s`
    STRIP_ASSUME_TAC THENL
     [SUBGOAL_THEN
       `&0 <= measure(s INTER {x:real^N | x$k <= &0}) / measure s /\
        measure(s INTER {x:real^N | x$k <= &0}) / measure s <= &1`
      MP_TAC THENL
       [ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_MUL_LZERO] THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC MEASURE_POS_LE;
          REWRITE_TAC[REAL_MUL_LID] THEN MATCH_MP_TAC MEASURE_SUBSET THEN
          REPEAT CONJ_TAC THENL
           [ALL_TAC;
            ASM_MESON_TAC[MEASURABLE_ELEMENTARY];
            SET_TAC[]]] THEN
        MATCH_MP_TAC MEASURABLE_COMPACT THEN
        MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
        REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE] THEN
        ASM_MESON_TAC[ELEMENTARY_COMPACT];
        SPEC_TAC(`measure(s INTER {x:real^N | x$k <= &0}) / measure s`,
                 `u:real`)] THEN
      X_GEN_TAC `u:real` THEN STRIP_TAC THEN
      SUBGOAL_THEN `?b:real. &0 < b /\ !x:real^N. x IN t ==> abs(x$k) <= b`
      STRIP_ASSUME_TAC THENL
       [SUBGOAL_THEN `bounded(t:real^N->bool)` MP_TAC THENL
         [ASM_MESON_TAC[ELEMENTARY_BOUNDED]; REWRITE_TAC[BOUNDED_POS]] THEN
        MATCH_MP_TAC MONO_EXISTS THEN
        ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LE_TRANS];
        ALL_TAC] THEN
      SUBGOAL_THEN
       `?a. a IN real_interval[--b,b] /\
            measure (t INTER {x:real^N | x$k <= a}) / measure t = u`
       (fun th -> MESON_TAC[th]) THEN
      MATCH_MP_TAC REAL_IVT_INCREASING THEN REPEAT CONJ_TAC THENL
       [ASM_REAL_ARITH_TAC;
        ALL_TAC;
        FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
         `&0 <= u ==> x = &0 ==> x <= u`)) THEN
        REWRITE_TAC[real_div; REAL_ENTIRE] THEN DISJ1_TAC THEN
        MATCH_MP_TAC MEASURE_EQ_0 THEN
        MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
        EXISTS_TAC `{x:real^N | x$k = --b}` THEN
        ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
        SIMP_TAC[SUBSET; IN_INTER; IN_ELIM_THM; GSYM REAL_LE_ANTISYM] THEN
        ASM_MESON_TAC[REAL_ARITH `abs x <= b ==> --b <= x`];
        FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
         `u <= &1 ==> x = &1 ==> u <= x`)) THEN
        ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_MUL_LID] THEN
        AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM] THEN
        ASM_MESON_TAC[REAL_ARITH `abs x <= b ==> x <= b`]] THEN
      REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_CONTINUOUS_ON_RMUL THEN
      REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
      GEN_TAC THEN DISCH_TAC THEN
      MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
      MATCH_MP_TAC REAL_CONTINUOUS_MEASURE_IN_HALFSPACE_LE THEN
      ASM_MESON_TAC[MEASURABLE_ELEMENTARY];
      ALL_TAC] THEN
    FIRST_X_ASSUM(MP_TAC o SPECL
     [`d1:(real^N->bool)->bool`;
      `IMAGE (IMAGE (\x:real^N. x - a % basis k)) d2`;
      `s:real^N->bool`;
      `IMAGE (\x:real^N. x - a % basis k) t`;
      `i:real^N->bool`; `j:real^N->bool`; `k:num`]) THEN
    ASM_REWRITE_TAC[] THEN
    ONCE_REWRITE_TAC[VECTOR_ARITH `x - a:real^N = --a + x`] THEN
    ASM_REWRITE_TAC[NEGLIGIBLE_TRANSLATION_EQ; DIVISION_OF_TRANSLATION] THEN
    ASM_REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ANTS_TAC THENL
     [CONJ_TAC THENL
       [EXPAND_TAC "n" THEN AP_TERM_TAC THEN
        MATCH_MP_TAC CARD_IMAGE_INJ THEN
        CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[DIVISION_OF_FINITE]] THEN
        MATCH_MP_TAC(MESON[]
         `(!x y. Q x y ==> R x y)
          ==> (!x y. P x /\ P y /\ Q x y ==> R x y)`) THEN
        REWRITE_TAC[INJECTIVE_IMAGE] THEN VECTOR_ARITH_TAC;
        ALL_TAC] THEN
      SUBGOAL_THEN
       `IMAGE (\x. --(a % basis k) + x) t INTER {x:real^N | x$k >= &0} =
        IMAGE (\x. --(a % basis k) + x) (t INTER {x | x$k >= a}) /\
        IMAGE (\x. --(a % basis k) + x) t INTER {x:real^N | x$k <= &0} =
        IMAGE (\x. --(a % basis k) + x) (t INTER {x | x$k <= a})`
      (CONJUNCTS_THEN SUBST1_TAC) THENL
       [CONJ_TAC THEN
        MATCH_MP_TAC(SET_RULE
         `!g. (!x. f(x) IN s' <=> x IN s) /\ (!x. g(f x) = x)
               ==> IMAGE f t INTER s' = IMAGE f (t INTER s)`) THEN
        ASM_SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
                     BASIS_COMPONENT; VECTOR_NEG_COMPONENT] THEN
        EXISTS_TAC `\x:real^N. a % basis k + x` THEN
        (CONJ_TAC THENL [REAL_ARITH_TAC; VECTOR_ARITH_TAC]);
        ALL_TAC] THEN
      REWRITE_TAC[MEASURE_TRANSLATION] THEN MATCH_MP_TAC(REAL_FIELD
       `&0 < s /\ &0 < t /\ t' / t = s' / s  /\ s' + s'' = s /\ t' + t'' = t
        ==> t' / t = s' / s /\ t'' / t = s'' / s`) THEN
      ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
      MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNION_EQ THEN
      (REPEAT CONJ_TAC THENL
        [MATCH_MP_TAC MEASURABLE_COMPACT THEN
         MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
         REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                     CLOSED_HALFSPACE_COMPONENT_GE] THEN
         ASM_MESON_TAC[ELEMENTARY_COMPACT];
         MATCH_MP_TAC MEASURABLE_COMPACT THEN
         MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
         REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                     CLOSED_HALFSPACE_COMPONENT_GE] THEN
         ASM_MESON_TAC[ELEMENTARY_COMPACT];
         MATCH_MP_TAC(SET_RULE
          `(!x. P x \/ Q x)
           ==> s INTER {x | P x} UNION s INTER {x | Q x} = s`) THEN
         REAL_ARITH_TAC;
         REWRITE_TAC[SET_RULE `(t INTER {x | P x}) INTER (t INTER {x | Q x}) =
                               t INTER {x | P x /\ Q x}`] THEN
         MATCH_MP_TAC(MESON[NEGLIGIBLE_SUBSET; INTER_SUBSET]
          `negligible t ==> negligible(s INTER t)`) THEN
         REWRITE_TAC[REAL_ARITH `x <= a /\ x >= a <=> x = a`] THEN
         ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE]]);
      REWRITE_TAC[MEASURE_TRANSLATION] THEN MATCH_MP_TAC(REAL_ARITH
       `a' = a ==> a' >= b ==> a >= b`) THEN AP_TERM_TAC THEN
      REWRITE_TAC[SET_RULE
       `{f x y | x IN s /\ y IN IMAGE g t} =
        {f x (g y) | x IN s /\ y IN t}`] THEN
      ONCE_REWRITE_TAC[VECTOR_ARITH `x + a + y:real^N = a + x + y`] THEN
      REWRITE_TAC[SET_RULE
       `{a + x + y:real^N | x IN s /\ y IN t} =
        IMAGE (\z. a + z) {x + y | x IN s /\ y IN t}`] THEN
      REWRITE_TAC[MEASURE_TRANSLATION]]] THEN
  REPEAT STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
  SUBGOAL_THEN `measurable(s:real^N->bool) /\ measurable(t:real^N->bool)`
  STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[MEASURABLE_ELEMENTARY]; ALL_TAC] THEN
  SUBGOAL_THEN `measurable {x + y:real^N | x IN s /\ y IN t}` ASSUME_TAC THENL
   [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
    ASM_MESON_TAC[ELEMENTARY_COMPACT];
    ALL_TAC] THEN
  SUBGOAL_THEN `&0 < measure(s:real^N->bool) /\ &0 < measure(t:real^N->bool)`
  STRIP_ASSUME_TAC THENL
    [ASM_MESON_TAC[MEASURABLE_MEASURE_POS_LT]; ALL_TAC] THEN
  SUBGOAL_THEN `FINITE(d1:(real^N->bool)->bool) /\
                FINITE(d2:(real^N->bool)->bool)`
  STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[DIVISION_OF_FINITE]; ALL_TAC] THEN
  W(MP_TAC o PART_MATCH (lhs o rand) REAL_LE_ROOT o snd) THEN
  ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; ROOT_POS_LE; REAL_LE_ADD] THEN
  DISCH_THEN SUBST1_TAC THEN
  ABBREV_TAC `dl = {l INTER {x:real^N | x$k <= &0} |l|
                    l IN d1 DELETE j /\ ~(l INTER {x | x$k <= &0} = {})}` THEN
  ABBREV_TAC `dr = {l INTER {x:real^N | x$k >= &0} |l|
                    l IN d1 DELETE i /\ ~(l INTER {x | x$k >= &0} = {})}` THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC
   `measure {x + y:real^N | x IN UNIONS dl /\ y IN (t INTER {x | x$k <= &0})} +
    measure {x + y | x IN UNIONS dr /\ y IN (t INTER {x | x$k >= &0})}` THEN
  CONJ_TAC THENL
   [ALL_TAC;
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC
     `measure {x + y:real^N | x IN (s INTER {x | x$k <= &0}) /\
                              y IN (t INTER {x | x$k <= &0})} +
      measure {x + y:real^N | x IN (s INTER {x | x$k >= &0}) /\
                              y IN (t INTER {x | x$k >= &0})}` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THEN
      (MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
       [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC COMPACT_UNIONS THEN
          MAP_EVERY EXPAND_TAC ["dl";
 "dr"] THEN
          ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
          ASM_SIMP_TAC[IN_DELETE; FINITE_DELETE; FINITE_IMAGE;
                       FINITE_RESTRICT; IMP_CONJ] THEN
          REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
          FIRST_ASSUM(fun th ->
            GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
          ASM_SIMP_TAC[INTERVAL_SPLIT; COMPACT_INTERVAL];
          MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
          REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                      CLOSED_HALFSPACE_COMPONENT_GE] THEN
          ASM_MESON_TAC[ELEMENTARY_COMPACT]];
        MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
        CONJ_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
        REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                    CLOSED_HALFSPACE_COMPONENT_GE] THEN
        ASM_MESON_TAC[ELEMENTARY_COMPACT];
        MATCH_MP_TAC(SET_RULE
         `s SUBSET s' ==> {x + y:real^N | x IN s /\ y IN t} SUBSET
                         {x + y:real^N | x IN s' /\ y IN t}`) THEN
        MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
        REWRITE_TAC[SUBSET; FORALL_IN_UNIONS] THEN
        REWRITE_TAC[FORALL_IN_GSPEC; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
        SIMP_TAC[IN_DELETE; IN_INTER; IN_ELIM_THM] THEN
        RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN
        ASM_MESON_TAC[IN_UNIONS]]);
      ALL_TAC] THEN
    SUBGOAL_THEN
     `s = (s INTER {x:real^N | x$k <= &0}) UNION (s INTER {x | x$k >= &0}) /\
      t = (t INTER {x:real^N | x$k <= &0}) UNION (t INTER {x | x$k >= &0})`
    MP_TAC THENL
     [CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
       `(!x. P x \/ Q x)
        ==> s = (s INTER {x | P x}) UNION (s INTER {x | Q x})`) THEN
      REAL_ARITH_TAC;
      DISCH_THEN(fun th ->
        GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th])] THEN
    W(MP_TAC o PART_MATCH (rand o rand)
       MEASURE_NEGLIGIBLE_UNION o lhand o snd) THEN
    ANTS_TAC THENL
     [REPEAT(CONJ_TAC THENL
       [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
        CONJ_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
        REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                    CLOSED_HALFSPACE_COMPONENT_GE] THEN
        ASM_MESON_TAC[ELEMENTARY_COMPACT];
        ALL_TAC]) THEN
      MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
      EXISTS_TAC `{x:real^N | x$k = &0}` THEN
      ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
      REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN MATCH_MP_TAC(SET_RULE
       `s SUBSET {x | P x} /\ t SUBSET {x | Q x}
        ==> (s INTER t) SUBSET {x | P x /\ Q x}`) THEN
      REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN
      SIMP_TAC[IN_INTER; IN_ELIM_THM; REAL_LE_ADD; VECTOR_ADD_COMPONENT;
        real_ge; REAL_ARITH `x <= &0 /\ y <= &0 ==> x + y <= &0`];
      DISCH_THEN(SUBST1_TAC o SYM)] THEN
    MATCH_MP_TAC MEASURE_SUBSET THEN REPEAT CONJ_TAC THENL
     [MATCH_MP_TAC MEASURABLE_UNION THEN CONJ_TAC THEN
      MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
      CONJ_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
      REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                  CLOSED_HALFSPACE_COMPONENT_GE] THEN
      ASM_MESON_TAC[ELEMENTARY_COMPACT];
      MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
      CONJ_TAC THEN MATCH_MP_TAC COMPACT_UNION THEN CONJ_TAC THEN
      MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
      REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                  CLOSED_HALFSPACE_COMPONENT_GE] THEN
      ASM_MESON_TAC[ELEMENTARY_COMPACT];
      SET_TAC[]]] THEN
  SUBGOAL_THEN
   `&0 < measure(s INTER {x:real^N | x$k <= &0}) /\
    &0 < measure(s INTER {x:real^N | x$k >= &0})`
  STRIP_ASSUME_TAC THENL
   [ASM_SIMP_TAC[MEASURABLE_MEASURE_POS_LT; MEASURABLE_INTER_HALFSPACE_LE;
                 MEASURABLE_INTER_HALFSPACE_GE] THEN
    CONJ_TAC THENL
     [UNDISCH_TAC `~negligible(i:real^N->bool)`;
      UNDISCH_TAC `~negligible(j:real^N->bool)`] THEN
    REWRITE_TAC[CONTRAPOS_THM] THEN MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT]
      NEGLIGIBLE_SUBSET) THEN
    ASM_REWRITE_TAC[SUBSET_INTER] THEN
    UNDISCH_TAC `d1 division_of (s:real^N->bool)` THEN
    REWRITE_TAC[division_of] THEN ASM SET_TAC[];
    ALL_TAC] THEN
  FIRST_X_ASSUM(fun th ->
    MP_TAC(SPECL [`dl:(real^N->bool)->bool`;
                  `{l INTER {x:real^N | x$k <= &0} |l|
                    l IN d2 /\ ~(l INTER {x | x$k <= &0} = {})}`;
                  `UNIONS dl :real^N->bool`;
                   `t INTER {x:real^N | x$k <= &0}`] th) THEN
    MP_TAC(SPECL [`dr:(real^N->bool)->bool`;
                  `{l INTER {x:real^N | x$k >= &0} |l|
                    l IN d2 /\ ~(l INTER {x | x$k >= &0} = {})}`;
                  `UNIONS dr :real^N->bool`;
                   `t INTER {x:real^N | x$k >= &0}`] th)) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [REPEAT CONJ_TAC THENL
     [EXPAND_TAC "n" THEN MATCH_MP_TAC LTE_ADD2 THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC LET_TRANS THEN
        EXISTS_TAC `CARD(d1 DELETE (i:real^N->bool))` THEN CONJ_TAC THENL
         [ALL_TAC; MATCH_MP_TAC CARD_PSUBSET THEN ASM SET_TAC[]];
        ALL_TAC] THEN
      MATCH_MP_TAC(ARITH_RULE
       `CARD {x | x IN IMAGE f s /\ P x} <= CARD(IMAGE f s) /\
        CARD(IMAGE f s) <= CARD s
        ==> CARD {x | x IN IMAGE f s /\ P x} <= CARD s`) THEN
      ASM_SIMP_TAC[CARD_IMAGE_LE; FINITE_DELETE] THEN
      MATCH_MP_TAC CARD_SUBSET THEN
      ASM_SIMP_TAC[FINITE_IMAGE; FINITE_DELETE] THEN SET_TAC[];
      REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_UNIONS] THEN
      ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
      EXISTS_TAC `j INTER {x:real^N | x$k >= &0}` THEN
      REWRITE_TAC[RIGHT_EXISTS_AND_THM; MEMBER_NOT_EMPTY] THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      REWRITE_TAC[IN_ELIM_THM; IN_IMAGE; IN_DELETE; GSYM CONJ_ASSOC] THEN
      CONJ_TAC THENL
       [EXISTS_TAC `j:real^N->bool` THEN ASM_REWRITE_TAC[];
        MATCH_MP_TAC(SET_RULE
         `~(s = {}) /\ s SUBSET t ==> ~(s INTER t = {})`) THEN
        ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[division_of]];
      DISCH_TAC THEN
      UNDISCH_TAC `measure (t INTER {x:real^N | x$k >= &0}) / measure t =
                   measure (s INTER {x:real^N | x$k >= &0}) / measure s` THEN
      ASM_SIMP_TAC[MEASURE_EMPTY; REAL_EQ_RDIV_EQ] THEN
      REWRITE_TAC[real_div; REAL_MUL_LZERO] THEN
      CONV_TAC(RAND_CONV SYM_CONV) THEN ASM_SIMP_TAC[REAL_LT_IMP_NZ];
      REWRITE_TAC[division_of] THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
      REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
      REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
      CONJ_TAC THENL
       [FIRST_ASSUM(fun th ->
            GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
        REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
        ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
         [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
        MATCH_MP_TAC(SET_RULE
         `x IN s ==> x SUBSET UNIONS s`) THEN
        ASM SET_TAC[];
        REPEAT STRIP_TAC THEN
        MATCH_MP_TAC(SET_RULE
         `interior(s) INTER interior(s') = {} /\
          interior(s INTER t) SUBSET interior s /\
          interior(s' INTER t) SUBSET interior s'
          ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
        SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
        ASM_MESON_TAC[division_of]];
      REWRITE_TAC[division_of] THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
      REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
      REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
      REPEAT CONJ_TAC THENL
       [FIRST_ASSUM(fun th ->
            GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
        REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
        ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
         [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
        MATCH_MP_TAC(SET_RULE
          `s SUBSET t ==> s INTER u SUBSET t INTER u`) THEN
        RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN ASM_MESON_TAC[];
        REPEAT STRIP_TAC THEN
        MATCH_MP_TAC(SET_RULE
         `interior(s) INTER interior(s') = {} /\
          interior(s INTER t) SUBSET interior s /\
          interior(s' INTER t) SUBSET interior s'
          ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
        SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
        ASM_MESON_TAC[division_of];
        REWRITE_TAC[SET_RULE `{x | x IN s /\ ~(x = a)} = s DELETE a`] THEN
        GEN_REWRITE_TAC LAND_CONV [SET_RULE `s = {} UNION s`] THEN
        REWRITE_TAC[GSYM UNIONS_INSERT] THEN
        REWRITE_TAC[SET_RULE `x INSERT (s DELETE x) = x INSERT s`] THEN
        REWRITE_TAC[UNIONS_INSERT; UNION_EMPTY] THEN
        REWRITE_TAC[GSYM SIMPLE_IMAGE; GSYM INTER_UNIONS] THEN
        AP_THM_TAC THEN AP_TERM_TAC THEN ASM_MESON_TAC[division_of]]];
    ALL_TAC] THEN
  ONCE_REWRITE_TAC[TAUT `p ==> q ==> r <=> q ==> p ==> r`] THEN ANTS_TAC THENL
   [REPEAT CONJ_TAC THENL
     [EXPAND_TAC "n" THEN MATCH_MP_TAC LTE_ADD2 THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      CONJ_TAC THENL
       [MATCH_MP_TAC LET_TRANS THEN
        EXISTS_TAC `CARD(d1 DELETE (j:real^N->bool))` THEN CONJ_TAC THENL
         [ALL_TAC; MATCH_MP_TAC CARD_PSUBSET THEN ASM SET_TAC[]];
        ALL_TAC] THEN
      MATCH_MP_TAC(ARITH_RULE
       `CARD {x | x IN IMAGE f s /\ P x} <= CARD(IMAGE f s) /\
        CARD(IMAGE f s) <= CARD s
        ==> CARD {x | x IN IMAGE f s /\ P x} <= CARD s`) THEN
      ASM_SIMP_TAC[CARD_IMAGE_LE; FINITE_DELETE] THEN
      MATCH_MP_TAC CARD_SUBSET THEN
      ASM_SIMP_TAC[FINITE_IMAGE; FINITE_DELETE] THEN SET_TAC[];
      REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_UNIONS] THEN
      ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
      EXISTS_TAC `i INTER {x:real^N | x$k <= &0}` THEN
      REWRITE_TAC[RIGHT_EXISTS_AND_THM; MEMBER_NOT_EMPTY] THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      REWRITE_TAC[IN_ELIM_THM; IN_IMAGE; IN_DELETE; GSYM CONJ_ASSOC] THEN
      CONJ_TAC THENL
       [EXISTS_TAC `i:real^N->bool` THEN ASM_REWRITE_TAC[];
        MATCH_MP_TAC(SET_RULE
         `~(s = {}) /\ s SUBSET t ==> ~(s INTER t = {})`) THEN
        ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[division_of]];
      DISCH_TAC THEN
      UNDISCH_TAC `measure (t INTER {x:real^N | x$k <= &0}) / measure t =
                   measure (s INTER {x:real^N | x$k <= &0}) / measure s` THEN
      ASM_SIMP_TAC[MEASURE_EMPTY; REAL_EQ_RDIV_EQ] THEN
      REWRITE_TAC[real_div; REAL_MUL_LZERO] THEN
      CONV_TAC(RAND_CONV SYM_CONV) THEN ASM_SIMP_TAC[REAL_LT_IMP_NZ];
      REWRITE_TAC[division_of] THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
      REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
      REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
      CONJ_TAC THENL
       [FIRST_ASSUM(fun th ->
            GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
        REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
        ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
         [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
        MATCH_MP_TAC(SET_RULE
         `x IN s ==> x SUBSET UNIONS s`) THEN
        ASM SET_TAC[];
        REPEAT STRIP_TAC THEN
        MATCH_MP_TAC(SET_RULE
         `interior(s) INTER interior(s') = {} /\
          interior(s INTER t) SUBSET interior s /\
          interior(s' INTER t) SUBSET interior s'
          ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
        SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
        ASM_MESON_TAC[division_of]];
      REWRITE_TAC[division_of] THEN
      MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
      ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                                     {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
      ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
      REWRITE_TAC[IN_ELIM_THM; IMP_CONJ; FORALL_IN_IMAGE; IN_DELETE] THEN
      REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
      REPEAT CONJ_TAC THENL
       [FIRST_ASSUM(fun th ->
            GEN_REWRITE_TAC I [MATCH_MP FORALL_IN_DIVISION th]) THEN
        REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN
        ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
         [ALL_TAC; ASM_SIMP_TAC[INTERVAL_SPLIT] THEN MESON_TAC[]] THEN
        MATCH_MP_TAC(SET_RULE
          `s SUBSET t ==> s INTER u SUBSET t INTER u`) THEN
        RULE_ASSUM_TAC(REWRITE_RULE[division_of]) THEN ASM_MESON_TAC[];
        REPEAT STRIP_TAC THEN
        MATCH_MP_TAC(SET_RULE
         `interior(s) INTER interior(s') = {} /\
          interior(s INTER t) SUBSET interior s /\
          interior(s' INTER t) SUBSET interior s'
          ==> interior(s INTER t) INTER interior(s' INTER t) = {}`) THEN
        SIMP_TAC[SUBSET_INTERIOR; INTER_SUBSET] THEN
        ASM_MESON_TAC[division_of];
        REWRITE_TAC[SET_RULE `{x | x IN s /\ ~(x = a)} = s DELETE a`] THEN
        GEN_REWRITE_TAC LAND_CONV [SET_RULE `s = {} UNION s`] THEN
        REWRITE_TAC[GSYM UNIONS_INSERT] THEN
        REWRITE_TAC[SET_RULE `x INSERT (s DELETE x) = x INSERT s`] THEN
        REWRITE_TAC[UNIONS_INSERT; UNION_EMPTY] THEN
        REWRITE_TAC[GSYM SIMPLE_IMAGE; GSYM INTER_UNIONS] THEN
        AP_THM_TAC THEN AP_TERM_TAC THEN ASM_MESON_TAC[division_of]]];
    ALL_TAC] THEN
  REWRITE_TAC[real_ge; IMP_IMP] THEN
  SUBGOAL_THEN
   `compact(UNIONS dl:real^N->bool) /\ compact(UNIONS dr:real^N->bool)`
  STRIP_ASSUME_TAC THENL
   [CONJ_TAC THEN MATCH_MP_TAC COMPACT_UNIONS THEN
    MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
    ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                               {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
    ASM_SIMP_TAC[FINITE_RESTRICT; FINITE_IMAGE; FINITE_DELETE] THEN
    REWRITE_TAC[IMP_CONJ; IN_ELIM_THM; FORALL_IN_IMAGE; IN_DELETE] THEN
    REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
    REWRITE_TAC[CLOSED_HALFSPACE_COMPONENT_LE;
                CLOSED_HALFSPACE_COMPONENT_GE] THEN
    ASM_MESON_TAC[division_of; COMPACT_INTERVAL];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `measurable(UNIONS dl:real^N->bool) /\
    measurable(UNIONS dr:real^N->bool)`
  STRIP_ASSUME_TAC THENL [ASM_SIMP_TAC[MEASURABLE_COMPACT]; ALL_TAC] THEN
  SUBGOAL_THEN
    `measurable { x + y:real^N |
                  x IN UNIONS dl /\ y IN t INTER {x | x$k <= &0}} /\
     measurable { x + y:real^N |
                  x IN UNIONS dr /\ y IN t INTER {x | &0 <= x$k}}`
  STRIP_ASSUME_TAC THENL
   [CONJ_TAC THEN MATCH_MP_TAC MEASURABLE_COMPACT THEN
    MATCH_MP_TAC COMPACT_SUMS THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC COMPACT_INTER_CLOSED THEN
    REWRITE_TAC[REAL_ARITH `&0 <= x <=> x >= &0`;
      CLOSED_HALFSPACE_COMPONENT_LE; CLOSED_HALFSPACE_COMPONENT_GE] THEN
    ASM_MESON_TAC[ELEMENTARY_COMPACT];
    ALL_TAC] THEN
 ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
  [REAL_LE_ROOT; DIMINDEX_NONZERO; REAL_LE_ADD; ROOT_POS_LE;
   MEASURE_POS_LE; MEASURABLE_INTER_HALFSPACE_LE;
   MEASURABLE_INTER_HALFSPACE_GE; REAL_ARITH `&0 <= x <=> x >= &0`] THEN
  MATCH_MP_TAC(REAL_ARITH
   `x <= a' + b' ==> a' <= a /\ b' <= b ==> x <= a + b`) THEN
  SUBGOAL_THEN
   `measure(UNIONS dl :real^N->bool) =
    measure(s INTER {x:real^N | x$k <= &0}) /\
    measure(UNIONS dr :real^N->bool) =
    measure(s INTER {x:real^N | x$k >= &0})`
   (CONJUNCTS_THEN SUBST1_TAC)
  THENL
   [MAP_EVERY EXPAND_TAC ["dl"; "dr"] THEN
    ONCE_REWRITE_TAC[SET_RULE `{f x |x| x IN s /\ ~(f x = a)} =
                               {t | t IN IMAGE f s /\ ~(t = a)}`] THEN
    REWRITE_TAC[SET_RULE `{x | x IN s /\ ~(x = a)} = s DELETE a`] THEN
    CONJ_TAC THEN
    GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SET_RULE `s = {} UNION s`] THEN
    REWRITE_TAC[GSYM UNIONS_INSERT] THEN
    REWRITE_TAC[SET_RULE `x INSERT (s DELETE x) = x INSERT s`] THEN
    REWRITE_TAC[UNIONS_INSERT; UNION_EMPTY] THEN
    REWRITE_TAC[GSYM SIMPLE_IMAGE; GSYM INTER_UNIONS] THEN
    MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN
    MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
    EXISTS_TAC `{x:real^N | x$k = &0}` THEN
    ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
    MATCH_MP_TAC(SET_RULE
     `s SUBSET t /\ t DIFF s SUBSET u
      ==> (s DIFF t UNION t DIFF s) SUBSET u`) THEN
    REWRITE_TAC[SET_RULE `s INTER u DIFF t INTER u = (s DIFF t) INTER u`] THEN
    (SUBGOAL_THEN `s:real^N->bool = UNIONS d1` SUBST1_TAC THENL
      [ASM_MESON_TAC[division_of]; ALL_TAC] THEN
     CONJ_TAC THENL [SET_TAC[]; ALL_TAC]) THEN
    REWRITE_TAC[GSYM REAL_LE_ANTISYM; real_ge; SET_RULE
     `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`]
    THENL
     [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> s INTER u SUBSET u INTER t`);
      MATCH_MP_TAC(SET_RULE `s SUBSET t ==> s INTER u SUBSET t INTER u`)] THEN
    RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN
    FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP
     (REWRITE_RULE[IMP_CONJ_ALT] SUBSET_TRANS)) THEN
    SET_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `root (dimindex (:N)) (measure (s INTER {x:real^N | x$k <= &0})) +
    root (dimindex (:N)) (measure (t INTER {x:real^N | x$k <= &0})) =
    root (dimindex (:N)) (measure (s INTER {x | x$k <= &0})) *
    (&1 + root (dimindex (:N)) (measure (t INTER {x | x$k <= &0})) /
          root (dimindex (:N)) (measure (s INTER {x | x$k <= &0}))) /\
   root (dimindex (:N)) (measure (s INTER {x:real^N | x$k >= &0})) +
    root (dimindex (:N)) (measure (t INTER {x:real^N | x$k >= &0})) =
    root (dimindex (:N)) (measure (s INTER {x | x$k >= &0})) *
    (&1 + root (dimindex (:N)) (measure (t INTER {x | x$k >= &0})) /
          root (dimindex (:N)) (measure (s INTER {x | x$k >= &0})))`
  (CONJUNCTS_THEN SUBST1_TAC) THENL
   [CONJ_TAC THEN
    MATCH_MP_TAC(REAL_FIELD `&0 < s ==> s + t = s * (&1 + t / s)`) THEN
    ASM_SIMP_TAC[ROOT_POS_LT; DIMINDEX_NONZERO];
    ALL_TAC] THEN
  ASM_SIMP_TAC[DIMINDEX_NONZERO; GSYM REAL_ROOT_DIV; MEASURE_POS_LE;
    MEASURABLE_INTER_HALFSPACE_LE; MEASURABLE_INTER_HALFSPACE_GE] THEN
  SUBGOAL_THEN
   `measure(t INTER {x:real^N | x$k <= &0}) /
    measure(s INTER {x:real^N | x$k <= &0}) = measure t / measure s /\
    measure(t INTER {x:real^N | x$k >= &0}) /
    measure(s INTER {x:real^N | x$k >= &0}) = measure t / measure s`
  (CONJUNCTS_THEN SUBST1_TAC) THENL
   [MATCH_MP_TAC(REAL_FIELD
     `tn / t = sn / s /\ tp / t = sp / s /\
      &0 < sp /\ &0 < sn /\ &0 < s /\ &0 < t
      ==> tn / sn = t / s /\ tp / sp = t / s`) THEN
    ASM_REWRITE_TAC[];
    ALL_TAC] THEN
  REWRITE_TAC[GSYM REAL_ADD_RDISTRIB; REAL_POW_MUL] THEN
  ASM_SIMP_TAC[REAL_POW_ROOT; DIMINDEX_NONZERO; MEASURE_POS_LE;
           MEASURABLE_INTER_HALFSPACE_LE; MEASURABLE_INTER_HALFSPACE_GE] THEN
  SUBGOAL_THEN
   `measure (s INTER {x | x$k <= &0}) + measure (s INTER {x | x$k >= &0}) =
    root (dimindex(:N)) (measure(s:real^N->bool)) pow (dimindex(:N))`
  SUBST1_TAC THENL
   [ASM_SIMP_TAC[REAL_POW_ROOT; DIMINDEX_NONZERO; REAL_LT_IMP_LE] THEN
    MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNION_EQ THEN
    ASM_SIMP_TAC[MEASURABLE_INTER_HALFSPACE_LE;
                 MEASURABLE_INTER_HALFSPACE_GE] THEN
    CONJ_TAC THENL
     [REWRITE_TAC[EXTENSION; IN_UNION; IN_INTER; IN_ELIM_THM] THEN
      X_GEN_TAC `x:real^N` THEN ASM_CASES_TAC `(x:real^N) IN s` THEN
      ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
      MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
      EXISTS_TAC `{x:real^N | x$k = &0}` THEN
      ASM_SIMP_TAC[NEGLIGIBLE_STANDARD_HYPERPLANE] THEN
      REWRITE_TAC[GSYM REAL_LE_ANTISYM; real_ge] THEN SET_TAC[]];
    ASM_SIMP_TAC[GSYM REAL_ROOT_MUL; MEASURE_POS_LE; DIMINDEX_NONZERO;
                 REAL_LE_DIV; GSYM REAL_POW_MUL;
                 REAL_ADD_LDISTRIB; REAL_MUL_RID] THEN
    ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_LE_REFL]]);;

(* ------------------------------------------------------------------------- *)
(* Now for open sets.                                                        *)
(* ------------------------------------------------------------------------- *)

let BRUNN_MINKOWSKI_OPEN = 
prove
 (`!s t:real^N->bool.
    (s = {} <=> t = {}) /\ bounded s /\ open s /\ bounded t /\ open t
    ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
        >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
  ASM_SIMP_TAC[SET_RULE `{x + y:real^N | x IN {} /\ y IN {}} = {}`;
               REAL_LE_REFL; MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO;
               real_ge; REAL_ADD_LID] THEN
  STRIP_TAC THEN
  MATCH_MP_TAC(ISPEC `atreal(&0) within {e | &0 <= e}` REALLIM_UBOUND) THEN
  EXISTS_TAC `\e. root (dimindex(:N)) (measure(s:real^N->bool) - e) +
                  root (dimindex(:N)) (measure(t:real^N->bool) - e)` THEN
  REPEAT CONJ_TAC THENL
   [MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
    EXISTS_TAC
     `\e. (measure(s:real^N->bool) - e) rpow (inv(&(dimindex(:N)))) +
          (measure(t:real^N->bool) - e) rpow (inv(&(dimindex(:N))))` THEN
    REWRITE_TAC[] THEN CONJ_TAC THENL
     [REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
      EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
      ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO;
                   MEASURE_OPEN_POS_LT] THEN
      REPEAT STRIP_TAC THEN BINOP_TAC THEN CONV_TAC SYM_CONV THEN
      MATCH_MP_TAC REAL_ROOT_RPOW THEN
      REWRITE_TAC[DIMINDEX_NONZERO] THEN ASM_REAL_ARITH_TAC;
      ASM_SIMP_TAC[REAL_ROOT_RPOW; MEASURE_OPEN_POS_LT; DIMINDEX_NONZERO;
                   REAL_LT_IMP_LE] THEN
      MATCH_MP_TAC REALLIM_ADD THEN CONJ_TAC THEN
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
       [REAL_ARITH `measure(s:real^N->bool) = measure s - &0`] THEN
      REWRITE_TAC[GSYM REAL_CONTINUOUS_WITHINREAL] THEN
      REWRITE_TAC[GSYM(REWRITE_CONV [o_DEF]
        `(\x. x rpow y) o (\e. s - e)`)] THEN
      MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE THEN
      ASM_SIMP_TAC[REAL_CONTINUOUS_SUB; REAL_CONTINUOUS_WITHIN_ID;
                   REAL_CONTINUOUS_CONST] THEN
      MATCH_MP_TAC REAL_CONTINUOUS_WITHIN_RPOW THEN
      REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS]];
    W(MP_TAC o PART_MATCH (lhand o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
      rand o snd) THEN
    ANTS_TAC THENL
     [REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN REAL_ARITH_TAC;
      DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[EXTENSION; IN_SING] THEN
      DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
      REAL_ARITH_TAC];
    REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
    EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
    ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO;
                 MEASURE_OPEN_POS_LT] THEN
    X_GEN_TAC `e:real` THEN REWRITE_TAC[real_abs] THEN
    ASM_CASES_TAC `&0 <= e` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
    MAP_EVERY (fun l -> MP_TAC(ISPECL l OPEN_MEASURABLE_INNER_DIVISION))
    [[`t:real^N->bool`; `e:real`]; [`s:real^N->bool`; `e:real`]] THEN
    ASM_SIMP_TAC[MEASURABLE_OPEN; GSYM REAL_LT_SUB_RADD] THEN
    DISCH_THEN(X_CHOOSE_THEN `D:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
    DISCH_THEN(X_CHOOSE_THEN `E:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
    MP_TAC(ISPECL [`UNIONS D:real^N->bool`; `UNIONS E:real^N->bool`]
        BRUNN_MINKOWSKI_ELEMENTARY) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[MEASURE_EMPTY; REAL_ARITH `e < s ==> ~(s - e < &0)`];
      ALL_TAC] THEN
    MATCH_MP_TAC(REAL_ARITH
     `s1 <= r1 /\ s2 <= r2 /\ rs <= s
      ==> rs >= r1 + r2 ==> s1 + s2 <= s`) THEN
    REPEAT CONJ_TAC THEN MATCH_MP_TAC ROOT_MONO_LE THEN
    ASM_SIMP_TAC[DIMINDEX_NONZERO; REAL_SUB_LE; REAL_LT_IMP_LE] THEN
    SUBGOAL_THEN
     `measurable {x + y :real^N | x IN UNIONS D /\ y IN UNIONS E}`
    ASSUME_TAC THENL
     [MATCH_MP_TAC MEASURABLE_COMPACT THEN MATCH_MP_TAC COMPACT_SUMS THEN
      ASM_MESON_TAC[ELEMENTARY_COMPACT];
      ALL_TAC] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC MEASURE_POS_LE; MATCH_MP_TAC MEASURE_SUBSET] THEN
    ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
    MATCH_MP_TAC MEASURABLE_OPEN THEN
    ASM_SIMP_TAC[BOUNDED_SUMS; OPEN_SUMS]]);;
(* ------------------------------------------------------------------------- *)
(* Now for convex sets.                                                      *)
(* ------------------------------------------------------------------------- *)

let BRUNN_MINKOWSKI_CONVEX = 
prove
 (`!s t:real^N->bool.
    (s = {} <=> t = {}) /\ bounded s /\ convex s /\ bounded t /\ convex t
    ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
        >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
  ASM_SIMP_TAC[BRUNN_MINKOWSKI_OPEN; OPEN_EMPTY] THEN STRIP_TAC THEN
  ASM_SIMP_TAC[GSYM MEASURE_INTERIOR; NEGLIGIBLE_CONVEX_FRONTIER; real_ge] THEN
  ASM_CASES_TAC `interior s:real^N->bool = {}` THENL
   [ASM_SIMP_TAC[MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO; REAL_ADD_LID] THEN
    MATCH_MP_TAC ROOT_MONO_LE THEN
    ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_INTERIOR] THEN
    SUBGOAL_THEN `?a:real^N. a IN s` STRIP_ASSUME_TAC THENL
     [ASM SET_TAC[]; ALL_TAC] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) t)` THEN CONJ_TAC THENL
     [ASM_SIMP_TAC[MEASURE_TRANSLATION; MEASURE_INTERIOR;
                   NEGLIGIBLE_CONVEX_FRONTIER; REAL_LE_REFL];
      MATCH_MP_TAC MEASURE_SUBSET THEN
      ASM_SIMP_TAC[MEASURABLE_TRANSLATION_EQ; MEASURABLE_CONVEX;
                   CONVEX_SUMS; BOUNDED_SUMS] THEN
      ASM SET_TAC[]];
    ALL_TAC] THEN
  ASM_CASES_TAC `interior t:real^N->bool = {}` THENL
   [ASM_SIMP_TAC[MEASURE_EMPTY; ROOT_0; DIMINDEX_NONZERO; REAL_ADD_RID] THEN
    MATCH_MP_TAC ROOT_MONO_LE THEN
    ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_INTERIOR] THEN
    SUBGOAL_THEN `?a:real^N. a IN t` STRIP_ASSUME_TAC THENL
     [ASM SET_TAC[]; ALL_TAC] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) s)` THEN CONJ_TAC THENL
     [ASM_SIMP_TAC[MEASURE_TRANSLATION; MEASURE_INTERIOR;
                   NEGLIGIBLE_CONVEX_FRONTIER; REAL_LE_REFL];
      MATCH_MP_TAC MEASURE_SUBSET THEN
      ASM_SIMP_TAC[MEASURABLE_TRANSLATION_EQ; MEASURABLE_CONVEX;
                   CONVEX_SUMS; BOUNDED_SUMS] THEN
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ADD_SYM] THEN
      ASM SET_TAC[]];
    ALL_TAC] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
    `root (dimindex (:N))
          (measure {x + y:real^N | x IN interior s /\ y IN interior t})` THEN
  ASM_SIMP_TAC[GSYM real_ge; BRUNN_MINKOWSKI_OPEN; BOUNDED_INTERIOR;
               OPEN_INTERIOR] THEN
  REWRITE_TAC[real_ge] THEN MATCH_MP_TAC ROOT_MONO_LE THEN
  REWRITE_TAC[DIMINDEX_NONZERO] THEN CONJ_TAC THENL
   [MATCH_MP_TAC MEASURE_POS_LE;
    MATCH_MP_TAC MEASURE_SUBSET] THEN
  ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE; BOUNDED_SUMS;
     MEASURABLE_CONVEX; BOUNDED_INTERIOR; CONVEX_SUMS; CONVEX_INTERIOR] THEN
  MATCH_MP_TAC(SET_RULE
   `s' SUBSET s /\ t' SUBSET t
    ==> {x + y:real^N | x IN s' /\ y IN t'} SUBSET
        {x + y | x IN s /\ y IN t}`) THEN
  REWRITE_TAC[INTERIOR_SUBSET]);;
(* ------------------------------------------------------------------------- *)
(* Now for compact sets.                                                     *)
(* ------------------------------------------------------------------------- *)

let INTERS_SUMS_CLOSED_BALL_SEQUENTIAL = 
prove
 (`!s:real^N->bool.
        closed s
        ==> INTERS {{x + d | x IN s /\ d IN ball(vec 0,inv(&n + &1))} |
                    n IN (:num)} = s`,

  REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
  REWRITE_TAC[INTERS_GSPEC; IN_ELIM_THM; IN_UNIV] THEN
  X_GEN_TAC `x:real^N` THEN EQ_TAC THENL
   [ASM_CASES_TAC `(x:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
    MP_TAC(ISPECL [`s:real^N->bool`; `x:real^N`] SEPARATE_POINT_CLOSED) THEN
    ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:real` THEN
    DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
    GEN_REWRITE_TAC LAND_CONV [REAL_ARCH_INV] THEN
    DISCH_THEN(X_CHOOSE_THEN `n:num` STRIP_ASSUME_TAC) THEN
    DISCH_THEN(MP_TAC o SPEC `n:num`) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`y:real^N`; `e:real^N`] THEN
    REWRITE_TAC[IN_BALL_0] THEN STRIP_TAC THEN
    FIRST_X_ASSUM SUBST_ALL_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N`) THEN
    ASM_REWRITE_TAC[NORM_ARITH `dist(y + e:real^N,y) = norm e`] THEN
    SUBGOAL_THEN `inv(&n + &1) <= inv(&n)` MP_TAC THENL
     [MATCH_MP_TAC REAL_LE_INV2 THEN
      REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
      ASM_ARITH_TAC;
      ASM_REAL_ARITH_TAC];
    DISCH_TAC THEN X_GEN_TAC `n:num` THEN
    MAP_EVERY EXISTS_TAC [`x:real^N`; `vec 0:real^N`] THEN
    ASM_REWRITE_TAC[CENTRE_IN_BALL; VECTOR_ADD_RID; REAL_LT_INV_EQ] THEN
    REAL_ARITH_TAC]);;
let MEASURE_SUMS_COMPACT_EPSILON = 
prove
 (`!s:real^N->bool.
        compact s
        ==> ((\e. measure {x + d | x IN s /\ d IN ball(vec 0,e)})
             ---> measure s)
            (atreal (&0) within {e | &0 <= e})`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPEC
   `\n. {x + d:real^N | x IN s /\ d IN ball(vec 0,inv(&n + &1))}`
   HAS_MEASURE_NESTED_INTERS) THEN
  ASM_SIMP_TAC[INTERS_SUMS_CLOSED_BALL_SEQUENTIAL; COMPACT_IMP_CLOSED] THEN
  ANTS_TAC THENL
   [ASM_SIMP_TAC[MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS;
                 COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL] THEN
    GEN_TAC THEN MATCH_MP_TAC(SET_RULE
     `t' SUBSET t
      ==> {x + y:real^N | x IN s /\ y IN t'} SUBSET
          {x + y | x IN s /\ y IN t}`) THEN
    MATCH_MP_TAC SUBSET_BALL THEN MATCH_MP_TAC REAL_LE_INV2 THEN
    REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
    ARITH_TAC;
    ALL_TAC] THEN
  REWRITE_TAC[GSYM(REWRITE_RULE[o_DEF] TENDSTO_REAL)] THEN
  REWRITE_TAC[REALLIM_SEQUENTIALLY; REALLIM_WITHINREAL] THEN
  STRIP_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `inv(&N + &1)` THEN
  ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN
  CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
  X_GEN_TAC `d:real` THEN REWRITE_TAC[IN_ELIM_THM; REAL_SUB_RZERO] THEN
  ASM_CASES_TAC `abs d = d` THENL
   [FIRST_X_ASSUM SUBST1_TAC THEN STRIP_TAC; ASM_REAL_ARITH_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `N:num`) THEN REWRITE_TAC[LE_REFL] THEN
  MATCH_MP_TAC(REAL_ARITH
   `m <= m1 /\ m1 <= m2
    ==> abs(m2 - m) < e ==> abs(m1 - m) < e`) THEN
  CONJ_TAC THEN MATCH_MP_TAC MEASURE_SUBSET THEN
  ASM_SIMP_TAC[MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS;
               COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL]
  THENL
   [REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `x:real^N` THEN
    DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`x:real^N`; `vec 0:real^N`] THEN
    ASM_REWRITE_TAC[CENTRE_IN_BALL; VECTOR_ADD_RID];
    MATCH_MP_TAC(SET_RULE
     `t' SUBSET t
      ==> {x + y:real^N | x IN s /\ y IN t'} SUBSET
          {x + y | x IN s /\ y IN t}`) THEN
    MATCH_MP_TAC SUBSET_BALL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE]]);;
let BRUNN_MINKOWSKI_COMPACT = 
prove
 (`!s t:real^N->bool.
    (s = {} <=> t = {}) /\ compact s /\ compact t
    ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
        >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,

  
let lemma1 = prove
   (`{ x + y:real^N | x IN {x + d | x IN s /\ d IN ball(vec 0,e)} /\
                      y IN {y + d | y IN t /\ d IN ball(vec 0,e)}} =
     { z + d | z IN {x + y | x IN s /\ y IN t} /\ d IN ball(vec 0,&2 * e) }`,
    MATCH_MP_TAC SUBSET_ANTISYM THEN
    REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN
    REWRITE_TAC[IN_ELIM_THM; IN_BALL_0] THEN CONJ_TAC THENL
     [X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
      X_GEN_TAC `d:real^N` THEN DISCH_TAC THEN
      X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
      X_GEN_TAC `k:real^N` THEN DISCH_TAC THEN
      EXISTS_TAC `x + y:real^N` THEN EXISTS_TAC `d + k:real^N` THEN
      CONJ_TAC THENL [ALL_TAC; VECTOR_ARITH_TAC] THEN
      ASM_SIMP_TAC[NORM_ARITH
       `norm(d:real^N) < e /\ norm(k) < e ==> norm(d + k) < &2 * e`] THEN
      EXISTS_TAC `x:real^N` THEN EXISTS_TAC `y:real^N` THEN
      ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC;
      X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
      X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
      X_GEN_TAC `d:real^N` THEN DISCH_TAC THEN
      EXISTS_TAC `x + inv(&2) % d:real^N` THEN
      EXISTS_TAC `y + inv(&2) % d:real^N` THEN
      CONJ_TAC THENL [ALL_TAC; VECTOR_ARITH_TAC] THEN CONJ_TAC THENL
       [EXISTS_TAC `x:real^N`; EXISTS_TAC `y:real^N`] THEN
      EXISTS_TAC `inv(&2) % d:real^N` THEN
      ASM_REWRITE_TAC[NORM_MUL] THEN ASM_REAL_ARITH_TAC])
  and lemma2 = prove
   (`(f ---> l) (atreal (&0) within {e | &0 <= e})
     ==> ((\e. f(&2 * e)) ---> l) (atreal (&0) within {e | &0 <= e})`,
    REWRITE_TAC[REALLIM_WITHINREAL] THEN DISCH_TAC THEN
    X_GEN_TAC `e:real` THEN DISCH_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
    REWRITE_TAC[IN_ELIM_THM; REAL_SUB_RZERO] THEN
    DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `d / &2` THEN ASM_REWRITE_TAC[REAL_HALF] THEN
    REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
    ASM_REAL_ARITH_TAC) in
  REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
  ASM_SIMP_TAC[BRUNN_MINKOWSKI_OPEN; OPEN_EMPTY; BOUNDED_EMPTY] THEN
  STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
  MATCH_MP_TAC(ISPEC `atreal (&0) within {e | &0 <= e}` REALLIM_LE) THEN
  EXISTS_TAC
   `\e. root (dimindex(:N))
             (measure {x + d:real^N | x IN s /\ d IN ball(vec 0,e)}) +
        root (dimindex(:N))
             (measure {x + d:real^N | x IN t /\ d IN ball(vec 0,e)})` THEN
  EXISTS_TAC
   `\e. root (dimindex(:N))
             (measure { x + y:real^N |
                   x IN {x + d | x IN s /\ d IN ball(vec 0,e)} /\
                   y IN {y + d | y IN t /\ d IN ball(vec 0,e)}})` THEN
  REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
   [ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
     [REAL_ROOT_RPOW; DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_COMPACT;
      MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS;
      COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL] THEN
    MATCH_MP_TAC REALLIM_ADD THEN CONJ_TAC THEN MATCH_MP_TAC REALLIM_RPOW THEN
    REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
    MATCH_MP_TAC MEASURE_SUMS_COMPACT_EPSILON THEN ASM_REWRITE_TAC[];
    REWRITE_TAC[lemma1] THEN MATCH_MP_TAC lemma2 THEN
    ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 6)
     [REAL_ROOT_RPOW; DIMINDEX_NONZERO; MEASURE_POS_LE; MEASURABLE_COMPACT;
      MEASURABLE_OPEN; BOUNDED_SUMS; OPEN_SUMS; COMPACT_SUMS;
      COMPACT_IMP_BOUNDED; BOUNDED_BALL; OPEN_BALL] THEN
    MATCH_MP_TAC REALLIM_RPOW THEN
    REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
    MATCH_MP_TAC MEASURE_SUMS_COMPACT_EPSILON THEN
    ASM_SIMP_TAC[COMPACT_SUMS];
    W(MP_TAC o PART_MATCH (lhand o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
      rand o snd) THEN
    ANTS_TAC THENL
     [REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN REAL_ARITH_TAC;
      DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[EXTENSION; IN_SING] THEN
      DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
      REAL_ARITH_TAC];
    MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `e:real` THEN
    REWRITE_TAC[GSYM real_ge] THEN
    MATCH_MP_TAC BRUNN_MINKOWSKI_OPEN THEN
    SIMP_TAC[OPEN_SUMS; OPEN_BALL] THEN
    ASM_SIMP_TAC[BOUNDED_SUMS; BOUNDED_BALL; COMPACT_IMP_BOUNDED] THEN
    ASM SET_TAC[]]);;
(* ------------------------------------------------------------------------- *)
(* Finally, for an arbitrary measurable set. In this general case, the       *)
(* measurability of the sum-set is needed as an additional hypothesis.       *)
(* ------------------------------------------------------------------------- *)

let BRUNN_MINKOWSKI_MEASURABLE = 
prove
 (`!s t:real^N->bool.
    (s = {} <=> t = {}) /\ measurable s /\ measurable t /\
    measurable {x + y | x IN s /\ y IN t}
    ==> root (dimindex(:N)) (measure {x + y | x IN s /\ y IN t})
        >= root (dimindex(:N)) (measure s) + root (dimindex(:N)) (measure t)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `t:real^N->bool = {}` THEN
  ASM_SIMP_TAC[BRUNN_MINKOWSKI_OPEN; OPEN_EMPTY; BOUNDED_EMPTY] THEN
  STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
  ASM_CASES_TAC `measure(s:real^N->bool) = &0` THENL
   [ASM_SIMP_TAC[ROOT_0; DIMINDEX_NONZERO; REAL_ADD_LID] THEN
    MATCH_MP_TAC ROOT_MONO_LE THEN
    ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE] THEN
    SUBGOAL_THEN `?a:real^N. a IN s` STRIP_ASSUME_TAC THENL
     [ASM SET_TAC[]; ALL_TAC] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) t)` THEN CONJ_TAC THENL
     [ASM_SIMP_TAC[MEASURE_TRANSLATION; REAL_LE_REFL];
      MATCH_MP_TAC MEASURE_SUBSET THEN
      ASM_REWRITE_TAC[MEASURABLE_TRANSLATION_EQ] THEN
      ASM SET_TAC[]];
    ALL_TAC] THEN
  ASM_CASES_TAC `measure(t:real^N->bool) = &0` THENL
   [ASM_SIMP_TAC[ROOT_0; DIMINDEX_NONZERO; REAL_ADD_RID] THEN
    MATCH_MP_TAC ROOT_MONO_LE THEN
    ASM_SIMP_TAC[DIMINDEX_NONZERO; MEASURE_POS_LE] THEN
    SUBGOAL_THEN `?a:real^N. a IN t` STRIP_ASSUME_TAC THENL
     [ASM SET_TAC[]; ALL_TAC] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC `measure(IMAGE (\x:real^N. a + x) s)` THEN CONJ_TAC THENL
     [ASM_SIMP_TAC[MEASURE_TRANSLATION; REAL_LE_REFL];
      MATCH_MP_TAC MEASURE_SUBSET THEN
      ASM_REWRITE_TAC[MEASURABLE_TRANSLATION_EQ] THEN
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ADD_SYM] THEN
      ASM SET_TAC[]];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `&0 < measure(s:real^N->bool) /\
    &0 < measure(t:real^N->bool)`
  STRIP_ASSUME_TAC THENL
   [ASM_MESON_TAC[MEASURABLE_MEASURE_POS_LT; MEASURABLE_MEASURE_EQ_0];
    ALL_TAC] THEN
  MATCH_MP_TAC(ISPEC `atreal(&0) within {e | &0 <= e}` REALLIM_UBOUND) THEN
  EXISTS_TAC `\e. root (dimindex(:N)) (measure(s:real^N->bool) - e) +
                  root (dimindex(:N)) (measure(t:real^N->bool) - e)` THEN
  REPEAT CONJ_TAC THENL
   [MATCH_MP_TAC REALLIM_TRANSFORM_EVENTUALLY THEN
    EXISTS_TAC
     `\e. (measure(s:real^N->bool) - e) rpow (inv(&(dimindex(:N)))) +
          (measure(t:real^N->bool) - e) rpow (inv(&(dimindex(:N))))` THEN
    REWRITE_TAC[] THEN CONJ_TAC THENL
     [REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
      EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
      ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO;
                   MEASURE_OPEN_POS_LT] THEN
      REPEAT STRIP_TAC THEN BINOP_TAC THEN CONV_TAC SYM_CONV THEN
      MATCH_MP_TAC REAL_ROOT_RPOW THEN
      REWRITE_TAC[DIMINDEX_NONZERO] THEN ASM_REAL_ARITH_TAC;
      ASM_SIMP_TAC[REAL_ROOT_RPOW; MEASURE_OPEN_POS_LT; DIMINDEX_NONZERO;
                   REAL_LT_IMP_LE] THEN
      MATCH_MP_TAC REALLIM_ADD THEN CONJ_TAC THEN
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
       [REAL_ARITH `measure(s:real^N->bool) = measure s - &0`] THEN
      REWRITE_TAC[GSYM REAL_CONTINUOUS_WITHINREAL] THEN
      REWRITE_TAC[GSYM(REWRITE_CONV [o_DEF]
        `(\x. x rpow y) o (\e. s - e)`)] THEN
      MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE THEN
      ASM_SIMP_TAC[REAL_CONTINUOUS_SUB; REAL_CONTINUOUS_WITHIN_ID;
                   REAL_CONTINUOUS_CONST] THEN
      MATCH_MP_TAC REAL_CONTINUOUS_WITHIN_RPOW THEN
      REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS]];
    W(MP_TAC o PART_MATCH (lhand o rand) TRIVIAL_LIMIT_WITHIN_REALINTERVAL o
      rand o snd) THEN
    ANTS_TAC THENL
     [REWRITE_TAC[is_realinterval; IN_ELIM_THM] THEN REAL_ARITH_TAC;
      DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[EXTENSION; IN_SING] THEN
      DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[IN_ELIM_THM] THEN
      REAL_ARITH_TAC];
    REWRITE_TAC[EVENTUALLY_WITHINREAL] THEN
    EXISTS_TAC `min (measure(s:real^N->bool)) (measure(t:real^N->bool))` THEN
    ASM_SIMP_TAC[REAL_LT_MIN; IN_ELIM_THM; REAL_SUB_RZERO] THEN
    X_GEN_TAC `e:real` THEN REWRITE_TAC[real_abs] THEN
    ASM_CASES_TAC `&0 <= e` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
    MAP_EVERY (fun l -> MP_TAC(ISPECL l MEASURABLE_INNER_COMPACT))
    [[`t:real^N->bool`; `e:real`]; [`s:real^N->bool`; `e:real`]] THEN
    ASM_SIMP_TAC[MEASURABLE_OPEN; GSYM REAL_LT_SUB_RADD] THEN
    DISCH_THEN(X_CHOOSE_THEN `s':real^N->bool` STRIP_ASSUME_TAC) THEN
    DISCH_THEN(X_CHOOSE_THEN `t':real^N->bool` STRIP_ASSUME_TAC) THEN
    MP_TAC(ISPECL [`s':real^N->bool`; `t':real^N->bool`]
        BRUNN_MINKOWSKI_COMPACT) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[MEASURE_EMPTY; REAL_ARITH `e < s ==> ~(s - e < &0)`];
      ALL_TAC] THEN
    MATCH_MP_TAC(REAL_ARITH
     `s1 <= r1 /\ s2 <= r2 /\ rs <= s
      ==> rs >= r1 + r2 ==> s1 + s2 <= s`) THEN
    REPEAT CONJ_TAC THEN MATCH_MP_TAC ROOT_MONO_LE THEN
    ASM_SIMP_TAC[DIMINDEX_NONZERO; REAL_SUB_LE; REAL_LT_IMP_LE] THEN
    ASM_SIMP_TAC[MEASURE_POS_LE; COMPACT_SUMS; MEASURABLE_COMPACT] THEN
    MATCH_MP_TAC MEASURE_SUBSET THEN
    ASM_SIMP_TAC[MEASURE_POS_LE; COMPACT_SUMS; MEASURABLE_COMPACT] THEN
    ASM SET_TAC[]]);;