3 (* ========================================================================= *)
4 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Authour : VU KHAC KY *)
7 (* Book lemma: UPFZBZM *)
8 (* Chaper : Packing (Clusters) *)
9 (* Date : October 3, 2010 *)
11 (* ========================================================================= *)
13 (* ========================================================================= *)
14 (* Supporting lemmas for UPFZBZM *)
15 (* Chaper : Packing (Clusters) *)
17 (* ========================================================================= *)
19 (* ========================================================================= *)
20 (* FILES NEED TO BE LOADED *)
21 (* ========================================================================= *)
23 flyspeck_needs "jordan/refinement.hl";;
24 flyspeck_needs "jordan/hash_term.hl";;
25 flyspeck_needs "jordan/parse_ext_override_interface.hl";;
26 flyspeck_needs "jordan/real_ext.hl";;
27 flyspeck_needs "jordan/lib_ext.hl";;
28 flyspeck_needs "jordan/tactics_jordan.hl";;
29 flyspeck_needs "jordan/num_ext_nabs.hl";;
30 flyspeck_needs "jordan/taylor_atn.hl";;
31 flyspeck_needs "jordan/float.hl";;
32 flyspeck_needs "jordan/flyspeck_constants.hl";;
33 (* flyspeck_needs "packing/lemma_negligible.hl";; *)
35 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
36 flyspeck_needs "packing/pack_defs.hl";;
37 flyspeck_needs "packing/pack_concl.hl";;
38 (* flyspeck_needs "packing/beta_pair_thm.hl";; *)
40 module Upfzbzm_support_lemmas = struct
42 open Flyspeck_constants;;
45 open Vukhacky_tactics;;
50 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
51 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
52 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
55 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
56 REPEAT COND_CASES_TAC THEN
57 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
58 REWRITE_TAC allthms in
61 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
64 let CHANGED_SET_RULE tm = prove(tm,CHANGED_SET_TAC[]);;
66 (*-------------------------------------------------------------------------- *)
70 `!V. saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\
72 lmfun_inequality V ==>
73 (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
76 (* ------------------------------------------------------------------------- *)
79 let SUM_GAMMAX_LMFUN_ESTIMATE_concl =
80 `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\
81 cell_cluster_estimate_v1 V /\ marchal_inequality /\
82 lmfun_inequality V ==>
83 c * r pow 2 <= sum {X | X SUBSET ball (vec 0, r) /\ mcell_set V X}
84 (\X. gammaX V X lmfun)`;;
87 let KIZHLTL3_new_concl =
88 `!V. ?c. !r. saturated V /\
92 sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
94 (\({u, v}). dihX V X (u,v) * lmfun (hl [u; v]))) +
97 sum (V INTER ball (vec 0,r))
99 {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0 }
100 (\v. lmfun (hl [u; v])))`;;
102 (* ========================================================================= *)
103 (* SOME COMPLEMENTARY LEMMAS *)
104 (* ========================================================================= *)
105 (* ========================================================================= *)
107 let tau0_not_zero = prove_by_refinement (
109 [(SUBGOAL_THEN `#1.54065 < tau0` ASSUME_TAC);
110 (REWRITE_TAC[bounds]);
112 (ASM_MESON_TAC[REAL_ARITH `~(#1.54065 < &0)`])]);;
114 (* ========================================================================= *)
116 let ZERO_LT_MM2_LEMMA = prove_by_refinement ( `&0 < mm2`,
117 [(SUBGOAL_THEN `#0.02541 < mm2` ASSUME_TAC);
118 (REWRITE_TAC[bounds]);
119 (ASM_REAL_ARITH_TAC)]);;
121 (* ========================================================================= *)
123 let FINITE_PACK_LEMMA = Packing3.KIUMVTC;;
125 let FINITE_PERMUTE_3 = prove_by_refinement
126 (`FINITE {p | p permutes {0, 1, 2}}`,
127 [MATCH_MP_TAC FINITE_PERMUTATIONS THEN MESON_TAC[FINITE_RULES]]);;
128 let FINITE_PERMUTE_4 = prove_by_refinement
129 (`FINITE {p | p permutes {0, 1, 2, 3}}`,
130 [MATCH_MP_TAC FINITE_PERMUTATIONS THEN MESON_TAC[FINITE_RULES]]);;
134 let john_harrison_lemma1 = prove
135 (`(\(x,y). P x y) = (\p. P (FST p) (SND p))`,
136 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
138 let john_harrison_lemma2 = MESON[] `(?x. P x) /\ (@x. P x) = a ==> P a`;;
140 let JOHN_SELECT_THM = prove
141 (`(?x y. P x /\ Q y /\ R x y) /\
142 (@(x,y). P x /\ Q y /\ R x y) = (a,b)
143 ==> P a /\ Q b /\ R a b`,
144 REWRITE_TAC[GSYM EXISTS_PAIRED_THM] THEN
145 REWRITE_TAC[john_harrison_lemma1] THEN
146 DISCH_THEN(MP_TAC o MATCH_MP john_harrison_lemma2) THEN
147 REWRITE_TAC[FST; SND]);;
149 (* ------------------------------------------------------------------------- *)
152 let SQRT_RULE_Euler_lemma = prove
153 (`!x y. x pow 2 = y /\ &0 <= x ==> x = sqrt y`,
154 REPEAT STRIP_TAC THEN
155 REWRITE_TAC[GSYM (ASSUME `x pow 2 = y`);REAL_POW_2] THEN
156 ASM_SIMP_TAC[SQRT_MUL] THEN
157 ASM_MESON_TAC[GSYM REAL_POW_2;SQRT_POW_2]);;
159 let SQRT_OF_32_lemma = prove_by_refinement (
160 `sqrt (&32) = &8 * sqrt (&1 / &2)`,
161 [ (REWRITE_WITH `&8 = sqrt (&64)`);
162 (MATCH_MP_TAC SQRT_RULE_Euler_lemma);
164 (REWRITE_TAC[REAL_ARITH `&32 = &64 * (&1 / &2)`]);
165 (MATCH_MP_TAC SQRT_MUL);
168 (* ------------------------------------------------------------------------- *)
171 let m1_minus_12m2 = prove_by_refinement (
172 `mm1 - &12 * mm2 = sqrt (&1 / &2)`,
174 [ (REWRITE_TAC[mm1;mm2]);
175 (REWRITE_TAC [REAL_ARITH `a * (b / c) = (a * b) / c`]);
177 `&12 * (&6 * sol0 - pi) * sqrt (&2) = ((&6 * sol0 - pi) * sqrt (&8)) * &6`);
178 (REWRITE_TAC[REAL_ARITH`&12 * a * b = (a * &2 * b) * &6`]);
179 (MATCH_MP_TAC (MESON[REAL_EQ_MUL_RCANCEL] `a = b ==> a * x = b * x`));
180 (MATCH_MP_TAC (MESON[REAL_EQ_MUL_LCANCEL] `a = b ==> x * a = x * b`));
182 (REWRITE_TAC[REAL_ARITH `&8 = &4 * &2`]);
183 (REWRITE_WITH `sqrt (&4 * &2) = sqrt (&4) * sqrt (&2)`);
184 (MATCH_MP_TAC SQRT_MUL);
186 (MATCH_MP_TAC (MESON[REAL_EQ_MUL_RCANCEL] `a = b ==> a * x = b * x`));
187 (MATCH_MP_TAC SQRT_RULE_Euler_lemma);
189 (REWRITE_TAC[REAL_ARITH `(m * &6) / (&6 * tau0) = m * &6 / (tau0 * &6)`]);
190 (REWRITE_WITH `((&6 * sol0 - pi) * sqrt (&8)) * &6 / (tau0 * &6) =
191 ((&6 * sol0 - pi) * sqrt (&8)) / tau0`);
192 (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
193 (REWRITE_TAC[REAL_ARITH `~(&6 = &0)`;tau0_not_zero]);
195 (REWRITE_TAC[REAL_ARITH `a / b - c / b = (a - c) / b`]);
196 (REWRITE_TAC[REAL_ARITH `a * x - b * x = (a - b) * x`]);
197 (REWRITE_WITH `sol0 - (&6 * sol0 - pi) = tau0 / &4`);
201 (REWRITE_TAC[REAL_ARITH
202 `(tau0 / &4 * x) / tau0 = (tau0 / tau0) * (x / &4)`]);
203 (REWRITE_WITH `sqrt (&8) / &4 = sqrt (&1 / &2)`);
204 (REWRITE_TAC[REAL_ARITH `&1 / &2 = &8 / &16`]);
205 (REWRITE_WITH `sqrt (&8 / &16) = sqrt (&8) / sqrt (&16)`);
206 (MATCH_MP_TAC SQRT_DIV THEN REAL_ARITH_TAC);
207 (REWRITE_WITH `sqrt (&16) = &4`);
209 (MATCH_MP_TAC (MESON[] `a = b ==> b = a`));
210 (MATCH_MP_TAC SQRT_RULE_Euler_lemma THEN REAL_ARITH_TAC);
211 (MATCH_MP_TAC (MESON[REAL_MUL_LID] `x = &1 ==> x * y = y`));
212 (MATCH_MP_TAC REAL_DIV_REFL);
213 (REWRITE_TAC[tau0_not_zero])]);;
216 (* ------------------------------------------------------------------------- *)
219 let ZERO_LE_MM2_LEMMA =
220 MATCH_MP (REAL_ARITH `&0 < x ==> &0 <= x`) ZERO_LT_MM2_LEMMA;;
222 (* ------------------------------------------------------------------------- *)
225 let FINITE_edgeX = prove_by_refinement (
226 `!V X. FINITE (edgeX V X)`,
227 [(REPEAT GEN_TAC THEN REWRITE_TAC[edgeX;VX]);
229 (* Break into 2 subgoal *)
231 (REWRITE_WITH `{{u:real^3, v} | {} u /\ {} v /\ ~(u = v)} = {}`);
232 (* New Subgoal 1.1 *)
233 (CHANGED_SET_TAC[]); (* End subgoal 1.1 *)
234 (MESON_TAC[FINITE_CASES]); (* End Subgoal 1 *)
237 `FINITE (set_of_list (truncate_simplex (k - 1) (ul:(real^3)list)))`
239 (REWRITE_TAC[FINITE_SET_OF_LIST]);
240 (ABBREV_TAC `S = set_of_list (truncate_simplex (k - 1) (ul:(real^3)list))`);
241 (MATCH_MP_TAC FINITE_SUBSET);
242 (EXISTS_TAC `{t:real^3->bool | t SUBSET S}`);
244 (ASM_MESON_TAC[FINITE_POWERSET]);
245 (REWRITE_TAC[SUBSET;IN_ELIM_THM]);
247 (REPLICATE_TAC 5 UP_ASM_TAC);
248 (CHANGED_SET_TAC[])]);;
251 (* ------------------------------------------------------------------------- *)
254 let FINITE_critical_edgeX = prove_by_refinement (
255 `!V X. FINITE (critical_edgeX V X)`,
257 (REWRITE_TAC[critical_edgeX]);
259 `{{u:real^3, v} | {u, v} IN edgeX V X /\ hminus <= hl [u; v] /\
260 hl [u; v] <= hplus} =
261 {{u, v} | hminus <= hl [u; v] /\ hl [u; v] <= hplus} INTER (edgeX V X)`);
262 (REPEAT GEN_TAC THEN SET_TAC[]);
263 (MESON_TAC[FINITE_edgeX;FINITE_INTER])]);;
266 (* ------------------------------------------------------------------------- *)
269 let DIHV_LE_0 = prove_by_refinement (
270 `!x:real^N y z t. &0 <= dihV x y z t`,
271 [ (REPEAT GEN_TAC THEN REWRITE_TAC[dihV]);
272 (REPEAT LET_TAC THEN REWRITE_TAC[arcV]);
273 (MATCH_MP_TAC (MESON[] `&0 <= acs y /\ acs y <= pi ==> &0 <= acs y`));
274 (MATCH_MP_TAC ACS_BOUNDS);
275 (REWRITE_TAC[GSYM REAL_ABS_BOUNDS; NORM_CAUCHY_SCHWARZ_DIV])]);;
278 (* ------------------------------------------------------------------------- *)
281 let DIHV_SYM = prove_by_refinement (
282 `!(x:real^N) y z t. dihV x y z t = dihV y x z t`,
284 (REWRITE_TAC[dihV] THEN REPEAT LET_TAC);
285 (MATCH_MP_TAC (MESON[]
286 `!a b c d x. (a = b) /\ (c = d) ==> arcV x a c = arcV x b d`));
288 (* Break into 2 subgoals with similar proofs *)
291 (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap");
293 (REWRITE_WITH `(va':real^N) = va - vc`);
294 (EXPAND_TAC "va'" THEN EXPAND_TAC "va" THEN EXPAND_TAC "vc");
297 (REWRITE_WITH `(vc':real^N) = --vc`);
298 (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
302 `(--vc dot --vc) % (va:real^N - vc) = (vc dot vc) % va - (vc dot vc) % vc`);
303 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);
306 (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));
307 (REWRITE_WITH `((va:real^N - vc) dot --vc) % --vc =
308 (va dot vc) % vc - (vc dot vc) % vc`);
309 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);
310 (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);
311 (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;
312 DOT_LSUB;VECTOR_SUB_RDISTRIB]);
316 (EXPAND_TAC "vbp'" THEN EXPAND_TAC "vbp");
317 (REWRITE_WITH `(vb':real^N) = vb - vc`);
318 (EXPAND_TAC "vb'" THEN EXPAND_TAC "vb" THEN EXPAND_TAC "vc");
321 (REWRITE_WITH `(vc':real^N) = --vc`);
322 (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
326 `(--vc dot --vc) % (vb:real^N - vc) = (vc dot vc) % vb - (vc dot vc) % vc`);
327 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);
330 (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));
331 (REWRITE_WITH `((vb:real^N - vc) dot --vc) % --vc =
332 (vb dot vc) % vc - (vc dot vc) % vc`);
333 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);
334 (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);
335 (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;
336 DOT_LSUB;VECTOR_SUB_RDISTRIB]);
337 (VECTOR_ARITH_TAC)]);;
339 (* ------------------------------------------------------------------------- *)
342 let DIHX_POS = prove_by_refinement (
343 `!u v V X. &0 <= dihX V X (u,v)`,
344 [(REPEAT STRIP_TAC THEN REWRITE_TAC[dihX; dihu2; dihu3;dihu4]);
349 (REWRITE_TAC[DIHV_RANGE]);
351 (REWRITE_TAC[DIHV_RANGE]);
353 (REWRITE_TAC[DIHV_RANGE]);
356 (* ------------------------------------------------------------------------- *)
359 let SUM_SET_OF_2_ELEMENTS = prove_by_refinement (
360 `!s t f. ~(s = t) ==> sum {s:A,t} f = f s + f t`,
362 (REWRITE_WITH `!s t f. f s = sum{s:A} f /\ f t = sum{t} f`);
363 (MESON_TAC[SUM_SING]);
364 (REWRITE_WITH `{s:A, t} = {s} UNION {t}`);
366 (MATCH_MP_TAC SUM_UNION);
367 (REWRITE_TAC[FINITE_SING]);
368 (UP_ASM_TAC THEN SET_TAC[])]);;
370 let pos_lemma = prove_by_refinement(
371 `!Q. (?C. (&0 <= C /\ (!r. &1 <= r ==> Q r <= C * r pow 2))) <=>
372 (?C. ( (!r. &1 <= r ==> Q r <= C * r pow 2)))`,
376 (EXISTS_TAC `C:real`);
379 (EXISTS_TAC `abs(C)`);
380 (REWRITE_TAC[REAL_ARITH `&0 <= abs C`]);
382 (ASSUME_TAC (REAL_ARITH `C <= abs C`));
383 (MATCH_MP_TAC REAL_LE_TRANS);
384 (EXISTS_TAC `C * r pow 2`);
387 (REWRITE_TAC[REAL_ARITH `a * b <= c * b <=> &0 <= (c - a) * b`]);
388 (MATCH_MP_TAC REAL_LE_MUL);
389 (REWRITE_TAC[REAL_LE_POW_2] THEN ASM_REAL_ARITH_TAC)]);;
391 let negligible_fun_any_C = prove(
392 `!f S. negligible_fun_0 f S <=>
393 (?C. (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`,
394 REWRITE_TAC[Pack_defs.negligible_fun_0;Pack_defs.negligible_fun_p;pos_lemma]);;