1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Nguyen Tat Thang *)
7 (* ========================================================================== *)
13 module type Pack1_type = sig
16 flyspeck_needs "volume/vol1.hl";;
18 module Pack1 (* : Pack1_type *) = struct
27 let int_ball = Vol1.int_ball;;
28 let hinhcau_ball = Vol1.hinhcau_ball;;
29 let finite_int_ball = Vol1.finite_int_ball;;
30 let FINITE_IMAGE_INJ = Vol1.FINITE_IMAGE_INJ;;
33 (TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;
36 let packing = new_definition `packing (S:real^3 -> bool) = (!u v. S u /\ S v /\ ~(u = v) ==> (&2 <= dist( u, v)))`;;
38 let map3=new_definition `(map3:real^3 -> real^3 ->real^3) x p = lambda i. floor(&2* (x$i - p$i))`;;
40 let bound_square=prove( `!(a:real)(b:real)(c:real). (a<=b /\ b<=c) ==> b pow 2 <= max ( a pow 2) (c pow 2)`,
41 REPEAT STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH `&0<= b \/ b< &0`)
42 THENL [MP_TAC(MESON[REAL_POW_LE2] `&0<= b /\ b<= c ==> b pow 2 <= c pow 2`) THEN ASM_SIMP_TAC[REAL_LE_MAX];MP_TAC(REAL_ARITH `b< &0 /\a<= b ==> &0<= -- b /\ --b<= --a`)] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(MESON[REAL_POW_LE2] `&0<= -- b /\ --b<= --a ==> --b pow 2 <= --a pow 2`) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[REAL_LE_MAX;REAL_ARITH `--(x:real) pow 2= x pow 2`]);;
45 let cauchy_ineq=prove( `!(a:real)(b:real). (a+b) pow 2<= &2* (a pow 2+ b pow 2)`,REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH `(x:real) <= y <=> &0<= y - x`] THEN REWRITE_TAC[REAL_FIELD `&2 * (a pow 2 + b pow 2) - (a + b) pow 2 = (a- b) pow 2`]
46 THEN REWRITE_TAC[REAL_FIELD `(a- b) pow 2 = (a-b) * (a-b)`;REAL_LE_SQUARE]);;
48 let bdt_emveque=prove(`!(r:real). &0 <= &8* (r pow 2) + &6`,GEN_TAC
49 THEN MP_TAC(MESON[REAL_LE_SQUARE; REAL_FIELD `r pow 2= r * r`] `&0<= r pow 2`) THEN
50 DISCH_TAC THEN MP_TAC(MESON[REAL_LE_MUL;REAL_ARITH `&0<= &8`] `&0<= r pow 2 ==> &0<= &8* (r pow 2)`)
51 THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
54 let norm_abs= MESON[NORM_POS_LE;REAL_ARITH `&0<= a ==> abs a= a`] `!(x:real^3 ). norm x= abs (norm x)`;;
56 let bp_bdt=prove( `!(a:real)(b:real). (&0<= a /\ &0<= b) ==> (a< b <=> a pow 2 < b pow 2)`,REPEAT GEN_TAC
57 THEN REWRITE_TAC[GSYM REAL_ABS_REFL] THEN ONCE_REWRITE_TAC[MESON[] `x:real = y<=> y=x`] THEN STRIP_TAC
58 THEN ASM_MESON_TAC[REAL_LT_SQUARE_ABS]);;
60 let bdt_emnguchua=prove( `!(k:real). floor (&2* k)* floor( &2*k)<= &2*( &4* (k pow 2) + &1)`,
61 GEN_TAC THEN MP_TAC(SPEC ` &2*k:real` FLOOR) THEN REWRITE_TAC[REAL_ARITH `a:real < b+ &1 <=> a- &1 < b`]
62 THEN STRIP_TAC THEN MP_TAC(SPECL [`&2 * k - &1:real`;`floor (&2 * k):real`;`&2 * k` ] bound_square)
63 THEN ASM_SIMP_TAC[REAL_ARITH `a:real < b ==> a<= b`]
64 THEN DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH `floor (&2 * k) pow 2 <= max ((&2 * k - &1) pow 2) ((&2 * k) pow 2) /\ max ((&2 * k - &1) pow 2) ((&2 * k) pow 2) <= &2 * (&4 * k pow 2 + &1) ==> floor (&2 * k) * floor (&2 * k) <= &2 * (&4 * k pow 2 + &1)`)
65 THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[REAL_MAX_LE] THEN SIMP_TAC[cauchy_ineq;REAL_FIELD `&2 * k - &1= (&2 * k) + ( -- &1)`;REAL_FIELD `(&2 * k) pow 2 = &4 * (k pow 2 )`; REAL_ARITH `( -- &1) pow 2 = &1`] THEN SIMP_TAC[cauchy_ineq;REAL_FIELD `&4 * (k pow 2 )= (&2 * k) pow 2`;
66 REAL_ARITH ` &1= ( -- &1) pow 2`]
67 THEN ONCE_REWRITE_TAC[REAL_ARITH `&2 * ((&2 * k) pow 2 + &1)= &2 * ((&2 * k) pow 2 + ( -- &1) pow 2)`]
68 THEN REWRITE_TAC[cauchy_ineq] THEN REWRITE_TAC[REAL_FIELD `(&2 * k) pow 2 <= &2 * ((&2 * k) pow 2 + -- &1 pow 2) <=> &4* (k pow 2)<= &8* (k pow 2) + &2`]
69 THEN ONCE_REWRITE_TAC[REAL_ARITH `a<=b <=> &0<= b-a `;REAL_FIELD `&8 * k pow 2 + &2- &4 * k pow 2= &4 * k pow 2 + &2`]
70 THEN ONCE_REWRITE_TAC[REAL_FIELD `(&8 * k pow 2 + &2) - &4 * k pow 2= &4 * k pow 2 + &2`]
71 THEN MP_TAC(MESON[REAL_LE_SQUARE; REAL_FIELD `k pow 2 = k * k`] `&0<= k pow 2`) THEN
72 DISCH_TAC THEN MP_TAC(MESON[REAL_LE_MUL;REAL_ARITH `&0<= &4`] `&0<= k pow 2 ==> &0<= &4* (k pow 2)`)
73 THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
77 let map3_define=prove(`!(v:real^3)(p:real^3)(r:real). &0<=r /\ v IN ball(p,r)
78 ==> map3 p v IN ball(vec 0, sqrt(&8* (r pow 2) + &6))`,REPEAT GEN_TAC THEN REWRITE_TAC[ball;IN_ELIM_THM]
79 THEN REWRITE_TAC[dist;VECTOR_ARITH `vec 0 - map3 (p:real^3) v = -- map3 p v`;NORM_NEG]
80 THEN MP_TAC (SPEC `(&8* (r pow 2) + &6):real` SQRT_POS_LE)
81 THEN SIMP_TAC[bdt_emveque] THEN DISCH_TAC THEN ASSUME_TAC(ISPEC `(p:real^3- v):real^3` NORM_POS_LE) THEN ASSUME_TAC(ISPEC `(map3 (p:real^3) v):real^3` NORM_POS_LE) THEN REWRITE_TAC[MESON[] `a/\b ==> c <=> a==> b==> c`]
82 THEN DISCH_TAC THEN ASM_SIMP_TAC[bp_bdt] THEN SIMP_TAC[NORM_POW_2;DOT_3] THEN REWRITE_TAC[map3]
83 THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=1/\1<=3 /\ 1<=2 /\ 2<= 3 /\ 1<= 3 /\ 3<=3`]
84 THEN DISCH_TAC THEN MP_TAC(SPEC `((p:real^3)$1 - (v:real^3)$1):real` bdt_emnguchua) THEN MP_TAC(SPEC `((p:real^3)$2 - (v:real^3)$2):real` bdt_emnguchua)
85 THEN MP_TAC(SPEC `((p:real^3)$3 - (v:real^3)$3):real` bdt_emnguchua)
86 THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH `q:real <= &2 * (&4 * ((p:real^3)$1 - (v:real^3)$1) pow 2 + &1) +
87 &2 * (&4 * (p$2 - v$2) pow 2 + &1) + &2 * (&4 * (p$3 - v$3) pow 2 + &1) /\ &2 * (&4 * (p$3 - v$3) pow 2 + &1) +
88 &2 * (&4 * (p$2 - v$2) pow 2 + &1) + &2 * (&4 * (p$1 - v$1) pow 2 + &1) < sqrt (&8 * r pow 2 + &6) pow 2
89 ==> q< sqrt (&8 * r pow 2 + &6) pow 2`)
90 THEN ASM_SIMP_TAC[REAL_ARITH `floor (&2 * ((p:real^3)$3 - (v:real^3)$3)) * floor (&2 * (p$3 - v$3)):real <=
91 &2 * (&4 * (p$3 - v$3) pow 2 + &1) /\ floor (&2 * (p$2 - v$2)) * floor (&2 * (p$2 - v$2)) <=
92 &2 * (&4 * (p$2 - v$2) pow 2 + &1) /\ floor (&2 * (p$1 - v$1)) * floor (&2 * (p$1 - v$1)) <=
93 &2 * (&4 * (p$1 - v$1) pow 2 + &1) ==> floor (&2 * (p$1 - v$1)) * floor (&2 * (p$1 - v$1)) +
94 floor (&2 * (p$2 - v$2)) * floor (&2 * (p$2 - v$2)) +
95 floor (&2 * (p$3 - v$3)) * floor (&2 * (p$3 - v$3)) <=
96 &2 * (&4 * (p$1 - v$1) pow 2 + &1) +
97 &2 * (&4 * (p$2 - v$2) pow 2 + &1) +
98 &2 * (&4 * (p$3 - v$3) pow 2 + &1)`]
99 THEN REWRITE_TAC[REAL_FIELD `&2 * (&4 * ((p:real^3)$3 - (v:real^3)$3) pow 2 + &1) +
100 &2 * (&4 * (p$2 - v$2) pow 2 + &1) +
101 &2 * (&4 * (p$1 - v$1) pow 2 + &1)= &8 * ( (p$1 - v$1) pow 2 + (p$2 - v$2) pow 2 + (p$3 - v$3) pow 2) + &6`]
102 THEN ASSUME_TAC (SPEC `r:real` bdt_emveque) THEN ASM_SIMP_TAC[SQRT_POW_2]
103 THEN REWRITE_TAC[REAL_ARITH `a + &6 < b+ &6 <=> a< b`] THEN SIMP_TAC[REAL_ARITH `&0< &8`;REAL_LT_LMUL_EQ]
104 THEN ASM_REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT;DIMINDEX_3] THEN REWRITE_TAC[REAL_ARITH `a pow 2= a*a`]
105 THEN ASM_MESON_TAC[REAL_ARITH `a pow 2= a*a`]);;
108 let floor_ineq=prove( `!(x:real)(y:real). floor x = floor y ==> abs (x- y)< &1`,REPEAT STRIP_TAC THEN MP_TAC(SPEC `x:real` FLOOR) THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC(SPEC `y:real` FLOOR)
109 THEN REPEAT STRIP_TAC THEN MP_TAC (REAL_ARITH `floor y <= x /\ y < floor y + &1 ==> y< x+ &1`)
110 THEN ASM_REWRITE_TAC[] THEN MP_TAC (REAL_ARITH `floor y <= y /\ x < floor y + &1 ==> x< y+ &1`)
111 THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
114 let bdt_canbatrenbon=prove( `sqrt ( &3/ &4)< &2`,MP_TAC (SPEC `&3 / &4 :real` SQRT_POS_LE) THEN REWRITE_TAC[REAL_ARITH `&0<= &3/ &4`] THEN REWRITE_TAC[REAL_ARITH ` &0<=a:real <=> a = abs a`] THEN MP_TAC(SPEC `&2:real` REAL_ABS_REFL)
115 THEN REWRITE_TAC[REAL_ARITH ` &0 <= &2`] THEN REWRITE_TAC[MESON[] `a:real = b ==> c:real = d ==> c< b <=> a:real = b ==> c:real = d ==> d< a`] THEN REWRITE_TAC[REAL_LT_SQUARE_ABS] THEN SIMP_TAC[REAL_ARITH `&2 pow 2 = &4`;SQRT_POW_2;REAL_ARITH `&0<= &3/ &4`] THEN REAL_ARITH_TAC);;
118 let inj_map3=prove(`!(p:real^3)(r:real) (S:real^3 -> bool). (&0 <= r) /\ (packing S) ==> INJ (map3 p) (S INTER ball(p,r)) (int_ball (vec 0) (sqrt( &8 * (r pow 2) + &6)))`,REPEAT GEN_TAC THEN REWRITE_TAC[INJ] THEN STRIP_TAC THEN REWRITE_TAC[int_ball;IN_ELIM_THM] THEN REWRITE_TAC[IN_INTER;hinhcau_ball] THEN ASM_SIMP_TAC[map3_define] THEN REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[map3] THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3;ARITH_RULE `1<=1/\1<=3 /\ 1<=2 /\ 2<= 3 /\ 1<= 3 /\ 3<=3`]
119 THEN REWRITE_TAC[FLOOR;(* GSYM INTEGER_IS_INT *)] THEN REWRITE_TAC[CART_EQ]
120 THEN SIMP_TAC[LAMBDA_BETA;DIMINDEX_3] THEN REPEAT GEN_TAC THEN REWRITE_TAC[FORALL_3]
121 THEN REWRITE_TAC[MESON[] `a/\b/\c/\d/\e ==> f <=> a==>b==>c==>d ==>e==>f`]
122 THEN REPLICATE_TAC 5 DISCH_TAC THEN MP_TAC(SPECL [`&2 * ((p:real^3)$1 - (x:real^3)$1):real`;`&2 * ((p:real^3)$1 - (y:real^3)$1):real`] floor_ineq) THEN ASM_REWRITE_TAC[]
123 THEN MP_TAC(SPECL [`&2 * ((p:real^3)$2 - (x:real^3)$2):real`;`&2 * ((p:real^3)$2 - (y:real^3)$2):real`] floor_ineq) THEN ASM_REWRITE_TAC[] THEN MP_TAC(SPECL [`&2 * ((p:real^3)$3 - (x:real^3)$3):real`;`&2 * ((p:real^3)$3 - (y:real^3)$3):real`] floor_ineq) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_FIELD `&2 * ((a:real) - b) - &2 * (a- c)= &2*(c - b) `] THEN REWRITE_TAC[REAL_ABS_MUL] THEN MP_TAC(SPEC `&2:real` REAL_ABS_REFL) THEN REWRITE_TAC[REAL_ARITH ` &0 <= &2`]
124 THEN SIMP_TAC[] THEN REWRITE_TAC[REAL_ARITH ` &2* a< b <=> a< b/ &2`]
125 THEN REWRITE_TAC[MESON[REAL_ARITH `&1/ &2= abs (&1/ &2)`;REAL_LT_SQUARE_ABS;REAL_ARITH ` (&1/ &2) pow 2 = &1/ &4`] `abs (a:real) < &1/ &2 <=> a pow 2 < &1/ &4`] THEN REPEAT DISCH_TAC THEN SUBGOAL_THEN `norm(y:real^3 - x)< sqrt(&3/ &4)` MP_TAC
126 THENL [REWRITE_TAC[vector_norm;dist] THEN MP_TAC(SPEC `((y:real^3 - x) dot (y - x)):real` SQRT_POS_LE)
127 THEN REWRITE_TAC[DOT_POS_LE] THEN REWRITE_TAC[REAL_ARITH `&0<= a <=> a= abs a`]
128 THEN REWRITE_TAC[MESON[] `a:real= b ==> a< sqrt (&3 / &4) <=> a= b ==> b < sqrt (&3 / &4)`]
129 THEN DISCH_TAC THEN MP_TAC (SPEC `&3 / &4 :real` SQRT_POS_LE) THEN REWRITE_TAC[REAL_ARITH `&0<= &3/ &4`]
130 THEN REWRITE_TAC[REAL_ARITH `&0<= a <=> a= abs a`] THEN REWRITE_TAC[MESON[] `a:real= b ==> c< a <=> a= b ==> c < b`]
131 THEN SIMP_TAC[REAL_LT_SQUARE_ABS;REAL_ARITH `&1/ &2= abs (&1/ &2)`;MESON[SQRT_POW_2;REAL_ARITH `&0<= &3/ &4`] `(sqrt (&3 / &4)) pow 2= &3/ &4`;SQRT_POW_2;DOT_POS_LE] THEN REWRITE_TAC[DOT_3;DIMINDEX_3] THEN REWRITE_TAC[VECTOR_SUB_COMPONENT;REAL_ARITH `(a:real) * a= a pow 2`] THEN ASM_MESON_TAC[REAL_ARITH `a:real< &1/ &4 /\ b< &1/ &4 /\ c< &1/ &4 ==> a+b+c < &3/ &4`]; DISCH_TAC THEN MP_TAC(MESON[REAL_RAT_REDUCE_CONV `sqrt (&3 / &4) < &2`;REAL_ARITH `a:real<b /\ b< c ==> a< c`] `norm (y:real^3 - x) < sqrt (&3 / &4)/\ sqrt (&3 / &4) < &2 ==> norm (y- x)< &2`)
132 THEN ASM_REWRITE_TAC[bdt_canbatrenbon] THEN UNDISCH_TAC `(packing (S:real^3 -> bool)):bool`
133 THEN REWRITE_TAC[packing] THEN REWRITE_TAC[dist] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [`y:real^3`;`x:real^3`]) THEN UNDISCH_TAC `((x:real^3) IN (S:real^3 -> bool) /\ x IN ball (p:real^3,r)):bool`
134 THEN UNDISCH_TAC `((y:real^3) IN (S:real^3 -> bool) /\ y IN ball (p:real^3,r)):bool`
135 THEN SIMP_TAC[SET_RULE `(a:real^3) IN (S:real^3 -> bool ) <=> S a`] THEN REPLICATE_TAC 2 DISCH_TAC
136 THEN REWRITE_TAC[REAL_ARITH `a:real < &2 <=> ~( &2<= a)`]
137 THEN REWRITE_TAC[MESON[] `a ==> b==> c <=> a/\b ==> c`] THEN ONCE_REWRITE_TAC[MESON[] ` ~ (P:bool) ==> Q <=> (~ Q ==> P)`] THEN SIMP_TAC[]]);;
140 (*-----------------------------------------------------------------*)
141 (* Lemma 5.1 [KIUMVTC] Finiteness of packing inter ball *)
142 (*-----------------------------------------------------------------*)
146 let KIUMVTC=prove(`!(p:real^3)(r:real) (S:real^3 -> bool).(&0 <= r) /\ (packing S) ==> FINITE (S INTER ball(p,r))`,
147 REPEAT STRIP_TAC THEN MATCH_MP_TAC(ISPECL [`(map3 (p:real^3)):real^3 -> real^3`;`(S INTER ball(p,r)):real^3 ->bool`;`(int_ball (vec 0) (sqrt( &8 * (r pow 2) + &6))):real^3 ->bool`] FINITE_IMAGE_INJ )
148 THEN ASM_SIMP_TAC[map3_define;finite_int_ball;inj_map3]
149 THEN REWRITE_TAC[int_ball;IN_INTER] THEN REWRITE_TAC[hinhcau_ball;IN_ELIM_THM;LAMBDA_BETA;DIMINDEX_3]
150 THEN ASM_SIMP_TAC[map3_define] THEN REWRITE_TAC[map3;IN_ELIM_THM;LAMBDA_BETA;DIMINDEX_3]
151 THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LAMBDA_BETA;DIMINDEX_3] THEN MESON_TAC[FLOOR;(* GSYM INTEGER_IS_INT *)]);;
153 (*-----------------------------------------------------------------*)
154 (* About voronoi_open cell *)
155 (*-----------------------------------------------------------------*)
159 let voronoi_open = new_definition `voronoi_open S v = { x | !w. ((S w) /\ ~(w=v)) ==> (dist( x, v) < dist( x, w)) }`;;
161 let bis = new_definition `bis u v = {x | dist(x,u) = dist(x,v)}`;;
163 let nua_kg=new_definition `nua_kg (u:real^3) (v:real^3) = {x:real^3 | dist(x,u) < dist(x,v)}`;;
165 let saturated=new_definition `saturated S= (!x. ?(y:real^N). y IN S /\ dist (x,y)< &2)`;;
167 let voronoi_version2=prove( `!(v:real^3) (S:real^3-> bool). voronoi_open S v = INTERS {nua_kg x y | y IN (S DELETE v)/\ x= v}`,
168 REPEAT GEN_TAC THEN REWRITE_TAC[EXTENSION;GSYM SUBSET_ANTISYM_EQ;voronoi_open;INTERS]
169 THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC
170 THENL [REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
171 THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_ASSUM (MP_TAC o ISPEC `y:real^3`) THEN UNDISCH_TAC `(((y:real^3) IN S DELETE (v:real^3) /\ x' = v) /\ u = nua_kg x' y):bool` THEN REWRITE_TAC[DELETE;IN_ELIM_THM] THEN SIMP_TAC[SET_RULE `y:real^3 IN S <=> S y`]
172 THEN REWRITE_TAC[nua_kg;IN_ELIM_THM];REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC] THEN GEN_TAC THEN FIRST_X_ASSUM(MP_TAC o ISPEC ` (nua_kg (v:real^3) (w:real^3)):real^3 ->bool`) THEN REWRITE_TAC[nua_kg;IN_ELIM_THM] THEN DISCH_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `(?(x:real^3) (y:real^3).
173 (y IN S DELETE v /\ x = v) /\
174 {x | dist (x,v) < dist (x,w)} = {x' | dist (x',x) < dist (x',y)})` ASSUME_TAC
175 THENL [EXISTS_TAC `(v):real^3` THEN EXISTS_TAC `w:real^3` THEN
176 ASM_REWRITE_TAC[DELETE;IN_ELIM_THM;SET_RULE `w:real^3 IN S <=> S w`];UNDISCH_TAC `((?(x:real^3) (y:real^3).
177 (y IN S DELETE v /\ x = (v:real^3)) /\
178 {x | dist (x,v) < dist (x,w)} = {x' | dist (x',x) < dist (x',y)})
179 ==> dist (x,v) < dist (x,w)):bool` THEN ASM_REWRITE_TAC[]]);;
182 let norm_ineq_lt= prove(`!(x:real^3)(y:real^3). norm x< norm y <=> x dot x < y dot y`,REPEAT GEN_TAC THEN REWRITE_TAC[MESON[NORM_POS_LE;REAL_ARITH ` &0<= a <=> a = abs a`] `norm (x:real^3) < norm (y:real^3) <=> abs (norm x) < abs (norm y)`] THEN MESON_TAC[REAL_LT_SQUARE_ABS;NORM_POW_2]);;
185 let nua_kg_version2=prove(`!(v:real^3)(y:real^3). ?(a:real^3)(b:real). nua_kg v y= { x:real^3 | x dot a < b}`,
186 REPEAT GEN_TAC THEN EXISTS_TAC `&2 %(y:real^3 - v):real^3` THEN EXISTS_TAC `((y:real^3)$1 * y$1+ y$2 * y$2 + y$3 * y$3 - (v:real^3)$1 * v$1- v$2 * v$2 - v$3 * v$3 ):real` THEN REWRITE_TAC[nua_kg;EXTENSION;IN_ELIM_THM] THEN GEN_TAC
187 THEN REWRITE_TAC[dist;norm_ineq_lt] THEN REWRITE_TAC[DOT_3] THEN ONCE_REWRITE_TAC[REAL_ARITH `a:real < b <=> &0< b - a`]
188 THEN REWRITE_TAC[VECTOR_MUL_COMPONENT;VECTOR_SUB_COMPONENT] THEN REWRITE_TAC[REAL_FIELD `(((x:real^3)$1 - (y:real^3)$1) * (x$1 - y$1) +
189 (x$2 - y$2) * (x$2 - y$2) +
190 (x$3 - y$3) * (x$3 - y$3)) -
191 ((x$1 - (v:real^3)$1) * (x$1 - v$1) +
192 (x$2 - v$2) * (x$2 - v$2) +
193 (x$3 - v$3) * (x$3 - v$3))= (y$1 * y$1 + y$2 * y$2 + y$3 * y$3 - v$1 * v$1 - v$2 * v$2 - v$3 * v$3) -
194 (x$1 * &2 * (y$1 - v$1) + x$2 * &2 * (y$2 - v$2) + x$3 * &2 * (y$3 - v$3))`]);;
197 let convex_nua_kg=prove(`!(v:real^3)(y:real^3). convex (nua_kg v y)`,REPEAT GEN_TAC THEN MP_TAC(ISPECL [`v:real^3`;`y:real^3`] nua_kg_version2) THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN ASM_SIMP_TAC[]
198 THEN ONCE_REWRITE_TAC[CONVEX_HALFSPACE_LT;DOT_SYM] THEN MESON_TAC[CONVEX_HALFSPACE_LT]);;
201 (*------------------------------------------------------------*)
202 (* Convexity of Voronoi *)
203 (*------------------------------------------------------------*)
207 let convex_voronoi=prove( `!(v:real^3) (S:real^3-> bool). convex (voronoi_open S v)`,REPEAT GEN_TAC THEN MP_TAC(ISPECL [`v:real^3`;`S:real^3 -> bool`] voronoi_version2) THEN SIMP_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `! s. s IN {nua_kg (x:real^3) (y:real^3) | y IN S DELETE (v:real^3) /\ x = v} ==> convex s` MP_TAC THENL [GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[convex_nua_kg];MESON_TAC[CONVEX_INTERS]]);;
210 (*------------------------------------------------------------*)
211 (* Boundness of voronoi_open *)
212 (*------------------------------------------------------------*)
215 let bound_voronoi=prove( `!(v:real^3) (S:real^3-> bool). saturated S ==> bounded(voronoi_open S v)`,
216 REPEAT GEN_TAC THEN DISJ_CASES_TAC (MESON[] `bounded (voronoi_open (S:real^3 ->bool) (v:real^3)) \/ ~(bounded (voronoi_open S v))`)
217 THENL [ASM_MESON_TAC[];UNDISCH_TAC `(~ bounded (voronoi_open (S:real^3 ->bool) (v:real^3))):bool`
218 THEN REWRITE_TAC[bounded] THEN REWRITE_TAC[MESON[] `~(?(a:real). !(x:real^3). x IN voronoi_open (S:real^3->bool) (v:real^3)
219 ==> norm x <= a) <=> !(a:real).
220 ~ (!(x:real^3). x IN voronoi_open (S:real^3->bool) (v:real^3) ==> norm x <= a)`]
221 THEN REWRITE_TAC[MESON[] `~(!x. x IN voronoi_open (S:real^3->bool) (v:real^3) ==> norm x <= a)
222 <=> ? (x:real^3). ~ ( x IN voronoi_open S v ==> norm x <= a)`]
223 THEN REWRITE_TAC[MESON[NOT_IMP] `~((x:real^3) IN voronoi_open (S:real^3->bool) (v:real^3) ==> norm x <= a)
224 <=> x IN voronoi_open S v /\ ~ (norm x <= a)`]
225 THEN REWRITE_TAC[REAL_ARITH ` ~ (norm (x:real^3)<= a:real) <=> a< norm x`]
226 THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `norm (v:real^3) + &2:real`)
227 THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN UNDISCH_TAC `(x:real^3
228 IN voronoi_open (S:real^3->bool) (v:real^3) /\ norm (v:real^3)+ &2 < norm x):bool`
229 THEN REWRITE_TAC[voronoi_open;saturated;IN_ELIM_THM]
230 THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `(x):real^3`)
231 THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
232 THEN UNDISCH_TAC `(!(w:real^3). S w /\ ~(w = v:real^3) ==> dist (x,v) < dist (x,w)):bool`
233 THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `y:real^3`)
234 THEN MP_TAC(MESON[REAL_ARITH `norm (v:real^3) + &2 < norm (x:real^3) ==> &2 < norm x - norm v`;
235 MESON[REAL_ABS_SUB_NORM;REAL_ABS_LE;REAL_ARITH `(a:real)<= b /\ b<= c ==> a<= c`] `norm (x:real^3) - norm (v:real^3)
236 <= norm (x- v)`;REAL_ARITH `a:real < b /\ b<= c ==> a< c`] `norm (v:real^3) + &2 < norm (x:real^3) ==> &2< norm ( x - v)`)
237 THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(y:real^3 IN (S:real^3 -> bool) /\ dist (x,y) < &2):bool` THEN STRIP_TAC
238 THEN REWRITE_TAC[GSYM dist] THEN DISCH_TAC THEN SUBGOAL_THEN `~ (y:real^3 = v)` MP_TAC
239 THENL [(*1*)DISJ_CASES_TAC(MESON[] `(y:real^3 = v) \/ ~(y=v)`) THENL [UNDISCH_TAC `(dist (x:real^3,y) < &2):bool`
240 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH ` ~ (dist (x:real^3,v) < &2) <=> &2<= dist(x, v)`]
241 THEN ASM_MESON_TAC[REAL_ARITH `&2< a ==> &2 <= a`];ASM_MESON_TAC[]];(*2*)ASM_SIMP_TAC[SET_RULE `y:real^3 IN S <=> S y`]
242 THEN DISCH_TAC THEN ASM_SIMP_TAC[SET_RULE `y:real^3 IN S <=> S y`] THEN UNDISCH_TAC `(y IN (S:real^3 ->bool)):bool`
243 THEN REWRITE_TAC[SET_RULE `y IN (S:real^3 ->bool) <=> S y`] THEN SIMP_TAC[] THEN DISCH_TAC
244 THEN UNDISCH_TAC `(dist (x:real^3,y) < &2):bool` THEN UNDISCH_TAC `(&2 < dist (x,v:real^3)):bool` THEN REAL_ARITH_TAC]]);;
246 (*--------------------------------------------------------------*)
249 let open_nua_kg=prove(`!(v:real^3)(y:real^3). open (nua_kg v y)`,REPEAT GEN_TAC THEN MP_TAC(ISPECL [`v:real^3`;`y:real^3`] nua_kg_version2) THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN ASM_SIMP_TAC[]
250 THEN ONCE_REWRITE_TAC[OPEN_HALFSPACE_LT;DOT_SYM] THEN MESON_TAC[OPEN_HALFSPACE_LT]);;
254 let map_to_nua_kg=new_definition`map_to_nua_kg ((x:real^3), (y:real^3))= nua_kg x y`;;
257 let surj_map_to_nua_kg=prove(`!(v:real^3)(S:real^3 ->bool). IMAGE (map_to_nua_kg) ({v:real^3} CROSS ((S DELETE v) INTER ball(v, &4))) = {nua_kg (x:real^3) (y:real^3) | (y IN (S DELETE v)) /\ (x = v) /\ (y IN ball(v, &4))}`,
258 REWRITE_TAC[IMAGE] THEN REWRITE_TAC[map_to_nua_kg] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_CROSS;map_to_nua_kg;IN_ELIM_THM] THEN ONCE_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN STRIP_TAC
259 THENL [(*1*)REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
260 THEN MP_TAC(ISPEC `x':real^3 # real^3` PAIR_SURJECTIVE) THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN UNDISCH_TAC `(x':real^3 # real^3 IN {v:real^3} CROSS ((S:real^3 -> bool) DELETE v INTER ball (v,&4)) /\ x = map_to_nua_kg x'):bool` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_CROSS;IN_SING] THEN REWRITE_TAC[map_to_nua_kg;IN_INTER]
261 THEN REPEAT STRIP_TAC THEN EXISTS_TAC `x'':real^3` THEN EXISTS_TAC `y:real^3` THEN ASM_SIMP_TAC[];(*2*)REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `(x':real^3, y:real^3):real^3 # real^3` THEN ASM_REWRITE_TAC[IN_SING;IN_CROSS;map_to_nua_kg;IN_INTER]]);;
265 let finite_voronoi2=prove(`!(v:real^3)(S:real^3 ->bool). packing S ==> FINITE ({nua_kg (x:real^3) (y:real^3) | y IN (S DELETE v)/\ x= v /\ y IN ball(v, &4)})`,REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM surj_map_to_nua_kg]
266 THEN SUBGOAL_THEN `FINITE ({v:real^3} CROSS (S:real^3 ->bool DELETE v INTER ball (v,&4)))` ASSUME_TAC THENL [(*1*)MATCH_MP_TAC FINITE_CROSS THEN SIMP_TAC[FINITE_SING] THEN MATCH_MP_TAC FINITE_SUBSET
267 THEN EXISTS_TAC `((S:real^3->bool) INTER ball(v:real^3, &4)):real^3 ->bool`
268 THEN REWRITE_TAC[SUBSET_INTER] THEN ASM_MESON_TAC[REAL_ARITH `&0<= &4`;KIUMVTC;SET_RULE `S DELETE v INTER ball (v,&4) SUBSET S /\
269 S DELETE v INTER ball (v,&4) SUBSET ball (v,&4)`];(*2*)ASM_MESON_TAC[FINITE_IMAGE]]);;
272 let real_sub_norm=prove(`!(x:real^3)(y:real^3)(z:real^3). dist (x,z) - dist (y,z)<= dist (x,y)`,
273 REWRITE_TAC[dist] THEN MESON_TAC[VECTOR_ARITH `x:real^3 - y= (x-z) - (y - z)`;REAL_ABS_SUB_NORM;REAL_ABS_LE;REAL_ARITH `a<= b /\ b<= c ==> a<= c`]);;
276 let not_open = prove (`!s:real^N->bool. ~ (open s) <=> ?a x. a IN s /\ (!n. ~(x n IN s)) /\ (x --> a) sequentially`,
277 REWRITE_TAC[OPEN_CLOSED; CLOSED_LIMPT; LIMPT_SEQUENTIAL] THEN
278 REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; IN_DELETE; IN_DIFF; IN_UNIV] THEN
281 let not_open_voronoi1 = prove (`!x y v (w:real^N) (A:real^N -> bool). FINITE A /\ (x --> w) sequentially /\ (!n. dist(x n,v) >= dist(x n,y n)) /\ ~(?N. !n. N < n ==> ~(y n IN A)) ==> ?a. a IN A /\ dist(w,v) >= dist(w,a)`, REPEAT GEN_TAC THEN ASM_CASES_TAC `A:real^N->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN REWRITE_TAC[NOT_EXISTS_THM; NOT_FORALL_THM; NOT_IMP] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[MESON[] `(?a. P a /\ Q a) <=> ~(!a. P a ==> ~Q a)`] THEN REWRITE_TAC[real_ge; REAL_NOT_LE] THEN DISCH_TAC THEN SUBGOAL_THEN `?e. &0 < e /\ !a. a IN A ==> dist(w:real^N,v) + e <= dist(w,a)` STRIP_ASSUME_TAC THENL [EXISTS_TAC `inf(IMAGE (\a:real^N. dist(w,a) - dist(w,v)) A)` THEN ASM_REWRITE_TAC[REAL_ARITH `x + inf s <= y <=> inf s <= y - x`] THEN ASM_SIMP_TAC[REAL_LT_INF_FINITE; REAL_INF_LE_FINITE; FINITE_IMAGE;IMAGE_EQ_EMPTY] THEN ASM_REWRITE_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; REAL_SUB_LT] THEN MESON_TAC[REAL_LE_REFL]; FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY]) THEN DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN DISCH_THEN(X_CHOOSE_THEN `N:num` (LABEL_TAC "*")) THEN FIRST_X_ASSUM(X_CHOOSE_THEN `n:num` MP_TAC o SPEC `N:num`) THEN STRIP_TAC THEN REMOVE_THEN "*" (MP_TAC o SPEC `n:num`) THEN FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `(y:num->real^N) n`)) THEN ASM_SIMP_TAC[LT_IMP_LE] THEN NORM_ARITH_TAC]);;
285 let not_open_voronoi2 = prove (`!x v w:real^N.(x --> w) sequentially /\(?N. !n. N < n ==> &2 <= dist(x n, v))==> &2 <= dist(w,v)`, REWRITE_TAC[dist] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`sequentially`; `\n. (x:num->real^N) n - v`; `w - v:real^N`; `&2`] LIM_NORM_LBOUND) THEN ASM_SIMP_TAC[LIM_SUB; LIM_CONST; TRIVIAL_LIMIT_SEQUENTIALLY] THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN EXISTS_TAC `N + 1` THEN ASM_REWRITE_TAC[ARITH_RULE `N + 1 <= n <=> N < n`]);;
288 let not_in_voronoi=prove( `!(x:real^3)(v:real^3)(S:real^3 -> bool). ~ (x IN voronoi_open S v) <=> ?y. y IN S /\ ~ (y = v) /\ dist (x,y)<= dist (x,v)`,
289 REWRITE_TAC[voronoi_open;IN_ELIM_THM] THEN REWRITE_TAC[NOT_FORALL_THM] THEN REWRITE_TAC[NOT_IMP] THEN MESON_TAC[SET_RULE ` y IN S <=> S y`;REAL_ARITH `~ (a< b) <=> b<= a`]);;
291 let not_open_voronoi3=prove( `!(v:real^3)(S:real^3 -> bool). ~ (open (voronoi_open S v)) ==> ?x a y. a IN (voronoi_open S v) /\ (!n. ~ (x n IN (voronoi_open S v))) /\ (x --> a) sequentially /\ (!n. (y n IN S) /\ ~ (y n = v) /\ dist (x n, y n)<= dist (x n, v))`,
292 REWRITE_TAC[not_open] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
293 THEN EXISTS_TAC `x:num -> real^3` THEN EXISTS_TAC `a:real^3` THEN ASM_SIMP_TAC[] THEN DISJ_CASES_TAC (MESON[] `( ?y. (!n. (y:num->real^3) n IN (S:real^3 ->bool) /\ ~(y n = v) /\ dist (x n,y n) <= dist (x n,v))) \/ ~ (?y. !n. (y n IN S /\ ~(y n = v) /\ dist (x n,y n) <= dist (x n,v)))`) THENL [(*1*)ASM_MESON_TAC[];(*2*)UNDISCH_TAC `~(?y. (!n. (y:num->real^3) n IN (S:real^3 ->bool) /\ ~(y n = v) /\ dist (x n,y n) <= dist (x n,v))):bool` THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM] THEN UNDISCH_TAC `((a:real^3) IN voronoi_open (S:real^3->bool) (v:real^3) /\ (!n. ~((x:num ->real^3) n IN voronoi_open S v)) /\ (x --> a) sequentially):bool` THEN REWRITE_TAC[not_in_voronoi] THEN MESON_TAC[]]);;
296 let voronoi_in_ball=prove(`!(x:real^3)(v:real^3)(S:real^3 -> bool).packing S /\ saturated S /\( x IN voronoi_open S v) ==> dist(x,v)< &2`,REWRITE_TAC[saturated;packing;voronoi_open;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `(!(x:real^3). ?(y:real^3). y IN (S:real^3 ->bool) /\ dist (x,y) < &2):bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:real^3`) THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN SUBGOAL_THEN `(S:real^3->bool) (y:real^3)` MP_TAC
297 THENL [(*1*)ASM_MESON_TAC[SET_RULE `(y:real^3) IN (S:real^3 -> bool) ==> S y`];(*2*)DISCH_TAC THEN UNDISCH_TAC `(!(w:real^3). (S:real^3->bool) w /\ ~(w = v) ==> dist (x:real^3,v) < dist (x,w)):bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `y:real^3`) THEN DISJ_CASES_TAC (MESON[] ` (y:real^3 = v) \/ ~ (y = v)`) THENL [(*2a*)ASM_MESON_TAC[];(*2b*)ASM_SIMP_TAC[]
298 THEN UNDISCH_TAC `((y:real^3) IN (S:real^3->bool) /\ dist (x:real^3,y) < &2):bool` THEN STRIP_TAC THEN ASM_MESON_TAC[REAL_ARITH `a<b /\ b< c ==> a< c`]]]);;
303 (*----------------------------------------------------------------*)
305 (*----------------------------------------------------------------*)
308 let open_voronoi=prove( `!(v:real^3)(S:real^3 -> bool).packing S /\ saturated S ==> open (voronoi_open S v)`,REPEAT STRIP_TAC THEN DISJ_CASES_TAC (MESON[] ` open (voronoi_open (S:real^3 ->bool) (v:real^3)) \/ ~ (open (voronoi_open S v))`) THENL [(*1*)ASM_MESON_TAC[];(*2*)MP_TAC(ISPECL [`v:real^3`;`S:real^3 -> bool`] not_open_voronoi3) THEN ASM_SIMP_TAC[] THEN ONCE_REWRITE_TAC[MESON[] `~ p <=> p ==> F`] THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
309 THEN UNDISCH_TAC `((a:real^3) IN voronoi_open (S:real^3->bool) (v:real^3) /\
310 (!n. ~((x:num ->real^3) n IN voronoi_open S v)) /\
311 (x --> a) sequentially /\
312 (!n. (y:num -> real^3) n IN S /\ ~(y n = v) /\ dist (x n,y n) <= dist (x n,v))):bool` THEN REPEAT STRIP_TAC
313 THEN DISJ_CASES_TAC(MESON[] `(?(N:num). !n. N< n ==> ~((y:num -> real^3) n IN ball(v, &4))) \/ ~ (?N. !n. N< n ==> ~(y n IN ball(v, &4)))`) THENL [(*2a*)UNDISCH_TAC `( (?(N:num). !n. N< n ==> ~((y:num -> real^3) n IN ball(v, &4)))):bool` THEN REWRITE_TAC[ball;IN_ELIM_THM] THEN REWRITE_TAC[REAL_ARITH ` ~ (a:real< b) <=> b<= a`] THEN STRIP_TAC
314 THEN SUBGOAL_THEN `!(n:num). N< n ==> &2 <= dist((x:num -> real^3) n,v)` MP_TAC
315 THENL [(*2a1*)REPEAT STRIP_TAC THEN MP_TAC(MESON[DIST_SYM] `dist ((x:num->real^3) n,(y:num -> real^3) n) <= dist (x n,v:real^3) ==> dist(x n, y n) <= dist (v, x n)`) THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(!(n:num). N < n ==> &4 <= dist (v:real^3,(y:num -> real^3) n)):bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[]
316 THEN MESON_TAC[REAL_ARITH `a:real <= b ==> (a+ b) <= &2* b`; DIST_TRIANGLE;REAL_ARITH `a<= b /\ b<= c ==> a<= c`;DIST_SYM;REAL_ARITH `&4<= &2* a <=> &2<= a`];(*2a2*)DISCH_TAC THEN MP_TAC(MESON[] `(!(n:num). (N:num) < n ==> &2 <= dist ((x:num -> real^3) n,v:real^3)) ==> (? (M:num). (!(n:num). M < n ==> &2 <= dist (x n,v)))`) THEN ASM_SIMP_TAC[] THEN ONCE_REWRITE_TAC[MESON[] `~ p <=> p ==> F`] THEN DISCH_TAC THEN MP_TAC(ISPECL [`x:num ->real^3`;`v:real^3`;`a:real^3`] not_open_voronoi2)
317 THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[REAL_ARITH `~ (a<= b ) <=> b< a`] THEN ASM_MESON_TAC[voronoi_in_ball]];(*2b*)MP_TAC(ISPECL [`x:num ->real^3`;`y:num -> real^3`;`v:real^3`;`a:real^3`;`(((S:real^3 ->bool) INTER ball(v:real^3, &4)) DELETE v):real^3 -> bool`] not_open_voronoi1) THEN ASM_REWRITE_TAC[IN_INTER;REAL_ARITH `a:real >= b <=> b<= a`] THEN REWRITE_TAC[IN_DELETE] THEN ASM_SIMP_TAC[IN_INTER] THEN MP_TAC(ISPECL [`v:real^3`;` &4:real`;`S:real^3 ->bool`] KIUMVTC ) THEN ASM_REWRITE_TAC[REAL_ARITH `&0<= &4`;DELETE_SUBSET;FINITE_SUBSET] THEN DISCH_TAC THEN MP_TAC (MESON[DELETE_SUBSET;FINITE_SUBSET] ` (FINITE ((S:real^3->bool) INTER ball (v:real^3,&4))) ==> (FINITE ((S INTER ball (v,&4)) DELETE v))`) THEN ASM_REWRITE_TAC[]
318 THEN UNDISCH_TAC `((a:real^3) IN voronoi_open (S:real^3 -> bool) (v:real^3)):bool` THEN REWRITE_TAC[voronoi_open;IN_ELIM_THM] THEN REWRITE_TAC[NOT_IMP] THEN SIMP_TAC[NOT_EXISTS_THM] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC ` (!(w:real^3). (S:real^3 ->bool) w /\ ~(w = v) ==> dist (a:real^3,v) < dist (a,w)):bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `a':real^3`) THEN ASM_MESON_TAC[SET_RULE `(a':real^3) IN (S:real^3 -> bool) <=> S a'`;REAL_ARITH ` a:real <= b <=> ~ (b< a)`]]]);;
321 (*----------------------------------------------------------------*)
322 (* Lemma 5.2 [DRUQUFE]About voronoi_open, this is not element *)
323 (*----------------------------------------------------------------*)
326 let DRUQUFE=prove(`!(v:real^3)(S:real^3 -> bool).packing S /\ saturated S ==> convex (voronoi_open S v) /\ bounded (voronoi_open S v) /\ open (voronoi_open S v) /\ measurable ( voronoi_open S v)`,MESON_TAC[convex_voronoi;bound_voronoi;open_voronoi;MEASURABLE_OPEN]);;
328 (*----------------------------------------------------------------*)
329 (* The following is to prove Lemma 5.3 *)
330 (*----------------------------------------------------------------*)
333 let measurable_voronoi=prove(`!(v:real^3)(S:real^3 -> bool).packing S /\ saturated S ==> measurable ( voronoi_open S v)`, MESON_TAC[DRUQUFE]);;
336 let negligible_fun = new_definition `negligible_fun f S = (? (C:real). (&0<= C)/\ ! (r:real) (p:real^3). ( &1 <= r) ==> (sum (S INTER ball(p,r)) f) <= C * (r pow 2))`;;
340 let negligible_fun_p = new_definition `negligible_fun_p f S p = (? (C:real). (&0<= C)/\ ! (r:real). ( &1 <= r) ==> (sum (S INTER ball(p,r)) f) <= C * (r pow 2))`;;
343 let fcc_compatible= new_definition `fcc_compatible f S = (!v. v IN S ==> sqrt( &32) <= measure(voronoi_open S v) + f v)`;;
346 let packing_subset_unions_ball=prove( `! (S:real^3 ->bool) (p:real^3) (r:real). ((UNIONS {ball(v:real^3, &1) | v IN S}) INTER ball(p,r)) SUBSET UNIONS {ball(v:real^3, &1) | v IN (S INTER ball (p,r+ &1))}`,REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET;IN_INTER;UNIONS] THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN EXISTS_TAC `ball(v:real^3, &1):real^3 ->bool` THEN STRIP_TAC THENL [(*1*)EXISTS_TAC `(v):real^3` THEN ASM_SIMP_TAC[] THEN UNDISCH_TAC `(x:real^3 IN u):bool`
347 THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(x IN ball (p:real^3,r)):bool` THEN REWRITE_TAC[ball;IN_ELIM_THM] THEN REWRITE_TAC[dist] THEN REWRITE_TAC[MESON[VECTOR_ARITH `(p:real^3- x) + (x- v)= p - v`] `norm (p:real^3 - v) < r + &1 <=> norm ((p- x) + (x- v))< r+ &1`] THEN MESON_TAC[NORM_SUB;NORM_TRIANGLE;REAL_ARITH `a<d /\ b<c/\ e<= a+ b ==> e< d+ c`]; (*2*)ASM_MESON_TAC[SET_RULE `u = ball(v:real^3, &1):real^3 ->bool /\ x IN u ==> (x:real^3) IN ball (v,&1)`]]);;
350 let measurable_packing_lm1=prove(`! (S:real^3 ->bool) (p:real^3) (r:real). measurable((UNIONS {ball(v:real^3, &1) | v IN S}) INTER ball(p,r))`,let em=CONJUNCT2 INTER_SUBSET in REPEAT GEN_TAC THEN MATCH_MP_TAC (ISPEC `(UNIONS {ball(v:real^3, &1) | v IN S} INTER ball(p,r)):real^3 ->bool` MEASURABLE_OPEN) THEN STRIP_TAC THENL [(*1*)MESON_TAC[BOUNDED_SUBSET;em;BOUNDED_BALL];(*2*)MATCH_MP_TAC OPEN_INTER THEN SIMP_TAC[OPEN_BALL] THEN MATCH_MP_TAC OPEN_UNIONS THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[OPEN_BALL]]);;
353 let map_to_ball=new_definition`map_to_ball (x:real^3)= ball(x, &1)`;;
356 let surj_map_to_ball=prove(`!(S:real^3 ->bool). IMAGE (map_to_ball) S = {ball(x:real^3, &1) | x IN S}`,
357 REWRITE_TAC[IMAGE] THEN REWRITE_TAC[map_to_ball] THEN REPEAT GEN_TAC THEN REWRITE_TAC[map_to_ball;IN_ELIM_THM] THEN ONCE_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN STRIP_TAC
358 THENL [(*1*)REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC;(*2*)REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC]);;
360 let finite_set_packing_in_ball=prove(`! (S:real^3 ->bool) (p:real^3) (r:real). &0<= r /\ packing S ==> FINITE ({ball(v:real^3, &1) | v IN (S INTER ball (p,r+ &1))})`,REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM surj_map_to_ball]
361 THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_MESON_TAC[KIUMVTC;REAL_ARITH `&0<= r ==> &0<= r+ &1`]);;
364 let measurable_packing_lm2=prove(`! (S:real^3 ->bool) (p:real^3) (r:real). &0<= r /\packing S ==> measurable (UNIONS {ball(v:real^3, &1) | v IN (S INTER ball (p,r+ &1))})`, REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURABLE_UNIONS
365 THEN ASM_SIMP_TAC[finite_set_packing_in_ball] THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM;MEASURABLE_BALL] THEN MESON_TAC[MEASURABLE_BALL]);;
368 let measure_ineq_lm53_1=prove( `! (S:real^3 ->bool) (p:real^3) (r:real). &0<= r /\packing S ==> measure ((UNIONS {ball(v:real^3, &1) | v IN S}) INTER ball(p,r)) <= measure(UNIONS {ball(v:real^3, &1) | v IN (S INTER ball (p,r+ &1))})`,MESON_TAC[MEASURE_SUBSET;packing_subset_unions_ball;measurable_packing_lm1;measurable_packing_lm2]);;
370 (*--------------------*)
372 (*--------------------*)
374 let measure_ineq_lm53_2=prove(`! (S:real^3 ->bool) (p:real^3) (r:real). &0<= r /\packing S ==> measure ((UNIONS {ball(v:real^3, &1) | v IN S}) INTER ball(p,r)) <= & (CARD {ball(v:real^3, &1) | v IN (S INTER ball (p,r+ &1))}) * &4*pi/ &3`,
375 REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`] measure_ineq_lm53_1)
376 THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `measure (UNIONS {ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)}) <= &(CARD {ball (v,&1) | v IN S INTER ball (p,r + &1)}) * &4 * pi / &3` (fun th -> MESON_TAC[th;REAL_ARITH `a<=b /\b <= c ==> a<= c`]) THEN MP_TAC(ISPEC `{ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)}` MEASURE_UNIONS_LE)
377 THEN ASM_SIMP_TAC[finite_set_packing_in_ball]
378 THEN SUBGOAL_THEN `(!(s:real^3 ->bool).s IN {ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)} ==> measurable s )` (fun thm -> SIMP_TAC[thm;MEASURABLE_BALL])
379 THENL [(*1*)GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM;MEASURABLE_BALL] THEN MESON_TAC[MEASURABLE_BALL];(*2*)SUBGOAL_THEN `sum {ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)} (\s. measure s)= sum {ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)} (\s. &4 * pi/ &3)` MP_TAC THENL [(*2a*)MATCH_MP_TAC SUM_EQ THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN ASM_REWRITE_TAC[] THEN MESON_TAC[VOLUME_BALL;REAL_ARITH `&0<= &1`;REAL_FIELD `&4* pi/ &3 = &4 / &3 * pi * ( &1 pow 3)`];(*2b*)SIMP_TAC[] THEN SUBGOAL_THEN `sum {ball (v:real^3,&1) | v IN (S:real^3 -> bool) INTER ball (p:real^3,r + &1)} (\s. &4 * pi / &3)= &(CARD {ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)}) * &4 * pi / &3` (fun th -> SIMP_TAC[th]) THEN MP_TAC(ISPECL [`&4 * pi / &3:real`;`{ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)}:(real^3 -> bool) -> bool`] SUM_CONST) THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[finite_set_packing_in_ball;REAL_ARITH `&0<= r ==> &0 <= r+ &1`]]]);;
382 let card_eq_ball_point=prove( `! (S:real^3 ->bool) (p:real^3) (r:real). &0<= r /\packing S ==> CARD {ball(v:real^3, &1) | v IN (S INTER ball (p,r+ &1))}= CARD(S INTER ball (p,r+ &1))`,REPEAT STRIP_TAC THEN SIMP_TAC[GSYM surj_map_to_ball] THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_SIMP_TAC[KIUMVTC;REAL_ARITH `&0<= r ==> &0<= r+ &1`] THEN REPEAT GEN_TAC THEN REWRITE_TAC[map_to_ball;IN_INTER] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `(packing(S:real^3 ->bool)):bool` THEN REWRITE_TAC[packing] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^3`;`y:real^3`]) THEN ASM_REWRITE_TAC[IN_INTER;SET_RULE ` (z:real^3) IN (S:real^3 ->bool) <=> S z`] THEN ASM_SIMP_TAC[SET_RULE ` (z:real^3) IN (S:real^3 ->bool) ==> S z`] THEN FIRST_X_ASSUM(fun th -> MP_TAC(th)) THEN REWRITE_TAC[EXTENSION] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:real^3`) THEN REWRITE_TAC[ball;IN_ELIM_THM;VECTOR_ARITH `x:real^3 - x = vec 0`] THEN REWRITE_TAC[DIST_REFL;REAL_ARITH ` &0< &1`] THEN MESON_TAC[DIST_SYM;REAL_ARITH `a< &1 ==> ~ (&2<= a)`]);;
386 (*------------------------------------------------------------------------------------------------------*)
387 (*Some results involving in set of balls or set of voronoi_open cells (finiteness,being image of another set)*)
388 (*------------------------------------------------------------------------------------------------------*)
391 let voronoi_subset_ball=prove( `!(x:real^3)(v:real^3)(S:real^3 -> bool).packing S /\ saturated S ==> (voronoi_open S v) SUBSET ball(v, &2)`, REWRITE_TAC[SUBSET;ball] THEN REWRITE_TAC[voronoi_in_ball;IN_ELIM_THM] THEN MESON_TAC[voronoi_in_ball;DIST_SYM]);;
394 let all_voronoi_subset_ball=prove(`!(v:real^3)(S:real^3 ->bool)(p:real^3)(r:real). packing S /\ saturated S /\ v IN ball(p, r+ &1) ==> (voronoi_open S v) SUBSET ball(p, r+ &3) `, REPEAT STRIP_TAC THEN MATCH_MP_TAC(SET_RULE `voronoi_open (S:real^3 -> bool) (v:real^3) SUBSET ball(v:real^3, &2) /\ ball(v:real^3, &2 ) SUBSET ball(p:real^3, r+ &3) ==> voronoi_open S v SUBSET ball (p,r + &3)`) THEN ASM_SIMP_TAC[ voronoi_subset_ball] THEN UNDISCH_TAC `((v:real^3) IN ball (p:real^3,r + &1)):bool` THEN REWRITE_TAC[ball;SUBSET;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`p:real^3`;`v:real^3`;`x:real^3`] DIST_TRIANGLE) THEN ASM_MESON_TAC[REAL_ARITH ` a< (r:real) + &1 /\ b< &2 /\ c <= a + b ==> c< r + &3`]);;
397 let unions_voronoi_subset_ball=prove( `!(S:real^3 ->bool)(p:real^3)(r:real). packing S /\ saturated S ==> UNIONS {voronoi_open S v | v IN ball(p, r+ &1)} SUBSET ball(p, r+ &3)`, REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN UNDISCH_TAC `((?(v:real^3). v IN ball (p:real^3,r + &1) /\ u = voronoi_open (S:real^3 ->bool) v) /\ (x:real^3) IN u):bool`
398 THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `(x:real^3 IN u:real^3 ->bool):bool` THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL [`v:real^3`;`S:real^3 ->bool`;`p:real^3`;`r:real`] all_voronoi_subset_ball) THEN ASM_SIMP_TAC[] THEN SET_TAC[]);;
400 let unions_voronoi_center_in_ball_subset_ball=prove( `!(S:real^3 ->bool)(p:real^3)(r:real). packing S /\ saturated S ==> UNIONS {voronoi_open w v | v IN (S INTER ball(p, r+ &1)) /\ w = S} SUBSET ball(p, r+ &3)`,REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM] THEN GEN_TAC THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `(x:real^3 IN u:real^3 ->bool):bool` THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL [`v:real^3`;`S:real^3 ->bool`;`p:real^3`;`r:real`] all_voronoi_subset_ball) THEN ASM_SIMP_TAC[] THEN ASM_SET_TAC[]);;
403 let map_to_voronoi=new_definition`map_to_voronoi ((x:real^3), (S:real^3 -> bool))= voronoi_open S x`;;
406 let surj_map_to_voronoi=prove(`!(M:real^3 ->bool)(S:real^3 ->bool). IMAGE (map_to_voronoi) (M CROSS {S}) = {voronoi_open S v | v IN M}`,REWRITE_TAC[IMAGE] THEN REWRITE_TAC[map_to_voronoi] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_CROSS;map_to_voronoi;IN_ELIM_THM] THEN ONCE_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN STRIP_TAC THENL [(*1*) REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN MP_TAC(ISPEC `x':real^3 # (real^3->bool)` PAIR_SURJECTIVE) THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN UNDISCH_TAC `(x':real^3 # (real^3 -> bool) IN ((M:real^3 ->bool) CROSS {S:real^3 -> bool}) /\ x = map_to_voronoi x'):bool` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_CROSS;IN_SING] THEN REWRITE_TAC[map_to_voronoi;IN_INTER] THEN REPEAT STRIP_TAC THEN EXISTS_TAC `x'':real^3` THEN ASM_SIMP_TAC[];(*2*)REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `(v:real^3, S:real^3->bool):real^3 # (real^3 ->bool)` THEN ASM_REWRITE_TAC[IN_SING;IN_CROSS;map_to_voronoi;IN_INTER]]);;
408 let surj_map_to_voronoi_db=prove( `! (S:real^3 ->bool) (p:real^3) (r:real). IMAGE (map_to_voronoi) ((S INTER ball (p,r + &1)) CROSS {S})= {voronoi_open w v | v IN (S INTER ball (p,r+ &1)) /\ w = S}`, REWRITE_TAC[IMAGE] THEN REWRITE_TAC[map_to_voronoi] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_CROSS;map_to_voronoi;IN_ELIM_THM] THEN ONCE_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN STRIP_TAC THENL [(*1*)REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN MP_TAC(ISPEC `x':real^3 # (real^3->bool)` PAIR_SURJECTIVE) THEN STRIP_TAC THEN UNDISCH_TAC `(x':real^3 # (real^3 -> bool) IN ((S:real^3 ->bool INTER ball (p:real^3,r + &1)) CROSS {S:real^3 -> bool}) /\ x = map_to_voronoi x'):bool` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_CROSS;IN_SING] THEN REWRITE_TAC[map_to_voronoi;IN_INTER] THEN REPEAT STRIP_TAC THEN EXISTS_TAC `y:real^3 ->bool` THEN EXISTS_TAC `x'':real^3` THEN ASM_SIMP_TAC[];(*2*) REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN REPEAT STRIP_TAC THEN EXISTS_TAC `(v, w):real^3 # (real^3 ->bool)` THEN ASM_REWRITE_TAC[IN_SING;IN_CROSS;map_to_voronoi;IN_INTER]]);;
412 let finite_set_voronoi_center_in_ball=prove(`! (S:real^3 ->bool) (p:real^3) (r:real). &0<= r /\ packing S ==> FINITE ({voronoi_open w v | v IN (S INTER ball (p,r+ &1)) /\ w= S})`, REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM surj_map_to_voronoi_db] THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_MESON_TAC[KIUMVTC;FINITE_CROSS;FINITE_SING;REAL_ARITH `&0<= r ==> &0<= r+ &1`]);;
416 let measurable_unions_voronoi=prove(`! (S:real^3 ->bool) (p:real^3) (r:real). &0<= r /\packing S /\ saturated S==> measurable (UNIONS {voronoi_open w v | v IN (S INTER ball (p,r+ &1)) /\ w = S})`, REPEAT STRIP_TAC THEN MATCH_MP_TAC MEASURABLE_UNIONS THEN ASM_SIMP_TAC[finite_set_voronoi_center_in_ball] THEN GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_MESON_TAC[measurable_voronoi]);;
418 let negligible_voronoi=prove( `!(S:real^3 ->bool)(p:real^3)(r:real). (!s t.
419 s IN {voronoi_open w v | v IN S INTER ball (p,r + &1) /\ w = S} /\
420 t IN {voronoi_open w v | v IN S INTER ball (p,r + &1) /\ w = S} /\
422 ==> negligible (s INTER t))`,REPEAT GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC (MESON[NEGLIGIBLE_EMPTY] `(s:real^3->bool) INTER (t:real^3 ->bool) = {} ==> negligible (s INTER t)`) THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN ` ~ (v:real^3 = v')` MP_TAC
423 THENL [(*1*)UNDISCH_TAC `( ~(s:real^3 ->bool = t)):bool` THEN REWRITE_TAC[MESON[] ` ~ p ==> ~q <=> q ==> p`] THEN ASM_MESON_TAC[];(*2*)DISCH_TAC THEN ASM_CASES_TAC `?(x:real^3). x IN (voronoi_open (S:real^3 ->bool) (v:real^3) INTER voronoi_open S (v':real^3))` THEN ASM_REWRITE_TAC[SET_RULE `(B:real^3 -> bool)= {} <=> ~ (?(x:real^3). x IN B)`] THEN FIRST_X_ASSUM CHOOSE_TAC THEN UNDISCH_TAC `((x:real^3) IN (voronoi_open (S:real^3 ->bool) (v:real^3) INTER voronoi_open S (v':real^3))):bool` THEN REWRITE_TAC[voronoi_open] THEN REWRITE_TAC[IN_INTER;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `v:real^3`) THEN FIRST_X_ASSUM(MP_TAC o SPEC `v':real^3`) THEN ASM_SIMP_TAC[MESON[] `e=f <=> f=e`;SET_RULE `(v':real^3) IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1) ==> S v'`] THEN MP_TAC(SET_RULE `(v':real^3) IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1) ==> S v'`) THEN ASM_SIMP_TAC[] THEN MP_TAC(SET_RULE `(v:real^3) IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1) ==> S v`) THEN ASM_SIMP_TAC[] THEN REAL_ARITH_TAC]);;
425 let inj_map_to_voronoi=prove( `!(S:real^3 ->bool)(p:real^3)(r:real) (x:real^3 # (real^3 -> bool)) (y:real^3 # (real^3 -> bool)).
426 x IN ((S INTER ball (p,r + &1)) CROSS {S}) /\
427 y IN (S INTER ball (p,r + &1)) CROSS {S} /\
428 map_to_voronoi x = map_to_voronoi y
429 ==> x = y`,REPEAT GEN_TAC THEN MP_TAC(ISPEC `x:real^3 # (real^3->bool)` PAIR_SURJECTIVE) THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN ASM_SIMP_TAC[] THEN MP_TAC(ISPEC `y:real^3 # (real^3->bool)` PAIR_SURJECTIVE) THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_CROSS;IN_SING] THEN SIMP_TAC[map_to_voronoi]
430 THEN REWRITE_TAC[PAIR_EQ] THEN REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `(voronoi_open (y':real^3->bool) (x':real^3) = voronoi_open (y'':real^3->bool) (x'':real^3)):bool` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
431 SUBGOAL_THEN `x':real^3 IN voronoi_open (S:real^3 ->bool) x'` MP_TAC THENL [(*1*)REWRITE_TAC[voronoi_open;IN_ELIM_THM]
432 THEN REWRITE_TAC[DIST_REFL] THEN REWRITE_TAC[GSYM DIST_NZ] THEN MESON_TAC[];(*2*)ASM_REWRITE_TAC[] THEN
433 REWRITE_TAC[voronoi_open;IN_ELIM_THM] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `x':real^3`) THEN ASM_SIMP_TAC[DIST_REFL;SET_RULE `(x':real^3) IN (S:real^3 ->bool) ==> S x'`] THEN REWRITE_TAC[REAL_ARITH `dist(x':real^3,x'':real^3) < &0 <=> ~ (&0<= dist (x',x''))`] THEN MESON_TAC[DIST_POS_LE]]);;
435 let measure_unions_sum_voronoi = prove
436 (`!(S:real^3 ->bool)(p:real^3)(r:real).
437 &0 <= r/\ packing S /\ saturated S
438 ==> measure(UNIONS { voronoi_open w v |
439 v IN (S INTER ball(p, r+ &1)) /\ w = S}) =
440 sum (S INTER ball(p, r+ &1)) (\v. measure (voronoi_open S v))`,
441 REPEAT STRIP_TAC THEN
442 MP_TAC(ISPECL [`\s:real^3->bool. measure s`;
444 v IN (S:real^3 ->bool INTER ball(p:real^3, r+ &1)) /\ w = S}`]
445 MEASURE_NEGLIGIBLE_UNIONS) THEN REWRITE_TAC[negligible_voronoi] THEN
446 ASM_SIMP_TAC[finite_set_voronoi_center_in_ball;IN_ELIM_THM;
447 measurable_voronoi;HAS_MEASURE_MEASURE] THEN ANTS_TAC THENL
448 [MP_TAC(MESON[HAS_MEASURE_MEASURE;measurable_voronoi]
449 `&0 <= r/\ packing (S:real^3 ->bool) /\ saturated S
450 ==> (!(s:real^3 ->bool). (?(v:real^3) (w:real^3->bool).
451 (v IN S INTER ball (p:real^3,r + &1) /\ w = S) /\
452 s = voronoi_open w v) ==> s has_measure (measure s))`) THEN
455 DISCH_THEN SUBST1_TAC THEN
456 REPEAT DISCH_TAC THEN
457 REWRITE_TAC[GSYM surj_map_to_voronoi_db] THEN MP_TAC(ISPECL
458 [`map_to_voronoi:real^3#(real^3->bool)->real^3->bool`;
459 `(\s:real^3->bool. measure s):(real^3-> bool) -> real`;
460 `(((S:real^3 ->bool) INTER ball (p:real^3,r + &1)) CROSS {S})
461 :real^3#(real^3->bool)->bool`] SUM_IMAGE) THEN
462 REWRITE_TAC[inj_map_to_voronoi] THEN SIMP_TAC[] THEN DISCH_TAC THEN
463 MATCH_MP_TAC SUM_EQ_GENERAL THEN
464 EXISTS_TAC `FST:real^3# (real^3 ->bool) -> real^3`
465 THEN REPEAT STRIP_TAC THENL [(*1*)REWRITE_TAC[EXISTS_UNIQUE] THEN
466 EXISTS_TAC `(y:real^3,S:real^3->bool):real^3 # (real^3 ->bool)` THEN
467 ASM_REWRITE_TAC[IN_CROSS;IN_SING;FST] THEN GEN_TAC THEN
468 MP_TAC(ISPEC `y':real^3 # (real^3 ->bool)` PAIR_SURJECTIVE) THEN
469 DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN
470 ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_CROSS;IN_SING] THEN
473 UNDISCH_TAC `(x:real^3 # (real^3 ->bool) IN (S:real^3 ->bool INTER
474 ball (p:real^3,r + &1)) CROSS {S}):bool` THEN
475 MP_TAC(ISPEC `x:real^3 # (real^3 ->bool)` PAIR_SURJECTIVE) THEN
476 DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN
477 ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_CROSS] THEN MESON_TAC[];
479 MP_TAC(ISPEC `x:real^3 # (real^3 ->bool)` PAIR_SURJECTIVE) THEN
480 DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN
481 FIRST_X_ASSUM CHOOSE_TAC THEN ASM_REWRITE_TAC[] THEN
482 REWRITE_TAC[o_THM] THEN ASM_MESON_TAC[map_to_voronoi;IN_CROSS;IN_SING]]]);;
484 (*------------------------*)
486 (*------------------------*)
488 let sum_measure_voronoi_le_ball=prove( `!(S:real^3 ->bool)(p:real^3)(r:real). &0<= r/\ packing S /\ saturated S ==> sum (S INTER ball (p,r + &1)) (\v. measure (voronoi_open S v)) <= measure (ball(p,r+ &3))`, REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GSYM measure_unions_sum_voronoi] THEN ASM_MESON_TAC[MEASURE_SUBSET;measurable_unions_voronoi; unions_voronoi_center_in_ball_subset_ball;MEASURABLE_BALL;REAL_ARITH `&0<= r ==> &0<= r+ &3`]);;
490 (*------------------------*)
492 (*------------------------*)
494 let ineq_lm5_3_step3=prove(`!(S:real^3 ->bool)(p:real^3)(r:real)(A:real^3 ->real). &0<= r/\ packing S /\ saturated S /\ (fcc_compatible A S)==> sqrt( &32) * &(CARD(S INTER ball (p,r + &1))) <= sum (S INTER ball (p,r + &1)) (\v. (A v + measure (voronoi_open S v)))`,REWRITE_TAC[fcc_compatible] THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN ` sum ((S:real^3 ->bool) INTER ball (p:real^3,r + &1)) (\v. sqrt( &32))<= sum (S INTER ball (p,r + &1)) (\v. A v + measure (voronoi_open S v)) ` MP_TAC
495 THENL [(*1*)MATCH_MP_TAC SUM_LE THEN ASM_SIMP_TAC[KIUMVTC;REAL_ARITH `&0<= r ==> &0<= r + &1`] THEN ASM_MESON_TAC[fcc_compatible;REAL_ARITH `a+b= b+a`;SET_RULE `x IN A INTER B ==> x IN A`];(*2*)ASM_SIMP_TAC[SUM_CONST;KIUMVTC;REAL_ARITH `&0<= r ==> &0<= r + &1`] THEN REAL_ARITH_TAC]);;
498 (*------------------------*)
500 (*------------------------*)
503 let ineq_lm5_3_step4=prove(
504 `!(c:real). (&0<= c) ==> ? (c':real).
505 !(r:real). (&1 <=r) ==>
506 ( pi/ sqrt( &18)*( &1+ &3/ r) pow 3 + c*((r+ &1) pow 2)/ (r pow 3 * sqrt( &32)) <= pi/ sqrt( &18) + c'/r)`,
507 REPEAT STRIP_TAC THEN
508 EXISTS_TAC `((pi/ sqrt( &18))* ( &9+ &27+ &27) + c* (&1/ sqrt( &32) + &2/ sqrt( &32)+ &1/ sqrt( &32))):real` THEN
509 REPEAT STRIP_TAC THEN
510 ONCE_REWRITE_TAC[REAL_ARITH `a:real<= b <=> &0<= b-a`] THEN ASM_SIMP_TAC[REAL_FIELD ` &1<= r==>(pi / sqrt (&18) +
511 (pi / sqrt (&18) * (&9 + &27 + &27) +
512 (c:real) * (&1 / sqrt (&32) + &2 / sqrt (&32) + &1 / sqrt (&32))) /
514 (pi / sqrt (&18) * ((&1 + &3 / r) pow 3) +
515 c * (r + &1) pow 2 / (r pow 3 * sqrt (&32))) =( (&1/ r) * pi/ sqrt( &18)) * ( (&27/r)*( r- &1)+ ( &27/(r pow 2)) * (r pow 2 - &1)) + ( (&1/ r)*c)* (( &2/(r* sqrt( &32)))*(r- &1) + (&1/ (r pow 2 * sqrt( &32))) * (r pow 2 - &1))`]
516 THEN REWRITE_TAC[REAL_FIELD `(&1 / (r:real) * pi / sqrt (&18)) *
517 (&27 / r * (r - &1) + &27 / r pow 2 * (r pow 2 - &1)) +
518 (&1 / r * (c:real)) *
519 (&2 / (r * sqrt (&32)) * (r - &1) +
520 &1 / (r pow 2 * sqrt (&32)) * (r pow 2 - &1))= (&1 / r * pi / sqrt (&18)) *
521 (&27 / r * (r - &1) + (&27 / r pow 2) * (r - &1) *(r + &1)) +
523 (&2 / (r * sqrt (&32)) * (r - &1) +
524 &1 / (r pow 2 * sqrt (&32)) * (r - &1)*(r + &1))`] THEN MP_TAC(PI_POS_LE) THEN MP_TAC(REAL_ARITH `&1<= r:real ==> &0<= r- &1`) THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH `&1<= r:real ==> &0<= r+ &1`) THEN ASM_REWRITE_TAC[] THEN MP_TAC(MESON[REAL_ARITH `&0<= &18 /\ &0<= &32`;SQRT_POS_LE] `&0<= sqrt( &18) /\ &0<= sqrt( &32)`) THEN MP_TAC(REAL_ARITH `&1<= r:real ==> &0<=r `) THEN ASM_REWRITE_TAC[] THEN MP_TAC(SPEC `r:real` REAL_LE_SQUARE) THEN REWRITE_TAC[REAL_ARITH ` r * r:real = r pow 2`] THEN MP_TAC(REAL_ARITH ` &0<= &1 /\ &0<= &27 /\ &0<= &2`) THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC (SPECL [`(&1 / (r:real) * pi / sqrt (&18)) *
525 (&27 / r * (r - &1) + &27 / r pow 2 * (r - &1) * (r + &1)):real`;`(&1 / r * (c:real)) *
526 (&2 / (r * sqrt (&32)) * (r - &1) +
527 &1 / (r pow 2 * sqrt (&32)) * (r - &1) * (r + &1)):real`] REAL_LE_ADD) THEN MP_TAC(MESON[REAL_LE_DIV;REAL_ARITH `&0<= &1`;REAL_LE_MUL;REAL_LE_ADD;REAL_ARITH ` a:real <= b /\ b<= c ==> a<= c`] `&0<= r /\ &0 <= pi /\ &0 <= sqrt (&18) ==> &0<= &1 / r * pi / sqrt (&18)`) THEN ASM_SIMP_TAC[] THEN MP_TAC(MESON[REAL_LE_DIV;REAL_ARITH `&0<= &1/\ &0<= &27`;REAL_ARITH `r- &1<= r+ &1`;REAL_LE_MUL;REAL_LE_ADD;REAL_ARITH ` a:real <= b /\ b<= c ==> a<= c`] `&0<= r pow 2 /\ &0<= r/\ &0<= r- &1 /\ &0 <= pi /\ &0 <= sqrt (&18) ==> &0<= (&27 / r * (r - &1) + &27 / r pow 2 * (r - &1) * (r + &1))`) THEN ASM_SIMP_TAC[REAL_LE_MUL] THEN REPEAT DISCH_TAC THEN MP_TAC(MESON[REAL_LE_DIV;REAL_ARITH `&0<= &1`;REAL_LE_MUL;REAL_LE_ADD;REAL_ARITH ` a:real <= b /\ b<= c ==> a<= c`] `&0<= r /\ &0 <= pi /\ &0 <= c ==> &0<= &1 / r * (c:real)`) THEN ASM_SIMP_TAC[] THEN DISCH_TAC
528 THEN MATCH_MP_TAC(SPECL [`&1 / (r:real) * (c:real):real`;`&2 / (r * sqrt (&32)) * (r - &1) +
529 &1 / (r pow 2 * sqrt (&32)) * (r - &1) * (r + &1):real`] REAL_LE_MUL) THEN ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_MUL;REAL_LE_ADD;REAL_ARITH ` a<= b /\ b<= c ==> a<= c`] THEN MATCH_MP_TAC(SPECL [`&2 / (r * sqrt (&32)) * (r - &1):real`;`&1 / (r pow 2 * sqrt (&32)) * (r - &1) * (r + &1):real`] REAL_LE_ADD) THEN ASM_MESON_TAC[REAL_LE_DIV;REAL_LE_MUL;REAL_LE_ADD;REAL_ARITH ` a:real <= b /\ b<= c ==> a<= c`]);;
531 (*-----------------------------------------------------------------*)
532 (* Lemma 5.3 If exist fcc_compatible,negligible fun then OK *)
533 (*-----------------------------------------------------------------*)
535 (* thales modified below to make the dependence on p explicit. *)
538 `!(S:real^3 ->bool) (p:real^3). packing S /\ saturated S /\ (? (A:real^3 ->real).(fcc_compatible A S)/\ (negligible_fun_p A S p)) ==> ? (c:real). (!(r:real). &1<= r ==> measure ((UNIONS {ball(v:real^3, &1) | v IN S}) INTER ball(p,r))/ measure (ball(p, r))<= pi/ sqrt( &18) + c/ r)`,
540 REWRITE_TAC[negligible_fun_p;fcc_compatible] THEN
541 REPEAT STRIP_TAC THEN
542 MP_TAC(SPEC `C:real` ineq_lm5_3_step4) THEN
544 REPEAT STRIP_TAC THEN
545 EXISTS_TAC `c':real` THEN
546 REPEAT STRIP_TAC THEN
547 FIRST_X_ASSUM(MP_TAC o SPEC `r:real`) THEN
549 SUBGOAL_THEN `measure (UNIONS {ball (v,&1) | v IN (S:real^3 ->bool)} INTER ball (p:real^3,r:real)) /
550 measure (ball (p,r))<= pi / sqrt (&18) * (&1 + &3 / r) pow 3 +
551 (C:real) * (r + &1) pow 2 / (r pow 3 * sqrt (&32))` (fun th -> ASM_MESON_TAC[th;REAL_ARITH `a<=b/\ b<= c ==> a<= c`]) THEN
552 MP_TAC(SPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`] measure_ineq_lm53_2) THEN
553 ASM_SIMP_TAC[REAL_ARITH `&1<= r ==> &0<= r`] THEN
555 MP_TAC(SPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`;`A:real^3 ->real`] ineq_lm5_3_step3) THEN
556 ASM_SIMP_TAC[REAL_ARITH `&1<= r ==> &0<= r`;fcc_compatible] THEN
557 ASM_SIMP_TAC[SUM_ADD;KIUMVTC;REAL_ARITH `&1<=r ==> &0<= r + &1`;] THEN
558 FIRST_X_ASSUM(MP_TAC o SPECL [`r+ &1:real`]) THEN
559 ASM_SIMP_TAC[REAL_ARITH `&1<=r ==> &1<= r+ &1`] THEN
560 MP_TAC(SPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`] sum_measure_voronoi_le_ball) THEN
561 ASM_SIMP_TAC[REAL_ARITH `&1<= r ==> &0<= r`] THEN
562 REPEAT DISCH_TAC THEN
563 MP_TAC(REAL_ARITH `sum ((S:real^3 ->bool) INTER ball (p:real^3,r + &1)) (\v:real^3. measure (voronoi_open S v)) <=
564 measure (ball (p,r + &3))
565 /\ sum (S INTER ball (p,r + &1)) (A:real^3 ->real) <= (C:real) * (r + &1) pow 2 /\ sqrt (&32) * &(CARD (S INTER ball (p,r + &1))) <=
566 sum (S INTER ball (p,r + &1)) A +
567 sum (S INTER ball (p,r + &1)) (\v:real^3. measure (voronoi_open S v))
568 ==> sqrt (&32) * &(CARD (S INTER ball (p,r + &1))) <= C * (r + &1) pow 2 + measure (ball (p,r + &3))`) THEN
571 ASM_SIMP_TAC[VOLUME_BALL;REAL_ARITH `&1<= r ==> &0<= r+ &3`] THEN
572 ASM_SIMP_TAC[REAL_FIELD `&1<= r ==> &4 / &3 * pi * (r + &3) pow 3 = ( &1 + &3/ r) pow 3 * (&4 / &3 * pi * r pow 3)`] THEN
573 ASM_SIMP_TAC[GSYM (ISPECL [`p:real^3`;`r:real`] VOLUME_BALL);REAL_ARITH `&1<= r ==> &0<= r`] THEN
574 ONCE_REWRITE_TAC[REAL_ARITH `sqrt (&32) * &(CARD ((S:real^3 -> bool) INTER ball (p:real^3,r + &1))) = &(CARD (S INTER ball (p,r + &1))) * sqrt (&32)`] THEN
575 SIMP_TAC[GSYM REAL_LE_RDIV_EQ;MESON[SQRT_POS_LT;REAL_ARITH `&0< &32`] `&0< sqrt( &32)`] THEN
577 SUBGOAL_THEN `measure (UNIONS {ball (v,&1) | v IN (S:real^3->bool)} INTER ball (p:real^3,r:real))<= ((C:real) * (r + &1) pow 2 + (&1 + &3 / r) pow 3 * measure (ball (p,r))) /
578 sqrt (&32) * &4 * pi / &3` MP_TAC THENL [(*1*)UNDISCH_TAC `(measure (UNIONS {ball (v,&1) | v IN (S:real^3 ->bool)} INTER ball (p:real^3,r:real)) <=
579 &(CARD {ball (v,&1) | v IN S INTER ball (p,r + &1)}) * &4 * pi / &3):bool` THEN
580 SUBGOAL_THEN `&(CARD {ball (v,&1) | v IN (S:real^3 ->bool) INTER ball (p:real^3,r + &1)}) * &4 * pi / &3 <= ((C:real) * (r + &1) pow 2 + (&1 + &3 / r) pow 3 * measure (ball (p,r))) /
583 pi / &3` (fun th -> MESON_TAC[th;REAL_ARITH `a<= b /\ b<= c ==> a<= c`]) THEN
584 ASM_MESON_TAC[card_eq_ball_point;REAL_ARITH `&1<= r ==> &0<= r`;REAL_OF_NUM_EQ;MESON[PI_POS;REAL_ARITH `&0< &4 /\ &0< &3`;REAL_LT_MUL;REAL_LT_DIV] `&0< &4 * pi/ &3`;REAL_ARITH `a<= b /\ b<= c ==> a<= c`;REAL_LE_RMUL_EQ];(*2*)ASM_SIMP_TAC[VOLUME_BALL;REAL_ARITH `&1<= r ==> &0<= r`]
586 MP_TAC(MESON[REAL_ARITH `&1<= r ==> &0< r`;PI_POS;REAL_ARITH `&0< &4 /\ &0< &3`;REAL_LT_MUL;REAL_LT_DIV;REAL_POW_LT] `&1<= r ==> &0< &4/ &3 *pi * r pow 3`) THEN
588 SIMP_TAC[REAL_LE_LDIV_EQ] THEN
589 SUBGOAL_THEN `((C:real) * (r + &1) pow 2 + (&1 + &3 / r) pow 3 * &4 / &3 * pi * r pow 3) /
592 pi / &3= (pi / sqrt (&18) * (&1 + &3 / r) pow 3 +
593 C * (r + &1) pow 2 / (r pow 3 * sqrt (&32))) *
596 r pow 3` (fun th -> MESON_TAC[th]) THEN
597 REWRITE_TAC[REAL_FIELD `((a:real) + b)/ c * d= ((a + b)*d )/c /\ ((x:real) + y ) * z = x *z + y* z`] THEN
598 ASM_SIMP_TAC[REAL_EQ_LDIV_EQ;MESON[SQRT_POS_LT;REAL_ARITH `&0< &32`] `&0< sqrt( &32)`;REAL_FIELD `((x:real) + y ) * z = x *z + y* z`] THEN
599 SUBGOAL_THEN `(C * (r + &1) pow 2) * &4 * pi / &3 = ((C * (r + &1) pow 2 / (r pow 3 * sqrt (&32))) * &4 / &3 * pi * r pow 3) *
600 sqrt (&32) /\ ((&1 + &3 / r) pow 3 * &4 / &3 * pi * r pow 3) * &4 * pi / &3 = ((pi / sqrt (&18) * (&1 + &3 / r) pow 3) * &4 / &3 * pi * r pow 3) *
601 sqrt (&32)` (fun th -> MESON_TAC[th;REAL_ARITH ` a= b /\ d= c ==> a+ d= c+ b`]) THEN
604 [(*2a*)REWRITE_TAC[REAL_FIELD `((C * (r + &1) pow 2 / (r pow 3 * sqrt (&32))) * &4 / &3 * pi * r pow 3) *
605 sqrt (&32)= ((C * (r + &1) pow 2 / (r pow 3 * sqrt (&32)))*(r pow 3 * sqrt (&32)))* (&4 / &3 * pi)`]
607 MATCH_MP_TAC (REAL_FIELD `~ (r pow 3 * sqrt (&32) = &0)==>(C * (r + &1) pow 2) * &4 * pi / &3= ((C * (r + &1) pow 2 / (r pow 3 * sqrt (&32)))*(r pow 3 * sqrt (&32)))* (&4 / &3 * pi)`) THEN
608 ASM_MESON_TAC[REAL_DIV_RMUL;REAL_MUL_ASSOC;REAL_MUL_SYM;REAL_ENTIRE;MESON[REAL_POW_NZ;REAL_ARITH `&1<= r ==> ~ (r= &0)`] `&1<=r ==> ~ (r pow 3 = &0)`;MESON[REAL_ARITH `&0< x ==> ~ (x= &0)`;SQRT_POS_LT;REAL_ARITH `&0< &32`] ` ~ (sqrt( &32) = &0)`];(*2b*)REWRITE_TAC[REAL_FIELD `((pi / sqrt (&18) * (&1 + &3 / r) pow 3) * &4 / &3 * pi * r pow 3) *
609 sqrt (&32)= ((pi* sqrt( &32) / sqrt (&18)) * (&1 + &3 / r) pow 3) * &4 / &3 * pi * r pow 3`]
611 SUBGOAL_THEN `sqrt (&32) / sqrt (&18)= &4/ &3` (fun th -> REWRITE_TAC[th;REAL_FIELD `((&1 + &3 / r) pow 3 * &4 / &3 * pi * r pow 3) * &4 * pi / &3 = ((pi * &4/ &3) * (&1 + &3 / r) pow 3) * &4 / &3 * pi * r pow 3`]) THEN
612 ONCE_REWRITE_TAC[REAL_ARITH ` &32= &4 pow 2 * &2 /\ &18= &3 pow 2 * &2`] THEN
613 SIMP_TAC[SQRT_MUL;REAL_ARITH ` &0<= &2 /\ &0<= &3 pow 2 /\ &0<= &4 pow 2`;POW_2_SQRT;REAL_ARITH `&0<= &3 /\ &0<= &4`] THEN
614 MATCH_MP_TAC(REAL_FIELD `~ (sqrt( &2) = &0) ==> (&4 * sqrt (&2)) / (&3 * sqrt (&2)) = &4 / &3`) THEN
615 MESON_TAC[REAL_ARITH `&0< x ==> ~ (x= &0)`;MESON[SQRT_POS_LT;REAL_ARITH `&0< &2`] ` &0< sqrt ( &2)`]]]);;
618 (*-------------------------------------------------------------------*)