text_formalization/packing/pack_defs.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Packing                                                            *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-21                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* definitions needed for the chapter Packing *)
  10
  11
  12 flyspeck_needs "volume/vol1.hl";;
  13
  14 module Pack_defs = struct
  15
  16   let sol = Vol1.sol;;
  17
  18    let negligible_fun_p = new_definition `negligible_fun_p f S (p:real^N) = (? (C:real). (&0<= C)/\ ! (r:real). ( &1 <= r) ==> (sum (S INTER ball(p,r)) f) <= C * (r pow 2))`;;
  19
  20    let negligible_fun_0 = new_definition `negligible_fun_0 f S  = negligible_fun_p f S ((vec:num->real^3) 0)`;;
  21
  22    let fcc_compatible= new_definition `fcc_compatible f (S:real^N->bool) = (!v. v IN S ==> sqrt( &32) <= measure(voronoi_open S v) + f v)`;;
  23
  24    let kepler_conjecture = new_definition `kepler_conjecture = (!V. packing V /\ saturated V ==> (?(c:real). !(r:real). (&1<= r ==> vol ((UNIONS {ball(v:real^3, &1) | v IN V}) INTER ball(vec 0 ,r))/ vol (ball(vec 0, r))<= pi/ sqrt( &18) + c/ r)))`;;
  25
  26 let HL = new_definition `hl (ul:(real^N)list) = radV (set_of_list ul)`;;
  27
  28 let REVERSE_TABLE  = define `(REVERSE_TABLE (f:num->A) 0 = []) /\
  29    (REVERSE_TABLE f (SUC i) = CONS (f i)  ( REVERSE_TABLE f i))`;;
  30
  31 let TABLE = new_definition `!(f:num->A) k. TABLE f k = REVERSE (REVERSE_TABLE f k)`;;
  32
  33 let left_action = new_definition `!p f x. left_action (p:A->C) (f:A->B) x = f(inverse p x)`;;
  34
  35 let left_action_list = new_definition `left_action_list p (ul:(A)list) = TABLE (\i. EL (inverse p i) ul) (LENGTH ul)`;;
  36
  37 let DROP = define `(DROP (ul:(A)list) 0  = TL ul) /\ (DROP ul (SUC i) = CONS(HD ul) (DROP (TL ul) i))`;;
  38
  39 let mxi = new_definition `!V ul. mxi V ul =
  40   if (hl (truncate_simplex 2 ul) >= sqrt(&2))
  41   then omega_list_n V ul 2
  42   else (@p. ((p IN convex hull
  43     { omega_list_n V ul 2  , omega_list_n V ul 3}) /\
  44     (dist(p, HD ul) = sqrt(&2))))`;;
  45
  46 let mcell0 =
  47   new_definition `!V ul. mcell0 V ul = rogers V ul DIFF ball(HD ul,sqrt(&2))`;;
  48
  49 (* June 17, 2011, changed to mcell1, mcell2 to
  50    weak ineq sqrt(&2) <= hl ul to fix an error
  51    reported by Ky *)
  52
  53 let mcell1 = new_definition `!V ul. mcell1 V ul =
  54    if (sqrt(&2) <= hl ul)
  55    then
  56      rogers V ul INTER cball(HD ul, (sqrt (&2))) DIFF
  57      rcone_gt (HD ul) (HD (TL ul))
  58         (hl (truncate_simplex 1 ul ) / (sqrt(&2)))
  59    else {}`;;
  60
  61 let mcell2 = new_definition `!V ul. mcell2 V ul =
  62   if (hl (truncate_simplex 1 ul) < sqrt(&2)) /\ (sqrt(&2) <= hl ul)
  63   then
  64      (let a =  hl (truncate_simplex 1 ul ) / (sqrt(&2)) in
  65     rcone_ge (HD ul) (HD (TL ul)) a INTER
  66     rcone_ge  (HD (TL ul)) (HD ul) a INTER
  67     aff_ge { HD ul, (HD (TL ul)) } { mxi V ul, omega_list_n V ul 3 })
  68   else {}`;;
  69
  70 let mcell3 = new_definition `!V (ul:(real^3)list). mcell3 V ul =
  71     if (hl (truncate_simplex 2 ul) < sqrt(&2)) /\ (sqrt(&2) <= hl ul) then
  72         convex hull (set_of_list (truncate_simplex 2 ul) UNION { mxi V ul })
  73     else {}`;;
  74
  75 let mcell4 = new_definition `!V ul. mcell4 (V:real^3->bool) (ul:(real^3)list) =
  76  if (hl ul < sqrt(&2))
  77  then convex hull (set_of_list ul)
  78  else {}`;;
  79
  80 let mcell = new_definition `!(V:real^3->bool) ul.  (mcell i V ul) =
  81    if (i=0) then mcell0 V ul else if (i=1) then mcell1 V ul else if (i=2) then mcell2 V ul
  82    else if (i=3) then mcell3 V ul else mcell4 V ul`;;
  83
  84 let mcell_set = new_definition `mcell_set V =
  85 { X |  ?i ul.  (X = mcell i V ul) /\ ul IN barV V 3 }`;;
  86
  87
  88 let cell_params = new_definition `!V X. cell_params V X = @(k,ul).
  89     (k <= 4) /\ (ul IN barV V 3) /\ (X = mcell k V ul)`;;
  90
  91 let VX = new_definition
  92  `!V X.
  93          VX V X =
  94          (if NULLSET X
  95           then {}
  96           else let k,ul = cell_params V X in
  97                (if k = 0 then {} else
  98                 set_of_list (truncate_simplex (k - 1) ul)))`;;
  99
 100 let edgeX = new_definition `!V X. edgeX V X =  { ({u,v}) | VX V X u /\ VX V X v /\ ~(u=v) }`;;
 101
 102 let total_solid = new_definition `!V X x. total_solid V X =  sum  ( VX V X  )  (\(x:real^3).   (sol x X))`;;
 103
 104 (* The definition of dihX is rather awkward, because a cell is essentially a quotient
 105     type, so it is not natural to make definitions with cells as a parameter.
 106     Several lemmas will have to be proved to make these definitions useable, such as
 107    dihX V (mcell 4 V ul) ((EL 0 ul),(EL 1 ul)) = dihV (EL 0 ul) (EL 1 ul) (EL 2 ul) (EL 3 ul).
 108 *)
 109
 110
 111 (* deprecated 1/16/2012, tchales
 112 let dihX2 = new_definition `!V X v0 (v1:real^3). dihX2 V X (v0,v1) =
 113   (let (k,ul) = cell_params V X in
 114      dihV v0 v1 (mxi V ul) (omega_list_n V ul 3))`;;
 115 p
 116 (* The sum has a single term *)
 117
 118 let dihX3 = new_definition `!V X v0 (v1:real^3). dihX3 V X (v0,v1) =
 119   (let (k,ul) = cell_params V X in
 120      sum { (vl,p) | p permutes {0,1,2} /\
 121          (vl = left_action_list p ul) /\ (v0 = EL 0 vl) /\ (v1 = EL 1 vl) }
 122          ( \ (vl,p) . dihV v0 v1 (EL 2 vl) (mxi V ul) ))`;;
 123
 124 (* The sum has two terms. Take the average *)
 125
 126 let dihX4 = new_definition `!V X v0 (v1:real^3). dihX4 V X (v0,v1) =
 127   (let (k,ul) = cell_params V X in
 128      (&1 / &2) * sum { (vl,p) | p permutes {0,1,2,3} /\
 129          (vl = left_action_list p ul) /\ (v0 = EL 0 vl) /\ (v1 = EL 1 vl) }
 130          ( \ (vl,p). dihV v0 v1 (EL 2 vl) (EL 3 ul) ))`;;
 131
 132 let dihX = new_definition `!V X v0 (v1:real^3). dihX V X (v0,v1) =
 133    if (NULLSET X) then &0 else
 134      (let (k,ul) = cell_params V X in
 135         if (k=2) then dihX2 V X (v0,v1)
 136         else if (k=3) then dihX3 V X (v0,v1)
 137         else if  (k=4) then dihX4 V X (v0,v1)
 138         else &0)`;;
 139 *)
 140
 141 let dihu2 =  new_definition `!V ul. dihu2 V ul =
 142    dihV (EL 0 ul) (EL 1 ul) (mxi V ul) (omega_list_n V ul 3)`;;
 143
 144 let dihu3 = new_definition `!V ul. dihu3 V ul =
 145    dihV (EL 0 ul) (EL 1 ul) (EL 2 ul) (mxi V ul)`;;
 146
 147 let dihu4 = new_definition `!(ul:((real^3)list)). dihu4 ul =
 148    dihV (EL 0 ul) (EL 1 ul) (EL 2 ul) (EL 3 ul)`;;
 149
 150 let cell_params_d = new_definition `!V X. cell_params_d V X vl = @(k,ul).
 151    (k <= 4) /\ (ul IN barV V 3) /\ (X = mcell k V ul) /\
 152    (initial_sublist vl ul)`;;
 153
 154 let dihX = new_definition `!V X v0 v1. dihX V X (v0,v1) =
 155    if (NULLSET X) then &0 else
 156      (let (k,ul) = cell_params_d V X [v0;v1] in
 157         if (k=2) then dihu2 V ul
 158         else if (k=3) then dihu3 V ul
 159         else if  (k=4) then dihu4 ul
 160         else &0)`;;
 161
 162
 163    let sol0 = new_definition `sol0 = &3 * acs (&1 / &3)  - pi`;;
 164    let tau0 = new_definition `tau0 = &4 * pi - &20 * sol0`;;
 165    let mm1 = new_definition `mm1 = sol0 * sqrt(&8)/tau0`;;
 166    let mm2 = new_definition `mm2 = (&6 * sol0 - pi) * sqrt(&2) /(&6 * tau0)`;;
 167    let hplus = new_definition `hplus = #1.3254`;;
 168
 169 (*
 170    let marchal_quartic = new_definition `marchal_quartic h =
 171       (sqrt(&2)-h)*(hplus - h)*(&17*h - &9*(h pow 2) - &3)/
 172       ((sqrt(&2) - &1)*(hplus - &1))`;;
 173 *)
 174
 175    let marchal =  new_definition `marchal h =
 176     (if (h <= sqrt(&2)) then marchal_quartic h else &0)`;;
 177
 178 (* changed March 16, 2012, following Ky's suggestion. *)
 179
 180 let gammaX = new_definition `!V X f.
 181     gammaX V X f = vol(X) - (&2*mm1 / pi)*total_solid V X +
 182      (&8*mm2/ pi) * sum (edgeX V X) (\{u,v}. (if {u,v} IN edgeX V X then (dihX V X (u ,v))* f(hl [u;v]) else (&0)))`;;
 183
 184 (*
 185    let gammaX = new_definition `!V X f.
 186     gammaX V X f = vol(X) - (&2*mm1 / pi)*total_solid V X +
 187      (&8*mm2/ pi) * sum (edgeX V X) (\{u,v}. (dihX V X (u ,v))* f(hl [u;v]))`;;
 188 *)
 189
 190 (* OBSOLETE, Dec 31, 2012:
 191 let marchal_inequality = new_definition `marchal_inequality =
 192     (!V X.  saturated V /\ packing V /\ mcell_set V X ==>
 193        gammaX V X marchal >= &0)`;;
 194 *)
 195
 196 let h0 = new_definition `h0 = #1.26`;;
 197
 198 let lfun = new_definition `lfun h =  (h0 - h)/(h0 - &1)`;;
 199
 200 let lmfun = new_definition `lmfun h = if (h<=h0) then (h0 - h)/(h0 - &1) else &0`;;
 201
 202 let hminus = new_definition `hminus = @x. #1.2 <= x /\ x < #1.3 /\ marchal_quartic x = lmfun x`;;
 203
 204 let critical_edgeX =new_definition
 205    `critical_edgeX V X = { {u,v} | {u,v} IN edgeX V X /\ hminus <= hl [u;v] /\
 206                                             hl[u;v] <= hplus}`;;
 207
 208 let subcritical_edgeX =new_definition
 209    `subcritical_edgeX V X = { {u,v} | {u,v} IN edgeX V X /\  hl [u;v] < hminus }`;;
 210
 211 let critical_weight = new_definition
 212   `! V X. critical_weight V X = &1/ &(CARD (critical_edgeX V X))`;;
 213
 214 let bump = new_definition `!h. bump h = #0.005*(&1 - ((h- h0) pow 2)/((hplus - h0) pow 2))`;;
 215
 216 let critical_edge_y = new_definition `critical_edge_y y = ((&2*hminus <= y) /\ (y <= &2 *hplus))`;;
 217
 218 (* deprecated Dec 1, 2012
 219 let beta_bump_y = new_definition `beta_bump_y y1 y2 y3 y4 y5 y6 =
 220   (if critical_edge_y y1 then &1 else &0) *
 221   (if critical_edge_y y2 then &0 else &1) *
 222   (if critical_edge_y y3 then &0 else &1) *
 223   (if critical_edge_y y4 then &1 else &0) *
 224   (if critical_edge_y y5 then &0 else &1) *
 225   (if critical_edge_y y6 then &0 else &1) *
 226     (bump (y1/ &2) - bump (y4 / &2))`;;
 227 *)
 228
 229 let wtcount3_y = new_definition `wtcount3_y y1 y2 y3  =
 230   (if critical_edge_y y1 then 1 else 0) +
 231   (if critical_edge_y y2 then 1 else 0) +
 232   (if critical_edge_y y3 then 1 else 0) `;;
 233
 234 let wtcount6_y = new_definition
 235  `wtcount6_y y1 y2 y3 y4 y5 y6 = wtcount3_y y1 y2 y3 + wtcount3_y y4 y5 y6`;;
 236
 237 let cell_cluster = new_definition
 238 `!V e. cell_cluster V e = { X |  e IN critical_edgeX V X /\ mcell_set V X }`;;
 239
 240 (* Next definitions deprecated, Dec 1, 2012.
 241    Obsolete Jan 2, 2013. *)
 242
 243 (*
 244 let beta_bump = new_definition `!V e X. beta_bump V e X =
 245   (let (k,ul) = cell_params V X in
 246     sum { (e',e'',p,vl) | (k=4) /\ (critical_edgeX V X = {e',e''}) /\ (e =e') /\ p permutes 0..3
 247                /\ (vl = left_action_list p ul) /\ (e' = {EL 0 vl, EL 1 vl}) /\ (e'' = {EL 2 vl, EL 3 vl} ) }
 248     ( \ (e',e'',p,vl). (bump(hl [EL 0 vl; EL 1 vl]) - bump(hl [EL 2 vl; EL 3 vl]) )/ &4 ))`;;
 249
 250 let cluster_gammaX = new_definition `!V e Z. cluster_gammaX V e Z=
 251    sum Z ( \ X.  gammaX V X lmfun  * critical_weight V X  + beta_bump V e X )`;;
 252
 253 let cell_cluster_estimate = new_definition `!V. cell_cluster_estimate V = (!e.
 254   (cluster_gammaX V e (cell_cluster V e) >= &0))`;;
 255
 256   (* average over all 4 = 2! x 2! possible representations *)
 257
 258 let beta_bumpA = new_definition `!V e X. beta_bumpA V e X =
 259   (let (k,ul) = cell_params V X in
 260     sum { (e',e'',p,vl) | (k=4) /\ (critical_edgeX V X = {e',e''}) /\ (e =e') /\ p permutes 0..3 /\
 261        (!e'''. e''' IN edgeX V X ==> ((e''' = e') \/ (e''' = e'') \/ (e''' IN subcritical_edgeX V X)))
 262                /\ (vl = left_action_list p ul) /\ (e' = {EL 0 vl, EL 1 vl}) /\ (e'' = {EL 2 vl, EL 3 vl} ) }
 263     ( \ (e',e'',p,vl). (bump(hl [EL 0 vl; EL 1 vl]) - bump(hl [EL 2 vl; EL 3 vl]) )/ &4 ))`;;
 264
 265 let cluster_gamma_AX = new_definition `!V e Z. cluster_gamma_AX V e Z=
 266    sum Z ( \ X.  gammaX V X lmfun  * critical_weight V X  + beta_bumpA V e X )`;;
 267
 268 let cell_cluster_estimate_A = new_definition `!V. cell_cluster_estimate_A V = (!e.
 269   (cluster_gamma_AX V e (cell_cluster V e) >= &0))`;;
 270
 271 *)
 272
 273 let beta_bump_v1 = new_definition `!V e X. beta_bump_v1 V e X =
 274   let e' = VX V X DIFF e in
 275     (
 276       if (X IN mcell_set V /\ ~NULLSET X /\ e IN critical_edgeX V X /\ e' IN critical_edgeX V X /\
 277             (!f. f IN edgeX V X ==> (f = e) \/ (f = e') \/ (f IN subcritical_edgeX V X)))
 278       then bump (radV e) - bump (radV e')
 279       else (&0)
 280     )`;;
 281
 282 let cluster_gamma_v1 = new_definition `!V e Z. cluster_gamma_v1 V e Z=
 283    sum Z ( \ X.  gammaX V X lmfun  * critical_weight V X  + beta_bump_v1 V e X )`;;
 284
 285 let cell_cluster_estimate_v1 = new_definition `!V. cell_cluster_estimate_v1 V = (!e.
 286   (cluster_gamma_v1 V e (cell_cluster V e) >= &0))`;;
 287
 288 let lmfun_inequality = new_definition
 289   `!(V:real^N->bool). lmfun_inequality V = (!u.  u IN V ==>
 290      sum { v | v IN V /\ ~(u=v) /\ dist(u,v) <= &2*h0 } ( \v. lmfun (hl [u;v]) ) <= &12)`;;
 291
 292 let ball_annulus = new_definition
 293   `ball_annulus = cball((vec 0:real^3) , &2 * h0) DIFF ball(vec 0, &2)`;;
 294
 295 let lmfun_ineq_center = new_definition `!(V:real^N->bool). lmfun_ineq_center V =
 296      sum V ( \v. lmfun (hl [vec 0;v]) ) <= &12`;;
 297
 298 let fan_of_polyhedron = new_definition `fan_of_polyhedron s =
 299    { (v:real^3) | v extreme_point_of s } ,
 300    { {v,w}  | ~(v=w) /\ (convex hull {v,w}) face_of s }`;;
 301
 302
 303  end;;
 304
 305
 306