(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: UPFZBZM                                                  *)
(*      Chaper    : Packing (Clusters)                                       *)
(*      Date      : October 3, 2010                                          *)
(*                                                                           *)
(* ========================================================================= *)


(* ========================================================================= *)
(*      Unproved lemmas for UPFZBZM                                          *)
(*      Chaper    : Packing (Clusters)                                       *)
(*                                                                           *)

(* ========================================================================= *)


module Upfzbzm_axioms = struct

(*  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 
will be completed 
*)

(* ========================================================================= *)
(*             LIST OF THINGS THAT HAS NOT BEEN PROVED                       *)
(* ========================================================================= *)

let tau0_not_zero = new_axiom `~(tau0 = &0)`;;
let ZERO_LT_MM2_LEMMA = new_axiom `&0 < mm2`;;

(* Can be proved by using the new calculation tool of Prof T.Hales           *)

let lmfun_vs_marchal = new_axiom 
  `!h. ~(hminus <= h /\ h <= hplus)  ==> lmfun (h) >= marchal (h)`;;

(* Prof T.Hales said he will formalize the above axiom *)

let FINITE_MCELL_SET_LEMMA = new_axiom 
   `!V r. FINITE {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}`;;

(* This will be formalized by using the fact that:
      -  each mcell has a vertex v IN V.
      - FINITE (B(0,r) INTER V)
*)

let DIHX_SYM = new_axiom 
        `!u v V X. dihX V X (u,v) = dihX V X (v,u)`;; 

let KIZHLTL1 = new_axiom KIZHLTL1_concl;;
let KIZHLTL2 = new_axiom KIZHLTL2_concl;;
let KIZHLTL3 = new_axiom KIZHLTL3_concl;;

(* Book lemmas from the previous parts. Will be formalized by someone else   *)

let SUM_GAMMAX_LMFUM_ESTIMATE_concl = 
  `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\ 
               cell_cluster_estimate V /\ marchal_inequality /\
               lmfun_inequality V ==> 
    c * r pow 2 <=  sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X} 
    (\X. gammaX V X lmfun)`;;

let SUM_GAMMAX_LMFUM_ESTIMATE = new_axiom SUM_GAMMAX_LMFUM_ESTIMATE_concl;;
(* This axiom is the most important here *)

let negligible_fun_any_C = new_axiom
   `!f S. negligible_fun_0 f S <=> 
    (?C.  (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`;;
(* ! This is done in file "ky_lemma_negligible.hl" by T.Hales. 
   ! But I cannot load it. Maybe he used a newer version of HOL
 *)

let FINITE_PACK_LEMMA = new_axiom
  `!V p:real^3 r. packing V ==> FINITE (V:real^3->bool INTER ball (p,r))` ;;  

let FINITE_PERMUTE_3 = new_axiom `FINITE {p | p permutes {0, 1, 2}}`;;
let FINITE_PERMUTE_4 = new_axiom `FINITE {p | p permutes {0, 1, 2, 3}}`;;

(*  The same technique apply for 2 above lemmas  *)

(* ========================================================================= *)
end;;