(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                            *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-21                                                           *)
(* ========================================================================== *)

(* 
Main conclusions of the chapter "Packing" 
The last section "Counting Spheres" has not been typed up.  It is waiting for the proof
of the existence of the correspondence needed in GOTCJAH.
*)

module Pack_concl = struct 

let GLTVHUM_concl = `!V (u0:real^3) p.  packing V /\ saturated V /\ (u0 IN V) ==>
   (p IN voronoi_closed V u0 <=>
  (?vl. vl IN barV V 3 /\ p IN rogers V vl /\ (truncate_simplex 0 vl = [u0])))`;;

let DUUNHOR_concl = `!V ul vl.   ul IN barV V 3 /\ vl IN barV V 3 /\ 
  ~(rogers V ul = rogers V vl) ==>
   coplanar (rogers V ul INTER rogers V vl)`;;

let QXSKIIT_concl = 
  `!(vf:A->real^N) b .  FINITE (IMAGE vf (:A)) /\ 
    ~ affine_dependent (IMAGE vf (:A)) /\  (!i j. (vf i = vf j) ==> (b i = b j))
   ==> (?!p.  p IN affine hull (IMAGE vf (:A)) /\ (!i j.  (p dot (vf i - vf j) = (b i - b j))))`;;

(*
let OAPVION_concl = `!S.  ~(S = {}) /\ ~affine_dependent S ==>
    ?!p. ?c.  (p IN affine hull S) /\ (!(v:real^N). (v IN S) ==> (dist(p,v) = c))`;;
*)

let OAPVION1_concl = `!(S:real^N->bool). ~(S = {}) /\ ~affine_dependent S ==>
    (circumcenter S) IN (affine hull S)`;;

let OAPVION2_concl = `!(S:real^N->bool).  ~affine_dependent S ==>
  (!w. w IN S ==> (radV S = dist(circumcenter S, w)))`;;

let OAPVION3_concl = `!(S:real^N->bool).  ~affine_dependent S ==>
  (!p.  (p IN affine hull S) /\ (?c. !w. (w IN S) ==> (dist(p,w) = c)) ==> (p = circumcenter S))`;;

let MHFTTZN1_concl = `!V ul k.  (k <= 3) /\ saturated V /\ packing V /\ barV V k ul ==>
  aff_dim (set_of_list ul) = int_of_num k`;;

let MHFTTZN2_concl = `!V ul k.  (k <= 3) /\ saturated V /\ packing V /\ barV V k ul ==>
   (!p. p IN   affine hull voronoi_list V ul <=> (!u.  (u IN set_of_list ul  ==> p IN bis (HD ul) u)))`;;

let MHFTTZN3_concl = `!V ul k.  (k <= 3) /\ saturated V /\ packing V /\ barV V k ul ==>
   ((affine hull (voronoi_list V ul)) INTER (affine hull (set_of_list ul)) =
   { circumcenter (set_of_list ul) } )`;;

let MHFTTZN4_concl = `!V ul k u v q.  (k <= 3) /\ saturated V /\ packing V /\ barV V k ul /\ (q = circumcenter (set_of_list ul)) /\
  u IN affine hull voronoi_list V ul /\ v IN affine hull (set_of_list ul) ==>
   ((u - q) dot (v - q) = &0)`;;

(* CHNGQBD *)


let XYOFCGX_concl =  
  `!V S (p:real^3).  S SUBSET V /\ ~affine_dependent S /\
   (p = circumcenter S) /\ (radV S < sqrt(&2)) ==>
   (!u v.  u IN S /\ v IN (V DIFF S) ==>dist(v,p) > dist(u,p))`;;

let XNHPWAB1_concl = 
`!V ul k.  saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
  (omega_list V ul = circumcenter (set_of_list ul))`;;

let XNHPWAB2_concl = 
`!V ul k.  saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
  (omega_list V ul IN convex hull  (set_of_list ul))`;;

(*
let XNHPWAB3_concl = 
`!V ul k.  saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
  (aff_dim (IMAGE (omega_list_n V ul) (0..k)) = &k)`;;
*)

let XNHPWAB3_concl = 
`!V ul k.  saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
  (aff_dim { omega_list_n V ul j | j IN  (0..k)} = &k)`;;

let XNHPWAB4_concl = 
`!V ul k.  saturated V /\ packing V /\ (k <= 3) /\ (ul IN barV V k) /\ (hl ul < sqrt(&2)) ==>
  (! i j.  (i < j) /\ (j <= k)  ==>  hl(truncate_simplex i ul) < hl(truncate_simplex j ul))`;;


let WAUFCHE1_concl = 
 `!V ul k.  saturated V /\ packing V /\ ul IN barV V k ==> hl ul <= 
    dist(omega_list V ul, HD ul)`;;

let WAUFCHE2_concl = 
 `!V ul k.  saturated V /\ packing V /\ ul IN barV V k /\
    hl ul < sqrt(&2) ==> (hl ul = dist(omega_list V ul, HD ul))`;;


(* rearrangement *)

let YIFVQDV_concl =  `!V ul k p.  packing V /\ saturated V /\ ul IN barV V k /\
     hl ul < sqrt(&2) /\ p permutes (0..k) ==>
  (left_action_list p ul IN barV V k) /\ (omega_list V (left_action_list p ul) = omega_list V ul)`;;

let KSOQKWL_concl = `!V ul p k.  saturated V /\ packing V /\ ul IN barV V k /\ hl ul < sqrt(&2) /\
p permutes (0..k) /\ (rogers V ul = rogers V (left_action_list p ul)) ==>  (p = I)`;;

(* TSIVSKG *)


let IVFICRK_concl = 
  `(!k. ?g.  (BIJ g { (i,sigma ) | i IN 0..(k+1) /\ sigma permutes (0..k) } { p | p permutes (0..(k+1)) })
    /\ (!(ul:(A)list) j.  (LENGTH ul = k+2) /\  j <= k ==> 
      (EL j ( left_action_list (g(i,sigma)) ul) = EL j (left_action_list sigma (DROP ul i) ))))`;;

let WQPRRDY_concl = 
  `!V ul k.  saturated V /\ packing V /\ ul IN barV V k /\ hl ul < sqrt(&2) ==>
    (convex hull (set_of_list ul) = UNIONS { rogers V (left_action_list p ul) |   p permutes (0..k) })`;;


let MXI_EXISTS_concl = `!V ul.  saturated V /\ packing V /\ barV V 3 ul /\
    sqrt(&2) <= hl ul ==>
    (mxi V ul IN convex hull { omega_list_n V ul 2  , omega_list_n V ul 3 }) /\
    (dist(mxi V ul, HD ul) = sqrt(&2))`;;


(* BGXEVQU , skip. Expand out using permutes *)

let EMNWUUS1_concl = `!V ul. saturated V /\ packing V /\ barV V 3 ul ==>
   (hl ul < sqrt(&2) <=> ~(mcell4 V ul = {}))`;;

let EMNWUUS2_concl = `!V ul. saturated V /\ packing V /\ barV V 3 ul ==>
   (hl ul < sqrt(&2) <=> (mcell0 V ul = {}) /\ (mcell1 V ul = {}) /\ (mcell2 V ul = {}) /\ 
  (mcell3 V ul = {}))`;;

let SLTSTLO1_concl = `!V ul p.  saturated V /\ packing V /\ barV V 3 ul /\ (p IN rogers V ul) ==>
   (?i.  (i <= 4) /\ (p IN mcell i V ul))`;;

let SLTSTLO2_concl = `!V ul. ?Z. !p.  saturated V /\ packing V /\ barV V 3 ul ==>
    (NULLSET Z) /\ (p IN rogers V ul DIFF Z ==>  (?!i.  (i <= 4) /\ (p IN mcell i V ul)))`;;

let RVFXZBU1_concl = `!V ul vl i j.   saturated V /\ packing V /\ 
  barV V 3 ul /\ barV V 3 vl /\ ~(i=j) ==>
  NULLSET (mcell i V ul INTER mcell j V vl)`;;

let RVFXZBU2_concl = `!V ul vl i.   saturated V /\ packing V /\ barV V 3 ul /\ barV V 3 vl /\
  ~(NULLSET (mcell i V ul INTER mcell i V vl)) ==>
   (?p. p permutes 0..(i-1) /\ (vl = left_action_list p ul))`;;

let RVFXZBU3_concl = `!V ul i p.   saturated V /\ packing V /\ barV V 3 ul /\
   (p permutes 0..(i-1)) ==> (mcell i V (left_action_list p ul) = mcell i V ul)`;;

let LEPJBDJ_concl = `!V ul k.  
  saturated V /\ packing V /\ barV V 3 ul /\ (1 <= k) /\ (k <= 4) /\ 
  ~(mcell k V ul = {})==>
  (V INTER mcell k V ul = set_of_list (truncate_simplex (k-1) ul))`;;

let LEPJBDJ_0_concl =
 `!V ul.
         saturated V /\
         packing V /\
         barV V 3 ul
        ==> V INTER mcell 0 V ul = {}`;;

let HDTFNFZ_concl = 
`!V ul k v X.
     saturated V /\
     packing V /\
     barV V 3 ul /\
     X = mcell k V ul /\ ~(NULLSET X)
     ==> VX V X = V INTER X`;;

let URRPHBZ1_concl = `!V ul k.
  saturated V /\ packing V /\ barV V 3 ul ==> 
  measurable (mcell k V ul)`;;

let URRPHBZ2_concl = `!V ul k v.
  saturated V /\ packing V /\ barV V 3 ul /\ (v IN V)==> 
  eventually_radial v (mcell k V ul)`;;

let URRPHBZ3_concl = `!V ul k v.
  saturated V /\ packing V /\ barV V 3 ul /\ ~(NULLSET (mcell k V ul)) /\
   (v IN V DIFF VX V (mcell k V ul))==> 
  (?t. t > &0 /\ (!p. p IN mcell k V ul ==> t < dist(p,v)))`;;

let QZYZMJC_concl = `!V v X. 
    saturated V /\ packing V /\ (v IN V) ==>
    (sum { X | mcell_set V X /\ v IN VX V X } (\t. sol v t) = &4 * pi)`;;


(*
let IJEKNGA_concl = 
*)

(*
JGXZYGW already done by Nguyen Tat Thang
*)


(* These individual statements rather than the entire lemma are what we need. *)

let KIZHLTL1_concl = `!(V:real^3->bool). ?c. !r. saturated V  /\ packing V /\ (&1 <= r) ==>
   (sum { X | X SUBSET ball(vec 0,r) /\  (mcell_set V X) }   vol  + c*r pow 2 
   <= sum (V INTER  ball(vec 0,r)) (\u. vol(voronoi_open V u)))`;;
      
let KIZHLTL2_concl = `!(V:real^3->bool). ?c. !r. saturated V /\ packing V /\ (&1 <= r) ==>
  ( &(CARD(V INTER ball(vec 0,r)))* &8*mm1    + c*r pow 2
  <=  (&2*mm1/pi)* sum { X | X SUBSET ball(vec 0, r) /\ mcell_set V X } 
    (total_solid V) )`;;

let KIZHLTL3_concl = `!(V:real^3->bool) f. ?c. !r. saturated V /\ packing V /\ (&1 <= r) /\
  (?c1. !x.  &2 <= x /\ x < sqrt(&8) ==> abs( f x) <= c1)
   ==>
   (( &8 * mm2 /pi)* 
         sum { X | X SUBSET ball(vec 0, r) /\  mcell_set V X } 
            ( \ X.   sum (edgeX V X) ( \ {u,v}. (dihX V X (u ,v))*f (hl[u;v])))
					  +c*r pow 2 <=
	&8*mm2 * 
         sum (V INTER ball(vec 0,r)) 
           ( \u.  sum { v | v IN V /\ ~(u=v) /\ dist(u,v) < sqrt(&8)} 
               ( \v.  f(hl [u;v]))))`;;

let OXLZLEZ_concl = `!V.  (saturated V /\ packing V ) ==> cell_cluster_estimate_v1 V`;;

let TSKAJXY_statement = new_definition
   `TSKAJXY_statement <=>
      (!V X.
          saturated V /\
          packing V /\
          mcell_set V X /\
          critical_edgeX V X = {}
          ==> gammaX V X lmfun >= &0)`;;
let UPFZBZM_concl = 
   `!V.  saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\ 
         TSKAJXY_statement /\
         lmfun_inequality V ==>
    (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;

(* Deprecated Dec 31, 2012 
let UPFZBZM_concl = `!V.  saturated V /\ packing V /\ cell_cluster_estimate_v1 V /\ 
   marchal_inequality /\
   lmfun_inequality V ==> (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
*)

(* RDW modified Dec 31, 2012  *)

let RDWKARC_concl = `~kepler_conjecture /\ 
     (!V. packing V /\ saturated V ==> cell_cluster_estimate_v1 V) /\ TSKAJXY_statement 
   ==> (?V.  packing V /\ V SUBSET ball_annulus /\ ~(lmfun_ineq_center V))`;;

let GOTCJAH_concl = `!s f (v:real^3) b WF h k. 
    polyhedron s /\ bounded s /\ (?r. r> &0 /\ ball(vec 0,r) SUBSET s) /\
    f facet_of s /\ 
    f = { p | p dot v = b } INTER s /\ 
    topological_component_yfan (vec 0,fan_of_polyhedron s) WF /\
    ~(f INTER WF = {}) /\
    rcone_gt (vec 0) v h SUBSET WF /\
    (k = CARD {u | u extreme_point_of f }) 
   ==> &2 * pi - &2* &k * asn (h* sin(pi/ &k)) <= sol (vec 0) WF`;;

(* Dec 28, 2011, content merged from scattered files *)

 let TIWWFYQ_concl = `!V (p:real^3). packing V /\ saturated V ==> (?v.  v IN V /\ p IN voronoi_closed V v)`;;


 let VORONOI_BALL2_concl = `!V (v:real^3).  packing V /\ saturated V /\ (v IN V) ==> voronoi_closed V v SUBSET ball(v, &2)`;;

 let VORONOI_INTER_BIS_LE_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==> 
   (voronoi_closed V v =INTERS { bis_le v u | u IN V /\ u IN ball(v, &4) /\  ~(u=v) })`;;

 let VORONOI_POLYHEDRON_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
   polyhedron (voronoi_closed V v)`;;
  
  let RHWVGNP_concl = VORONOI_POLYHEDRON_concl;;

 let DRUQUFE_concl = `!V (v:real^3). packing V /\ saturated V  ==>
     compact (voronoi_closed V v) /\ convex (voronoi_closed V v) /\ measurable (voronoi_closed V v)`;;

  let BBDTRGC_VORONOI_SET = Sphere.VORONOI_SET;;

  let BBDTRGC_VORONOI_LIST  =  Sphere.VORONOI_LIST;;

  let NOPZSEH = Sphere.BARV;;

  let JNRJQSM = Sphere.TRUNCATE_SIMPLEX;;

  let KHEJKCI_concl = `!V k ul. saturated V /\ packing V /\ vor_list V k ul ==>
   ((voronoi_list V ul)   face_of (voronoi_closed V (HD ul)) )`;;

  let JJGTQMN = Sphere.OMEGA_LIST;;

  let PHZVPFY = Sphere.ROGERS;;


  (* deprecated, replaced with GRUTOTI1_concl

  let GRUTOTI_concl = 
    `!V u0 u1 e. 
      saturated V /\ packing V /\ 
      u0 IN V /\ u1 IN V /\ 
      dist (u0, u1) < sqrt (&2) /\ 
      e = {u0, u1} ==>
    sum {X | e IN (edgeX V X)} (\t. dihX V t (u0,u1)) = &2 * pi`;;

  *)

let GRUTOTI1_concl = 
`!V u0 u1 e.
     saturated V /\
     packing V /\
     u0 IN V /\
     u1 IN V /\
     ~(u0 = u1) /\
     hl [u0;u1] < sqrt (&2) /\
     e = {u0, u1}
     ==> sum {X | mcell_set V X /\ e IN edgeX V X } (\t. dihX V t (u0,u1)) =
         &2 * pi`;;

let REUHADY_concl = `!V u0 u1 vl1 vl2 v1 v2 e.
  saturated V /\ packing V /\
  dist(u0,u1) < sqrt8 /\
  e = {u0,u1} /\
  ~(azim u0 u1 w1 w2 = &0) /\
  hl vl1 < sqrt2 /\ hl vl2 < sqrt2 /\
  vl1 IN barV V 2 /\ vl2 IN barV V 2 /\
  set_of_list (truncate_simplex 1 vl1)= e  /\
  set_of_list (truncate_simplex 1 vl2) =e /\
  v1 = EL 2 vl1 /\
  v2 = EL 2 vl2 /\
  (!X. X IN mcell_set V /\ e IN edgeX V X ==>
     (X SUBSET wedge_ge u0 u1 v1 v2 \/
     X SUBSET wedge_ge u0 u1 v2 v1)) ==> 
  (sum {X | mcell_set V X /\ e IN edgeX V X /\ X SUBSET wedge_ge u0 u1 v1 v2 } 
     (\t. dihX V t (u0,u1)) = azim u0 u1 v1 v2)`;;

(* WEDGE_GE_ALMOST_DISJOINT gives the intersection of wedges hypothesis in the following verion *)

let REUHADY_concl_version2 = `!V u0 u1 vl1 vl2 v1 v2 e.
  saturated V /\ packing V /\
  dist(u0,u1) < sqrt8 /\
  e = {u0,u1} /\
  wedge_ge u0 u1 v1 v2 INTER wedge_ge u0 u1 v2 v1 SUBSET aff_ge {u0,u1} {v1} UNION aff_ge {u0,u1} {v2} /\ 
  hl vl1 < sqrt2 /\ hl vl2 < sqrt2 /\
  vl1 IN barV V 2 /\ vl2 IN barV V 2 /\
  set_of_list (truncate_simplex 1 vl1)= e  /\
  set_of_list (truncate_simplex 1 vl2) =e /\
  v1 = EL 2 vl1 /\
  v2 = EL 2 vl2 /\
  (!X. X IN mcell_set V /\ e IN edgeX V X ==>
     (X SUBSET wedge_ge u0 u1 v1 v2 \/
     X SUBSET wedge_ge u0 u1 v2 v1)) ==> 
  (sum {X | mcell_set V X /\ e IN edgeX V X /\ X SUBSET wedge_ge u0 u1 v1 v2 } 
     (\t. dihX V t (u0,u1)) = azim u0 u1 v1 v2)`;;



end;;