text_formalization/packing/KIZHLTL.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*      Authour   : VU KHAC KY                                               *)
   5 (*      Book lemma: KIZHLTL                                                  *)
   6 (*      Chaper    : Packing (Marchal cells)                                  *)
   7 (*                                                                           *)
   8 (* ========================================================================= *)
   9 (* KIZHLTL1                                                                  *)
  10 (* ========================================================================  *)
  11
  12 module Kizhltl = struct
  13
  14
  15 open Sphere;;
  16 open Euler_main_theorem;;
  17 open Pack_defs;;
  18 open Pack_concl;;
  19 open Pack1;;
  20 open Pack2;;
  21 open Packing3;;
  22 open Rogers;;
  23 open Vukhacky_tactics;;
  24 open Marchal_cells;;
  25 open Emnwuus;;
  26 (* open Marchal_cells_2;; *)
  27 open Marchal_cells_2_new;;
  28 open Urrphbz1;;
  29 open Lepjbdj;;
  30 open Hdtfnfz;;
  31 open Rvfxzbu;;
  32 open Sltstlo;;
  33 open Urrphbz2;;
  34 open Urrphbz3;;
  35 open Ynhyjit;;
  36 open Njiutiu;;
  37 open Tezffsk;;
  38 open Qzksykg;;
  39 open Ddzuphj;;
  40 open Ajripqn;;
  41 open Qzyzmjc;;
  42 open Upfzbzm_support_lemmas;;
  43 open Marchal_cells_3;;
  44 open Grutoti;;
  45
  46 let KIZHLTL1 = prove_by_refinement (KIZHLTL1_concl,
  47
  48 [(GEN_TAC);
  49  (ASM_CASES_TAC `saturated V /\ packing (V:real^3->bool)`);
  50  (UP_ASM_TAC THEN STRIP_TAC);
  51
  52
  53  (NEW_GOAL `!r. &1 <= r
  54          ==> sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol <=
  55              vol (ball (vec 0, r))`);
  56  (REPEAT STRIP_TAC);
  57  (ABBREV_TAC `S = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
  58  (REWRITE_WITH `sum S vol = vol (UNIONS S)`);
  59  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
  60  (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS);
  61  (REPEAT STRIP_TAC);
  62  (EXPAND_TAC "S");
  63  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
  64  (REWRITE_TAC[GSYM HAS_MEASURE_MEASURE]);
  65  (UP_ASM_TAC THEN EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
  66  (REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
  67  (ASM_REWRITE_TAC[]);
  68  (MATCH_MP_TAC MEASURABLE_MCELL);
  69  (ASM_REWRITE_TAC[]);
  70  (UP_ASM_TAC THEN REWRITE_TAC[IN]);
  71
  72  (ASM_CASES_TAC `~NULLSET (s INTER t)`);
  73  (NEW_GOAL `F`);
  74  (UNDISCH_TAC `s:real^3->bool IN S` THEN UNDISCH_TAC `t:real^3->bool IN S`);
  75  (EXPAND_TAC "S" THEN REWRITE_TAC[IN;IN_ELIM_THM]);
  76  (REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
  77  (NEW_GOAL `s = t:real^3->bool`);
  78  (REWRITE_TAC[ASSUME `t = mcell i V ul`; ASSUME `s = mcell i' V ul'`]);
  79  (ABBREV_TAC `j = if i <= 4 then i else 4`);
  80  (ABBREV_TAC `j' = if i' <= 4 then i' else 4`);
  81  (REWRITE_WITH `mcell i V ul = mcell j V ul`);
  82  (EXPAND_TAC "j" THEN COND_CASES_TAC);
  83  (REFL_TAC);
  84  (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
  85    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
  86  (REWRITE_WITH `mcell i' V ul' = mcell j' V ul'`);
  87  (EXPAND_TAC "j'" THEN COND_CASES_TAC);
  88  (REFL_TAC);
  89  (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
  90    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
  91  (REWRITE_WITH `j' = j /\ mcell j' V ul' = mcell j V ul`);
  92  (MATCH_MP_TAC Ajripqn.AJRIPQN);
  93
  94  (REPEAT STRIP_TAC);
  95  (ASM_REWRITE_TAC[]);
  96  (ASM_REWRITE_TAC[]);
  97  (ASM_MESON_TAC[IN]);
  98  (ASM_MESON_TAC[IN]);
  99  (EXPAND_TAC "j'" THEN COND_CASES_TAC);
 100  (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `i <= 4 <=> i=0\/i=1\/i=2\/i=3\/i=4`]
 101    THEN SET_TAC[]);
 102  (SET_TAC[]);
 103  (EXPAND_TAC "j" THEN COND_CASES_TAC);
 104  (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `i <= 4 <=> i=0\/i=1\/i=2\/i=3\/i=4`]
 105    THEN SET_TAC[]);
 106  (SET_TAC[]);
 107  (UP_ASM_TAC);
 108  (REWRITE_WITH `mcell j V ul = mcell i V ul`);
 109  (EXPAND_TAC "j" THEN COND_CASES_TAC);
 110  (REFL_TAC);
 111  (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
 112    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
 113  (REWRITE_WITH `mcell j' V ul' = mcell i' V ul'`);
 114  (EXPAND_TAC "j'" THEN COND_CASES_TAC);
 115  (REFL_TAC);
 116  (ASM_SIMP_TAC[ARITH_RULE `~(i <= 4) ==> i >= 4`;
 117    ARITH_RULE `4 >= 4`; MCELL_EXPLICIT]);
 118  (ASM_MESON_TAC[]);
 119  (ASM_MESON_TAC[]);
 120  (ASM_MESON_TAC[]);
 121  (ASM_MESON_TAC[]);
 122
 123  (MATCH_MP_TAC MEASURE_SUBSET);
 124  (REWRITE_TAC[MEASURABLE_BALL]);
 125  (REPEAT STRIP_TAC);
 126  (EXPAND_TAC "S" THEN MATCH_MP_TAC MEASURABLE_UNIONS);
 127  (REPEAT STRIP_TAC);
 128  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 129  (UP_ASM_TAC THEN REWRITE_TAC[IN;IN_ELIM_THM; mcell_set]);
 130  (REPEAT STRIP_TAC);
 131  (ASM_SIMP_TAC[MEASURABLE_MCELL]);
 132  (EXPAND_TAC "S" THEN SET_TAC[]);
 133
 134 (* ----------------------------------------------------------------------- *)
 135
 136  (NEW_GOAL `?c. !r. &1 <= r
 137          ==> vol (ball (vec 0, r)) + c * r pow 2 <=
 138             sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 139  (EXISTS_TAC `-- (&24 / &3) * pi`);
 140  (REPEAT STRIP_TAC);
 141
 142  (ASM_CASES_TAC `r < &6`);
 143  (NEW_GOAL `&0 <= sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 144  (MATCH_MP_TAC SUM_POS_LE);
 145  (ASM_SIMP_TAC[Packing3.KIUMVTC]);
 146  (REPEAT STRIP_TAC);
 147  (MATCH_MP_TAC MEASURE_POS_LE);
 148  (ASM_SIMP_TAC[Pack1.measurable_voronoi]);
 149
 150  (NEW_GOAL `vol (ball ((vec 0):real^3,r)) + (--(&24 / &3) * pi) * r pow 2 <= &0`);
 151  (REWRITE_TAC[REAL_ARITH `a + (--b * c) * d <= &0 <=> a <= b * c * d`]);
 152  (ASM_SIMP_TAC [VOLUME_BALL; REAL_ARITH `&1 <= r ==> &0 <= r`]);
 153  (REWRITE_TAC[REAL_ARITH `&4 / &3 * pi * r pow 3 <= &24 / &3 * pi * r pow 2
 154    <=> &0 <= &4 / &3 * pi * r pow 2 * (&6 - r)`]);
 155  (MATCH_MP_TAC REAL_LE_MUL);
 156  (STRIP_TAC);
 157  (MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC);
 158  (MATCH_MP_TAC REAL_LE_MUL);
 159  (REWRITE_TAC[PI_POS_LE]);
 160  (MATCH_MP_TAC REAL_LE_MUL);
 161  (REWRITE_TAC[REAL_LE_POW_2]);
 162  (ASM_REAL_ARITH_TAC);
 163  (ASM_REAL_ARITH_TAC);
 164
 165
 166  (NEW_GOAL `vol (ball (vec 0,r - &2)) <=
 167    sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 168  (REWRITE_WITH
 169    `sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u)) =
 170     sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_closed V u))`);
 171  (MATCH_MP_TAC SUM_EQ);
 172  (REPEAT STRIP_TAC);
 173  (REWRITE_TAC[BETA_THM]);
 174  (REWRITE_TAC[GSYM Pack2.MEASURE_VORONOI_CLOSED_OPEN]);
 175
 176  (ABBREV_TAC `S:real^3->bool = V INTER ball (vec 0, r)`);
 177  (ABBREV_TAC `g = (\t:real^3. voronoi_closed V t)`);
 178
 179  (REWRITE_WITH `sum S (\u:real^3. vol (voronoi_closed V u)) = sum S (\t. vol (g t))`);
 180  (EXPAND_TAC "g" THEN REWRITE_TAC[]);
 181  (REWRITE_WITH `sum S (\t:real^3. vol (g t)) = measure (UNIONS (IMAGE g S))`);
 182  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 183  (MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNIONS_IMAGE);
 184  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "g");
 185  (REPEAT STRIP_TAC);
 186  (EXPAND_TAC "S");
 187  (ASM_SIMP_TAC[Packing3.KIUMVTC]);
 188  (MATCH_MP_TAC Pack2.MEASURABLE_VORONOI_CLOSED);
 189  (ASM_REWRITE_TAC[]);
 190  (MATCH_MP_TAC Pack2.NEGLIGIBLE_INTER_VORONOI_CLOSED);
 191  (ASM_SET_TAC[]);
 192  (EXPAND_TAC "g" THEN REWRITE_TAC[IMAGE]);
 193  (MATCH_MP_TAC MEASURE_SUBSET);
 194  (REWRITE_TAC[MEASURABLE_BALL]);
 195  (REPEAT STRIP_TAC);
 196  (MATCH_MP_TAC MEASURABLE_UNIONS);
 197  (STRIP_TAC);
 198  (MATCH_MP_TAC FINITE_IMAGE_EXPAND);
 199  (EXPAND_TAC "S");
 200  (ASM_SIMP_TAC[Packing3.KIUMVTC]);
 201
 202  (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 203  (ASM_REWRITE_TAC[]);
 204  (MATCH_MP_TAC Pack2.MEASURABLE_VORONOI_CLOSED);
 205  (ASM_REWRITE_TAC[]);
 206  (REWRITE_TAC[SUBSET; IN_BALL; IN_UNIONS]);
 207  (REPEAT STRIP_TAC);
 208  (MP_TAC (ASSUME `saturated (V:real^3->bool)`));
 209  (REWRITE_TAC[saturated] THEN STRIP_TAC);
 210  (NEW_GOAL `?y. y IN V /\ dist (x:real^3,y) < &2`);
 211  (ASM_MESON_TAC[]);
 212  (UP_ASM_TAC THEN STRIP_TAC);
 213  (NEW_GOAL `?v:real^3. v IN V /\ x IN voronoi_closed V v`);
 214  (MATCH_MP_TAC Packing3.TIWWFYQ);
 215  (ASM_REWRITE_TAC[]);
 216  (UP_ASM_TAC THEN STRIP_TAC);
 217
 218  (EXISTS_TAC `voronoi_closed V (v:real^3)`);
 219  (ASM_REWRITE_TAC[]);
 220
 221  (ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
 222  (EXISTS_TAC `v:real^3`);
 223  (STRIP_TAC);
 224  (EXPAND_TAC "S" THEN REWRITE_TAC[IN_INTER]);
 225  (ASM_REWRITE_TAC[IN_BALL]);
 226
 227  (NEW_GOAL `dist (vec 0,v) <= dist (vec 0,x) + dist (x, v:real^3)`);
 228  (REWRITE_TAC[DIST_TRIANGLE]);
 229  (NEW_GOAL `dist (x, v:real^3) < &2`);
 230  (NEW_GOAL `dist (x, v) <= dist (x, y:real^3)`);
 231  (UNDISCH_TAC `x:real^3 IN voronoi_closed V v`);
 232  (REWRITE_TAC[IN; voronoi_closed; IN_ELIM_THM]);
 233  (STRIP_TAC);
 234  (FIRST_ASSUM MATCH_MP_TAC);
 235  (ASM_SET_TAC[]);
 236  (ASM_REAL_ARITH_TAC);
 237  (ASM_REAL_ARITH_TAC);
 238  (REFL_TAC);
 239
 240  (NEW_GOAL `vol (ball (vec 0,r)) + (--(&24 / &3) * pi) * r pow 2 <=
 241              vol (ball (vec 0,r - &2))`);
 242  (ASM_SIMP_TAC[VOLUME_BALL; REAL_ARITH `~(r < &6) ==> &0 <= r`;
 243    REAL_ARITH `~(r < &6) ==> &0 <= (r - &2)` ]);
 244  (REWRITE_TAC[REAL_ARITH
 245  `&4 / &3 * pi * r pow 3 + (--(&24 / &3) * pi) * r pow 2 <=
 246   &4 / &3 * pi * (r - &2) pow 3 <=>
 247   &0 <= &4 / &3 * pi * (&12 * r - &8)`]);
 248  (MATCH_MP_TAC REAL_LE_MUL);
 249  (STRIP_TAC);
 250  (MATCH_MP_TAC REAL_LE_DIV THEN REAL_ARITH_TAC);
 251  (MATCH_MP_TAC REAL_LE_MUL);
 252  (STRIP_TAC);
 253  (REWRITE_TAC[PI_POS_LE]);
 254  (NEW_GOAL `&12 * r >= &72`);
 255  (ASM_REAL_ARITH_TAC);
 256  (ASM_REAL_ARITH_TAC);
 257
 258  (ASM_REAL_ARITH_TAC);
 259  (UP_ASM_TAC THEN STRIP_TAC);
 260
 261  (EXISTS_TAC `c:real`);
 262  (REPEAT STRIP_TAC);
 263
 264  (NEW_GOAL `sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol <=
 265               vol (ball (vec 0,r))`);
 266  (ASM_SIMP_TAC[]);
 267  (NEW_GOAL `vol (ball (vec 0,r)) + c * r pow 2 <=
 268             sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 269  (ASM_SIMP_TAC[]);
 270  (ABBREV_TAC `a1 = sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol`);
 271  (ABBREV_TAC `a2 = vol (ball ((vec 0):real^3,r))`);
 272  (ABBREV_TAC `a3 = sum (V INTER ball (vec 0,r)) (\u:real^3. vol (voronoi_open V u))`);
 273  (ASM_REAL_ARITH_TAC);
 274
 275  (EXISTS_TAC `&0`);
 276  (REPEAT STRIP_TAC);
 277  (NEW_GOAL `F`);
 278  (ASM_MESON_TAC[]);
 279  (ASM_MESON_TAC[])]);;
 280
 281 (* ======================================================================== *)
 282 (* KIZHLTL2                                                                 *)
 283 (* ======================================================================== *)
 284
 285 let KIZHLTL2 = prove_by_refinement (KIZHLTL2_concl,
 286
 287 [(REPEAT STRIP_TAC);
 288  (ASM_CASES_TAC `saturated V /\ packing V`);
 289  (NEW_GOAL
 290   `?C. !r. &1 <= r ==>
 291    &(CARD (V INTER ball ((vec 0):real^3,r) DIFF V INTER ball (vec 0,r - &8))) <=
 292    C * r pow 2`);
 293  (REWRITE_WITH `!r p. V INTER ball (p:real^3,r) DIFF V INTER ball (p,r - &8)
 294     = V INTER ball (p:real^3,r + &0) DIFF V INTER ball (p,r - &8)`);
 295  (ASM_REWRITE_TAC[REAL_ARITH `a + &0 = a`]);
 296  (ASM_SIMP_TAC[PACKING_BALL_BOUNDARY]);
 297  (TAKE_TAC);
 298  (EXISTS_TAC `(&2 * mm1 / pi) * (&4 * pi) * (--C)`);
 299  (REPEAT STRIP_TAC);
 300  (NEW_GOAL `&(CARD (V INTER ball ((vec 0):real^3,r) DIFF
 301                      V INTER ball (vec 0,r - &8))) <= C * r pow 2`);
 302  (ASM_SIMP_TAC[]);
 303  (NEW_GOAL `total_solid V = (\X. total_solid V X)`);
 304  (REWRITE_TAC[GSYM ETA_AX]);
 305  (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
 306  (REWRITE_TAC[total_solid]);
 307  (ABBREV_TAC `B = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 308  (NEW_GOAL `FINITE (B:(real^3->bool) ->bool)`);
 309  (EXPAND_TAC "B" THEN MATCH_MP_TAC FINITE_MCELL_SET_LEMMA);
 310  (ASM_REWRITE_TAC[]);
 311  (ABBREV_TAC `A1:real^3->bool = V INTER ball (vec 0,r)`);
 312  (ABBREV_TAC `A2:real^3->bool = V INTER ball (vec 0,r - &8)`);
 313  (NEW_GOAL `FINITE (A1:real^3->bool)`);
 314  (EXPAND_TAC "A1" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
 315  (ASM_REWRITE_TAC[]);
 316  (NEW_GOAL `FINITE (A2:real^3->bool)`);
 317  (EXPAND_TAC "A2" THEN MATCH_MP_TAC FINITE_PACK_LEMMA);
 318  (ASM_REWRITE_TAC[]);
 319
 320  (NEW_GOAL `sum B (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X))
 321           <= sum B (\X. sum (VX V X) (\x. sol x X))`);
 322  (MATCH_MP_TAC SUM_LE);
 323  (ASM_REWRITE_TAC[BETA_THM]);
 324  (REPEAT STRIP_TAC);
 325  (MATCH_MP_TAC SUM_SUBSET_SIMPLE);
 326  (REPEAT STRIP_TAC);
 327  (REWRITE_TAC[VX] THEN COND_CASES_TAC);
 328  (REWRITE_TAC[FINITE_EMPTY]);
 329  (LET_TAC);
 330  (COND_CASES_TAC);
 331  (REWRITE_TAC[FINITE_EMPTY]);
 332  (REWRITE_TAC[FINITE_SET_OF_LIST]);
 333  (SET_TAC[]);
 334  (REWRITE_TAC[BETA_THM]);
 335
 336  (UNDISCH_TAC `x:real^3->bool IN B`);
 337  (EXPAND_TAC "B" THEN REWRITE_TAC[IN; IN_ELIM_THM; mcell_set_2]);
 338  (REPEAT STRIP_TAC);
 339  (ASM_REWRITE_TAC[]);
 340
 341  (NEW_GOAL `eventually_radial x' (mcell i V ul)`);
 342  (MATCH_MP_TAC Urrphbz2.URRPHBZ2);
 343  (ASM_REWRITE_TAC[]);
 344  (SUBGOAL_THEN `x' IN (VX V x)` MP_TAC);
 345  (ASM_SET_TAC[]);
 346  (REWRITE_TAC[VX]);
 347  (COND_CASES_TAC);
 348  (SET_TAC[]);
 349  (LET_TAC);
 350  (COND_CASES_TAC);
 351  (SET_TAC[]);
 352  (STRIP_TAC);
 353
 354  (UNDISCH_TAC `cell_params V x = k,ul'`);
 355  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 356  (REWRITE_TAC[cell_params]);
 357  (ABBREV_TAC `P = (\(k,ul). k <= 4 /\ ul IN barV V 3 /\ x = mcell k V ul)`);
 358  (DISCH_TAC);
 359  (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);
 360  (ASM_REWRITE_TAC[]);
 361  (MATCH_MP_TAC SELECT_AX);
 362  (EXISTS_TAC `(i:num,ul:(real^3)list)`);
 363  (EXPAND_TAC "P");
 364  (REWRITE_TAC[BETA_THM]);
 365  (REWRITE_TAC[IN] THEN ASM_REWRITE_TAC[]);
 366  (UP_ASM_TAC THEN EXPAND_TAC "P" THEN REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
 367  (NEW_GOAL `set_of_list (truncate_simplex (k - 1) ul') SUBSET V:real^3->bool`);
 368  (MATCH_MP_TAC Packing3.BARV_SUBSET);
 369  (EXISTS_TAC `k - 1`);
 370  (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
 371  (EXISTS_TAC `3`);
 372  (STRIP_TAC);
 373  (ASM_SET_TAC[]);
 374  (ASM_ARITH_TAC);
 375  (ASM_SET_TAC[]);
 376
 377
 378  (UP_ASM_TAC THEN REWRITE_TAC[eventually_radial]);
 379  (REPEAT STRIP_TAC);
 380  (REWRITE_WITH `sol x' (mcell i V ul) =
 381   &3 * vol ((mcell i V ul) INTER normball x' r') / r' pow 3`);
 382  (MATCH_MP_TAC sol);
 383  (ASM_REWRITE_TAC[GSYM Marchal_cells_2_new.RADIAL_VS_RADIAL_NORM; NORMBALL_BALL]);
 384  (MATCH_MP_TAC MEASURABLE_INTER);
 385  (ASM_SIMP_TAC[MEASURABLE_BALL; MEASURABLE_MCELL]);
 386  (MATCH_MP_TAC REAL_LE_MUL);
 387  (REWRITE_TAC[REAL_ARITH `&0 <= &3`] THEN MATCH_MP_TAC REAL_LE_DIV);
 388  (STRIP_TAC);
 389  (MATCH_MP_TAC MEASURE_POS_LE);
 390  (MATCH_MP_TAC MEASURABLE_INTER);
 391  (ASM_SIMP_TAC[MEASURABLE_BALL; NORMBALL_BALL; MEASURABLE_MCELL]);
 392  (MATCH_MP_TAC REAL_POW_LE THEN ASM_REAL_ARITH_TAC);
 393
 394 (* ------------------------------------------------------------------------- *)
 395
 396  (NEW_GOAL `sum B  (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X)) =
 397              sum A2 (\u. sum  {X | X IN B /\ VX V X u} (\X. sol u X))`);
 398  (MATCH_MP_TAC SUM_SUM_RESTRICT);
 399  (ASM_REWRITE_TAC[]);
 400
 401  (NEW_GOAL `sum A2 (\u. sum {X | X IN B /\ VX V X u} (\X. sol u X)) =
 402              sum A2 (\u. sum {X | mcell_set V X /\ u IN VX V X}
 403                     (\X. sol u X))`);
 404  (MATCH_MP_TAC SUM_EQ);
 405  (EXPAND_TAC "A2" THEN REWRITE_TAC[IN_INTER; IN_DIFF] THEN
 406    REWRITE_TAC[IN_BALL; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 407  (REWRITE_WITH `{X | B X /\ VX V X x} =
 408                  {X | mcell_set V X /\ VX V X x}`);
 409  (REWRITE_TAC[SET_RULE `a = b <=> a SUBSET b /\ b SUBSET a`]);
 410  (STRIP_TAC);
 411  (EXPAND_TAC "B");
 412  (SET_TAC[]);
 413  (REWRITE_WITH `!x:real^3->bool. B x <=> x IN B`);
 414  (REWRITE_TAC[IN]);
 415  (EXPAND_TAC "B" THEN REWRITE_TAC[SUBSET; IN_INTER; IN_DIFF] THEN
 416    REWRITE_TAC[IN_BALL; IN; IN_ELIM_THM]);
 417  (REWRITE_TAC[MESON[] `A /\ X /\ Y ==> (B /\ A) /\ X /\ Y <=> A /\ X /\ Y ==> B`]);
 418  (REPEAT STRIP_TAC);
 419  (NEW_GOAL `x IN VX V x'`);
 420  (ASM_REWRITE_TAC[IN]);
 421  (NEW_GOAL `~NULLSET x'`);
 422  (UNDISCH_TAC `x IN VX V x'` THEN REWRITE_TAC[VX] THEN COND_CASES_TAC);
 423  (SET_TAC[]);
 424  (MESON_TAC[]);
 425
 426  (NEW_GOAL `dist (vec 0, x'':real^3) <= dist (vec 0, x) + dist (x, x'')`);
 427  (REWRITE_TAC[DIST_TRIANGLE]);
 428  (NEW_GOAL `?p. x' SUBSET ball (p:real^3,&4)`);
 429  (MATCH_MP_TAC MCELL_SUBSET_BALL_4);
 430  (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
 431  (UP_ASM_TAC THEN REWRITE_TAC[SUBSET; IN_BALL] THEN STRIP_TAC);
 432  (NEW_GOAL `dist (x, x'':real^3) <= dist (x, p) + dist (p, x'')`);
 433  (REWRITE_TAC[DIST_TRIANGLE]);
 434  (NEW_GOAL `dist (x, p:real^3) < &4`);
 435  (ONCE_REWRITE_TAC[DIST_SYM]);
 436  (FIRST_ASSUM MATCH_MP_TAC);
 437  (NEW_GOAL `VX V x' = V INTER x'`);
 438  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 439  (UNDISCH_TAC `mcell_set V x'` THEN REWRITE_TAC[mcell_set; IN_ELIM_THM] THEN STRIP_TAC);
 440  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 441  (ASM_REWRITE_TAC[]);
 442  (ASM_SET_TAC[]);
 443  (ASM_SET_TAC[]);
 444  (NEW_GOAL `dist (p:real^3,x'') < &4`);
 445  (FIRST_ASSUM MATCH_MP_TAC);
 446  (ASM_REWRITE_TAC[IN]);
 447  (ASM_REAL_ARITH_TAC);
 448  (ASM_REWRITE_TAC[]);
 449  (ASM_REWRITE_TAC[]);
 450
 451 (* ------------------------------------------------------------------------ *)
 452
 453  (UP_ASM_TAC);
 454  (REWRITE_WITH `sum A2 (\u. sum {X | mcell_set V X /\ u IN VX V X} (\X. sol u X)) = sum A2 (\u. &4 * pi)`);
 455  (MATCH_MP_TAC SUM_EQ);
 456  (REWRITE_TAC[BETA_THM] THEN REPEAT STRIP_TAC);
 457  (MATCH_MP_TAC Qzyzmjc.QZYZMJC);
 458  (ASM_REWRITE_TAC[]);
 459  (ASM_SET_TAC[]);
 460  (ASM_SIMP_TAC[SUM_CONST]);
 461  (STRIP_TAC);
 462
 463  (ABBREV_TAC `s1 = sum B (\X. sum (VX V X) (\x. sol x X))`);
 464  (NEW_GOAL `&(CARD (A2:real^3->bool)) * &4 * pi <= s1`);
 465  (ABBREV_TAC `s2 = sum B (\X. sum {u | u IN A2 /\ VX V X u} (\u. sol u X))`);
 466  (ABBREV_TAC `s3 = sum A2 (\u. sum {X | X IN B /\ VX V X u} (\X. sol u X))`);
 467  (ASM_REAL_ARITH_TAC);
 468  (NEW_GOAL `(&2 * mm1 / pi) * &(CARD (A2:real^3->bool)) * &4 * pi <= (&2 * mm1 / pi) * s1`);
 469  (REWRITE_TAC[REAL_ARITH `a * b <= a * c <=> &0 <= (c - b) * a`]);
 470  (MATCH_MP_TAC REAL_LE_MUL);
 471  (STRIP_TAC);
 472  (ASM_REAL_ARITH_TAC);
 473  (MATCH_MP_TAC REAL_LE_MUL);
 474  (STRIP_TAC);
 475  (REAL_ARITH_TAC);
 476  (MATCH_MP_TAC REAL_LE_DIV);
 477  (REWRITE_TAC[PI_POS_LE]);
 478  (NEW_GOAL `#1.012080 < mm1`);
 479  (REWRITE_TAC[Flyspeck_constants.bounds]);
 480  (UP_ASM_TAC THEN REAL_ARITH_TAC);
 481
 482  (NEW_GOAL `&(CARD (A1:real^3->bool)) * &8 * mm1 +
 483              ((&2 * mm1 / pi) * (&4 * pi) * --C) * r pow 2 <=
 484              (&2 * mm1 / pi) * &(CARD (A2:real^3->bool)) * &4 * pi`);
 485  (REWRITE_TAC[REAL_ARITH `((&2 * mm1 / pi) * (&4 * pi) * --C) * r pow 2 =
 486   (--C * r pow 2) * (&8 * mm1) * (pi / pi)`]);
 487  (REWRITE_TAC[REAL_ARITH `(&2 * mm1 / pi) * &(CARD A2) * &4 * pi =
 488   &(CARD A2) * (&8 * mm1) * (pi / pi)`]);
 489  (REWRITE_WITH `pi / pi = &1`);
 490  (MATCH_MP_TAC REAL_DIV_REFL);
 491  (MP_TAC PI_POS THEN REAL_ARITH_TAC);
 492  (REWRITE_TAC[REAL_MUL_RID; REAL_ARITH `a * b + c * b <= d * b <=>
 493   &0 <= (d - a - c) * b `]);
 494  (MATCH_MP_TAC REAL_LE_MUL);
 495  (STRIP_TAC);
 496  (REWRITE_TAC[REAL_ARITH `&0 <= a - b - (--c * x) <=> b - a <= c * x`]);
 497
 498  (NEW_GOAL `A2 SUBSET A1:real^3->bool`);
 499  (EXPAND_TAC "A1" THEN EXPAND_TAC "A2");
 500  (MATCH_MP_TAC (SET_RULE `A SUBSET B ==> V INTER A SUBSET V INTER B`));
 501  (MATCH_MP_TAC SUBSET_BALL);
 502  (REAL_ARITH_TAC);
 503  (REWRITE_WITH `&(CARD (A1:real^3->bool)) - &(CARD (A2:real^3->bool)) =
 504    &(CARD A1 - CARD A2)`);
 505  (MATCH_MP_TAC REAL_OF_NUM_SUB);
 506  (MATCH_MP_TAC CARD_SUBSET);
 507  (ASM_REWRITE_TAC[]);
 508
 509  (REWRITE_WITH `CARD (A1:real^3->bool) - CARD (A2:real^3->bool) =
 510    CARD (A1 DIFF A2)`);
 511  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 512  (MATCH_MP_TAC CARD_DIFF);
 513  (ASM_REWRITE_TAC[]);
 514  (ASM_REWRITE_TAC[]);
 515
 516  (MATCH_MP_TAC REAL_LE_MUL);
 517  (NEW_GOAL `#1.012080 < mm1`);
 518  (REWRITE_TAC[Flyspeck_constants.bounds]);
 519  (UP_ASM_TAC THEN REAL_ARITH_TAC);
 520
 521
 522  (ASM_REAL_ARITH_TAC);
 523  (EXISTS_TAC `&0`);
 524  (REPEAT STRIP_TAC);
 525  (NEW_GOAL `F`);
 526  (ASM_MESON_TAC[]);
 527  (ASM_MESON_TAC[])]);;
 528
 529 (* ======================================================================== *)
 530 (* KIZHLTL4                                                                 *)
 531 (* ======================================================================== *)
 532
 533 let KIZHLTL4_concl =
 534   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r
 535                ==> (&8 * mm2 / pi) *
 536                    sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
 537                    (\X. sum (edgeX V X)
 538                         (\({u, v}). if {u, v} IN edgeX V X
 539                                     then dihX V X (u,v) * lmfun (hl [u; v])
 540                                     else &0)) +
 541                    c * r pow 2 <=
 542                    &8 *
 543                    mm2 *
 544                    sum (V INTER ball (vec 0,r))
 545                    (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 546                         (\v. lmfun (hl [u; v])))`;;
 547
 548 let KIZHLTL4 = prove_by_refinement (KIZHLTL4_concl,
 549
 550 [(REPEAT STRIP_TAC);
 551  (ASM_CASES_TAC `saturated V /\ packing V`);
 552  (ABBREV_TAC `c = &8 * mm2 * (&0)`);
 553  (EXISTS_TAC `c:real`);  (* choose d later *)
 554
 555 (* ------------------------------------------------------------------------- *)
 556
 557  (REPEAT STRIP_TAC);
 558  (ABBREV_TAC `S1 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`);
 559  (ABBREV_TAC `V1:real^3->bool = V INTER ball (vec 0, r)`);
 560  (ABBREV_TAC `T1 = {{u,v:real^3} | u IN V1 /\ v IN V1}`);
 561
 562  (NEW_GOAL `FINITE (S1:(real^3->bool)->bool)`);
 563  (EXPAND_TAC "S1");
 564  (ASM_SIMP_TAC[FINITE_MCELL_SET_LEMMA]);
 565
 566  (NEW_GOAL `FINITE (T1:(real^3->bool)->bool)`);
 567  (EXPAND_TAC "T1");
 568  (REWRITE_TAC[GSYM set_of_list]);
 569  (MATCH_MP_TAC FINITE_SUBSET);
 570  (EXISTS_TAC `IMAGE (set_of_list) {[u; v:real^3] | u IN V1 /\ v IN V1}`);
 571  (STRIP_TAC);
 572  (MATCH_MP_TAC FINITE_IMAGE);
 573  (REWRITE_TAC[SET_RULE `{[u;v] | u IN s /\ v IN s} =
 574                          {y | ?u0 u1. u0 IN s /\ u1 IN s /\ y = [u0; u1]}`]);
 575  (MATCH_MP_TAC FINITE_LIST_KY_LEMMA_2);
 576  (EXPAND_TAC "V1" THEN MATCH_MP_TAC Packing3.KIUMVTC);
 577  (ASM_REWRITE_TAC[]);
 578  (SET_TAC[]);
 579
 580  (ABBREV_TAC
 581    `S2 = {X | X SUBSET ball (vec 0,r) /\ mcell_set V X /\ ~NULLSET X}`);
 582  (NEW_GOAL `FINITE (S2:(real^3->bool)->bool)`);
 583  (MATCH_MP_TAC FINITE_SUBSET);
 584  (EXISTS_TAC `S1:(real^3->bool)->bool`);
 585  (ASM_REWRITE_TAC[]);
 586  (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN SET_TAC[]);
 587
 588  (ABBREV_TAC `g = (\X. (\({u, v}).
 589                             if {u, v} IN edgeX V X
 590                             then dihX V X (u,v) * lmfun (hl [u; v])
 591                             else &0))`);
 592  (REWRITE_WITH
 593 `sum S1  (\X. sum (edgeX V X)
 594                  (\({u, v}). if {u, v} IN edgeX V X
 595                              then dihX V X (u,v) * lmfun (hl [u; v])
 596                              else &0)) =
 597  sum S1 (\X. sum (edgeX V X) (\({u, v}). g X {u,v}))`);
 598  (MATCH_MP_TAC SUM_EQ);
 599
 600  (EXPAND_TAC "S1" THEN REWRITE_TAC[IN_ELIM_THM; IN; mcell_set_2]);
 601  (REPEAT STRIP_TAC);
 602  (MATCH_MP_TAC SUM_EQ);
 603  (REWRITE_WITH `!x'. x' IN edgeX V x <=>
 604                       ?u v. VX V x u /\ VX V x v /\ ~(u = v) /\ x' = {u, v}`);
 605  (REWRITE_TAC[IN; IN_ELIM_THM; edgeX]);
 606  (MESON_TAC[]);
 607  (REPEAT STRIP_TAC);
 608
 609  (ABBREV_TAC `f_temp = (\u v. if edgeX V x {u, v}
 610              then dihX V x (u,v) * lmfun (hl [u; v])
 611              else &0)`);
 612  (NEW_GOAL `!u v. (f_temp:real^3->real^3->real) u v = f_temp v u`);
 613  (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);
 614  (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);
 615  (REPEAT GEN_TAC THEN COND_CASES_TAC);
 616  (COND_CASES_TAC);
 617  (REWRITE_WITH `dihX V x (u',v') = dihX V x (v',u')`);
 618  (MATCH_MP_TAC DIHX_SYM);
 619  (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);
 620  (EXISTS_TAC `i:num` THEN EXISTS_TAC `ul:(real^3)list` THEN ASM_REWRITE_TAC[]);
 621  (UP_ASM_TAC THEN MESON_TAC[]);
 622  (COND_CASES_TAC);
 623  (UP_ASM_TAC THEN MESON_TAC[]);
 624  (REFL_TAC);
 625
 626  (REWRITE_WITH `(\({u, v}). if edgeX V x {u, v}
 627              then dihX V x (u,v) * lmfun (hl [u; v])
 628              else &0) = (\({u, v}). f_temp u v)`);
 629  (EXPAND_TAC "f_temp");
 630  (REWRITE_TAC[]);
 631
 632  (REWRITE_TAC[BETA_SET_2_THM; ASSUME `x' = {u,v:real^3}`]);
 633  (REWRITE_WITH `(\({u, v}). f_temp u v) {u, v} =
 634                              (f_temp:real^3->real^3->real) u v`);
 635  (MATCH_MP_TAC BETA_PAIR_THM);
 636  (ASM_REWRITE_TAC[]);
 637
 638  (REWRITE_WITH `(g:(real^3->bool)->(real^3->bool)->real) x =
 639                  (\({u, v}). f_temp u v)`);
 640  (EXPAND_TAC "f_temp" THEN EXPAND_TAC "g" THEN REWRITE_TAC[IN]);
 641  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 642  (MATCH_MP_TAC BETA_PAIR_THM);
 643  (ASM_REWRITE_TAC[]);
 644
 645 (* ----------------------------------------------------------------------- *)
 646
 647  (REWRITE_WITH `sum S1 (\X. sum (edgeX V X) (\({u, v}). g X {u, v})) =
 648                  sum S1 (\X. sum (edgeX V X)  (g X))`);
 649  (MATCH_MP_TAC SUM_EQ);
 650  (REWRITE_TAC[] THEN REPEAT STRIP_TAC);
 651  (MATCH_MP_TAC SUM_EQ);
 652  (REWRITE_TAC[edgeX; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
 653  (ASM_REWRITE_TAC[BETA_SET_2_THM]);
 654
 655  (REWRITE_WITH `sum S1 (\X. sum (edgeX V X) (g X)) =
 656                  sum S2 (\X. sum (edgeX V X) (g X))`);
 657  (MATCH_MP_TAC SUM_SUPERSET);
 658  (STRIP_TAC);
 659  (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN SET_TAC[]);
 660  (EXPAND_TAC "S1" THEN EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 661  (REPEAT STRIP_TAC);
 662  (MATCH_MP_TAC SUM_EQ_0);
 663  (REPEAT STRIP_TAC);
 664
 665  (ABBREV_TAC `f_temp = (\u v. if edgeX V x {u, v}
 666              then dihX V x (u,v) * lmfun (hl [u; v])
 667              else &0)`);
 668  (NEW_GOAL `!u v. (f_temp:real^3->real^3->real) u v = f_temp v u`);
 669  (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);
 670  (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);
 671  (REPEAT GEN_TAC THEN COND_CASES_TAC);
 672  (COND_CASES_TAC);
 673  (REWRITE_WITH `dihX V x (u,v) = dihX V x (v,u)`);
 674
 675  (MATCH_MP_TAC DIHX_SYM);
 676  (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);
 677  (UP_ASM_TAC THEN MESON_TAC[]);
 678  (COND_CASES_TAC);
 679  (UP_ASM_TAC THEN MESON_TAC[]);
 680  (REFL_TAC);
 681
 682  (REWRITE_WITH `(g:(real^3->bool)->(real^3->bool)->real) x =
 683                  (\({u, v}). f_temp u v)`);
 684  (EXPAND_TAC "f_temp" THEN EXPAND_TAC "g" THEN REWRITE_TAC[IN]);
 685  (UNDISCH_TAC `x' IN edgeX V x` THEN REWRITE_TAC[IN;IN_ELIM_THM; edgeX]);
 686  (STRIP_TAC);
 687  (ASM_SIMP_TAC[BETA_PAIR_THM]);
 688  (EXPAND_TAC "f_temp");
 689  (COND_CASES_TAC);
 690  (REWRITE_TAC[dihX]);
 691  (COND_CASES_TAC);
 692  (REAL_ARITH_TAC);
 693  (NEW_GOAL `F`);
 694  (ASM_MESON_TAC[]);
 695  (UP_ASM_TAC THEN MESON_TAC[]);
 696  (REFL_TAC);
 697
 698  (REWRITE_WITH
 699  `sum S2 (\X. sum (edgeX V X) (g X)) =
 700   sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X))`);
 701  (MATCH_MP_TAC SUM_EQ);
 702  (EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 703  (REPEAT STRIP_TAC);
 704  (AP_THM_TAC THEN AP_TERM_TAC);
 705  (REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
 706  (STRIP_TAC);
 707  (SET_TAC[]);
 708  (REWRITE_TAC[SET_RULE `A SUBSET {y | T2 y /\ A y} <=> A SUBSET T2`]);
 709  (EXPAND_TAC "T1" THEN REWRITE_TAC[SUBSET; edgeX; IN; IN_ELIM_THM]);
 710  (REPEAT STRIP_TAC);
 711  (EXPAND_TAC "V1" THEN REWRITE_TAC[IN_ELIM_THM]);
 712  (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);
 713  (REWRITE_TAC[ASSUME `x' = {u, v:real^3}`; IN_INTER;
 714                MESON[IN] `V (x:real^3) <=> x IN V`]);
 715  (NEW_GOAL `VX V x = V INTER x`);
 716  (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
 717  (UNDISCH_TAC `mcell_set V x` THEN REWRITE_TAC[mcell_set; IN; IN_ELIM_THM]);
 718  (STRIP_TAC);
 719  (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
 720  (ASM_REWRITE_TAC[]);
 721  (ASM_SET_TAC[]);
 722
 723  (REWRITE_WITH
 724   `sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X)) =
 725    sum T1 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x))`);
 726  (REWRITE_WITH
 727   `sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (g X)) =
 728    sum S2 (\X. sum {e | e IN T1 /\ edgeX V X e} (\x.g X x))`);
 729  (REWRITE_TAC[ETA_AX]);
 730  (ASM_SIMP_TAC[SUM_SUM_RESTRICT]);
 731
 732 (* May 09 - OK here *)
 733
 734  (ABBREV_TAC
 735   `T2 = {{u0:real^3, u1} | u0 IN V1 /\ u1 IN V1 /\ ~(u0 = u1) /\
 736                            hl[u0;u1] <= h0}`);
 737  (NEW_GOAL `sum T1 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x)) =
 738              sum T2 (\x. sum {X | X IN S2 /\ edgeX V X x} (\X. g X x))`);
 739  (MATCH_MP_TAC SUM_SUPERSET);
 740  (EXPAND_TAC "T1" THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM] THEN
 741    REPEAT STRIP_TAC);
 742  (SET_TAC[]);
 743  (MATCH_MP_TAC SUM_EQ_0);
 744  (EXPAND_TAC "g" THEN REPEAT STRIP_TAC);
 745  (ASM_REWRITE_TAC[]);
 746
 747  (ABBREV_TAC `f_temp = (\u v. if {u, v} IN edgeX V x'
 748              then dihX V x' (u,v) * lmfun (hl [u; v])
 749              else &0)`);
 750  (REWRITE_WITH `(\({u, v}). if {u, v} IN edgeX V x'
 751              then dihX V x' (u,v) * lmfun (hl [u; v])
 752              else &0) = (\({u, v}). f_temp u v)`);
 753  (EXPAND_TAC "f_temp");
 754  (REWRITE_TAC[]);
 755  (ASM_REWRITE_TAC[]);
 756
 757  (REWRITE_WITH `(\({u, v}). f_temp u v) {u, v} =
 758                              (f_temp:real^3->real^3->real) u v`);
 759  (MATCH_MP_TAC BETA_PAIR_THM);
 760  (ASM_REWRITE_TAC[]);
 761  (EXPAND_TAC "f_temp");
 762  (REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC);
 763  (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} ={b,a}`]);
 764  (REWRITE_WITH `dihX V x' (u',v') = dihX V x' (v',u')`);
 765  (MATCH_MP_TAC DIHX_SYM);
 766  (ASM_REWRITE_TAC[]);
 767  (UNDISCH_TAC `x' IN {X | S2 X /\ edgeX V X x}`);
 768  (EXPAND_TAC "S2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 769  (MESON_TAC[]);
 770  (NEW_GOAL `F`);
 771  (UP_ASM_TAC THEN REWRITE_TAC[]);
 772  (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`]);
 773  (ASM_REWRITE_TAC[]);
 774  (UP_ASM_TAC THEN MESON_TAC[]);
 775  (NEW_GOAL `F`);
 776  (UP_ASM_TAC THEN REWRITE_TAC[]);
 777  (ONCE_REWRITE_TAC[SET_RULE `{a,b} = {b,a}`]);
 778  (ASM_REWRITE_TAC[]);
 779  (UP_ASM_TAC THEN MESON_TAC[]);
 780  (REFL_TAC);
 781
 782  (EXPAND_TAC "f_temp");
 783  (COND_CASES_TAC);
 784
 785  (ASM_CASES_TAC `hl [u; v:real^3] <= h0`);
 786  (NEW_GOAL `F`);
 787  (UNDISCH_TAC `~(?u0 u1.
 788             (V1 u0 /\ V1 u1 /\ ~(u0 = u1) /\ hl [u0; u1] <= h0) /\
 789             x = {u0, u1:real^3})` THEN REWRITE_TAC[]);
 790  (EXISTS_TAC `u:real^3` THEN EXISTS_TAC `v:real^3`);
 791  (ASM_REWRITE_TAC[]);
 792  (UNDISCH_TAC `{u, v} IN edgeX V x'` THEN REWRITE_TAC[IN; IN_ELIM_THM; edgeX]);
 793  (REPEAT STRIP_TAC);
 794  (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
 795  (UP_ASM_TAC THEN MESON_TAC[]);
 796  (REWRITE_WITH `lmfun (hl [u; v:real^3]) = &0`);
 797  (ASM_REWRITE_TAC[lmfun]);
 798  (REAL_ARITH_TAC);
 799  (REFL_TAC);
 800
 801  (ASM_REWRITE_TAC[]);
 802 (* ==================================================================== *)
 803 (* REALLY OK Here *)
 804
 805  (MATCH_MP_TAC (REAL_ARITH `(?b. a <= b /\ b + d <= e) ==> a + d <= e`));
 806  (EXISTS_TAC `(&8 * mm2 / pi) *
 807      sum T2 (\x. sum {X | mcell_set V X /\ x IN edgeX V X} (\X. g X x))`);
 808  (STRIP_TAC);
 809  (REWRITE_TAC[REAL_ARITH `a * b <= a * c <=> &0 <= a * (c - b)`]);
 810  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 811  (MATCH_MP_TAC REAL_LE_MUL THEN STRIP_TAC);
 812  (REAL_ARITH_TAC);
 813  (MATCH_MP_TAC REAL_LE_DIV THEN SIMP_TAC[ZERO_LE_MM2_LEMMA; PI_POS_LE]);
 814  (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
 815  (MATCH_MP_TAC SUM_LE THEN REPEAT STRIP_TAC);
 816  (MATCH_MP_TAC FINITE_SUBSET);
 817  (EXISTS_TAC `T1:(real^3->bool)->bool`);
 818  (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
 819  (REWRITE_TAC[BETA_THM]);
 820  (MATCH_MP_TAC SUM_SUBSET_SIMPLE);
 821
 822  (STRIP_TAC);
 823  (REWRITE_TAC[IN] THEN MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 824  (UP_ASM_TAC THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]
 825    THEN STRIP_TAC);
 826  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 827  (REPEAT STRIP_TAC);
 828
 829  (EXPAND_TAC "S2" THEN REWRITE_TAC[IN] THEN SET_TAC[]);
 830  (REWRITE_TAC[BETA_THM]);
 831  (REWRITE_WITH `g x' x = gammaY V x' lmfun x`);
 832  (EXPAND_TAC "g" THEN REWRITE_TAC[gammaY]);
 833  (MATCH_MP_TAC gamma_y_pos_le);
 834
 835  (UP_ASM_TAC THEN ASM_REWRITE_TAC[IN_DIFF; IN; IN_ELIM_THM]);
 836  (MESON_TAC[]);
 837  (REWRITE_WITH
 838   `sum T2 (\x. sum {X | mcell_set V X /\ x IN edgeX V X} (\X. g X x)) =
 839    sum T2 (\x. &2 * pi * lmfun (radV x))`);
 840  (MATCH_MP_TAC SUM_EQ);
 841  (REPEAT STRIP_TAC);
 842  (REWRITE_TAC[BETA_THM]);
 843  (EXPAND_TAC "g");
 844
 845  (REWRITE_TAC[HL; BETA_THM; set_of_list]);
 846  (UP_ASM_TAC THEN EXPAND_TAC "T2" THEN REWRITE_TAC[IN; IN_ELIM_THM]);
 847  (STRIP_TAC);
 848
 849  (REWRITE_WITH `sum {X | mcell_set V X /\ edgeX V X x}
 850  (\X. (\({u, v}). if edgeX V X {u, v}
 851                   then dihX V X (u,v) * lmfun (radV {u, v}) else &0) x) =
 852                 sum {X | mcell_set V X /\ edgeX V X x}
 853  (\X. (if edgeX V X {u0, u1}
 854                   then dihX V X (u0,u1) * lmfun (radV {u0, u1}) else &0))`);
 855  (MATCH_MP_TAC SUM_EQ);
 856  (ASM_REWRITE_TAC[IN; IN_ELIM_THM; BETA_THM] THEN REPEAT STRIP_TAC);
 857  (ABBREV_TAC
 858   `f_temp = (\u v. if edgeX V x' {u, v}
 859                    then dihX V x' (u,v) * lmfun (radV {u, v}) else &0)`);
 860  (NEW_GOAL `!u:real^3 v:real^3.
 861             (f_temp:real^3->real^3->real) u v = f_temp v u`);
 862  (EXPAND_TAC "f_temp" THEN REWRITE_TAC[BETA_THM]);
 863  (REWRITE_TAC[HL; set_of_list; SET_RULE `{a,b} = {b,a}`]);
 864  (REPEAT GEN_TAC THEN COND_CASES_TAC);
 865  (COND_CASES_TAC);
 866  (REWRITE_WITH `dihX V x' (u,v) = dihX V x' (v,u)`);
 867
 868  (MATCH_MP_TAC DIHX_SYM);
 869  (ASM_REWRITE_TAC[IN; mcell_set; IN_ELIM_THM]);
 870  (UP_ASM_TAC THEN MESON_TAC[]);
 871  (COND_CASES_TAC);
 872  (UP_ASM_TAC THEN MESON_TAC[]);
 873  (REFL_TAC);
 874
 875  (REWRITE_WITH
 876  `(\({u, v}). if edgeX V x' {u, v}
 877               then dihX V x' (u,v) * lmfun (radV {u, v})
 878               else &0)
 879     = (\({u, v}). f_temp u v)`);
 880  (EXPAND_TAC "f_temp" THEN REWRITE_TAC[IN]);
 881  (REWRITE_WITH
 882   `(if edgeX V x' {u0, u1}
 883    then dihX V x' (u0,u1) * lmfun (radV {u0, u1}) else &0) =
 884    f_temp u0 u1`);
 885  (EXPAND_TAC "f_temp" THEN REWRITE_TAC[IN]);
 886  (MATCH_MP_TAC BETA_PAIR_THM);
 887  (ASM_REWRITE_TAC[]);
 888
 889  (NEW_GOAL `FINITE {X | mcell_set V X /\ edgeX V X x}`);
 890  (MATCH_MP_TAC Marchal_cells_3.FINITE_EDGE_X2);
 891  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);
 892  (ASM_SIMP_TAC [SUM_CASES]);
 893
 894  (REWRITE_TAC[SET_RULE
 895  `{X | X IN {X | mcell_set V X /\ edgeX V X {u0, u1}} /\ edgeX V X {u0, u1}} =
 896   {X | mcell_set V X /\ edgeX V X {u0, u1}} /\
 897   {X | X IN {X | mcell_set V X /\ edgeX V X {u0, u1}} /\
 898       ~edgeX V X {u0, u1}} = {}`; SUM_CLAUSES; REAL_ARITH `a + &0 = a`]);
 899  (REWRITE_TAC[SUM_RMUL]);
 900  (REWRITE_WITH
 901   `sum {X | mcell_set V X /\ edgeX V X {u0, u1}} (\X. dihX V X (u0,u1)) =
 902    &2 * pi`);
 903  (REWRITE_WITH
 904   `{X | mcell_set V X /\ edgeX V X {u0, u1}} =
 905    {X | mcell_set V X /\ {u0, u1} IN edgeX V X}`);
 906  (REWRITE_TAC[IN]);
 907  (MATCH_MP_TAC GRUTOTI);
 908  (ASM_REWRITE_TAC[]);
 909  (REPEAT STRIP_TAC);
 910  (ASM_SET_TAC[]);
 911  (ASM_SET_TAC[]);
 912  (NEW_GOAL `h0 < sqrt (&2)`);
 913  (REWRITE_TAC[H0_LT_SQRT2]);
 914  (ASM_REAL_ARITH_TAC);
 915  (REAL_ARITH_TAC);
 916  (REWRITE_TAC[SUM_LMUL; REAL_ARITH `(&8 * mm2 / pi) * &2 * pi * a =
 917                                      (&8 * mm2) * (pi / pi) * (&2 * a)`]);
 918  (REWRITE_WITH `pi / pi = &1`);
 919  (MATCH_MP_TAC REAL_DIV_REFL);
 920  (REWRITE_TAC[PI_NZ]);
 921  (REWRITE_TAC[REAL_ARITH `&1 * a = a`]);
 922  (EXPAND_TAC "c");
 923  (REWRITE_TAC[REAL_ARITH
 924   `(&8 * mm2) * a + (&8 * mm2 * d) * b <= &8 * mm2 * c <=>
 925    &0 <= (&8 * mm2) * (c - a - d * b)`]);
 926  (MATCH_MP_TAC REAL_LE_MUL);
 927  (SIMP_TAC[REAL_LE_MUL; REAL_ARITH `&0 <= &8`; ZERO_LE_MM2_LEMMA]);
 928  (REWRITE_TAC[REAL_ARITH `&0 <= a - b - c <=> b + c <= a`]);
 929
 930  (EXPAND_TAC "T2");
 931  (REWRITE_TAC[Marchal_cells_3.HL_2;
 932    REAL_ARITH `inv (&2) * x <= y <=> x <= &2 * y`]);
 933  (REWRITE_WITH `&2 *
 934  sum
 935  {{u0:real^3, u1} | u0 IN V1 /\ u1 IN V1 /\
 936                    ~(u0 = u1) /\ dist (u0,u1) <= &2 * h0}
 937  (\x. lmfun (radV x)) =
 938  sum
 939  {u0:real^3,u1 | u0 IN V1 /\ u1 IN V1 /\
 940                 ~(u0 = u1) /\ dist (u0,u1) <= &2 * h0}
 941  (\(u0,u1). (\x. lmfun (radV x)) {u0, u1})`);
 942  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 943  (MATCH_MP_TAC SUM_PAIR_2_SET);
 944  (EXPAND_TAC "V1");
 945  (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 946  (REWRITE_TAC[GSYM Marchal_cells_3.HL_2; HL;set_of_list]);
 947
 948  (ABBREV_TAC
 949   `t = (\u:real^3. {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0})`);
 950  (ABBREV_TAC `f_temp = (\u v. lmfun (radV {u:real^3, v}))`);
 951
 952  (REWRITE_WITH
 953 `sum V1
 954  (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v:real^3) <= &2 * h0}
 955  (\v. lmfun (radV {u, v}))) =
 956  sum V1
 957  (\u:real^3. sum
 958  ((t:real^3->real^3->bool) u) ((f_temp:real^3->real^3->real) u))`);
 959
 960  (EXPAND_TAC "f_temp" THEN EXPAND_TAC "t");
 961  (REWRITE_TAC[]);
 962
 963  (REWRITE_WITH
 964  `sum V1 (\i. sum (t i) (f_temp i)) =
 965   sum {u0:real^3,u1:real^3 | u0 IN V1 /\ u1 IN t u0} (\(u0,u1). f_temp u0 u1)`);
 966  (MATCH_MP_TAC SUM_SUM_PRODUCT);
 967  (REPEAT STRIP_TAC);
 968  (EXPAND_TAC "V1");
 969  (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 970  (EXPAND_TAC "t");
 971  (MATCH_MP_TAC FINITE_SUBSET);
 972  (EXISTS_TAC `(V:real^3->bool) INTER ball (vec 0, r + &2 * h0)`);
 973  (STRIP_TAC);
 974  (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 975  (REWRITE_TAC[SUBSET; IN; IN_INTER; IN_BALL; IN_ELIM_THM]);
 976  (REPEAT STRIP_TAC);
 977  (ASM_REWRITE_TAC[]);
 978  (NEW_GOAL `dist (vec 0, x) <= dist (vec 0, u0) + dist (u0, x:real^3)`);
 979  (NORM_ARITH_TAC);
 980  (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
 981  (REWRITE_TAC[GSYM IN_BALL]);
 982  (UNDISCH_TAC `u0:real^3 IN V1` THEN EXPAND_TAC "V1" THEN SET_TAC[]);
 983  (ASM_REAL_ARITH_TAC);
 984  (EXPAND_TAC "t" THEN EXPAND_TAC "f_temp");
 985  (REWRITE_TAC[IN; IN_ELIM_THM]);
 986  (REWRITE_TAC[REAL_ARITH `a + &0 * r pow 2 = a`]);
 987  (MATCH_MP_TAC SUM_SUBSET_SIMPLE);
 988  (REPEAT STRIP_TAC);
 989
 990  (MATCH_MP_TAC FINITE_SUBSET);
 991  (EXISTS_TAC
 992   `{u0:real^3,u1:real^3 |u0 IN V1 /\u1 IN V INTER ball (vec 0, r + &2 * h0)}`);
 993  (STRIP_TAC);
 994  (MATCH_MP_TAC FINITE_PRODUCT);
 995  (STRIP_TAC);
 996  (EXPAND_TAC "V1");
 997  (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 998  (ASM_SIMP_TAC [Packing3.KIUMVTC]);
 999  (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM]);
1000  (REPEAT STRIP_TAC);
1001  (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
1002  (ASM_REWRITE_TAC[]);
1003  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`]);
1004  (REWRITE_TAC[IN_BALL; IN_INTER; IN]);
1005  (ASM_REWRITE_TAC[]);
1006
1007  (NEW_GOAL `dist (vec 0, u1) <= dist (vec 0, u0) + dist (u0, u1:real^3)`);
1008  (NORM_ARITH_TAC);
1009  (NEW_GOAL `dist (vec 0, u0:real^3) < r`);
1010  (REWRITE_TAC[GSYM IN_BALL]);
1011  (UNDISCH_TAC `(V1:real^3->bool) u0` THEN EXPAND_TAC "V1");
1012  (REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`]);
1013  (SET_TAC[]);
1014  (ASM_REAL_ARITH_TAC);
1015  (EXPAND_TAC "V1" THEN
1016    REWRITE_TAC[MESON[IN] `(A:real^3->bool) s <=> s IN A`; IN_INTER] THEN
1017    SET_TAC[]);
1018  (UP_ASM_TAC THEN REWRITE_TAC[IN_DIFF; IN_ELIM_THM; IN]);
1019  (REPEAT STRIP_TAC);
1020  (ASM_REWRITE_TAC[]);
1021  (REWRITE_TAC[lmfun_pos_le]);
1022
1023  (EXISTS_TAC `&0`);
1024  (REPEAT STRIP_TAC);
1025  (NEW_GOAL `F`);
1026  (ASM_MESON_TAC[]);
1027  (ASM_MESON_TAC[])]);;
1028
1029 (* ------ Finish the proof of KIZHLTL 1, KIZHLTL 2, KIZHLTL 4  -------- *)
1030
1031
1032  end;;