(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Packing *)
(* Author: Nguyen Tat Thang *)
(* Date: 2010-02-09 *)
(* ========================================================================== *)
module type Pack1_type = sig
end;;
flyspeck_needs "volume/vol1.hl";;
module Pack1 (* : Pack1_type *) = struct
(* *)
let int_ball = Vol1.int_ball;;
let hinhcau_ball = Vol1.hinhcau_ball;;
let finite_int_ball = Vol1.finite_int_ball;;
let FINITE_IMAGE_INJ = Vol1.FINITE_IMAGE_INJ;;
let ASM_SET_TAC l =
(TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;
let bound_square=prove( `!(a:real)(b:real)(c:real). (a<=b /\ b<=c) ==> b pow 2 <= max ( a pow 2) (c pow 2)`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH `&0<= b \/ b< &0`)
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`]);;
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`]
THEN REWRITE_TAC[REAL_FIELD `(a- b) pow 2 = (a-b) * (a-b)`;
REAL_LE_SQUARE]);;
let bdt_emveque=prove(`!(r:real). &0 <= &8* (r pow 2) + &6`,
GEN_TAC
THEN MP_TAC(MESON[
REAL_LE_SQUARE; REAL_FIELD `r pow 2= r * r`] `&0<= r pow 2`) THEN
DISCH_TAC THEN MP_TAC(MESON[
REAL_LE_MUL;REAL_ARITH `&0<= &8`] `&0<= r pow 2 ==> &0<= &8* (r pow 2)`)
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let bp_bdt=prove( `!(a:real)(b:real). (&0<= a /\ &0<= b) ==> (a< b <=> a pow 2 < b pow 2)`,
REPEAT GEN_TAC
THEN REWRITE_TAC[GSYM
REAL_ABS_REFL] THEN ONCE_REWRITE_TAC[MESON[] `x:real = y<=> y=x`] THEN STRIP_TAC
THEN ASM_MESON_TAC[
REAL_LT_SQUARE_ABS]);;
let bdt_emnguchua=prove( `!(k:real). floor (&2* k)* floor( &2*k)<= &2*( &4* (k pow 2) + &1)`,
GEN_TAC THEN MP_TAC(SPEC ` &2*k:real`
FLOOR) THEN REWRITE_TAC[REAL_ARITH `a:real < b+ &1 <=> a- &1 < b`]
THEN STRIP_TAC THEN MP_TAC(SPECL [`&2 * k - &1:real`;`floor (&2 * k):real`;`&2 * k` ]
bound_square)
THEN ASM_SIMP_TAC[REAL_ARITH `a:real < b ==> a<= b`]
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)`)
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`;
REAL_ARITH ` &1= ( -- &1) pow 2`]
THEN ONCE_REWRITE_TAC[REAL_ARITH `&2 * ((&2 * k) pow 2 + &1)= &2 * ((&2 * k) pow 2 + ( -- &1) pow 2)`]
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`]
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`]
THEN ONCE_REWRITE_TAC[REAL_FIELD `(&8 * k pow 2 + &2) - &4 * k pow 2= &4 * k pow 2 + &2`]
THEN MP_TAC(MESON[
REAL_LE_SQUARE; REAL_FIELD `k pow 2 = k * k`] `&0<= k pow 2`) THEN
DISCH_TAC THEN MP_TAC(MESON[
REAL_LE_MUL;REAL_ARITH `&0<= &4`] `&0<= k pow 2 ==> &0<= &4* (k pow 2)`)
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let map3_define=prove(`!(v:real^3)(p:real^3)(r:real). &0<=r /\ v
IN ball(p,r)
==> map3 p v
IN ball(
vec 0,
sqrt(&8* (r pow 2) + &6))`,
REPEAT GEN_TAC THEN REWRITE_TAC[
ball;
IN_ELIM_THM]
THEN REWRITE_TAC[
dist;VECTOR_ARITH `
vec 0 - map3 (p:real^3) v = -- map3 p v`;
NORM_NEG]
THEN MP_TAC (SPEC `(&8* (r pow 2) + &6):real`
SQRT_POS_LE)
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`]
THEN DISCH_TAC THEN ASM_SIMP_TAC[
bp_bdt] THEN SIMP_TAC[
NORM_POW_2;
DOT_3] 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`]
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)
THEN MP_TAC(SPEC `((p:real^3)$3 - (v:real^3)$3):real`
bdt_emnguchua)
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) +
&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) +
&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
==> q<
sqrt (&8 * r pow 2 + &6) pow 2`)
THEN ASM_SIMP_TAC[REAL_ARITH `floor (&2 * ((p:real^3)$3 - (v:real^3)$3)) * floor (&2 * (p$3 - v$3)):real <=
&2 * (&4 * (p$3 - v$3) pow 2 + &1) /\ floor (&2 * (p$2 - v$2)) * floor (&2 * (p$2 - v$2)) <=
&2 * (&4 * (p$2 - v$2) pow 2 + &1) /\ floor (&2 * (p$1 - v$1)) * floor (&2 * (p$1 - v$1)) <=
&2 * (&4 * (p$1 - v$1) pow 2 + &1) ==> floor (&2 * (p$1 - v$1)) * floor (&2 * (p$1 - v$1)) +
floor (&2 * (p$2 - v$2)) * floor (&2 * (p$2 - v$2)) +
floor (&2 * (p$3 - v$3)) * floor (&2 * (p$3 - v$3)) <=
&2 * (&4 * (p$1 - v$1) pow 2 + &1) +
&2 * (&4 * (p$2 - v$2) pow 2 + &1) +
&2 * (&4 * (p$3 - v$3) pow 2 + &1)`]
THEN REWRITE_TAC[REAL_FIELD `&2 * (&4 * ((p:real^3)$3 - (v:real^3)$3) pow 2 + &1) +
&2 * (&4 * (p$2 - v$2) pow 2 + &1) +
&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`]
THEN ASSUME_TAC (SPEC `r:real`
bdt_emveque) THEN ASM_SIMP_TAC[
SQRT_POW_2]
THEN REWRITE_TAC[REAL_ARITH `a + &6 < b+ &6 <=> a< b`] THEN SIMP_TAC[REAL_ARITH `&0< &8`;
REAL_LT_LMUL_EQ]
THEN ASM_REWRITE_TAC[GSYM
VECTOR_SUB_COMPONENT;DIMINDEX_3] THEN REWRITE_TAC[REAL_ARITH `a pow 2= a*a`]
THEN ASM_MESON_TAC[REAL_ARITH `a pow 2= a*a`]);;
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)
THEN REPEAT STRIP_TAC THEN MP_TAC (REAL_ARITH `floor y <= x /\ y < floor y + &1 ==> y< x+ &1`)
THEN ASM_REWRITE_TAC[] THEN MP_TAC (REAL_ARITH `floor y <= y /\ x < floor y + &1 ==> x< y+ &1`)
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
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)
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);;
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`]
THEN REWRITE_TAC[
FLOOR;(* GSYM INTEGER_IS_INT *)] THEN REWRITE_TAC[
CART_EQ]
THEN SIMP_TAC[
LAMBDA_BETA;DIMINDEX_3] THEN REPEAT GEN_TAC THEN REWRITE_TAC[
FORALL_3]
THEN REWRITE_TAC[MESON[] `a/\b/\c/\d/\e ==> f <=> a==>b==>c==>d ==>e==>f`]
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[]
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`]
THEN SIMP_TAC[] THEN REWRITE_TAC[REAL_ARITH ` &2* a< b <=> a< b/ &2`]
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
THENL [REWRITE_TAC[
vector_norm;
dist] THEN MP_TAC(SPEC `((y:real^3 - x)
dot (y - x)):real`
SQRT_POS_LE)
THEN REWRITE_TAC[
DOT_POS_LE] THEN REWRITE_TAC[REAL_ARITH `&0<= a <=> a= abs a`]
THEN REWRITE_TAC[MESON[] `a:real= b ==> a<
sqrt (&3 / &4) <=> a= b ==> b <
sqrt (&3 / &4)`]
THEN DISCH_TAC THEN MP_TAC (SPEC `&3 / &4 :real`
SQRT_POS_LE) THEN REWRITE_TAC[REAL_ARITH `&0<= &3/ &4`]
THEN REWRITE_TAC[REAL_ARITH `&0<= a <=> a= abs a`] THEN REWRITE_TAC[MESON[] `a:real= b ==> c< a <=> a= b ==> c < b`]
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`)
THEN ASM_REWRITE_TAC[
bdt_canbatrenbon] THEN UNDISCH_TAC `(packing (S:real^3 -> bool)):bool`
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`
THEN UNDISCH_TAC `((y:real^3)
IN (S:real^3 -> bool) /\ y
IN ball (p:real^3,r)):bool`
THEN SIMP_TAC[SET_RULE `(a:real^3)
IN (S:real^3 -> bool ) <=> S a`] THEN REPLICATE_TAC 2 DISCH_TAC
THEN REWRITE_TAC[REAL_ARITH `a:real < &2 <=> ~( &2<= a)`]
THEN REWRITE_TAC[MESON[] `a ==> b==> c <=> a/\b ==> c`] THEN ONCE_REWRITE_TAC[MESON[] ` ~ (P:bool) ==> Q <=> (~ Q ==> P)`] THEN SIMP_TAC[]]);;
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}`,
REPEAT GEN_TAC THEN REWRITE_TAC[
EXTENSION;GSYM
SUBSET_ANTISYM_EQ;
voronoi_open;
INTERS]
THEN REWRITE_TAC[
IN_ELIM_THM] THEN STRIP_TAC
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
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`]
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).
(y
IN S
DELETE v /\ x = v) /\
{x |
dist (x,v) <
dist (x,w)} = {x' |
dist (x',x) <
dist (x',y)})` ASSUME_TAC
THENL [EXISTS_TAC `(v):real^3` THEN EXISTS_TAC `w:real^3` THEN
ASM_REWRITE_TAC[
DELETE;
IN_ELIM_THM;SET_RULE `w:real^3
IN S <=> S w`];UNDISCH_TAC `((?(x:real^3) (y:real^3).
(y
IN S
DELETE v /\ x = (v:real^3)) /\
{x |
dist (x,v) <
dist (x,w)} = {x' |
dist (x',x) <
dist (x',y)})
==>
dist (x,v) <
dist (x,w)):bool` THEN ASM_REWRITE_TAC[]]);;
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}`,
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
THEN REWRITE_TAC[
dist;
norm_ineq_lt] THEN REWRITE_TAC[
DOT_3] THEN ONCE_REWRITE_TAC[REAL_ARITH `a:real < b <=> &0< b - a`]
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) +
(x$2 - y$2) * (x$2 - y$2) +
(x$3 - y$3) * (x$3 - y$3)) -
((x$1 - (v:real^3)$1) * (x$1 - v$1) +
(x$2 - v$2) * (x$2 - v$2) +
(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) -
(x$1 * &2 * (y$1 - v$1) + x$2 * &2 * (y$2 - v$2) + x$3 * &2 * (y$3 - v$3))`]);;
let bound_voronoi=prove( `!(v:real^3) (S:real^3-> bool). saturated S ==>
bounded(
voronoi_open S v)`,
REPEAT GEN_TAC THEN DISJ_CASES_TAC (MESON[] `
bounded (
voronoi_open (S:real^3 ->bool) (v:real^3)) \/ ~(
bounded (
voronoi_open S v))`)
THENL [ASM_MESON_TAC[];UNDISCH_TAC `(~
bounded (
voronoi_open (S:real^3 ->bool) (v:real^3))):bool`
THEN REWRITE_TAC[
bounded] THEN REWRITE_TAC[MESON[] `~(?(a:real). !(x:real^3). x
IN voronoi_open (S:real^3->bool) (v:real^3)
==>
norm x <= a) <=> !(a:real).
~ (!(x:real^3). x
IN voronoi_open (S:real^3->bool) (v:real^3) ==>
norm x <= a)`]
THEN REWRITE_TAC[MESON[] `~(!x. x
IN voronoi_open (S:real^3->bool) (v:real^3) ==>
norm x <= a)
<=> ? (x:real^3). ~ ( x
IN voronoi_open S v ==>
norm x <= a)`]
THEN REWRITE_TAC[MESON[NOT_IMP] `~((x:real^3)
IN voronoi_open (S:real^3->bool) (v:real^3) ==>
norm x <= a)
<=> x
IN voronoi_open S v /\ ~ (
norm x <= a)`]
THEN REWRITE_TAC[REAL_ARITH ` ~ (
norm (x:real^3)<= a:real) <=> a<
norm x`]
THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `
norm (v:real^3) + &2:real`)
THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN UNDISCH_TAC `(x:real^3
IN voronoi_open (S:real^3->bool) (v:real^3) /\
norm (v:real^3)+ &2 <
norm x):bool`
THEN REWRITE_TAC[
voronoi_open;saturated;
IN_ELIM_THM]
THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `(x):real^3`)
THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
THEN UNDISCH_TAC `(!(w:real^3). S w /\ ~(w = v:real^3) ==>
dist (x,v) <
dist (x,w)):bool`
THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `y:real^3`)
THEN MP_TAC(MESON[REAL_ARITH `
norm (v:real^3) + &2 <
norm (x:real^3) ==> &2 <
norm x -
norm v`;
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)
<=
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)`)
THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(y:real^3
IN (S:real^3 -> bool) /\
dist (x,y) < &2):bool` THEN STRIP_TAC
THEN REWRITE_TAC[GSYM
dist] THEN DISCH_TAC THEN SUBGOAL_THEN `~ (y:real^3 = v)` MP_TAC
THENL [(*1*)DISJ_CASES_TAC(MESON[] `(y:real^3 = v) \/ ~(y=v)`) THENL [UNDISCH_TAC `(
dist (x:real^3,y) < &2):bool`
THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH ` ~ (
dist (x:real^3,v) < &2) <=> &2<=
dist(x, v)`]
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`]
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`
THEN REWRITE_TAC[SET_RULE `y
IN (S:real^3 ->bool) <=> S y`] THEN SIMP_TAC[] THEN DISCH_TAC
THEN UNDISCH_TAC `(
dist (x:real^3,y) < &2):bool` THEN UNDISCH_TAC `(&2 <
dist (x,v:real^3)):bool` THEN REAL_ARITH_TAC]]);;
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))`,
REWRITE_TAC[
not_open] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC
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[]]);;
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
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[]
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`]]]);;
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
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 /\
(!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
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
THEN SUBGOAL_THEN `!(n:num). N< n ==> &2 <=
dist((x:num -> real^3) n,v)` MP_TAC
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[]
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)
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[]
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)`]]]);;
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`
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)`]]);;
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`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`]
measure_ineq_lm53_1)
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)
THEN ASM_SIMP_TAC[
finite_set_packing_in_ball]
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])
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`]]]);;
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)`]);;
let negligible_voronoi=prove( `!(S:real^3 ->bool)(p:real^3)(r:real). (!s t.
s
IN {
voronoi_open w v | v
IN S
INTER ball (p,r + &1) /\ w = S} /\
t
IN {
voronoi_open w v | v
IN S
INTER ball (p,r + &1) /\ w = S} /\
~(s = t)
==>
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
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]);;
let ineq_lm5_3_step4=prove(
`!(c:real). (&0<= c) ==> ? (c':real).
!(r:real). (&1 <=r) ==>
( pi/
sqrt( &18)*( &1+ &3/ r) pow 3 + c*((r+ &1) pow 2)/ (r pow 3 *
sqrt( &32)) <= pi/
sqrt( &18) + c'/r)`,
REPEAT STRIP_TAC THEN
EXISTS_TAC `((pi/
sqrt( &18))* ( &9+ &27+ &27) + c* (&1/
sqrt( &32) + &2/
sqrt( &32)+ &1/
sqrt( &32))):real` THEN
REPEAT STRIP_TAC THEN
ONCE_REWRITE_TAC[REAL_ARITH `a:real<= b <=> &0<= b-a`] THEN ASM_SIMP_TAC[REAL_FIELD ` &1<= r==>(
pi /
sqrt (&18) +
(
pi /
sqrt (&18) * (&9 + &27 + &27) +
(c:real) * (&1 /
sqrt (&32) + &2 /
sqrt (&32) + &1 /
sqrt (&32))) /
(r:real)) -
(
pi /
sqrt (&18) * ((&1 + &3 / r) pow 3) +
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))`]
THEN REWRITE_TAC[REAL_FIELD `(&1 / (r:real) *
pi /
sqrt (&18)) *
(&27 / r * (r - &1) + &27 / r pow 2 * (r pow 2 - &1)) +
(&1 / r * (c:real)) *
(&2 / (r *
sqrt (&32)) * (r - &1) +
&1 / (r pow 2 *
sqrt (&32)) * (r pow 2 - &1))= (&1 / r *
pi /
sqrt (&18)) *
(&27 / r * (r - &1) + (&27 / r pow 2) * (r - &1) *(r + &1)) +
(&1 / r * c) *
(&2 / (r *
sqrt (&32)) * (r - &1) +
&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)) *
(&27 / r * (r - &1) + &27 / r pow 2 * (r - &1) * (r + &1)):real`;`(&1 / r * (c:real)) *
(&2 / (r *
sqrt (&32)) * (r - &1) +
&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
THEN MATCH_MP_TAC(SPECL [`&1 / (r:real) * (c:real):real`;`&2 / (r *
sqrt (&32)) * (r - &1) +
&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`]);;
let JGXZYGW=prove(
`!(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)`,
REPEAT GEN_TAC THEN
REWRITE_TAC[
negligible_fun_p;
fcc_compatible] THEN
REPEAT STRIP_TAC THEN
MP_TAC(SPEC `C:real`
ineq_lm5_3_step4) THEN
ASM_SIMP_TAC[] THEN
REPEAT STRIP_TAC THEN
EXISTS_TAC `c':real` THEN
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `r:real`) THEN
ASM_SIMP_TAC[] THEN
SUBGOAL_THEN `
measure (
UNIONS {
ball (v,&1) | v
IN (S:real^3 ->bool)}
INTER ball (p:real^3,r:real)) /
measure (
ball (p,r))<=
pi /
sqrt (&18) * (&1 + &3 / r) pow 3 +
(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
MP_TAC(SPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`]
measure_ineq_lm53_2) THEN
ASM_SIMP_TAC[REAL_ARITH `&1<= r ==> &0<= r`] THEN
DISCH_TAC THEN
MP_TAC(SPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`;`A:real^3 ->
real`]
ineq_lm5_3_step3) THEN
ASM_SIMP_TAC[REAL_ARITH `&1<= r ==> &0<= r`;
fcc_compatible] THEN
ASM_SIMP_TAC[
SUM_ADD;
KIUMVTC;REAL_ARITH `&1<=r ==> &0<= r + &1`;] THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`r+ &1:real`]) THEN
ASM_SIMP_TAC[REAL_ARITH `&1<=r ==> &1<= r+ &1`] THEN
MP_TAC(SPECL [`S:real^3 ->bool`;`p:real^3`;`r:real`]
sum_measure_voronoi_le_ball) THEN
ASM_SIMP_TAC[REAL_ARITH `&1<= r ==> &0<= r`] THEN
REPEAT DISCH_TAC THEN
MP_TAC(REAL_ARITH `
sum ((S:real^3 ->bool)
INTER ball (p:real^3,r + &1)) (\v:real^3.
measure (
voronoi_open S v)) <=
measure (
ball (p,r + &3))
/\
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))) <=
sum (S
INTER ball (p,r + &1)) A +
sum (S
INTER ball (p,r + &1)) (\v:real^3.
measure (
voronoi_open S v))
==>
sqrt (&32) * &(
CARD (S
INTER ball (p,r + &1))) <= C * (r + &1) pow 2 +
measure (
ball (p,r + &3))`) THEN
ASM_SIMP_TAC[]
THEN
ASM_SIMP_TAC[
VOLUME_BALL;REAL_ARITH `&1<= r ==> &0<= r+ &3`] THEN
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
ASM_SIMP_TAC[GSYM (ISPECL [`p:real^3`;`r:real`]
VOLUME_BALL);REAL_ARITH `&1<= r ==> &0<= r`] THEN
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
SIMP_TAC[GSYM
REAL_LE_RDIV_EQ;MESON[
SQRT_POS_LT;REAL_ARITH `&0< &32`] `&0<
sqrt( &32)`] THEN
DISCH_TAC THEN
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))) /
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)) <=
&(
CARD {
ball (v,&1) | v
IN S
INTER ball (p,r + &1)}) * &4 *
pi / &3):bool` THEN
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))) /
sqrt (&32) *
&4 *
pi / &3` (fun
th -> MESON_TAC[
th;REAL_ARITH `a<= b /\ b<= c ==> a<= c`]) THEN
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`]
THEN
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
ASM_SIMP_TAC[] THEN
SIMP_TAC[
REAL_LE_LDIV_EQ] THEN
SUBGOAL_THEN `((C:real) * (r + &1) pow 2 + (&1 + &3 / r) pow 3 * &4 / &3 *
pi * r pow 3) /
sqrt (&32) *
&4 *
pi / &3= (
pi /
sqrt (&18) * (&1 + &3 / r) pow 3 +
C * (r + &1) pow 2 / (r pow 3 *
sqrt (&32))) *
&4 / &3 *
pi *
r pow 3` (fun
th -> MESON_TAC[
th]) THEN
REWRITE_TAC[REAL_FIELD `((a:real) + b)/ c * d= ((a + b)*d )/c /\ ((x:real) + y ) * z = x *z + y* z`] THEN
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
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) *
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) *
sqrt (&32)` (fun
th -> MESON_TAC[
th;REAL_ARITH ` a= b /\ d= c ==> a+ d= c+ b`]) THEN
STRIP_TAC
THENL
[(*2a*)REWRITE_TAC[REAL_FIELD `((C * (r + &1) pow 2 / (r pow 3 *
sqrt (&32))) * &4 / &3 *
pi * r pow 3) *
sqrt (&32)= ((C * (r + &1) pow 2 / (r pow 3 *
sqrt (&32)))*(r pow 3 *
sqrt (&32)))* (&4 / &3 *
pi)`]
THEN
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
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) *
sqrt (&32)= ((pi*
sqrt( &32) /
sqrt (&18)) * (&1 + &3 / r) pow 3) * &4 / &3 *
pi * r pow 3`]
THEN
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
ONCE_REWRITE_TAC[REAL_ARITH ` &32= &4 pow 2 * &2 /\ &18= &3 pow 2 * &2`] THEN
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
MATCH_MP_TAC(REAL_FIELD `~ (
sqrt( &2) = &0) ==> (&4 *
sqrt (&2)) / (&3 *
sqrt (&2)) = &4 / &3`) THEN
MESON_TAC[REAL_ARITH `&0< x ==> ~ (x= &0)`;MESON[
SQRT_POS_LT;REAL_ARITH `&0< &2`] ` &0<
sqrt ( &2)`]]]);;