legacy/oldpacking/ky_packing/UPFZBZM_axioms.hl

   1
   2 (* ========================================================================= *)
   3 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   4 (*                                                                           *)
   5 (*      Authour   : VU KHAC KY                                               *)
   6 (*      Book lemma: UPFZBZM                                                  *)
   7 (*      Chaper    : Packing (Clusters)                                       *)
   8 (*      Date      : October 3, 2010                                          *)
   9 (*                                                                           *)
  10 (* ========================================================================= *)
  11
  12
  13 (* ========================================================================= *)
  14 (*      Unproved lemmas for UPFZBZM                                          *)
  15 (*      Chaper    : Packing (Clusters)                                       *)
  16 (*                                                                           *)
  17
  18 (* ========================================================================= *)
  19
  20
  21 module Upfzbzm_axioms = struct
  22
  23 (*  This file is to help other people who want to continue my work can see what are left. When all the axioms in this file are proved, the main theorem UPFZBZM
  24 will be completed
  25 *)
  26
  27 (* ========================================================================= *)
  28 (*             LIST OF THINGS THAT HAS NOT BEEN PROVED                       *)
  29 (* ========================================================================= *)
  30
  31 let tau0_not_zero = new_axiom `~(tau0 = &0)`;;
  32 let ZERO_LT_MM2_LEMMA = new_axiom `&0 < mm2`;;
  33
  34 (* Can be proved by using the new calculation tool of Prof T.Hales           *)
  35
  36 let lmfun_vs_marchal = new_axiom
  37   `!h. ~(hminus <= h /\ h <= hplus)  ==> lmfun (h) >= marchal (h)`;;
  38
  39 (* Prof T.Hales said he will formalize the above axiom *)
  40
  41 let FINITE_MCELL_SET_LEMMA = new_axiom
  42    `!V r. FINITE {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`;;
  43
  44 (* This will be formalized by using the fact that:
  45       -  each mcell has a vertex v IN V.
  46       - FINITE (B(0,r) INTER V)
  47 *)
  48
  49 let DIHX_SYM = new_axiom
  50         `!u v V X. dihX V X (u,v) = dihX V X (v,u)`;;
  51
  52 let KIZHLTL1 = new_axiom KIZHLTL1_concl;;
  53 let KIZHLTL2 = new_axiom KIZHLTL2_concl;;
  54 let KIZHLTL3 = new_axiom KIZHLTL3_concl;;
  55
  56 (* Book lemmas from the previous parts. Will be formalized by someone else   *)
  57
  58 let SUM_GAMMAX_LMFUM_ESTIMATE_concl =
  59   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\
  60                cell_cluster_estimate V /\ marchal_inequality /\
  61                lmfun_inequality V ==>
  62     c * r pow 2 <=  sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}
  63     (\X. gammaX V X lmfun)`;;
  64
  65 let SUM_GAMMAX_LMFUM_ESTIMATE = new_axiom SUM_GAMMAX_LMFUM_ESTIMATE_concl;;
  66 (* This axiom is the most important here *)
  67
  68 let negligible_fun_any_C = new_axiom
  69    `!f S. negligible_fun_0 f S <=>
  70     (?C.  (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`;;
  71 (* ! This is done in file "ky_lemma_negligible.hl" by T.Hales.
  72    ! But I cannot load it. Maybe he used a newer version of HOL
  73  *)
  74
  75 let FINITE_PACK_LEMMA = new_axiom
  76   `!V p:real^3 r. packing V ==> FINITE (V:real^3->bool INTER ball (p,r))` ;;
  77
  78 let FINITE_PERMUTE_3 = new_axiom `FINITE {p | p permutes {0, 1, 2}}`;;
  79 let FINITE_PERMUTE_4 = new_axiom `FINITE {p | p permutes {0, 1, 2, 3}}`;;
  80
  81 (*  The same technique apply for 2 above lemmas  *)
  82
  83 (* ========================================================================= *)
  84 end;;