11 let RADIAL_NORM_RADIAL = prove(`radial_norm = radial`,
12 REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;radial_norm;radial]
15 let EVENTUALLY_RADIAL_UNNORM = prove(`eventually_radial_norm = eventually_radial`,
16 REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;RADIAL_NORM_RADIAL;eventually_radial_norm;eventually_radial] );;
22 let RADIAL_EVENTUALLY_RADIAL = prove(`!C x:real^N. (?r. (r> &0) /\ radial r x C) ==> eventually_radial x C`,
23 REWRITE_TAC[radial;eventually_radial] THEN
25 REWRITE_TAC[SET_RULE`x IN a INTER b <=> x IN a /\ x IN b`] THEN
26 EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[] THEN
29 (*1*) ASM_MESON_TAC[SET_RULE `a SUBSET b ==> a INTER b SUBSET b`];
32 REPEAT STRIP_TAC THENL
37 REWRITE_TAC[IN_BALL;dist;VECTOR_ARITH `x:real^N -(x+y) = -- y`;NORM_MUL;NORM_NEG] THEN
38 ASM_SIMP_TAC[REAL_ARITH `t > &0 ==> (abs t = t)`]
41 let LBWOPAH = RADIAL_EVENTUALLY_RADIAL;;
45 let VQFENMT1 = prove(`!r x C. volume_prop vol /\ measurable C /\ radial_norm r x C ==>
46 (vol C = sol C x * (r pow 3)/(&3))`,
51 (* -- work in progres --
52 let VQFENMT2 = prove(`!x C.
53 volume_prop vol /\ measurable C /\ (?r. (r > &0) /\ (!y. y IN C ==> dist(x,y) >= r)) ==>
54 eventually_radial_norm x C /\ (sol C (x:real^3) = &0)`,
55 REWRITE_TAC[TAUT `(a ==> b /\ c) = ((a ==> b) /\ (a /\ b ==> c))`] THEN
56 STRIP_TAC THEN STRIP_TAC THEN
58 REWRITE_TAC[eventually_radial_norm;radial_norm] THEN
60 REWRITE_TAC[NORMBALL_BALL] THEN
61 EXISTS_TAC `r:real` THEN
62 ASM_REWRITE_TAC[INTER_SUBSET] THEN
64 SUBGOAL_THEN `C INTER ball((x:real^3),r) = EMPTY` ASSUME_TAC THEN
66 REWRITE_TAC[ball] THEN
67 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
68 REWRITE_TAC[elimin NOT_IN_EMPTY;elimin IN_INTER;elimin IN_ELIM_THM] THEN
69 ASM_MESON_TAC[IN;REAL_ARITH `!a b. a >= b ==> ~(a < b)`] THEN
71 ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN