Update from HH
[Flyspeck/.git] / legacy / oldvolume / ch_volume / vol2.hl
1 (*
2
3 Volume files
4
5 Author: Thomas Hales
6
7 Date: 2010-02-08
8
9 *)
10
11 let RADIAL_NORM_RADIAL = prove(`radial_norm = radial`,
12    REWRITE_TAC[FUN_EQ_THM;NORMBALL_BALL;radial_norm;radial] 
13                                 );;
14
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]                                );;
17
18
19
20 (* LBWOPAH *)
21
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
24     REPEAT STRIP_TAC 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
27    CONJ_TAC THENL
28    [
29     (*1*) ASM_MESON_TAC[SET_RULE `a SUBSET b ==> a INTER b SUBSET b`];
30     (*2*) ALL_TAC
31     ] THEN
32     REPEAT STRIP_TAC THENL
33     [
34     (*1*)ASM_MESON_TAC[];
35      (*2*)ALL_TAC
36     ] THEN
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)`] 
39                              );;
40
41 let LBWOPAH = RADIAL_EVENTUALLY_RADIAL;;
42
43
44 (* -- to here --
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))`,
47
48   );;
49 *)
50
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
57    CONJ_TAC THEN
58    REWRITE_TAC[eventually_radial_norm;radial_norm] THEN
59    REPEAT STRIP_TAC THEN
60    REWRITE_TAC[NORMBALL_BALL] THEN
61    EXISTS_TAC `r:real` THEN
62    ASM_REWRITE_TAC[INTER_SUBSET] THEN
63    GEN_TAC THEN
64      SUBGOAL_THEN `C INTER ball((x:real^3),r) = EMPTY` ASSUME_TAC THEN
65    (* branch 1 *)
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
70    (* branch 2 *)
71    ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
72    (* branch 3 *)
73    REPEAT STRIP_TAC THEN
74
75 *)