1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Authour : VU KHAC KY *)
5 (* Book lemma: UPFZBZM *)
6 (* SUM_GAMMAX_LMFUN_ESTIMATE - a supported lemma. *)
7 (* Chaper : Packing (Clusters) *)
9 (* ========================================================================= *)
12 let TSKAJXY_statement = new_definition
13 `TSKAJXY_statement <=>
18 critical_edgeX V X = {}
19 ==> gammaX V X lmfun >= &0)`;;
21 let SUM_GAMMAX_LMFUN_ESTIMATE_concl =
22 `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\
23 cell_cluster_estimate V /\ TSKAJXY_statement ==>
24 c * r pow 2 <= sum {X | X SUBSET ball (vec 0, r) /\ mcell_set V X}
25 (\X. gammaX V X lmfun)`;;
27 (* ========================================================================= *)
28 (* ========================================================================= *)
30 let SUM_GAMMAX_LMFUN_ESTIMATE = prove_by_refinement (
31 SUM_GAMMAX_LMFUN_ESTIMATE_concl,
35 (* ================== Choose the constants ================================= *)
37 (NEW_GOAL `?cc1. (&1 <= cc1) /\ (!V X.
38 packing V /\ saturated V /\ mcell_set V X
39 ==> gammaX V X lmfun <= cc1)`);
40 (MP_TAC BOUND_GAMMA_X_lmfun THEN STRIP_TAC);
41 (EXISTS_TAC `max (c:real) (&1)`);
45 (NEW_GOAL `gammaX V X lmfun <= c`);
48 (UP_ASM_TAC THEN STRIP_TAC);
50 (NEW_GOAL `?cc2. (&1 <= cc2) /\
52 saturated V /\ packing V /\ u0 IN V
53 ==> & (CARD {X | mcell_set V X /\ VX V X u0}) <= cc2)`);
55 (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma);
57 (EXISTS_TAC `max (&c:real) (&1)`);
61 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= (&c:real)`);
62 (REWRITE_TAC[REAL_OF_NUM_LE]);
64 (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`);
66 (UP_ASM_TAC THEN STRIP_TAC);
71 saturated V /\ packing V /\ mcell_set V X /\ critical_edgeX V X e
72 ==> beta_bump V e X <= cc3)`);
73 (MP_TAC BOUND_BETA_BUMP THEN STRIP_TAC);
74 (EXISTS_TAC `max (c:real) (&1)`);
78 (NEW_GOAL `beta_bump V e X <= c`);
81 (UP_ASM_TAC THEN STRIP_TAC);
86 saturated V /\ packing V /\ u0 IN V
87 ==> &(CARD {X | mcell_set V X /\ VX V X u0}) <= cc4)`);
88 (MP_TAC CARD_MCELL_CONTAINS_POINT_klemma THEN STRIP_TAC);
89 (EXISTS_TAC `max (&c) (&1)`);
93 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= &c`);
94 (REWRITE_TAC[REAL_OF_NUM_LE]);
96 (ABBREV_TAC `s = &(CARD {X | mcell_set V X /\ VX V X u0})`);
98 (UP_ASM_TAC THEN STRIP_TAC);
100 (ASM_CASES_TAC `saturated V /\ packing V`);
103 `?dd1. !r. &1 <= r ==>
104 &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &8))) <=
107 (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &8)
108 = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &8)`);
109 (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
110 (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);
113 (ABBREV_TAC `dd2 = max dd1 (&1)`);
114 (ABBREV_TAC `dd = &1 / &2 * dd2 * (&4) pow 3 * cc2 * cc1`);
117 `?dd3. !r. &1 <= r ==>
118 &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &16))) <=
121 (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &16)
122 = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &16)`);
123 (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
124 (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);
127 (ABBREV_TAC `dd4 = max dd3 (&1)`);
128 (ABBREV_TAC `ss1 = (&4) pow 3 * cc4 * cc3`);
129 (ABBREV_TAC `ss = &1 / &2 * dd4 * ss1`);
131 (ABBREV_TAC `c:real = -- (dd + ss)`);
132 (EXISTS_TAC `c:real`);
135 (* ============================================================================ *)
138 (NEW_GOAL `!X. mcell_set V X /\ critical_edgeX V X = {} ==>
139 gammaX V X lmfun >= &0`);
140 (UP_ASM_TAC THEN REWRITE_TAC[TSKAJXY_statement]);
144 (ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r) /\ mcell_set V X}`);
145 (ABBREV_TAC `B0 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
146 critical_edgeX V X = {}}`);
147 (ABBREV_TAC `B1 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
148 ~(critical_edgeX V X = {})}`);
149 (NEW_GOAL `FINITE (B1:(real^3->bool)->bool)`);
151 (MATCH_MP_TAC FINITE_SUBSET);
152 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
154 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
157 (REWRITE_WITH `B = B0 UNION B1:(real^3->bool)->bool`);
158 (EXPAND_TAC "B" THEN EXPAND_TAC "B1" THEN EXPAND_TAC "B0");
160 (REWRITE_WITH `sum (B0 UNION B1) (\X. gammaX V X lmfun) =
161 sum B0 (\X. gammaX V X lmfun) + sum B1 (\X. gammaX V X lmfun)`);
162 (MATCH_MP_TAC SUM_UNION);
165 (MATCH_MP_TAC FINITE_SUBSET);
166 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
168 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
171 (EXPAND_TAC "B1" THEN EXPAND_TAC "B0");
173 (MATCH_MP_TAC (REAL_ARITH `&0 <= b /\ a <= c ==> a <= b + c`));
175 (MATCH_MP_TAC SUM_POS_LE);
178 (MATCH_MP_TAC FINITE_SUBSET);
179 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
181 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
183 (REWRITE_TAC[BETA_THM; REAL_ARITH `&0 <= a <=> a >= &0`]);
184 (EXPAND_TAC "B0" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
189 `sum B1 (\X. gammaX V X lmfun) =
190 sum B1 (\X. (gammaX V X lmfun) *
191 sum (critical_edgeX V X) (\e. critical_weight V X))`);
192 (MATCH_MP_TAC SUM_EQ);
193 (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
195 (REWRITE_TAC[critical_weight]);
197 `sum (critical_edgeX V x) (\e. &1 / &(CARD (critical_edgeX V x))) =
198 &(CARD (critical_edgeX V x)) * (&1 / &(CARD (critical_edgeX V x)))`);
199 (MATCH_MP_TAC SUM_CONST);
200 (REWRITE_TAC[FINITE_critical_edgeX]);
201 (REWRITE_TAC[REAL_ARITH `a * &1 / a = a / a`]);
202 (REWRITE_WITH `&(CARD (critical_edgeX V x)) / &(CARD (critical_edgeX V x)) = &1`);
203 (MATCH_MP_TAC REAL_DIV_REFL);
204 (REWRITE_TAC[REAL_OF_NUM_EQ]);
205 (REWRITE_WITH `CARD (critical_edgeX V x) = 0 <=> critical_edgeX V x = {}`);
206 (MATCH_MP_TAC CARD_EQ_0);
207 (REWRITE_TAC[FINITE_critical_edgeX]);
211 (* ------------------------------------------------------------------------- *)
212 (* Hint: - See proofs of KIZHLTL1; KIZHLTL2 to adapt *)
213 (* ------------------------------------------------------------------------- *)
215 (REWRITE_TAC[GSYM SUM_LMUL]);
217 (ABBREV_TAC `T1:real^3->bool = V INTER ball (vec 0, r)`);
218 (ABBREV_TAC `T2 = {{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\
219 hl [u0; u1] <= hplus}`);
220 (NEW_GOAL `FINITE (T2:(real^3->bool)->bool)`);
221 (EXPAND_TAC "T2" THEN MATCH_MP_TAC FINITE_SUBSET);
222 (EXISTS_TAC `{{u0, u1:real^3} | u0 IN T1 /\ u1 IN T1}`);
224 (MATCH_MP_TAC FINITE_SET_PRODUCT_KY_LEMMA);
225 (EXPAND_TAC "T1" THEN MATCH_MP_TAC Pack2.KIUMVTC);
230 `sum B1 (\X. sum (critical_edgeX V X)
231 (\x. gammaX V X lmfun * critical_weight V X)) =
232 sum B1 (\X. sum {y:real^3->bool| y IN T2 /\ critical_edgeX V X y}
233 (\x. gammaX V X lmfun * critical_weight V X))`);
234 (MATCH_MP_TAC SUM_EQ);
235 (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
237 (AP_THM_TAC THEN AP_TERM_TAC);
238 (REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
241 (REWRITE_TAC[SET_RULE `A SUBSET {y | T2 y /\ A y} <=> A SUBSET T2`]);
242 (EXPAND_TAC "T2" THEN REWRITE_TAC[SUBSET; critical_edgeX; IN; IN_ELIM_THM; edgeX]);
244 (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_ELIM_THM]);
245 (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`);
246 (REWRITE_TAC[ASSUME `~(u' = v':real^3)`]);
248 (REWRITE_TAC[ASSUME `x' = {u, v:real^3}`; MESON[IN] `V (x:real^3) <=> x IN V`;
249 GSYM (ASSUME `{u, v} = {u', v':real^3}`); IN_INTER]);
251 (NEW_GOAL `VX V x = V INTER x`);
252 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
253 (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
255 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
258 (NEW_GOAL `VX V x = {}`);
261 (UNDISCH_TAC `VX V x u'` THEN ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
268 (REWRITE_WITH `hl [u'; v':real^3] = hl [u; v:real^3]`);
269 (ASM_REWRITE_TAC[HL; set_of_list]);
272 (ABBREV_TAC `f = (\X. (\x:real^3->bool.
273 gammaX V X lmfun * critical_weight V X))`);
275 `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y}
276 (\x:real^3->bool. gammaX V X lmfun * critical_weight V X)) =
277 sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y}
278 (\x:real^3->bool. f X x))`);
279 (EXPAND_TAC "f" THEN REFL_TAC);
281 `sum B1 (\X. sum {y | y IN T2 /\ critical_edgeX V X y} (\x. f X x)) =
282 sum T2 (\x. sum {X | X IN B1 /\ critical_edgeX V X x} (\X. f X x))`);
283 (ASM_SIMP_TAC[SUM_SUM_RESTRICT]);
285 (EXPAND_TAC "B1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
286 (REWRITE_TAC[MESON[] `(A/\B/\C)/\D <=> A/\B/\C/\D`]);
289 {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
290 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
292 sum T2 (\x. sum {X | mcell_set V X /\
293 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
295 sum T2 (\x. sum {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
296 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
298 (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]);
302 {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
303 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
307 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
308 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
312 {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\
313 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
316 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
317 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}
319 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
320 (MATCH_MP_TAC SUM_ADD);
322 (MATCH_MP_TAC SUM_EQ);
323 (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);
327 {X | X SUBSET ball (vec 0,r) /\
329 ~(critical_edgeX V X = {}) /\
330 critical_edgeX V X x}
333 {X | ~(X SUBSET ball (vec 0,r)) /\
335 ~(critical_edgeX V X = {}) /\
336 critical_edgeX V X x}
338 sum ({X | X SUBSET ball (vec 0,r) /\
340 ~(critical_edgeX V X = {}) /\
341 critical_edgeX V X x} UNION
342 {X | ~(X SUBSET ball (vec 0,r)) /\
344 ~(critical_edgeX V X = {}) /\
345 critical_edgeX V X x})
347 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
348 (MATCH_MP_TAC SUM_UNION);
351 (MATCH_MP_TAC FINITE_SUBSET);
352 (EXISTS_TAC `B1:(real^3->bool)->bool`);
354 (EXPAND_TAC "B1" THEN SET_TAC[]);
356 (UP_ASM_TAC THEN EXPAND_TAC "T2");
357 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
358 (MATCH_MP_TAC FINITE_SUBSET);
359 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
361 (ASM_SIMP_TAC[Marchal_cells_3.FINITE_MCELL_SET_LEMMA]);
362 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
364 (NEW_GOAL `x SUBSET VX V x'`);
365 (UNDISCH_TAC `critical_edgeX V x' x` THEN REWRITE_TAC[critical_edgeX;edgeX]);
366 (REWRITE_TAC[IN_ELIM_THM]);
368 (REWRITE_TAC[ASSUME `x = {u, v:real^3}`; ASSUME `{u, v:real^3} = {u', v'}`]);
369 (SET_TAC[ASSUME `VX V x' u'`; ASSUME `VX V x' v'`]);
370 (NEW_GOAL `VX V x' = V INTER x'`);
371 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
372 (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]);
374 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
377 (NEW_GOAL `VX V x' = {}`);
378 (ASM_REWRITE_TAC[VX]);
379 (UNDISCH_TAC `x SUBSET VX V x'` THEN REWRITE_TAC[ASSUME `VX V x' = {}`]);
380 (REWRITE_TAC[ASSUME `x = {u0, u1:real^3}`] THEN SET_TAC[]);
381 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_BALL]);
382 (NEW_GOAL `dist (vec 0, x'') <= dist (vec 0, u0:real^3) + dist (u0, x'')`);
384 (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
385 (REWRITE_TAC[GSYM IN_BALL]);
386 (UNDISCH_TAC `(T1:real^3->bool) u0` THEN EXPAND_TAC "T1");
387 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`] THEN SET_TAC[]);
388 (NEW_GOAL `dist (u0, x'':real^3) < &8`);
389 (REWRITE_TAC[GSYM IN_BALL]);
390 (NEW_GOAL `x' SUBSET ball (u0:real^3,&8)`);
391 (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM; IN]);
394 (MATCH_MP_TAC MCELL_SUBSET_BALL8);
396 (REWRITE_TAC[GSYM (ASSUME `x' = mcell i V ul`)]);
397 (UNDISCH_TAC `x SUBSET VX V x'` THEN UNDISCH_TAC `VX V x' = V INTER x'`);
400 (SUBGOAL_THEN `(x'':real^3) IN x'` MP_TAC);
401 (UNDISCH_TAC `(x':real^3->bool) x''` THEN SET_TAC[]);
402 (UP_ASM_TAC THEN SET_TAC[]);
403 (ASM_REAL_ARITH_TAC);
407 (REWRITE_WITH ` ({X | X SUBSET ball (vec 0,r) /\
409 ~(critical_edgeX V X = {}) /\
410 critical_edgeX V X x} UNION
411 {X | ~(X SUBSET ball (vec 0,r)) /\
413 ~(critical_edgeX V X = {}) /\
414 critical_edgeX V X x}) =
415 {X | mcell_set V X /\ ~(critical_edgeX V X = {}) /\ critical_edgeX V X x}`);
419 {X | mcell_set V X /\
420 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) =
422 {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`);
423 (REWRITE_TAC[FUN_EQ_THM]);
426 `{X | mcell_set V X /\
427 ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} =
428 {X | mcell_set V X /\ critical_edgeX V X x}`);
429 (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]);
432 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
434 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
435 (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]);
441 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
442 ~(critical_edgeX V X = {}) /\ critical_edgeX V X x} (\X. f X x)) =
444 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
445 critical_edgeX V X x} (\X. f X x))`);
446 (REWRITE_TAC[FUN_EQ_THM]);
449 `{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\
450 ~(!x. critical_edgeX V X x <=> {} x) /\ critical_edgeX V X x} =
451 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}`);
452 (REWRITE_TAC[SET_RULE `A = B <=> A SUBSET B /\ B SUBSET A`]);
455 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
456 (GEN_TAC THEN DISCH_TAC);
458 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
459 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
460 (REWRITE_TAC[MESON[IN] `(A:(real^3->bool)->bool) x <=> x IN A`]);
465 (MATCH_MP_TAC (REAL_ARITH `(?x. c <= x /\ a + x <= b) ==> a <= b - c`));
466 (EXISTS_TAC `dd * r pow 2`);
470 `T3:real^3->bool = V INTER ball (vec 0, r) DIFF ball (vec 0, r - &8)`);
471 (ABBREV_TAC `T4 = {{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3 /\
472 ~(u0 = u1) /\ hl [u0; u1] <= hplus}`);
473 (REWRITE_WITH `sum T2
475 {X | ~(X SUBSET ball (vec 0,r)) /\
477 critical_edgeX V X x}
478 (\X. f X x)) = sum T4
480 {X | ~(X SUBSET ball (vec 0,r)) /\
482 critical_edgeX V X x}
486 (MATCH_MP_TAC SUM_SUPERSET);
488 (EXPAND_TAC "T4" THEN EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN SET_TAC[]);
490 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
492 `{X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x} =
494 (REWRITE_TAC[SET_RULE `x = {} <=> ~(?s. s IN x)`]);
495 (REWRITE_TAC[IN; IN_ELIM_THM] THEN STRIP_TAC);
497 (NEW_GOAL `(x:real^3->bool) SUBSET s`);
498 (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL);
499 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
501 (NEW_GOAL `?p:real^3. p IN s DIFF ball (vec 0,r)`);
502 (UNDISCH_TAC `~(s SUBSET ball ((vec 0):real^3,r))` THEN SET_TAC[]);
503 (UP_ASM_TAC THEN STRIP_TAC);
504 (UP_ASM_TAC THEN REWRITE_TAC[IN_DIFF; IN_BALL; REAL_ARITH
505 `~(a < r) <=> r <= a`] THEN STRIP_TAC);
506 (NEW_GOAL `s SUBSET ball (p:real^3,&8)`);
507 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
508 (EXISTS_TAC `V:real^3->bool`);
510 (NEW_GOAL `u0:real^3 IN ball (p,&8) /\ u1 IN ball (p,&8)`);
512 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN STRIP_TAC);
513 (UNDISCH_TAC `~(T4:(real^3->bool)->bool) x`);
514 (REWRITE_TAC[MESON[IN] `(T4:(real^3->bool)->bool) x <=> x IN T4`]);
515 (EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN_INTER; IN_DIFF; IN_BALL]);
516 (REWRITE_TAC[IN; IN_ELIM_THM]);
517 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
518 (UNDISCH_TAC `(T1:(real^3->bool)) u0` THEN
519 UNDISCH_TAC `(T1:(real^3->bool)) u1`);
520 (REWRITE_WITH `!x. T1 x <=> x:real^3 IN T1`);
521 (ASM_REWRITE_TAC[IN]);
522 (EXPAND_TAC "T1" THEN REWRITE_TAC[IN_INTER; IN_BALL]);
523 (REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
524 (NEW_GOAL `dist (vec 0,p) <= dist (p, u0) + dist (vec 0, u0:real^3)`);
526 (ASM_REAL_ARITH_TAC);
527 (NEW_GOAL `dist (vec 0,p) <= dist (p, u1) + dist (vec 0, u1:real^3)`);
529 (ASM_REAL_ARITH_TAC);
530 (REWRITE_TAC[SUM_CLAUSES]);
532 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
533 (EXISTS_TAC `sum T4 (\x:real^3->bool. cc2 * cc1)`);
535 (MATCH_MP_TAC SUM_LE);
537 (MATCH_MP_TAC FINITE_SUBSET);
538 (EXISTS_TAC `{{u0:real^3, u1} | u0 IN T3 /\ u1 IN T3}`);
540 (MATCH_MP_TAC FINITE_SUBSET);
541 (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN T3 /\ u1 IN T3}`);
542 (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
543 (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
545 (MATCH_MP_TAC FINITE_IMAGE);
546 (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
547 (MATCH_MP_TAC FINITE_SUBSET);
548 (EXISTS_TAC `T1:real^3->bool`);
550 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
552 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN
553 REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
555 (EXISTS_TAC `u0:real^3, u1:real^3` THEN ASM_REWRITE_TAC[]);
556 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
558 (REWRITE_TAC[IN] THEN EXPAND_TAC "T4" THEN EXPAND_TAC "T3" THEN
559 REWRITE_TAC[ABS_SIMP; IN_DIFF; IN_INTER; IN_ELIM_THM]);
562 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
564 `sum {X| ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}
567 (MATCH_MP_TAC SUM_LE);
569 (MATCH_MP_TAC FINITE_SUBSET);
570 (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`);
572 (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
573 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
574 (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]);
575 (REWRITE_TAC[BETA_THM; ABS_SIMP; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
577 (NEW_GOAL `critical_weight V x' <= &1`);
578 (REWRITE_TAC[critical_weight]);
579 (REWRITE_WITH `&1 / &(CARD (critical_edgeX V x')) <= &1 <=>
580 &1 <= &(CARD (critical_edgeX V x'))`);
581 (MATCH_MP_TAC Packing3.REAL_DIV_LE_1);
582 (REWRITE_TAC[REAL_OF_NUM_LT; ARITH_RULE `0 < a <=> ~(a = 0)`]);
583 (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`);
584 (MATCH_MP_TAC CARD_EQ_0);
585 (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET);
587 (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`);
589 (MATCH_MP_TAC FINITE_SUBSET);
590 (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`);
591 (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
592 (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
594 (MATCH_MP_TAC FINITE_IMAGE);
595 (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
596 (MATCH_MP_TAC FINITE_VX);
598 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN
599 REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
601 (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]);
602 (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]);
604 (UP_ASM_TAC THEN SET_TAC[]);
605 (REWRITE_TAC[REAL_OF_NUM_LE; ARITH_RULE `1 <= a <=> ~(a = 0)`]);
606 (REWRITE_WITH `CARD (critical_edgeX V x') = 0 <=> critical_edgeX V x' = {}`);
607 (MATCH_MP_TAC CARD_EQ_0);
608 (REWRITE_TAC[critical_edgeX; edgeX] THEN MATCH_MP_TAC FINITE_SUBSET);
609 (EXISTS_TAC `{{u0:real^3, u1} | u0 IN VX V x' /\ u1 IN VX V x'}`);
611 (MATCH_MP_TAC FINITE_SUBSET);
612 (ABBREV_TAC `S_temp = {u0, u1:real^3 | u0 IN VX V x' /\ u1 IN VX V x'}`);
613 (ABBREV_TAC `f_temp = (\(u0,u1:real^3). {u0, u1})`);
614 (EXISTS_TAC `IMAGE (f_temp:real^3#real^3->real^3->bool) S_temp`);
616 (MATCH_MP_TAC FINITE_IMAGE);
617 (EXPAND_TAC "S_temp" THEN MATCH_MP_TAC FINITE_PRODUCT THEN REWRITE_TAC[]);
618 (MATCH_MP_TAC FINITE_VX);
620 (EXPAND_TAC "f_temp" THEN EXPAND_TAC "S_temp" THEN
621 REWRITE_TAC[IMAGE; SUBSET; IN; IN_ELIM_THM]);
623 (EXISTS_TAC `u0':real^3, u1':real^3` THEN ASM_REWRITE_TAC[]);
624 (EXISTS_TAC `u0':real^3` THEN EXISTS_TAC `u1':real^3` THEN ASM_REWRITE_TAC[]);
626 (UP_ASM_TAC THEN SET_TAC[]);
627 (NEW_GOAL `&0 <= critical_weight V x'`);
628 (REWRITE_TAC[critical_weight] THEN MATCH_MP_TAC REAL_LE_DIV);
629 (REWRITE_TAC[REAL_ARITH `&0 <= &1`; REAL_OF_NUM_LE]);
631 (NEW_GOAL `gammaX V x' lmfun <= cc1`);
632 (FIRST_ASSUM MATCH_MP_TAC);
634 (NEW_GOAL `gammaX V x' lmfun * critical_weight V x' <= cc1 * critical_weight V x'`);
636 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
637 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
638 (MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC);
640 (NEW_GOAL `cc1 * critical_weight V x' <= cc1`);
641 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
642 (REWRITE_WITH `!x b. b - b * x = b * (&1 - x)`);
644 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
645 (ASM_REAL_ARITH_TAC);
646 (ASM_REAL_ARITH_TAC);
647 (ASM_REAL_ARITH_TAC);
650 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x}
653 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x})
655 (MATCH_MP_TAC SUM_CONST);
656 (MATCH_MP_TAC FINITE_SUBSET);
657 (EXISTS_TAC `{X | mcell_set V X /\ edgeX V X x}`);
659 (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
660 (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
661 (REWRITE_TAC[critical_edgeX] THEN SET_TAC[]);
663 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
664 (REWRITE_TAC[REAL_ARITH `a * x - b * x = x * (a - b)`]);
665 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
666 (ASM_REAL_ARITH_TAC);
669 {X | ~(X SUBSET ball (vec 0,r)) /\ mcell_set V X /\ critical_edgeX V X x})
670 <= &(CARD {X | mcell_set V X /\ VX V X u0})`);
671 (REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC CARD_SUBSET);
673 (ASM_REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM]);
675 (MATCH_MP_TAC FINITE_SUBSET);
676 (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`);
678 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
680 (ONCE_REWRITE_TAC[SUBSET]);
681 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
682 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
683 (EXISTS_TAC `V:real^3->bool`);
685 (NEW_GOAL `VX V x' = V INTER x'`);
686 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
687 (UNDISCH_TAC `mcell_set V x'` THEN
688 REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
689 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
692 (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]);
693 (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
695 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
698 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X u0}) <= cc2`);
701 (ABBREV_TAC `s1_temp = &(CARD
702 {X | ~(X SUBSET ball (vec 0,r)) /\
704 critical_edgeX V X x})`);
705 (ABBREV_TAC `s2_temp = &(CARD {X | mcell_set V X /\ VX V X u0})`);
706 (ASM_REAL_ARITH_TAC);
708 (ABBREV_TAC `g = (\x:real^3->bool. cc2 * cc1)`);
711 `sum T4 (g:(real^3->bool)->real) =
713 sum {m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
714 (\(m:real^3,n). g {m, n})`);
715 (ONCE_REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]);
717 (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]);
718 (MATCH_MP_TAC SUM_PAIR_2_SET);
719 (MATCH_MP_TAC FINITE_SUBSET);
720 (EXISTS_TAC `T1:real^3->bool`);
722 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
724 (REWRITE_TAC[REAL_ARITH `&1 / &2 * s <= t <=> s <= &2 * t`]);
727 `h = (\m:real^3. {n | n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`);
729 `{m,n | m IN T3 /\ n IN T3 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} =
730 {m:real^3,n | m IN T3 /\ n IN h m}`);
733 (ABBREV_TAC `k = (\m n. (g:(real^3->bool)->real) {m,n})`);
734 (REWRITE_WITH `(\(m,n). (g:(real^3->bool)->real) {m, n}) = (\(m,n). k m n)`);
735 (REWRITE_TAC[FUN_EQ_THM]);
737 (NEW_GOAL `(x:real^3#real^3) = FST x, SND x`);
739 (ONCE_REWRITE_TAC[ASSUME `(x:real^3#real^3) = FST x, SND x`]);
740 (EXPAND_TAC "k" THEN REWRITE_TAC[]);
742 `sum {m:real^3,n:real^3 | m IN T3 /\ n IN h m} (\(m,n). k m n) =
743 sum T3 (\m. sum (h m) (k m))`);
744 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
745 (MATCH_MP_TAC SUM_SUM_PRODUCT);
748 (MATCH_MP_TAC FINITE_SUBSET);
749 (EXISTS_TAC `T1:real^3->bool`);
751 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
756 (MATCH_MP_TAC FINITE_SUBSET);
757 (EXISTS_TAC `T3:real^3->bool`);
759 (MATCH_MP_TAC FINITE_SUBSET);
760 (EXISTS_TAC `T1:real^3->bool`);
762 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
766 (EXPAND_TAC "k" THEN EXPAND_TAC "g");
767 (NEW_GOAL `sum T3 (\m. sum ((h:real^3->real^3->bool) m) (\n. cc2 * cc1)) <=
768 sum T3 (\m. (&4) pow 3 * cc2 * cc1)`);
769 (MATCH_MP_TAC SUM_LE);
771 (MATCH_MP_TAC FINITE_SUBSET);
772 (EXISTS_TAC `T1:real^3->bool`);
774 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
776 (EXPAND_TAC "h" THEN REPEAT STRIP_TAC THEN REWRITE_TAC[]);
778 `sum {n:real^3 | n IN T3 /\ ~(x = n) /\
779 dist (x,n) <= &2 * hplus} (\n. cc2 * cc1) =
780 &(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) *
782 (MATCH_MP_TAC SUM_CONST);
783 (MATCH_MP_TAC FINITE_SUBSET);
784 (EXISTS_TAC `T3:real^3->bool`);
786 (MATCH_MP_TAC FINITE_SUBSET);
787 (EXISTS_TAC `T1:real^3->bool`);
789 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
793 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
794 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
795 (MATCH_MP_TAC REAL_LE_MUL);
797 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]);
801 `&(CARD {n | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus}) <=
802 &(CARD (V INTER ball (x:real^3, &3)))`);
803 (REWRITE_TAC[REAL_OF_NUM_LE]);
804 (MATCH_MP_TAC CARD_SUBSET);
806 (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN_BALL]);
807 (REWRITE_TAC[IN_INTER; IN_BALL; IN_ELIM_THM; SUBSET; IN]);
810 (NEW_GOAL `&2 * hplus < &3`);
811 (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC);
812 (ASM_REAL_ARITH_TAC);
813 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
814 (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`);
815 (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]);
816 (MATCH_MP_TAC BOUNDS_VGEN_klemma);
817 (ASM_REWRITE_TAC[REAL_ARITH `&0 <= &3`]);
819 `s1 = &(CARD {n:real^3 | n IN T3 /\ ~(x = n) /\ dist (x,n) <= &2 * hplus})`);
820 (ASM_REAL_ARITH_TAC);
821 (MATCH_MP_TAC REAL_LE_MUL);
822 (ASM_REAL_ARITH_TAC);
823 (NEW_GOAL `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) <= &2 * dd * r pow 2`);
825 `sum T3 (\m:real^3. &4 pow 3 * cc2 * cc1) =
826 &(CARD T3) * &4 pow 3 * cc2 * cc1`);
827 (MATCH_MP_TAC SUM_CONST);
828 (MATCH_MP_TAC FINITE_SUBSET);
829 (EXISTS_TAC `T1:real^3->bool`);
831 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
835 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
836 (REWRITE_TAC[REAL_ARITH
837 `&2 * (&1 / &2 * dd2 * &4 pow 3 * cc2 * cc1) * r pow 2 -
838 &(CARD (T3:real^3->bool)) * &4 pow 3 * cc2 * cc1 =
839 (&4 pow 3 * cc2 * cc1) * (dd2 * r pow 2 - &(CARD T3))`]);
840 (MATCH_MP_TAC REAL_LE_MUL);
842 (REWRITE_TAC[REAL_ARITH `&0 <= &4 pow 3 * x <=> &0 <= x`]);
843 (MATCH_MP_TAC REAL_LE_MUL);
844 (ASM_REAL_ARITH_TAC);
845 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `(a <= b <=> &0 <= b - a)`)]);
848 (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]);
849 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
850 (EXISTS_TAC `dd1 * r pow 2`);
852 (FIRST_ASSUM MATCH_MP_TAC);
854 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
855 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]);
856 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
857 (ASM_REAL_ARITH_TAC);
858 (REWRITE_TAC[REAL_LE_POW_2]);
859 (ASM_REAL_ARITH_TAC);
861 (* ======================================================================== *)
862 (* CHECK DEN DAY LA OK ROI - (._o) (0_o) *)
863 (* ==================================================================== *)
866 `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x)) =
867 sum T2 (\e. cluster_gammaX V e (cell_cluster V e)) -
868 sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`);
869 (REWRITE_TAC[REAL_ARITH `a = b - c <=> b = a + c`]);
871 `f1 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (\X. f X x))`);
873 `f2 = (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))`);
875 `sum T2 (\e. cluster_gammaX V e (cell_cluster V e)) =
876 sum T2 (\e:real^3->bool. f1 e + f2 e)`);
877 (MATCH_MP_TAC SUM_EQ);
878 (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
879 (EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[cluster_gammaX; cell_cluster]);
880 (REWRITE_TAC[FUN_EQ_THM] THEN REPEAT STRIP_TAC);
882 (REWRITE_TAC[SET_RULE `{X | x IN critical_edgeX V X /\ mcell_set V X} =
883 {X | mcell_set V X /\ critical_edgeX V X x}`]);
884 (MATCH_MP_TAC SUM_ADD);
885 (MATCH_MP_TAC FINITE_SUBSET);
886 (EXISTS_TAC `{X | X SUBSET ball (u0,&8) /\ mcell_set V X}`);
888 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
890 (ONCE_REWRITE_TAC[SUBSET]);
891 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
892 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
893 (EXISTS_TAC `V:real^3->bool`);
895 (NEW_GOAL `VX V x' = V INTER x'`);
896 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
897 (UNDISCH_TAC `mcell_set V x'` THEN
898 REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
899 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
902 (UNDISCH_TAC `critical_edgeX V x' x` THEN
903 REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC);
904 (NEW_GOAL `VX V x' u0`);
905 (NEW_GOAL `u0 = u' \/ u0 = v':real^3`);
907 (UP_ASM_TAC THEN STRIP_TAC);
908 (REWRITE_TAC[ASSUME `u0 = u':real^3`]);
910 (REWRITE_TAC[ASSUME `u0 = v':real^3`]);
913 (UNDISCH_TAC `VX V x' u0` THEN ASM_REWRITE_TAC[VX]);
914 (REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
917 (NEW_GOAL `VX V x' u0`);
918 (UNDISCH_TAC `mcell_set V x'` THEN
919 REWRITE_TAC[mcell_set; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
920 (UNDISCH_TAC `critical_edgeX V x' x` THEN
921 REWRITE_TAC[critical_edgeX; edgeX; IN; IN_ELIM_THM] THEN STRIP_TAC);
922 (NEW_GOAL `u0 = u' \/ u0 = v':real^3`);
924 (UP_ASM_TAC THEN STRIP_TAC);
925 (REWRITE_TAC[ASSUME `u0 = u':real^3`]);
927 (REWRITE_TAC[ASSUME `u0 = v':real^3`]);
929 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
931 (MATCH_MP_TAC SUM_ADD);
934 (MATCH_MP_TAC (REAL_ARITH `&0 <= a /\ b + x <= &0 ==> x <= a - b`));
936 (MATCH_MP_TAC SUM_POS_LE);
938 (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
941 (UNDISCH_TAC `cell_cluster_estimate V`);
942 (REWRITE_TAC[cell_cluster_estimate]);
943 (REWRITE_TAC[REAL_ARITH `&0 <= a <=> a >= &0`] THEN STRIP_TAC);
947 `f1 = (\x. sum {X | X SUBSET ball (vec 0, r + &8) /\
948 ~(X SUBSET ball (vec 0, r - &8)) /\
950 critical_edgeX V X x} (beta_bump V x))`);
952 `f2 = (\x. sum {X | X SUBSET ball (vec 0, r - &8) /\ mcell_set V X /\
953 critical_edgeX V X x} (beta_bump V x))`);
955 `sum T2 (\x. sum {X | mcell_set V X /\ critical_edgeX V X x} (beta_bump V x))
956 = sum (T2:(real^3->bool)->bool) f1 + sum T2 f2`);
958 `sum (T2:(real^3->bool)->bool) f1 + sum T2 f2 = sum T2 (\x. f1 x + f2 x)`);
959 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
960 (MATCH_MP_TAC SUM_ADD);
963 (MATCH_MP_TAC SUM_EQ);
964 (EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
965 (EXPAND_TAC "f1" THEN EXPAND_TAC "f2");
967 `s1 = {X | X SUBSET ball (vec 0,r + &8) /\ ~(X SUBSET ball (vec 0,r - &8)) /\
968 mcell_set V X /\ critical_edgeX V X x}`);
969 (ABBREV_TAC `s2 = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\
970 critical_edgeX V X x}`);
971 (REWRITE_WITH `{X | mcell_set V X /\ critical_edgeX V X x} = s1 UNION s2`);
972 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN
973 REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; IN_ELIM_THM; IN]);
977 (ASM_CASES_TAC `x' SUBSET ball ((vec 0):real^3,r - &8)`);
979 (ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_BALL]);
982 (NEW_GOAL `x' SUBSET ball (u0:real^3, &8)`);
983 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
985 (EXISTS_TAC `V:real^3->bool`);
987 (NEW_GOAL `x:real^3->bool SUBSET x'`);
988 (MATCH_MP_TAC CRITICAL_EDGEX_SUBSET_MCELL);
989 (EXISTS_TAC `V:real^3->bool`);
991 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
993 (NEW_GOAL `dist (u0:real^3, x'') < &8`);
994 (REWRITE_TAC[GSYM IN_BALL] THEN ASM_SET_TAC[]);
995 (NEW_GOAL `dist (vec 0, x'') <= dist (u0, x'') + dist (vec 0, u0:real^3)`);
997 (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
998 (REWRITE_TAC[GSYM IN_BALL]);
999 (UNDISCH_TAC `(T1:real^3->bool) u0`);
1000 (EXPAND_TAC "T1" THEN REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1002 (ASM_REAL_ARITH_TAC);
1003 (ASM_REWRITE_TAC[]);
1005 (ASM_REWRITE_TAC[]);
1006 (ASM_REWRITE_TAC[]);
1007 (ASM_REWRITE_TAC[]);
1008 (MATCH_MP_TAC SUM_UNION);
1010 (MATCH_MP_TAC FINITE_SUBSET);
1011 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
1013 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]);
1015 (MATCH_MP_TAC FINITE_SUBSET);
1016 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`);
1018 (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA_2]);
1021 (* ======================================================================== *)
1022 (* ======================================================================== *)
1024 (EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN SET_TAC[]);
1026 (REWRITE_WITH `sum (T2:(real^3->bool)->bool) f2 = &0`);
1028 (REWRITE_TAC[SET_RULE
1029 `!V r x. {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X /\
1030 critical_edgeX V X x} =
1031 {X | X IN {X| X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
1032 critical_edgeX V X x}`]);
1036 {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
1037 critical_edgeX V X x}
1041 {X | X IN {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X} /\
1042 critical_edgeX V X x}
1043 (\X. beta_bump V x X))`);
1044 (REWRITE_WITH `!x V. (\X. beta_bump V x X) = beta_bump V x`);
1045 (REWRITE_TAC[FUN_EQ_THM] THEN ASM_REWRITE_TAC[]);
1047 (ABBREV_TAC `t = {X | X SUBSET ball (vec 0,r - &8) /\ mcell_set V X}`);
1048 (ABBREV_TAC `g = beta_bump V`);
1049 (ABBREV_TAC `s = T2:(real^3->bool)->bool`);
1051 `sum s (\x. sum {X | X IN t /\ critical_edgeX V X x} (\X. g x X)) =
1052 sum t (\X. sum {x | x IN s /\ critical_edgeX V X x} (\x. g x X))`);
1053 (MATCH_MP_TAC SUM_SUM_RESTRICT);
1055 (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[]);
1057 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
1058 (ASM_REWRITE_TAC[]);
1059 (EXPAND_TAC "s" THEN EXPAND_TAC "t" THEN EXPAND_TAC "g");
1060 (MATCH_MP_TAC SUM_EQ_0);
1061 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC);
1063 (REWRITE_WITH `{x' | T2 x' /\ critical_edgeX V x x'} =
1064 {x' | x' IN critical_edgeX V x}`);
1065 (MATCH_MP_TAC (SET_RULE `A SUBSET B /\ B SUBSET A ==> A = B`));
1068 (ASM_REWRITE_TAC[IN]);
1069 (REWRITE_TAC[GSYM (ASSUME `{{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\
1070 ~(u0 = u1) /\ hl [u0; u1] <= hplus} = s`)]);
1072 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX]);
1074 (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3` THEN ASM_REWRITE_TAC[]);
1076 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`; IN_INTER; IN_BALL]);
1077 (NEW_GOAL `VX V x = V INTER x`);
1078 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
1079 (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
1081 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
1082 (ASM_REWRITE_TAC[IN]);
1083 (STRIP_TAC THEN UNDISCH_TAC `VX V x u'`);
1084 (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
1085 (REWRITE_WITH `u':real^3 IN V /\ v' IN V`);
1089 (NEW_GOAL `u':real^3 IN ball (vec 0, r - &8)`);
1091 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC);
1092 (NEW_GOAL `v':real^3 IN ball (vec 0, r - &8)`);
1094 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL] THEN REAL_ARITH_TAC);
1095 (REWRITE_WITH `hl [u'; v':real^3] = hl [u; v:real^3]`);
1096 (REWRITE_TAC[HL; set_of_list]);
1097 (ASM_REWRITE_TAC[]);
1098 (ASM_REWRITE_TAC[]);
1100 (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);
1101 (ASM_REWRITE_TAC[]);
1102 (EXISTS_TAC `u':real^3` THEN EXISTS_TAC `v':real^3`);
1103 (ASM_REWRITE_TAC[]);
1104 (MATCH_MP_TAC SUM_BETA_BUMP_LEMMA);
1105 (ASM_REWRITE_TAC[]);
1107 (REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
1109 (REWRITE_TAC[HL_2; REAL_ARITH `inv (&2) * a <= b <=> a <= &2 * b`]);
1111 `sum {{u0:real^3, u1} | u0 IN T1 /\ u1 IN T1 /\ ~(u0 = u1) /\
1112 dist (u0,u1) <= &2 * hplus} f1 =
1114 sum {m,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1115 (\(m,n). f1 {m, n})`);
1116 (REWRITE_TAC[REAL_ARITH `a = &1 / &2 * b <=> b = &2 * a`]);
1117 (MATCH_MP_TAC SUM_PAIR_2_SET);
1118 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
1119 (ASM_REWRITE_TAC[]);
1122 `T3 = V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0, r - &16)`);
1124 `sum {m:real^3,n | m IN T1 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1125 (\(m,n). f1 {m, n}) =
1126 sum {m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1127 (\(m,n). f1 {m, n})`);
1128 (MATCH_MP_TAC SUM_SUPERSET);
1130 (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN
1131 REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
1133 (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3` THEN ASM_REWRITE_TAC[]);
1134 (EXPAND_TAC "T1" THEN UNDISCH_TAC
1135 `(V INTER ball ((vec 0):real^3,r) DIFF ball (vec 0,r - &16)) m` THEN
1136 REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1138 (EXPAND_TAC "T1" THEN EXPAND_TAC "T3" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
1140 (ASM_REWRITE_TAC[]);
1143 `{X | X SUBSET ball (vec 0,r + &8) /\
1144 ~(X SUBSET ball (vec 0,r - &8)) /\
1146 critical_edgeX V X {m, n}} = {}`);
1147 (REWRITE_TAC[SET_RULE `y = {} <=> ~(?x. x IN y)`]);
1149 (UNDISCH_TAC `~(?m n.
1150 ((V INTER ball (vec 0,r) DIFF ball (vec 0,r - &16)) m /\
1151 (V INTER ball (vec 0,r)) n /\
1153 dist (m:real^3,n) <= &2 * hplus) /\
1154 x = m,n) ` THEN REWRITE_TAC[]);
1155 (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3`);
1156 (ASM_REWRITE_TAC[]);
1157 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1158 (EXPAND_TAC "T3" THEN REWRITE_TAC[IN_DIFF; IN; IN_BALL]);
1159 (ASM_REWRITE_TAC[]);
1160 (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM]);
1162 (NEW_GOAL `?p:real^3. p IN x' /\ ~(p IN ball (vec 0,r - &8))`);
1163 (UNDISCH_TAC `~(x' SUBSET ball ((vec 0):real^3,r - &8))`);
1165 (UP_ASM_TAC THEN STRIP_TAC);
1166 (UP_ASM_TAC THEN REWRITE_TAC[IN_BALL]);
1167 (NEW_GOAL `x' SUBSET ball (p:real^3, &8)`);
1168 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
1169 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
1170 (NEW_GOAL `m:real^3 IN x'`);
1171 (UNDISCH_TAC `critical_edgeX V x' {m, n}` THEN
1172 REWRITE_TAC[critical_edgeX; edgeX; IN_ELIM_THM; IN]);
1175 (NEW_GOAL `VX V x' = V INTER x'`);
1176 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
1177 (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
1179 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
1180 (ASM_REWRITE_TAC[IN]);
1181 (STRIP_TAC THEN UNDISCH_TAC `VX V x' u'`);
1182 (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
1184 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1186 (NEW_GOAL `dist (p, m:real^3) < &8`);
1187 (REWRITE_TAC[GSYM IN_BALL]);
1189 (NEW_GOAL `dist (vec 0, p) <= dist (vec 0, m:real^3) + dist (p, m)`);
1191 (ASM_REAL_ARITH_TAC);
1192 (REWRITE_TAC[SUM_CLAUSES]);
1195 `g = (\m:real^3. {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus})`);
1197 `{m,n | m IN T3 /\ n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus} =
1198 {m,n:real^3 | m IN T3 /\ n IN g m}`);
1199 (EXPAND_TAC "g" THEN ASM_REWRITE_TAC[] THEN SET_TAC[]);
1200 (ABBREV_TAC `h = (\m. (\n. (f1:(real^3->bool)->real) {m, n}))`);
1201 (REWRITE_WITH `(\(m,n). (f1:(real^3->bool)->real) {m, n}) =
1203 (REWRITE_TAC[FUN_EQ_THM]);
1204 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
1205 (NEW_GOAL `x:real^3#real^3 = FST x, SND x`);
1206 (REWRITE_TAC[PAIR]);
1207 (ONCE_ASM_REWRITE_TAC[]);
1208 (EXPAND_TAC "h" THEN REWRITE_TAC[]);
1210 (REWRITE_WITH `sum {m,n | m IN T3 /\ n IN g m} (\(m,n). h m n) =
1211 sum T3 (\m. sum (g m) ((h:real^3->real^3->real) m))`);
1212 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
1213 (MATCH_MP_TAC SUM_SUM_PRODUCT);
1216 (MATCH_MP_TAC FINITE_SUBSET);
1217 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1219 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1220 (EXPAND_TAC "T3" THEN SET_TAC[]);
1223 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
1224 (MATCH_MP_TAC FINITE_SUBSET);
1225 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1227 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1228 (EXPAND_TAC "T1" THEN SET_TAC[]);
1231 `sum T3 (\m. sum ((g:real^3->real^3->bool) m) (h m)) <=
1232 sum T3 (\n:real^3. ss1)`);
1233 (MATCH_MP_TAC SUM_LE);
1235 (MATCH_MP_TAC FINITE_SUBSET);
1236 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1238 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1239 (EXPAND_TAC "T3" THEN SET_TAC[]);
1240 (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
1242 (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (h x) <= sum (g x) (\x. cc4 * cc3)`);
1243 (MATCH_MP_TAC SUM_LE);
1245 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
1246 (MATCH_MP_TAC FINITE_SUBSET);
1247 (EXISTS_TAC `V:real^3->bool INTER ball (vec 0,r)`);
1249 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1250 (EXPAND_TAC "T1" THEN SET_TAC[]);
1252 (REPEAT STRIP_TAC THEN EXPAND_TAC "h" THEN REWRITE_TAC[]);
1254 (ABBREV_TAC `S1 = {X | X SUBSET ball (vec 0,r + &8) /\
1255 ~(X SUBSET ball (vec 0,r - &8)) /\
1257 critical_edgeX V X {x, x'}}`);
1258 (NEW_GOAL `sum (S1:(real^3->bool)->bool) (beta_bump V {x, x'}) <=
1260 (MATCH_MP_TAC SUM_LE);
1262 (MATCH_MP_TAC FINITE_SUBSET);
1263 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
1265 (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
1266 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
1267 (ASM_REWRITE_TAC[]);
1268 (EXPAND_TAC "S1" THEN SET_TAC[]);
1271 (FIRST_ASSUM MATCH_MP_TAC);
1272 (UP_ASM_TAC THEN EXPAND_TAC "S1" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
1273 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
1275 (NEW_GOAL `sum S1 (\x:real^3->bool. cc3) = &(CARD S1) * cc3`);
1276 (MATCH_MP_TAC SUM_CONST);
1277 (MATCH_MP_TAC FINITE_SUBSET);
1278 (EXISTS_TAC `{X | X SUBSET ball (vec 0,r + &8) /\ mcell_set V X}`);
1280 (REPEAT STRIP_TAC THEN REWRITE_TAC[]);
1281 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
1282 (ASM_REWRITE_TAC[]);
1283 (EXPAND_TAC "S1" THEN SET_TAC[]);
1284 (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <= cc4`);
1285 (NEW_GOAL `&(CARD (S1:(real^3->bool)->bool)) <=
1286 &(CARD {X | mcell_set V X /\ VX V X x})`);
1287 (REWRITE_TAC[REAL_OF_NUM_LE]);
1288 (MATCH_MP_TAC CARD_SUBSET);
1290 (EXPAND_TAC "S1" THEN
1291 REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; critical_edgeX; edgeX] THEN
1293 (ASM_REWRITE_TAC[]);
1294 (NEW_GOAL `x:real^3 = u' \/ x = v'`);
1296 (UP_ASM_TAC THEN STRIP_TAC);
1297 (ASM_REWRITE_TAC[]);
1298 (ASM_REWRITE_TAC[]);
1300 (MATCH_MP_TAC FINITE_SUBSET);
1301 (EXISTS_TAC `{X | X SUBSET ball (x:real^3, &8) /\ mcell_set V X}`);
1303 (MATCH_MP_TAC FINITE_MCELL_SET_LEMMA_2);
1304 (ASM_REWRITE_TAC[]);
1305 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
1306 (REWRITE_TAC[MESON[IN] `(A:real^3->bool) x <=> x IN A`]);
1307 (NEW_GOAL `VX V x'' = V INTER x''`);
1308 (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
1309 (UNDISCH_TAC `mcell_set V x''` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
1311 (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
1312 (ASM_REWRITE_TAC[IN]);
1313 (STRIP_TAC THEN UNDISCH_TAC `VX V x'' x`);
1314 (ASM_REWRITE_TAC[VX; MESON[IN] `{} x <=> x IN {}`] THEN SET_TAC[]);
1315 (NEW_GOAL `x'' SUBSET ball (x:real^3, &8)`);
1316 (MATCH_MP_TAC MCELL_SUBSET_BALL8_2);
1317 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
1320 (ASM_REWRITE_TAC[]);
1321 (NEW_GOAL `&(CARD {X | mcell_set V X /\ VX V X x}) <= cc4`);
1322 (FIRST_ASSUM MATCH_MP_TAC);
1323 (ASM_REWRITE_TAC[]);
1324 (UNDISCH_TAC `x IN (T3:real^3->bool)` THEN EXPAND_TAC "T3");
1326 (ABBREV_TAC `s_temp = &(CARD {X | mcell_set V X /\ VX V X x})`);
1327 (ASM_REAL_ARITH_TAC);
1328 (NEW_GOAL `sum (S1:(real^3->bool)->bool) (\x. cc3) <= cc4 * cc3`);
1329 (ASM_REWRITE_TAC[]);
1330 (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
1331 (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
1332 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1333 (ASM_REAL_ARITH_TAC);
1334 (ASM_REAL_ARITH_TAC);
1335 (ABBREV_TAC `s_temp = sum (S1:(real^3->bool)->bool) (\x. cc3)`);
1336 (ASM_REAL_ARITH_TAC);
1340 (NEW_GOAL `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) <= ss1`);
1342 `sum ((g:real^3->real^3->bool) x) (\x. cc4 * cc3) =
1343 &(CARD (g x)) * cc4 * cc3`);
1344 (MATCH_MP_TAC SUM_CONST);
1346 (MATCH_MP_TAC FINITE_SUBSET);
1347 (EXISTS_TAC `T1:real^3->bool`);
1349 (EXPAND_TAC "T1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
1350 (ASM_REWRITE_TAC[]);
1353 (NEW_GOAL `&(CARD ((g:real^3->real^3->bool) x)) <=
1354 &(CARD (V INTER ball (x:real^3, &3)))`);
1355 (REWRITE_TAC[REAL_OF_NUM_LE]);
1356 (MATCH_MP_TAC CARD_SUBSET);
1358 (EXPAND_TAC "g" THEN EXPAND_TAC "T1" THEN
1359 REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; IN_INTER; IN_BALL]);
1361 (ASM_REWRITE_TAC[]);
1362 (NEW_GOAL `&2 * hplus < &3`);
1363 (REWRITE_TAC[hplus] THEN REAL_ARITH_TAC);
1364 (ASM_REAL_ARITH_TAC);
1365 (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
1368 (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
1369 (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
1370 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1371 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]);
1372 (NEW_GOAL `&(CARD (V INTER ball (x:real^3,&3))) <= &4 pow 3`);
1373 (REWRITE_TAC[REAL_ARITH `&4 = &3 + &1`]);
1374 (MATCH_MP_TAC BOUNDS_VGEN_klemma);
1375 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1376 (ASM_REAL_ARITH_TAC);
1377 (MATCH_MP_TAC REAL_LE_MUL);
1378 (ASM_REAL_ARITH_TAC);
1380 (ASM_REAL_ARITH_TAC);
1383 (REWRITE_TAC[REAL_ARITH `&1 / &2 * x + a <= &0 <=> x <= &2 * (-- a)`]);
1384 (REWRITE_TAC[REAL_ARITH `c * r pow 2 + d * r pow 2 = (c + d) * r pow 2`]);
1385 (REWRITE_WITH `(c:real) + dd = -- ss`);
1388 (REWRITE_TAC[REAL_ARITH `&2 * --(--ss * r pow 2) = &2 * ss * r pow 2`]);
1389 (NEW_GOAL `sum T3 (\n:real^3. ss1) <= &2 * ss * r pow 2`);
1390 (REWRITE_WITH `sum T3 (\n:real^3. ss1) = &(CARD (T3)) * ss1`);
1391 (MATCH_MP_TAC SUM_CONST);
1392 (MATCH_MP_TAC FINITE_SUBSET);
1393 (EXISTS_TAC `(V:real^3->bool) INTER ball (vec 0,r)`);
1395 (MATCH_MP_TAC FINITE_PACK_LEMMA THEN ASM_REWRITE_TAC[]);
1396 (EXPAND_TAC "T3" THEN SET_TAC[]);
1398 (REWRITE_TAC[REAL_ARITH
1399 `&2 * (&1 / &2 * dd4 * ss1) * r pow 2 = (dd4 * r pow 2) * ss1`]);
1400 (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
1401 (ONCE_REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
1402 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1403 (ONCE_REWRITE_TAC[GSYM (REAL_ARITH `a <= b <=> &0 <= b - a`)]);
1405 (ONCE_REWRITE_TAC[SET_RULE `A INTER B DIFF C = A INTER B DIFF A INTER C`]);
1407 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
1408 (EXISTS_TAC `dd3 * r pow 2`);
1410 (FIRST_ASSUM MATCH_MP_TAC);
1411 (ASM_REWRITE_TAC[]);
1412 (ONCE_REWRITE_TAC[REAL_ARITH `(a <= b <=> &0 <= b - a)`]);
1413 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b ) * x`]);
1414 (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
1415 (ASM_REAL_ARITH_TAC);
1416 (REWRITE_TAC[REAL_LE_POW_2]);
1418 (MATCH_MP_TAC REAL_LE_MUL);
1420 (ASM_REAL_ARITH_TAC);
1421 (MATCH_MP_TAC REAL_LE_MUL);
1422 (ASM_REAL_ARITH_TAC);
1425 `sum T3 (\m:real^3. sum {n | n IN T1 /\ ~(m = n) /\ dist (m,n) <= &2 * hplus}
1427 sum T3 (\m. sum (g m) (h m))`);
1428 (EXPAND_TAC "g" THEN REWRITE_TAC[]);
1429 (ASM_REAL_ARITH_TAC);
1434 (UNDISCH_TAC `~(saturated V /\ packing V)` THEN ASM_REWRITE_TAC[]);
1435 (ASM_MESON_TAC[])]);;