legacy/oldpacking/packing/development/Backup/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_beta_bump.hl                                                          *)
  13 (* sum_gammaX_lmfun_estimate.hl                                              *)
  14 (* ========================================================================= *)
  15
  16 let UPFZBZM_concl =
  17    `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\
  18          TSKAJXY_statement /\
  19          lmfun_inequality V ==>
  20     (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
  21
  22 let FCC_COMPATABILITY_FUNC_concl =
  23  `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\
  24    TSKAJXY_statement /\
  25    lmfun_inequality V /\ G = (\u. --vol(voronoi_open V u) +
  26    &8 * mm1 - &8 * mm2 * sum { v | v IN V /\ ~(u=v) /\ dist(u,v) <= &2*h0 }
  27    (\v. lmfun (hl [u;v])))
  28    ==> fcc_compatible G V`;;
  29
  30 let NEGLIGIBLE_FUNC_concl =
  31   `!V. saturated V /\
  32        packing V /\
  33        cell_cluster_estimate V /\
  34        TSKAJXY_statement /\
  35        lmfun_inequality V /\
  36        G =
  37        (\u. --vol (voronoi_open V u) +
  38             &8 * mm1 -
  39             &8 *
  40             mm2 *
  41             sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
  42             (\v. lmfun (hl [u; v])))
  43        ==> negligible_fun_0 G V`;;
  44
  45 (* ========================================================================= *)
  46 (*                            THE THEOREM                                    *)
  47 (* ========================================================================= *)
  48
  49 (* PART 1 OF THE LEMMA *)
  50
  51 let FCC_COMPATABILITY_FUNC = prove_by_refinement (
  52  FCC_COMPATABILITY_FUNC_concl,
  53 [(REWRITE_TAC[lmfun_inequality;fcc_compatible]);
  54  (REPEAT STRIP_TAC);
  55  (ASM_REWRITE_TAC[Pack2.MEASURE_VORONOI_CLOSED_OPEN]);
  56  (ASM_REWRITE_TAC[REAL_ARITH `a + --a + b - c = b - c`]);
  57  (MATCH_MP_TAC (REAL_ARITH
  58   `x = &8 * mm1 - &8 * (&12 * mm2) /\ y <= &8 * (&12 * mm2) ==>
  59    x <= &8 * mm1 - y`));
  60  (STRIP_TAC);
  61  (REWRITE_TAC[SQRT_OF_32_lemma]);
  62  (REWRITE_TAC[REAL_ARITH `a * b - a * c = a * (b - c)`]);
  63  (REWRITE_TAC[m1_minus_12m2]);
  64  (MATCH_MP_TAC REAL_LE_LMUL);
  65  (REWRITE_TAC[REAL_ARITH `&0 <= &8`]);
  66  (REWRITE_TAC[REAL_ARITH `&12 * mm2 = mm2 * &12`]);
  67  (MATCH_MP_TAC REAL_LE_LMUL);
  68  (REWRITE_TAC[ZERO_LE_MM2_LEMMA]);
  69  (ASM_MESON_TAC[])]);;
  70
  71
  72
  73 (* ========================================================================= *)
  74 (* PART 2 OF THE LEMMA *)
  75 (* ========================================================================= *)
  76
  77 let NEGLIGIBLE_FUNC = prove_by_refinement (
  78  NEGLIGIBLE_FUNC_concl,
  79 [(REWRITE_TAC[negligible_fun_0; negligible_fun_any_C]);
  80  (REPEAT STRIP_TAC);
  81
  82  (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL1));
  83  (STRIP_TAC);
  84  (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL2));
  85  (STRIP_TAC);
  86  (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL4));
  87  (STRIP_TAC);
  88
  89  (MP_TAC (SPEC `V:real^3->bool` SUM_GAMMAX_LMFUN_ESTIMATE));
  90  (STRIP_TAC);
  91
  92  (NEW_GOAL
  93    `!r. saturated V /\ packing V /\ &1 <= r
  94           ==> c''' * r pow 2 <=
  95               sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
  96               (\X. gammaX V X lmfun)`);
  97  (REPEAT STRIP_TAC);
  98  (FIRST_ASSUM MATCH_MP_TAC);
  99  (ASM_REWRITE_TAC[]);
 100  (UP_ASM_TAC THEN REWRITE_TAC[gammaX] THEN STRIP_TAC);
 101
 102  (EXISTS_TAC `--c''' - c - c' - c''`);
 103  (REPEAT STRIP_TAC);
 104
 105  (ABBREV_TAC `f1 =  (\u:real^3. --vol (voronoi_open V u))`);
 106  (ABBREV_TAC `f2 =  (\u:real^3.  &8 * mm1 -  &8 * mm2 *
 107                      sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 108                      (\v. lmfun (hl [u; v])))`);
 109  (REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) G =
 110                  sum (V INTER ball (vec 0,r)) f1 +
 111                  sum (V INTER ball (vec 0,r)) f2`);
 112  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "f1" THEN EXPAND_TAC "f2");
 113  (MATCH_MP_TAC SUM_ADD);
 114  (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
 115  (ABBREV_TAC `f3 =  (\u:real^3.  &8 * mm1)`);
 116  (ABBREV_TAC `f4 =  (\u:real^3.  &8 * mm2 *
 117                      sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 118                      (\v. lmfun (hl [u; v])))`);
 119  (REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) f2 =
 120                  sum (V INTER ball (vec 0,r)) f3 -
 121                  sum (V INTER ball (vec 0,r)) f4`);
 122  (EXPAND_TAC "f2" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f4");
 123  (MATCH_MP_TAC SUM_SUB);
 124  (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
 125  (EXPAND_TAC "f4" THEN DEL_TAC THEN
 126    ASM_SIMP_TAC[SUM_NEG;SUM_CONST;SUM_LMUL;FINITE_PACK_LEMMA]);
 127  (ABBREV_TAC `f5 =  (\u:real^3.
 128                      sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 129                      (\v. lmfun (hl [u; v])))`);
 130  (ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);
 131  (ABBREV_TAC `T1 = sum B vol`);
 132  (ABBREV_TAC `T2 = --(&2 * mm1 / pi) * sum B (total_solid V)`);
 133  (ABBREV_TAC `T3 = (&8 * mm2 / pi) * sum B (\X. sum (edgeX V X)
 134                      (\({u, v}). if {u, v} IN edgeX V X
 135                                then dihX V X (u,v) * lmfun (hl [u; v])
 136                                else &0))`);
 137
 138  (NEW_GOAL `sum (V:real^3->bool INTER ball (vec 0,r)) f1 <= --T1 - c * r pow 2`);
 139  (EXPAND_TAC "T1" THEN EXPAND_TAC "B");
 140  (EXPAND_TAC "f1");
 141  (REWRITE_TAC[SUM_NEG; REAL_ARITH `-- a <= --b - c <=> b + c <= a`]);
 142  (FIRST_ASSUM MATCH_MP_TAC);
 143  (ASM_REWRITE_TAC[]);
 144
 145  (NEW_GOAL
 146   `sum (V:real^3->bool INTER ball (vec 0,r)) f3 <= --T2 - c' * r pow 2`);
 147  (EXPAND_TAC "T2" THEN EXPAND_TAC "B");
 148  (EXPAND_TAC "f3");
 149  (REWRITE_TAC[SUM_NEG; REAL_ARITH `a <= --(-- b * d) - c<=> a + c <= b * d`]);
 150  (REWRITE_WITH `sum (V INTER ball (vec 0,r)) (\u:real^3. &8 * mm1) =
 151    &(CARD (V INTER ball (vec 0,r))) * (&8 * mm1)`);
 152  (MATCH_MP_TAC SUM_CONST);
 153  (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
 154  (FIRST_ASSUM MATCH_MP_TAC);
 155  (ASM_REWRITE_TAC[]);
 156
 157  (NEW_GOAL `T3 + c'' * r pow 2 <=
 158    &8 * mm2 * sum (V:real^3->bool INTER ball (vec 0,r)) f5`);
 159  (EXPAND_TAC "T3" THEN EXPAND_TAC "B");
 160
 161  (FIRST_ASSUM MATCH_MP_TAC);
 162  (ASM_REWRITE_TAC[]);
 163
 164  (MATCH_MP_TAC (REAL_ARITH `(?s. A <= s /\ s <= b) ==> A <= b`));
 165  (EXISTS_TAC `--T1 + --T2 + --T3  - (c + c' + c'') * r pow 2`);
 166  (STRIP_TAC);
 167  (ASM_REAL_ARITH_TAC);
 168  (REWRITE_TAC[REAL_ARITH
 169    `--T1 + --T2 + --T3 - (c + c' + c'') * r pow 2 <=
 170    (--c''' - c - c' - c'') * r pow 2
 171    <=> c''' * r pow 2 <= T1 + T2 + T3`]);
 172  (REWRITE_WITH `T1 + T2 + T3 =
 173                  sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
 174                  (\X. gammaX V X lmfun)`);
 175  (ASM_REWRITE_TAC[]);
 176  (REWRITE_TAC[gammaX]);
 177  (NEW_GOAL `FINITE (B:(real^3->bool)->bool)`);
 178  (EXPAND_TAC "B");
 179  (ASM_SIMP_TAC [FINITE_MCELL_SET_LEMMA]);
 180  (ASM_SIMP_TAC[SUM_ADD; SUM_SUB; SUM_LMUL; ETA_AX]);
 181  (EXPAND_TAC "T2");
 182  (REAL_ARITH_TAC);
 183  (FIRST_ASSUM MATCH_MP_TAC);
 184  (ASM_REWRITE_TAC[])]);;
 185
 186
 187 (* ========================================================================= *)
 188 (*             Main theorm                                                   *)
 189 (* ========================================================================= *)
 190
 191 let UPFZBZM = prove (UPFZBZM_concl,
 192  (REPEAT STRIP_TAC) THEN (ABBREV_TAC `G = (\u. --vol (voronoi_open V u) +
 193               &8 * mm1 -
 194               &8 *
 195               mm2 *
 196               sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 197               (\v. lmfun (hl [u; v])))`) THEN
 198  (EXISTS_TAC `G:real^3->real`) THEN
 199  (ASM_MESON_TAC[NEGLIGIBLE_FUNC;FCC_COMPATABILITY_FUNC]));;
 200
 201