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;;