1 (* ========================================================================= *)
2 (* Minkowski's convex body theorem. *)
3 (* ========================================================================= *)
5 needs "Multivariate/measure.ml";;
7 (* ------------------------------------------------------------------------- *)
9 (* ------------------------------------------------------------------------- *)
12 (`!f:real^N->bool t s:real^N->bool.
13 FINITE { u | u IN f /\ ~(t u = {})} /\
14 measurable s /\ &1 < measure s /\
15 (!u. u IN f ==> measurable(t u)) /\
16 s SUBSET UNIONS (IMAGE t f) /\
17 (!u v. u IN f /\ v IN f /\ ~(u = v) ==> DISJOINT (t u) (t v)) /\
18 (!u. u IN f ==> (IMAGE (\x. x - u) (t u)) SUBSET interval[vec 0,vec 1])
19 ==> ?u v. u IN f /\ v IN f /\ ~(u = v) /\
20 ~(DISJOINT (IMAGE (\x. x - u) (t u))
21 (IMAGE (\x. x - v) (t v)))`,
22 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [TAUT `p <=> ~ ~p`] THEN
23 PURE_REWRITE_TAC[NOT_EXISTS_THM] THEN
24 REWRITE_TAC[TAUT `~(a /\ b /\ ~c /\ ~d) <=> a /\ b /\ ~c ==> d`] THEN
26 MP_TAC(ISPECL [`\u:real^N. IMAGE (\x:real^N. x - u) (t u)`;
28 HAS_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG) THEN
29 ASM_REWRITE_TAC[IMAGE_EQ_EMPTY; NOT_IMP] THEN CONJ_TAC THENL
30 [REWRITE_TAC[VECTOR_ARITH `x - u:real^N = --u + x`] THEN
31 ASM_REWRITE_TAC[MEASURABLE_TRANSLATION_EQ];
33 MP_TAC(ISPECL [`vec 0:real^N`; `vec 1:real^N`] (CONJUNCT1
34 HAS_MEASURE_INTERVAL)) THEN
35 REWRITE_TAC[CONTENT_UNIT] THEN
36 MATCH_MP_TAC(TAUT `(b /\ a ==> F) ==> a ==> ~b`) THEN
37 DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE
38 [TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`] HAS_MEASURE_SUBSET)) THEN
39 ASM_REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_IMAGE; REAL_NOT_LE] THEN
40 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
41 `&1 < a ==> a <= b ==> &1 < b`)) THEN
42 MATCH_MP_TAC REAL_LE_TRANS THEN
43 EXISTS_TAC `measure(UNIONS (IMAGE (t:real^N->real^N->bool) f))` THEN
45 [MATCH_MP_TAC MEASURE_SUBSET THEN ASM_REWRITE_TAC[] THEN
47 `UNIONS (IMAGE (t:real^N->real^N->bool) f) =
48 UNIONS (IMAGE t {u | u IN f /\ ~(t u = {})})`
50 [GEN_REWRITE_TAC I [EXTENSION] THEN
51 REWRITE_TAC[IN_UNIONS; IN_IMAGE; IN_ELIM_THM] THEN
52 MESON_TAC[NOT_IN_EMPTY];
54 MATCH_MP_TAC MEASURABLE_UNIONS THEN
55 ASM_REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
56 ASM_SIMP_TAC[FINITE_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
58 MP_TAC(ISPECL [`t:real^N->real^N->bool`; `f:real^N->bool`]
59 HAS_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG) THEN
60 ASM_REWRITE_TAC[IMAGE_EQ_EMPTY; NOT_IMP] THEN
61 DISCH_THEN(SUBST1_TAC o MATCH_MP MEASURE_UNIQUE) THEN
62 REWRITE_TAC[VECTOR_ARITH `x - u:real^N = --u + x`] THEN
63 ASM_SIMP_TAC[MEASURE_TRANSLATION; REAL_LE_REFL]);;
65 (* ------------------------------------------------------------------------- *)
66 (* This is also interesting, and Minkowski follows easily from it. *)
67 (* ------------------------------------------------------------------------- *)
69 let BLICHFELDT = prove
71 bounded s /\ measurable s /\ &1 < measure s
72 ==> ?x y. x IN s /\ y IN s /\ ~(x = y) /\
73 !i. 1 <= i /\ i <= dimindex(:N) ==> integer(x$i - y$i)`,
75 MP_TAC(ISPECL [`{ u:real^N | !i. 1 <= i /\ i <= dimindex(:N)
77 `\u. {x | (x:real^N) IN s /\
78 !i. 1 <= i /\ i <= dimindex(:N)
79 ==> (u:real^N)$i <= x$i /\ x$i < u$i + &1 }`;
82 ASM_REWRITE_TAC[IN_ELIM_THM] THEN ANTS_TAC THENL
84 REWRITE_TAC[DISJOINT; GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN
85 MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN
86 REWRITE_TAC[EXISTS_IN_IMAGE; IN_INTER] THEN
87 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
88 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN
89 REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN
90 REWRITE_TAC[VECTOR_ARITH `x - u:real^N = y - v <=> x + (v - u) = y`] THEN
91 REWRITE_TAC[UNWIND_THM1] THEN STRIP_TAC THEN
92 EXISTS_TAC `x + (v - u):real^N` THEN
93 ASM_REWRITE_TAC[VECTOR_ARITH `x = x + (v - u) <=> v:real^N = u`] THEN
94 ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; VECTOR_ADD_COMPONENT] THEN
95 ASM_SIMP_TAC[REAL_ARITH `x - (x + v - u) = u - v`; INTEGER_CLOSED]] THEN
98 `?N. !x:real^N i. x IN s /\ 1 <= i /\ i <= dimindex(:N) ==> abs(x$i) < &N`
99 STRIP_ASSUME_TAC THENL
100 [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BOUNDED_POS]) THEN
101 DISCH_THEN(X_CHOOSE_TAC `B:real`) THEN
102 MP_TAC(SPEC `B:real` (MATCH_MP REAL_ARCH REAL_LT_01)) THEN
103 MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[REAL_MUL_RID] THEN
104 X_GEN_TAC `N:num` THEN
105 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN
106 SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_POW2] THEN
107 ASM_MESON_TAC[COMPONENT_LE_NORM; REAL_LE_TRANS; REAL_LET_TRANS];
109 MATCH_MP_TAC FINITE_SUBSET THEN
111 `{u:real^N | !i. 1 <= i /\ i <= dimindex(:N)
112 ==> integer (u$i) /\ abs(u$i) <= &N}` THEN
114 [MATCH_MP_TAC FINITE_CART THEN
115 REWRITE_TAC[GSYM REAL_BOUNDS_LE; FINITE_INTSEG];
117 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `u:real^N` THEN
118 STRIP_TAC THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN
119 MATCH_MP_TAC REAL_LE_REVERSE_INTEGERS THEN
120 ASM_SIMP_TAC[INTEGER_CLOSED] THEN
121 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
122 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
123 X_GEN_TAC `y:real^N` THEN
124 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `k:num`)) THEN
125 FIRST_X_ASSUM(MP_TAC o SPECL [`y:real^N`; `k:num`]) THEN
126 ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
127 X_GEN_TAC `u:real^N` THEN DISCH_TAC THEN
128 MATCH_MP_TAC MEASURABLE_ALMOST THEN
129 EXISTS_TAC `s INTER interval[u:real^N,u + vec 1]` THEN
130 ASM_SIMP_TAC[MEASURABLE_INTER_INTERVAL] THEN
131 EXISTS_TAC `interval[u:real^N,u + vec 1] DIFF interval(u,u + vec 1)` THEN
132 REWRITE_TAC[NEGLIGIBLE_FRONTIER_INTERVAL] THEN
133 MATCH_MP_TAC(SET_RULE
134 `s' SUBSET i /\ j INTER s' = j INTER s
135 ==> (s INTER i) UNION (i DIFF j) = s' UNION (i DIFF j)`) THEN
136 REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INTERVAL; IN_INTER; EXTENSION;
138 CONJ_TAC THEN X_GEN_TAC `x:real^N` THEN
139 ASM_CASES_TAC `(x:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN TRY EQ_TAC THEN
140 REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
141 REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN
142 GEN_TAC THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
143 ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VEC_COMPONENT] THEN REAL_ARITH_TAC;
144 REWRITE_TAC[SUBSET; IN_UNIONS; EXISTS_IN_IMAGE; IN_ELIM_THM] THEN
145 X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
146 EXISTS_TAC `(lambda i. floor((x:real^N)$i)):real^N` THEN
147 ASM_SIMP_TAC[LAMBDA_BETA; FLOOR];
148 MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN
149 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
150 ASM_SIMP_TAC[CART_EQ; REAL_EQ_INTEGERS] THEN
151 REWRITE_TAC[NOT_FORALL_THM; LEFT_IMP_EXISTS_THM; NOT_IMP; REAL_NOT_LT] THEN
152 X_GEN_TAC `k:num` THEN STRIP_TAC THEN REWRITE_TAC[DISJOINT] THEN
153 REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_ELIM_THM] THEN
154 REPEAT STRIP_TAC THEN
155 REPEAT(FIRST_X_ASSUM (MP_TAC o SPEC `k:num`)) THEN
156 ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
157 X_GEN_TAC `u:real^N` THEN DISCH_THEN(K ALL_TAC) THEN
158 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM; IN_INTERVAL] THEN
159 GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
160 MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
161 SIMP_TAC[VECTOR_SUB_COMPONENT; VEC_COMPONENT] THEN
162 MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN REAL_ARITH_TAC]);;
164 (* ------------------------------------------------------------------------- *)
165 (* The usual form of the theorem. *)
166 (* ------------------------------------------------------------------------- *)
168 let MINKOWSKI = prove
172 (!x. x IN s ==> (--x) IN s) /\
173 &2 pow dimindex(:N) < measure s
174 ==> ?u. ~(u = vec 0) /\
175 (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\
177 REPEAT STRIP_TAC THEN
178 MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 / &2) % x) s` BLICHFELDT) THEN
179 ASM_SIMP_TAC[MEASURABLE_SCALING; MEASURE_SCALING; MEASURABLE_CONVEX;
180 BOUNDED_SCALING] THEN
181 REWRITE_TAC[real_div; REAL_MUL_LID; REAL_ABS_INV; REAL_ABS_NUM] THEN
182 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
183 REWRITE_TAC[GSYM real_div; REAL_POW_INV] THEN
184 ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_POW2; REAL_MUL_LID] THEN
185 REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_IN_IMAGE] THEN
186 REWRITE_TAC[VECTOR_ARITH `inv(&2) % x:real^N = inv(&2) % y <=> x = y`] THEN
187 REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
188 SIMP_TAC[VECTOR_MUL_COMPONENT; GSYM REAL_SUB_LDISTRIB] THEN
189 MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
190 EXISTS_TAC `inv(&2) % (u - v):real^N` THEN
191 ASM_SIMP_TAC[VECTOR_ARITH `inv(&2) % (u - v):real^N = vec 0 <=> u = v`] THEN
192 ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT] THEN
193 REWRITE_TAC[VECTOR_SUB; VECTOR_ADD_LDISTRIB] THEN
194 FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN
195 ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
197 (* ------------------------------------------------------------------------- *)
198 (* A slightly sharper variant for use when the set is also closed. *)
199 (* ------------------------------------------------------------------------- *)
201 let MINKOWSKI_COMPACT = prove
203 convex s /\ compact s /\
204 (!x. x IN s ==> (--x) IN s) /\
205 &2 pow dimindex(:N) <= measure s
206 ==> ?u. ~(u = vec 0) /\
207 (!i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)) /\
209 GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THENL
210 [ASM_REWRITE_TAC[GSYM REAL_NOT_LT; MEASURE_EMPTY; REAL_LT_POW2];
213 SUBGOAL_THEN `(vec 0:real^N) IN s` ASSUME_TAC THENL
214 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
215 DISCH_THEN(X_CHOOSE_TAC `a:real^N`) THEN
216 SUBST1_TAC(VECTOR_ARITH `vec 0:real^N = inv(&2) % a + inv(&2) % --a`) THEN
217 FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [convex]) THEN
218 ASM_SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV;
220 REPEAT STRIP_TAC THEN
223 `{u | !i. 1 <= i /\ i <= dimindex(:N) ==> integer(u$i)}
224 DELETE (vec 0:real^N)`]
225 SEPARATE_COMPACT_CLOSED) THEN
226 REWRITE_TAC[EXTENSION; IN_DELETE; IN_ELIM_THM; IN_INTER; NOT_IN_EMPTY] THEN
228 `(~e ==> c) /\ a /\ b /\ (d ==> e)
229 ==> (a /\ b /\ c ==> d) ==> e`) THEN
230 CONJ_TAC THENL [MESON_TAC[]; ASM_REWRITE_TAC[]] THEN CONJ_TAC THENL
231 [MATCH_MP_TAC DISCRETE_IMP_CLOSED THEN
232 EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01; IN_DELETE; IN_ELIM_THM] THEN
234 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
235 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
236 REWRITE_TAC[CART_EQ; REAL_NOT_LT; NOT_FORALL_THM; NOT_IMP] THEN
237 DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
238 MATCH_MP_TAC REAL_LE_TRANS THEN
239 EXISTS_TAC `abs((y - x:real^N)$k)` THEN
240 ASM_SIMP_TAC[COMPONENT_LE_NORM; VECTOR_SUB_COMPONENT] THEN
241 ASM_MESON_TAC[REAL_EQ_INTEGERS; REAL_NOT_LE];
243 SIMP_TAC[dist] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
244 FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
245 REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
246 X_GEN_TAC `B:real` THEN STRIP_TAC THEN
247 MP_TAC(ISPEC `IMAGE (\x:real^N. (&1 + d / &2 / B) % x) s` MINKOWSKI) THEN
249 [ASM_SIMP_TAC[CONVEX_SCALING; BOUNDED_SCALING; COMPACT_IMP_BOUNDED] THEN
250 ASM_SIMP_TAC[MEASURABLE_COMPACT; MEASURE_SCALING] THEN CONJ_TAC THENL
251 [REWRITE_TAC[FORALL_IN_IMAGE; IN_IMAGE] THEN
252 REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_ARITH
253 `--(a % x):real^N = a % y <=> a % (x + y) = vec 0`] THEN
254 ASM_MESON_TAC[VECTOR_ADD_RINV];
256 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
257 `d <= m ==> m < n ==> d < n`)) THEN
258 REWRITE_TAC[REAL_ARITH `m < a * m <=> &0 < m * (a - &1)`] THEN
259 MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC THENL
260 [ASM_SIMP_TAC[MEASURABLE_COMPACT; MEASURABLE_MEASURE_POS_LT] THEN
261 REWRITE_TAC[GSYM HAS_MEASURE_0] THEN
262 DISCH_THEN(SUBST_ALL_TAC o MATCH_MP MEASURE_UNIQUE) THEN
263 ASM_MESON_TAC[REAL_NOT_LT; REAL_LT_POW2];
265 REWRITE_TAC[REAL_SUB_LT] THEN MATCH_MP_TAC REAL_POW_LT_1 THEN
266 REWRITE_TAC[DIMINDEX_NONZERO] THEN
267 MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &1 < abs(&1 + x)`) THEN
268 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH];
270 ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> c /\ b /\ a`] THEN
271 REWRITE_TAC[EXISTS_IN_IMAGE; VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN
272 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:real^N` THEN
273 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
274 FIRST_X_ASSUM(MP_TAC o SPECL
275 [`u:real^N`; `(&1 + d / &2 / B) % u:real^N`]) THEN
276 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0] THEN
277 REWRITE_TAC[VECTOR_ARITH `u - (&1 + e) % u:real^N = --(e % u)`] THEN
278 REWRITE_TAC[NORM_NEG; NORM_MUL] THEN
279 MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[REAL_NOT_LE] THEN
280 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(d / &2 / B) * B` THEN
281 ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ABS_POS] THEN
282 ASM_REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NUM] THEN
283 ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> abs x = x`] THEN
284 ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN
285 UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC);;