(*

Volume files

Author: Thomas Hales

Date: 2010-02-08

*)

let RADIAL_NORM_RADIAL = 
prove(`radial_norm = radial`,
REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;radial_norm;radial] );;
let EVENTUALLY_RADIAL_UNNORM = 
prove(`eventually_radial_norm = eventually_radial`,
(* LBWOPAH *)
let RADIAL_EVENTUALLY_RADIAL = 
prove(`!C x:real^N. (?r. (r> &0) /\ radial r x C) ==> eventually_radial x C`,
REWRITE_TAC[radial;eventually_radial] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[SET_RULE`x IN a INTER b <=> x IN a /\ x IN b`] THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ (*1*) ASM_MESON_TAC[SET_RULE `a SUBSET b ==> a INTER b SUBSET b`]; (*2*) ALL_TAC ] THEN REPEAT STRIP_TAC THENL [ (*1*)ASM_MESON_TAC[]; (*2*)ALL_TAC ] THEN REWRITE_TAC[IN_BALL;dist;VECTOR_ARITH `x:real^N -(x+y) = -- y`;NORM_MUL;NORM_NEG] THEN ASM_SIMP_TAC[REAL_ARITH `t > &0 ==> (abs t = t)`] );;
let LBWOPAH = RADIAL_EVENTUALLY_RADIAL;; (* -- to here -- let VQFENMT1 = prove(`!r x C. volume_prop vol /\ measurable C /\ radial_norm r x C ==> (vol C = sol C x * (r pow 3)/(&3))`, );; *) (* -- work in progres -- let VQFENMT2 = prove(`!x C. volume_prop vol /\ measurable C /\ (?r. (r > &0) /\ (!y. y IN C ==> dist(x,y) >= r)) ==> eventually_radial_norm x C /\ (sol C (x:real^3) = &0)`, REWRITE_TAC[TAUT `(a ==> b /\ c) = ((a ==> b) /\ (a /\ b ==> c))`] THEN STRIP_TAC THEN STRIP_TAC THEN CONJ_TAC THEN REWRITE_TAC[eventually_radial_norm;radial_norm] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[NORMBALL_BALL] THEN EXISTS_TAC `r:real` THEN ASM_REWRITE_TAC[INTER_SUBSET] THEN GEN_TAC THEN SUBGOAL_THEN `C INTER ball((x:real^3),r) = EMPTY` ASSUME_TAC THEN (* branch 1 *) REWRITE_TAC[ball] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN REWRITE_TAC[elimin NOT_IN_EMPTY;elimin IN_INTER;elimin IN_ELIM_THM] THEN ASM_MESON_TAC[IN;REAL_ARITH `!a b. a >= b ==> ~(a < b)`] THEN (* branch 2 *) ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN (* branch 3 *) REPEAT STRIP_TAC THEN *)