Update from HH
[Flyspeck/.git] / text_formalization / packing / UPFZBZM.hl
1 (* ========================================================================= *)
2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
3 (*                                                                           *)
4 (*      Authour   : VU KHAC KY                                               *)
5 (*      Book lemma: UPFZBZM                                                  *)
6 (*      Chaper    : Packing (Clusters)                                       *)
7 (*                                                                           *)
8 (* ========================================================================= *)
9
10 (* ========================================================================= *)
11 (*                     FILES NEED TO BE LOADED                               *)
12 (* sum_gammaX_lmfun_estimate.hl                                              *)
13 (* ========================================================================= *)
14
15 module Upfzbzm = struct
16
17
18 open Sphere;;
19 open Euler_main_theorem;;
20 open Pack_defs;;
21 open Pack_concl;; 
22 open Pack1;;
23 open Pack2;;
24 open Packing3;;
25 open Rogers;; 
26 open Vukhacky_tactics;;
27 open Marchal_cells;;
28 open Emnwuus;;
29 (* open Marchal_cells_2;; *)
30 open Marchal_cells_2_new;;
31 open Urrphbz1;;
32 open Lepjbdj;;
33 open Hdtfnfz;;
34 open Rvfxzbu;;
35 open Sltstlo;;
36 open Urrphbz2;;
37 open Urrphbz3;;
38 open Ynhyjit;;
39 open Njiutiu;;
40 open Tezffsk;;
41 open Qzksykg;;
42 open Ddzuphj;;
43 open Ajripqn;;
44 open Qzyzmjc;;
45 open Upfzbzm_support_lemmas;;
46 open Marchal_cells_3;;
47 open Grutoti;;
48
49 open Sum_gammax_lmfun_estimate;;
50 open Kizhltl;;
51   
52 let UPFZBZM_concl = 
53    `!V.  saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\ 
54          TSKAJXY_statement /\
55          lmfun_inequality V ==>
56     (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
57
58 let FCC_COMPATABILITY_FUNC_concl =  
59  `!V.  saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\ 
60    TSKAJXY_statement /\
61    lmfun_inequality V /\ G = (\u. --vol(voronoi_open V u) + 
62    &8 * mm1 - &8 * mm2 * sum { v | v IN V /\ ~(u=v) /\ dist(u,v) <= &2*h0 } 
63    (\v. lmfun (hl [u;v]))) 
64    ==> fcc_compatible G V`;;
65
66 let NEGLIGIBLE_FUNC_concl = 
67   `!V. saturated V /\
68        packing V /\
69        cell_cluster_estimate_v1 V /\
70        TSKAJXY_statement /\
71        lmfun_inequality V /\
72        G =
73        (\u. --vol (voronoi_open V u) +
74             &8 * mm1 -
75             &8 *
76             mm2 *
77             sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
78             (\v. lmfun (hl [u; v])))
79        ==> negligible_fun_0 G V`;;
80
81 (* ========================================================================= *)
82 (*                            THE THEOREM                                    *)
83 (* ========================================================================= *)
84
85 (* PART 1 OF THE LEMMA *)
86
87 let FCC_COMPATABILITY_FUNC = prove_by_refinement (
88  FCC_COMPATABILITY_FUNC_concl,
89 [(REWRITE_TAC[lmfun_inequality;fcc_compatible]);
90  (REPEAT STRIP_TAC);
91  (ASM_REWRITE_TAC[Pack2.MEASURE_VORONOI_CLOSED_OPEN]);
92  (ASM_REWRITE_TAC[REAL_ARITH `a + --a + b - c = b - c`]);
93  (MATCH_MP_TAC (REAL_ARITH 
94   `x = &8 * mm1 - &8 * (&12 * mm2) /\ y <= &8 * (&12 * mm2) ==> 
95    x <= &8 * mm1 - y`));
96  (STRIP_TAC);
97  (REWRITE_TAC[SQRT_OF_32_lemma]);
98  (REWRITE_TAC[REAL_ARITH `a * b - a * c = a * (b - c)`]);
99  (REWRITE_TAC[m1_minus_12m2]);
100  (MATCH_MP_TAC REAL_LE_LMUL);
101  (REWRITE_TAC[REAL_ARITH `&0 <= &8`]);
102  (REWRITE_TAC[REAL_ARITH `&12 * mm2 = mm2 * &12`]);
103  (MATCH_MP_TAC REAL_LE_LMUL);
104  (REWRITE_TAC[ZERO_LE_MM2_LEMMA]);
105  (ASM_MESON_TAC[])]);;
106
107
108
109 (* ========================================================================= *)
110 (* PART 2 OF THE LEMMA *)
111 (* ========================================================================= *)
112
113 let NEGLIGIBLE_FUNC = prove_by_refinement (
114  NEGLIGIBLE_FUNC_concl,
115 [(REWRITE_TAC[negligible_fun_0; negligible_fun_any_C]);
116  (REPEAT STRIP_TAC);
117
118  (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL1));
119  (STRIP_TAC);
120  (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL2));
121  (STRIP_TAC);
122  (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL4));
123  (STRIP_TAC);
124
125  (MP_TAC (SPEC `V:real^3->bool` SUM_GAMMAX_LMFUN_ESTIMATE));
126  (STRIP_TAC);
127
128  (NEW_GOAL 
129    `!r. saturated V /\ packing V /\ &1 <= r
130           ==> c''' * r pow 2 <=
131               sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
132               (\X. gammaX V X lmfun)`);
133  (REPEAT STRIP_TAC);
134  (FIRST_ASSUM MATCH_MP_TAC);
135  (ASM_REWRITE_TAC[]);
136  (UP_ASM_TAC THEN REWRITE_TAC[gammaX] THEN STRIP_TAC);
137
138  (EXISTS_TAC `--c''' - c - c' - c''`);
139  (REPEAT STRIP_TAC);
140
141  (ABBREV_TAC `f1 =  (\u:real^3. --vol (voronoi_open V u))`);
142  (ABBREV_TAC `f2 =  (\u:real^3.  &8 * mm1 -  &8 * mm2 *
143                      sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
144                      (\v. lmfun (hl [u; v])))`);
145  (REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) G = 
146                  sum (V INTER ball (vec 0,r)) f1 + 
147                  sum (V INTER ball (vec 0,r)) f2`);
148  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "f1" THEN EXPAND_TAC "f2");
149  (MATCH_MP_TAC SUM_ADD);
150  (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
151  (ABBREV_TAC `f3 =  (\u:real^3.  &8 * mm1)`);
152  (ABBREV_TAC `f4 =  (\u:real^3.  &8 * mm2 *
153                      sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
154                      (\v. lmfun (hl [u; v])))`);
155  (REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) f2 = 
156                  sum (V INTER ball (vec 0,r)) f3 - 
157                  sum (V INTER ball (vec 0,r)) f4`);
158  (EXPAND_TAC "f2" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f4");
159  (MATCH_MP_TAC SUM_SUB);
160  (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
161  (EXPAND_TAC "f4" THEN DEL_TAC THEN 
162    ASM_SIMP_TAC[SUM_NEG;SUM_CONST;SUM_LMUL;FINITE_PACK_LEMMA]);
163  (ABBREV_TAC `f5 =  (\u:real^3.  
164                      sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
165                      (\v. lmfun (hl [u; v])))`);
166  (ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);
167  (ABBREV_TAC `T1 = sum B vol`);
168  (ABBREV_TAC `T2 = --(&2 * mm1 / pi) * sum B (total_solid V)`);
169  (ABBREV_TAC `T3 = (&8 * mm2 / pi) * sum B (\X. sum (edgeX V X)
170                      (\({u, v}). if {u, v} IN edgeX V X
171                                then dihX V X (u,v) * lmfun (hl [u; v])
172                                else &0))`);
173
174  (NEW_GOAL `sum (V:real^3->bool INTER ball (vec 0,r)) f1 <= --T1 - c * r pow 2`);
175  (EXPAND_TAC "T1" THEN EXPAND_TAC "B");
176  (EXPAND_TAC "f1");
177  (REWRITE_TAC[SUM_NEG; REAL_ARITH `-- a <= --b - c <=> b + c <= a`]);
178  (FIRST_ASSUM MATCH_MP_TAC);
179  (ASM_REWRITE_TAC[]);
180
181  (NEW_GOAL 
182   `sum (V:real^3->bool INTER ball (vec 0,r)) f3 <= --T2 - c' * r pow 2`);
183  (EXPAND_TAC "T2" THEN EXPAND_TAC "B");
184  (EXPAND_TAC "f3");
185  (REWRITE_TAC[SUM_NEG; REAL_ARITH `a <= --(-- b * d) - c<=> a + c <= b * d`]);
186  (REWRITE_WITH `sum (V INTER ball (vec 0,r)) (\u:real^3. &8 * mm1) = 
187    &(CARD (V INTER ball (vec 0,r))) * (&8 * mm1)`);
188  (MATCH_MP_TAC SUM_CONST);
189  (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
190  (FIRST_ASSUM MATCH_MP_TAC);
191  (ASM_REWRITE_TAC[]);
192
193  (NEW_GOAL `T3 + c'' * r pow 2 <= 
194    &8 * mm2 * sum (V:real^3->bool INTER ball (vec 0,r)) f5`);
195  (EXPAND_TAC "T3" THEN EXPAND_TAC "B");
196
197  (FIRST_ASSUM MATCH_MP_TAC);
198  (ASM_REWRITE_TAC[]);
199
200  (MATCH_MP_TAC (REAL_ARITH `(?s. A <= s /\ s <= b) ==> A <= b`));
201  (EXISTS_TAC `--T1 + --T2 + --T3  - (c + c' + c'') * r pow 2`);
202  (STRIP_TAC);
203  (ASM_REAL_ARITH_TAC);
204  (REWRITE_TAC[REAL_ARITH 
205    `--T1 + --T2 + --T3 - (c + c' + c'') * r pow 2 <=
206    (--c''' - c - c' - c'') * r pow 2 
207    <=> c''' * r pow 2 <= T1 + T2 + T3`]);
208  (REWRITE_WITH `T1 + T2 + T3 = 
209                  sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
210                  (\X. gammaX V X lmfun)`);
211  (ASM_REWRITE_TAC[]);
212  (REWRITE_TAC[gammaX]);
213  (NEW_GOAL `FINITE (B:(real^3->bool)->bool)`);
214  (EXPAND_TAC "B");
215  (ASM_SIMP_TAC [FINITE_MCELL_SET_LEMMA]);
216  (ASM_SIMP_TAC[SUM_ADD; SUM_SUB; SUM_LMUL; ETA_AX]);
217  (EXPAND_TAC "T2");
218  (REAL_ARITH_TAC);
219  (FIRST_ASSUM MATCH_MP_TAC);
220  (ASM_REWRITE_TAC[])]);;
221  
222
223 (* ========================================================================= *)
224 (*             Main theorm                                                   *)
225 (* ========================================================================= *)
226
227 let UPFZBZM = prove (UPFZBZM_concl,
228  (REPEAT STRIP_TAC) THEN (ABBREV_TAC `G = (\u. --vol (voronoi_open V u) +
229               &8 * mm1 -
230               &8 *
231               mm2 *
232               sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
233               (\v. lmfun (hl [u; v])))`) THEN
234  (EXISTS_TAC `G:real^3->real`) THEN 
235  (ASM_MESON_TAC[NEGLIGIBLE_FUNC;FCC_COMPATABILITY_FUNC]));;
236
237
238 end;;