1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Authour : VU KHAC KY *)
5 (* Book lemma: UPFZBZM *)
6 (* Chaper : Packing (Clusters) *)
8 (* ========================================================================= *)
10 (* ========================================================================= *)
11 (* FILES NEED TO BE LOADED *)
12 (* sum_gammaX_lmfun_estimate.hl *)
13 (* ========================================================================= *)
15 module Upfzbzm = struct
19 open Euler_main_theorem;;
26 open Vukhacky_tactics;;
29 (* open Marchal_cells_2;; *)
30 open Marchal_cells_2_new;;
45 open Upfzbzm_support_lemmas;;
46 open Marchal_cells_3;;
49 open Sum_gammax_lmfun_estimate;;
53 `!V. saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\
55 lmfun_inequality V ==>
56 (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
58 let FCC_COMPATABILITY_FUNC_concl =
59 `!V. saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\
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`;;
66 let NEGLIGIBLE_FUNC_concl =
69 cell_cluster_estimate_v1 V /\
73 (\u. --vol (voronoi_open V u) +
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`;;
81 (* ========================================================================= *)
83 (* ========================================================================= *)
85 (* PART 1 OF THE LEMMA *)
87 let FCC_COMPATABILITY_FUNC = prove_by_refinement (
88 FCC_COMPATABILITY_FUNC_concl,
89 [(REWRITE_TAC[lmfun_inequality;fcc_compatible]);
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) ==>
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[])]);;
109 (* ========================================================================= *)
110 (* PART 2 OF THE LEMMA *)
111 (* ========================================================================= *)
113 let NEGLIGIBLE_FUNC = prove_by_refinement (
114 NEGLIGIBLE_FUNC_concl,
115 [(REWRITE_TAC[negligible_fun_0; negligible_fun_any_C]);
118 (MP_TAC (SPEC `V:real^3->bool` KIZHLTL1));
120 (MP_TAC (SPEC `V:real^3->bool` KIZHLTL2));
122 (MP_TAC (SPEC `V:real^3->bool` KIZHLTL4));
125 (MP_TAC (SPEC `V:real^3->bool` SUM_GAMMAX_LMFUN_ESTIMATE));
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)`);
134 (FIRST_ASSUM MATCH_MP_TAC);
136 (UP_ASM_TAC THEN REWRITE_TAC[gammaX] THEN STRIP_TAC);
138 (EXISTS_TAC `--c''' - c - c' - c''`);
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])
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");
177 (REWRITE_TAC[SUM_NEG; REAL_ARITH `-- a <= --b - c <=> b + c <= a`]);
178 (FIRST_ASSUM MATCH_MP_TAC);
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");
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);
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");
197 (FIRST_ASSUM MATCH_MP_TAC);
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`);
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)`);
212 (REWRITE_TAC[gammaX]);
213 (NEW_GOAL `FINITE (B:(real^3->bool)->bool)`);
215 (ASM_SIMP_TAC [FINITE_MCELL_SET_LEMMA]);
216 (ASM_SIMP_TAC[SUM_ADD; SUM_SUB; SUM_LMUL; ETA_AX]);
219 (FIRST_ASSUM MATCH_MP_TAC);
220 (ASM_REWRITE_TAC[])]);;
223 (* ========================================================================= *)
225 (* ========================================================================= *)
227 let UPFZBZM = prove (UPFZBZM_concl,
228 (REPEAT STRIP_TAC) THEN (ABBREV_TAC `G = (\u. --vol (voronoi_open V u) +
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]));;