(* ========================================================================= *)
(* Minkowski's convex body theorem.                                          *)
(* ========================================================================= *)

needs "Multivariate/measure.ml";;

(* ------------------------------------------------------------------------- *)
(* An ad hoc lemma.                                                          *)
(* ------------------------------------------------------------------------- *)

let LEMMA = 
prove (`!f:real^N->bool t s:real^N->bool. FINITE { u | u IN f /\ ~(t u = {})} /\ measurable s /\ &1 < measure s /\ (!u. u IN f ==> measurable(t u)) /\ s SUBSET UNIONS (IMAGE t f) /\ (!u v. u IN f /\ v IN f /\ ~(u = v) ==> DISJOINT (t u) (t v)) /\ (!u. u IN f ==> (IMAGE (\x. x - u) (t u)) SUBSET interval[vec 0,vec 1]) ==> ?u v. u IN f /\ v IN f /\ ~(u = v) /\ ~(DISJOINT (IMAGE (\x. x - u) (t u)) (IMAGE (\x. x - v) (t v)))`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [TAUT `p <=> ~ ~p`] THEN PURE_REWRITE_TAC[NOT_EXISTS_THM] THEN REWRITE_TAC[TAUT `~(a /\ b /\ ~c /\ ~d) <=> a /\ b /\ ~c ==> d`] THEN DISCH_TAC THEN MP_TAC(ISPECL [`\u:real^N. IMAGE (\x:real^N. x - u) (t u)`; `f:real^N->bool`] HAS_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG) THEN ASM_REWRITE_TAC[IMAGE_EQ_EMPTY; NOT_IMP] THEN CONJ_TAC THENL [REWRITE_TAC[VECTOR_ARITH `x - u:real^N = --u + x`] THEN ASM_REWRITE_TAC[MEASURABLE_TRANSLATION_EQ]; ALL_TAC] THEN MP_TAC(ISPECL [`vec 0:real^N`; `vec 1:real^N`] (CONJUNCT1 HAS_MEASURE_INTERVAL)) THEN REWRITE_TAC[CONTENT_UNIT] THEN MATCH_MP_TAC(TAUT `(b /\ a ==> F) ==> a ==> ~b`) THEN DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE [TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`] HAS_MEASURE_SUBSET)) THEN ASM_REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_IMAGE; REAL_NOT_LE] THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `&1 < a ==> a <= b ==> &1 < b`)) THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `measure(UNIONS (IMAGE (t:real^N->real^N->bool) f))` THEN CONJ_TAC THENL [MATCH_MP_TAC MEASURE_SUBSET THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `UNIONS (IMAGE (t:real^N->real^N->bool) f) = UNIONS (IMAGE t {u | u IN f /\ ~(t u = {})})` SUBST1_TAC THENL [GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_UNIONS; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[NOT_IN_EMPTY]; ALL_TAC] THEN MATCH_MP_TAC MEASURABLE_UNIONS THEN ASM_REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC] THEN MP_TAC(ISPECL [`t:real^N->real^N->bool`; `f:real^N->bool`] HAS_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG) THEN ASM_REWRITE_TAC[IMAGE_EQ_EMPTY; NOT_IMP] THEN DISCH_THEN(SUBST1_TAC o MATCH_MP MEASURE_UNIQUE) THEN REWRITE_TAC[VECTOR_ARITH `x - u:real^N = --u + x`] THEN ASM_SIMP_TAC[MEASURE_TRANSLATION; REAL_LE_REFL]);;
(* ------------------------------------------------------------------------- *) (* This is also interesting, and Minkowski follows easily from it. *) (* ------------------------------------------------------------------------- *)
let BLICHFELDT = 
prove (`!s:real^N->bool. bounded s /\ measurable s /\ &1 < measure s ==> ?x y. x IN s /\ y IN s /\ ~(x = y) /\ !i. 1 <= i /\ i <= dimindex(:N) ==> integer(x$i - y$i)`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`{ u:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i) }`; `\u. {x | (x:real^N) IN s /\ !i. 1 <= i /\ i <= dimindex(:N) ==> (u:real^N)$i <= x$i /\ x$i < u$i + &1 }`; `s:real^N->bool`] LEMMA) THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN ANTS_TAC THENL [ALL_TAC; REWRITE_TAC[DISJOINT; GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN REWRITE_TAC[EXISTS_IN_IMAGE; IN_INTER] THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN REWRITE_TAC[VECTOR_ARITH `x - u:real^N = y - v <=> x + (v - u) = y`] THEN REWRITE_TAC[UNWIND_THM1] THEN STRIP_TAC THEN EXISTS_TAC `x + (v - u):real^N` THEN ASM_REWRITE_TAC[VECTOR_ARITH `x = x + (v - u) <=> v:real^N = u`] THEN ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT] THEN ASM_SIMP_TAC[REAL_ARITH `x - (x + v - u) = u - v`; INTEGER_CLOSED]] THEN REPEAT CONJ_TAC THENL [SUBGOAL_THEN `?N. !x:real^N i. x IN s /\ 1 <= i /\ i <= dimindex(:N) ==> abs(x$i) < &N` STRIP_ASSUME_TAC THENL [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BOUNDED_POS]) THEN DISCH_THEN(X_CHOOSE_TAC `B:real`) THEN MP_TAC(SPEC `B:real` (MATCH_MP REAL_ARCH REAL_LT_01)) THEN MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[REAL_MUL_RID] THEN X_GEN_TAC `N:num` THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_POW2] THEN ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LE_TRANS; REAL_LET_TRANS]; ALL_TAC] THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{u:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> integer (u$i) /\ abs(u$i) <= &N}` THEN CONJ_TAC THENL [MATCH_MP_TAC FINITE_CART THEN REWRITE_TAC[GSYM REAL_BOUNDS_LE; FINITE_INTSEG]; ALL_TAC] THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `u:real^N` THEN STRIP_TAC THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LE_REVERSE_INTEGERS THEN ASM_SIMP_TAC[INTEGER_CLOSED] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `y:real^N` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `k:num`)) THEN FIRST_X_ASSUM(MP_TAC o SPECL [`y:real^N`; `k:num`]) THEN ASM_SIMP_TAC[] THEN REAL_ARITH_TAC; X_GEN_TAC `u:real^N` THEN DISCH_TAC THEN MATCH_MP_TAC MEASURABLE_ALMOST THEN EXISTS_TAC `s INTER interval[u:real^N,u + vec 1]` THEN ASM_SIMP_TAC[MEASURABLE_INTER_INTERVAL] THEN EXISTS_TAC `interval[u:real^N,u + vec 1] DIFF interval(u,u + vec 1)` THEN REWRITE_TAC[NEGLIGIBLE_FRONTIER_INTERVAL] THEN MATCH_MP_TAC(SET_RULE `s' SUBSET i /\ j INTER s' = j INTER s ==> (s INTER i) UNION (i DIFF j) = s' UNION (i DIFF j)`) THEN REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTERVAL; IN_INTER; EXTENSION; IN_ELIM_THM] THEN CONJ_TAC THEN X_GEN_TAC `x:real^N` THEN ASM_CASES_TAC `(x:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN TRY EQ_TAC THEN REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN GEN_TAC THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VEC_COMPONENT] THEN REAL_ARITH_TAC; REWRITE_TAC[SUBSET; IN_UNIONS; EXISTS_IN_IMAGE; IN_ELIM_THM] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN EXISTS_TAC `(lambda i. floor((x:real^N)$i)):real^N` THEN ASM_SIMP_TAC[LAMBDA_BETA; FLOOR]; MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN ASM_SIMP_TAC[CART_EQ; REAL_EQ_INTEGERS] THEN REWRITE_TAC[NOT_FORALL_THM; LEFT_IMP_EXISTS_THM; NOT_IMP; REAL_NOT_LT] THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN REWRITE_TAC[DISJOINT] THEN REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN REPEAT(FIRST_X_ASSUM (MP_TAC o SPEC `k:num`)) THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC; X_GEN_TAC `u:real^N` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM; IN_INTERVAL] THEN GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN SIMP_TAC[VECTOR_SUB_COMPONENT; VEC_COMPONENT] THEN MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *) (* The usual form of the theorem. *) (* ------------------------------------------------------------------------- *)
let MINKOWSKI = 
prove (`!s:real^N->bool. convex s /\ bounded s /\ (!x. x IN s ==> (--x) IN s) /\ &2 pow dimindex(:N) < measure s ==> ?u. ~(u = vec 0) /\ (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\ u IN s`,
REPEAT STRIP_TAC THEN MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 / &2) % x) s` BLICHFELDT) THEN ASM_SIMP_TAC[MEASURABLE_SCALING; MEASURE_SCALING; MEASURABLE_CONVEX; BOUNDED_SCALING] THEN REWRITE_TAC[real_div; REAL_MUL_LID; REAL_ABS_INV; REAL_ABS_NUM] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div; REAL_POW_INV] THEN ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_POW2; REAL_MUL_LID] THEN REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_IN_IMAGE] THEN REWRITE_TAC[VECTOR_ARITH `inv(&2) % x:real^N = inv(&2) % y <=> x = y`] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN SIMP_TAC[VECTOR_MUL_COMPONENT; GSYM REAL_SUB_LDISTRIB] THEN MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN EXISTS_TAC `inv(&2) % (u - v):real^N` THEN ASM_SIMP_TAC[VECTOR_ARITH `inv(&2) % (u - v):real^N = vec 0 <=> u = v`] THEN ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT] THEN REWRITE_TAC[VECTOR_SUB; VECTOR_ADD_LDISTRIB] THEN FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
(* ------------------------------------------------------------------------- *) (* A slightly sharper variant for use when the set is also closed. *) (* ------------------------------------------------------------------------- *)
let MINKOWSKI_COMPACT = 
prove (`!s:real^N->bool. convex s /\ compact s /\ (!x. x IN s ==> (--x) IN s) /\ &2 pow dimindex(:N) <= measure s ==> ?u. ~(u = vec 0) /\ (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\ u IN s`,
GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THENL [ASM_REWRITE_TAC[GSYM REAL_NOT_LT; MEASURE_EMPTY; REAL_LT_POW2]; ALL_TAC] THEN STRIP_TAC THEN SUBGOAL_THEN `(vec 0:real^N) IN s` ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN SUBST1_TAC(VECTOR_ARITH `vec 0:real^N = inv(&2) % a + inv(&2) % --a`) THEN FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`s:real^N->bool`; `{u | !i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)} DELETE (vec 0:real^N)`] SEPARATE_COMPACT_CLOSED) THEN REWRITE_TAC[EXTENSION; IN_DELETE; IN_ELIM_THM; IN_INTER; NOT_IN_EMPTY] THEN MATCH_MP_TAC(TAUT `(~e ==> c) /\ a /\ b /\ (d ==> e) ==> (a /\ b /\ c ==> d) ==> e`) THEN CONJ_TAC THENL [MESON_TAC[]; ASM_REWRITE_TAC[]] THEN CONJ_TAC THENL [MATCH_MP_TAC DISCRETE_IMP_CLOSED THEN EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01; IN_DELETE; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[CART_EQ; REAL_NOT_LT; NOT_FORALL_THM; NOT_IMP] THEN DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs((y - x:real^N)$k)` THEN ASM_SIMP_TAC[COMPONENT_LE_NORM; VECTOR_SUB_COMPONENT] THEN ASM_MESON_TAC[REAL_EQ_INTEGERS; REAL_NOT_LE]; ALL_TAC] THEN SIMP_TAC[dist] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `B:real` THEN STRIP_TAC THEN MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 + d / &2 / B) % x) s` MINKOWSKI) THEN ANTS_TAC THENL [ASM_SIMP_TAC[CONVEX_SCALING; BOUNDED_SCALING; COMPACT_IMP_BOUNDED] THEN ASM_SIMP_TAC[MEASURABLE_COMPACT; MEASURE_SCALING] THEN CONJ_TAC THENL [REWRITE_TAC[FORALL_IN_IMAGE; IN_IMAGE] THEN REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_ARITH `--(a % x):real^N = a % y <=> a % (x + y) = vec 0`] THEN ASM_MESON_TAC[VECTOR_ADD_RINV]; ALL_TAC] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `d <= m ==> m < n ==> d < n`)) THEN REWRITE_TAC[REAL_ARITH `m < a * m <=> &0 < m * (a - &1)`] THEN MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC THENL [ASM_SIMP_TAC[MEASURABLE_COMPACT; MEASURABLE_MEASURE_POS_LT] THEN REWRITE_TAC[GSYM HAS_MEASURE_0] THEN DISCH_THEN(SUBST_ALL_TAC o MATCH_MP MEASURE_UNIQUE) THEN ASM_MESON_TAC[REAL_NOT_LT; REAL_LT_POW2]; ALL_TAC] THEN REWRITE_TAC[REAL_SUB_LT] THEN MATCH_MP_TAC REAL_POW_LT_1 THEN REWRITE_TAC[DIMINDEX_NONZERO] THEN MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &1 < abs(&1 + x)`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH]; ALL_TAC] THEN ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> c /\ b /\ a`] THEN REWRITE_TAC[EXISTS_IN_IMAGE; VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:real^N` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o SPECL [`u:real^N`; `(&1 + d / &2 / B) % u:real^N`]) THEN ASM_REWRITE_TAC[VECTOR_MUL_EQ_0] THEN REWRITE_TAC[VECTOR_ARITH `u - (&1 + e) % u:real^N = --(e % u)`] THEN REWRITE_TAC[NORM_NEG; NORM_MUL] THEN MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[REAL_NOT_LE] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(d / &2 / B) * B` THEN ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ABS_POS] THEN ASM_REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NUM] THEN ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> abs x = x`] THEN ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC);;