(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma: UPFZBZM                                                  *)
(*      Chaper    : Packing (Clusters)                                       *)
(*                                                                           *)
(* ========================================================================= *)

(* ========================================================================= *)
(*                     FILES NEED TO BE LOADED                               *)
(* sum_beta_bump.hl                                                          *)
(* sum_gammaX_lmfun_estimate.hl                                              *)
(* ========================================================================= *)
  
let UPFZBZM_concl = 
   `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\ 
         TSKAJXY_statement /\
         lmfun_inequality V ==>
    (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;

let FCC_COMPATABILITY_FUNC_concl =  
 `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\ 
   TSKAJXY_statement /\
   lmfun_inequality V /\ G = (\u. --vol(voronoi_open V u) + 
   &8 * mm1 - &8 * mm2 * sum { v | v IN V /\ ~(u=v) /\ dist(u,v) <= &2*h0 } 
   (\v. lmfun (hl [u;v]))) 
   ==> fcc_compatible G V`;;

let NEGLIGIBLE_FUNC_concl = 
  `!V. saturated V /\
       packing V /\
       cell_cluster_estimate V /\
       TSKAJXY_statement /\
       lmfun_inequality V /\
       G =
       (\u. --vol (voronoi_open V u) +
            &8 * mm1 -
            &8 *
            mm2 *
            sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
            (\v. lmfun (hl [u; v])))
       ==> negligible_fun_0 G V`;;

(* ========================================================================= *)
(*                            THE THEOREM                                    *)
(* ========================================================================= *)

(* PART 1 OF THE LEMMA *)

let FCC_COMPATABILITY_FUNC = prove_by_refinement (
 FCC_COMPATABILITY_FUNC_concl,
[(REWRITE_TAC[lmfun_inequality;fcc_compatible]);
 (REPEAT STRIP_TAC);
 (ASM_REWRITE_TAC[Pack2.MEASURE_VORONOI_CLOSED_OPEN]);
 (ASM_REWRITE_TAC[REAL_ARITH `a + --a + b - c = b - c`]);
 (MATCH_MP_TAC (REAL_ARITH 
  `x = &8 * mm1 - &8 * (&12 * mm2) /\ y <= &8 * (&12 * mm2) ==> 
   x <= &8 * mm1 - y`));
 (STRIP_TAC);
 (REWRITE_TAC[SQRT_OF_32_lemma]);
 (REWRITE_TAC[REAL_ARITH `a * b - a * c = a * (b - c)`]);
 (REWRITE_TAC[m1_minus_12m2]);
 (MATCH_MP_TAC REAL_LE_LMUL);
 (REWRITE_TAC[REAL_ARITH `&0 <= &8`]);
 (REWRITE_TAC[REAL_ARITH `&12 * mm2 = mm2 * &12`]);
 (MATCH_MP_TAC REAL_LE_LMUL);
 (REWRITE_TAC[ZERO_LE_MM2_LEMMA]);
 (ASM_MESON_TAC[])]);;



(* ========================================================================= *)
(* PART 2 OF THE LEMMA *)
(* ========================================================================= *)

let NEGLIGIBLE_FUNC = prove_by_refinement (
 NEGLIGIBLE_FUNC_concl,
[(REWRITE_TAC[negligible_fun_0; negligible_fun_any_C]);
 (REPEAT STRIP_TAC);

 (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL1));
 (STRIP_TAC);
 (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL2));
 (STRIP_TAC);
 (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL4));
 (STRIP_TAC);

 (MP_TAC (SPEC `V:real^3->bool` SUM_GAMMAX_LMFUN_ESTIMATE));
 (STRIP_TAC);

 (NEW_GOAL 
   `!r. saturated V /\ packing V /\ &1 <= r
          ==> c''' * r pow 2 <=
              sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
              (\X. gammaX V X lmfun)`);
 (REPEAT STRIP_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);
 (UP_ASM_TAC THEN REWRITE_TAC[gammaX] THEN STRIP_TAC);

 (EXISTS_TAC `--c''' - c - c' - c''`);
 (REPEAT STRIP_TAC);

 (ABBREV_TAC `f1 =  (\u:real^3. --vol (voronoi_open V u))`);
 (ABBREV_TAC `f2 =  (\u:real^3.  &8 * mm1 -  &8 * mm2 *
                     sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
                     (\v. lmfun (hl [u; v])))`);
 (REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) G = 
                 sum (V INTER ball (vec 0,r)) f1 + 
                 sum (V INTER ball (vec 0,r)) f2`);
 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "f1" THEN EXPAND_TAC "f2");
 (MATCH_MP_TAC SUM_ADD);
 (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
 (ABBREV_TAC `f3 =  (\u:real^3.  &8 * mm1)`);
 (ABBREV_TAC `f4 =  (\u:real^3.  &8 * mm2 *
                     sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
                     (\v. lmfun (hl [u; v])))`);
 (REWRITE_WITH `sum ((V:real^3->bool) INTER ball (vec 0,r)) f2 = 
                 sum (V INTER ball (vec 0,r)) f3 - 
                 sum (V INTER ball (vec 0,r)) f4`);
 (EXPAND_TAC "f2" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f4");
 (MATCH_MP_TAC SUM_SUB);
 (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
 (EXPAND_TAC "f4" THEN DEL_TAC THEN 
   ASM_SIMP_TAC[SUM_NEG;SUM_CONST;SUM_LMUL;FINITE_PACK_LEMMA]);
 (ABBREV_TAC `f5 =  (\u:real^3.  
                     sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
                     (\v. lmfun (hl [u; v])))`);
 (ABBREV_TAC `B = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);
 (ABBREV_TAC `T1 = sum B vol`);
 (ABBREV_TAC `T2 = --(&2 * mm1 / pi) * sum B (total_solid V)`);
 (ABBREV_TAC `T3 = (&8 * mm2 / pi) * sum B (\X. sum (edgeX V X)
                     (\({u, v}). if {u, v} IN edgeX V X
                               then dihX V X (u,v) * lmfun (hl [u; v])
                               else &0))`);

 (NEW_GOAL `sum (V:real^3->bool INTER ball (vec 0,r)) f1 <= --T1 - c * r pow 2`);
 (EXPAND_TAC "T1" THEN EXPAND_TAC "B");
 (EXPAND_TAC "f1");
 (REWRITE_TAC[SUM_NEG; REAL_ARITH `-- a <= --b - c <=> b + c <= a`]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL 
  `sum (V:real^3->bool INTER ball (vec 0,r)) f3 <= --T2 - c' * r pow 2`);
 (EXPAND_TAC "T2" THEN EXPAND_TAC "B");
 (EXPAND_TAC "f3");
 (REWRITE_TAC[SUM_NEG; REAL_ARITH `a <= --(-- b * d) - c<=> a + c <= b * d`]);
 (REWRITE_WITH `sum (V INTER ball (vec 0,r)) (\u:real^3. &8 * mm1) = 
   &(CARD (V INTER ball (vec 0,r))) * (&8 * mm1)`);
 (MATCH_MP_TAC SUM_CONST);
 (ASM_SIMP_TAC[FINITE_PACK_LEMMA]);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (NEW_GOAL `T3 + c'' * r pow 2 <= 
   &8 * mm2 * sum (V:real^3->bool INTER ball (vec 0,r)) f5`);
 (EXPAND_TAC "T3" THEN EXPAND_TAC "B");

 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[]);

 (MATCH_MP_TAC (REAL_ARITH `(?s. A <= s /\ s <= b) ==> A <= b`));
 (EXISTS_TAC `--T1 + --T2 + --T3  - (c + c' + c'') * r pow 2`);
 (STRIP_TAC);
 (ASM_REAL_ARITH_TAC);
 (REWRITE_TAC[REAL_ARITH 
   `--T1 + --T2 + --T3 - (c + c' + c'') * r pow 2 <=
   (--c''' - c - c' - c'') * r pow 2 
   <=> c''' * r pow 2 <= T1 + T2 + T3`]);
 (REWRITE_WITH `T1 + T2 + T3 = 
                 sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
                 (\X. gammaX V X lmfun)`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[gammaX]);
 (NEW_GOAL `FINITE (B:(real^3->bool)->bool)`);
 (EXPAND_TAC "B");
 (ASM_SIMP_TAC [FINITE_MCELL_SET_LEMMA]);
 (ASM_SIMP_TAC[SUM_ADD; SUM_SUB; SUM_LMUL; ETA_AX]);
 (EXPAND_TAC "T2");
 (REAL_ARITH_TAC);
 (FIRST_ASSUM MATCH_MP_TAC);
 (ASM_REWRITE_TAC[])]);;
 

(* ========================================================================= *)
(*             Main theorm                                                   *)
(* ========================================================================= *)

let UPFZBZM = prove (UPFZBZM_concl,
 (REPEAT STRIP_TAC) THEN (ABBREV_TAC `G = (\u. --vol (voronoi_open V u) +
              &8 * mm1 -
              &8 *
              mm2 *
              sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
              (\v. lmfun (hl [u; v])))`) THEN
 (EXISTS_TAC `G:real^3->real`) THEN 
 (ASM_MESON_TAC[NEGLIGIBLE_FUNC;FCC_COMPATABILITY_FUNC]));;