1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
9 (* definitions needed for the chapter Packing *)
12 flyspeck_needs "volume/vol1.hl";;
14 module Pack_defs = struct
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))`;;
20 let negligible_fun_0 = new_definition `negligible_fun_0 f S = negligible_fun_p f S ((vec:num->real^3) 0)`;;
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)`;;
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)))`;;
26 let HL = new_definition `hl (ul:(real^N)list) = radV (set_of_list ul)`;;
28 let REVERSE_TABLE = define `(REVERSE_TABLE (f:num->A) 0 = []) /\
29 (REVERSE_TABLE f (SUC i) = CONS (f i) ( REVERSE_TABLE f i))`;;
31 let TABLE = new_definition `!(f:num->A) k. TABLE f k = REVERSE (REVERSE_TABLE f k)`;;
33 let left_action = new_definition `!p f x. left_action (p:A->C) (f:A->B) x = f(inverse p x)`;;
35 let left_action_list = new_definition `left_action_list p (ul:(A)list) = TABLE (\i. EL (inverse p i) ul) (LENGTH ul)`;;
37 let DROP = define `(DROP (ul:(A)list) 0 = TL ul) /\ (DROP ul (SUC i) = CONS(HD ul) (DROP (TL ul) i))`;;
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))))`;;
47 new_definition `!V ul. mcell0 V ul = rogers V ul DIFF ball(HD ul,sqrt(&2))`;;
49 (* June 17, 2011, changed to mcell1, mcell2 to
50 weak ineq sqrt(&2) <= hl ul to fix an error
53 let mcell1 = new_definition `!V ul. mcell1 V ul =
54 if (sqrt(&2) <= hl ul)
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)))
61 let mcell2 = new_definition `!V ul. mcell2 V ul =
62 if (hl (truncate_simplex 1 ul) < sqrt(&2)) /\ (sqrt(&2) <= hl ul)
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 })
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 })
75 let mcell4 = new_definition `!V ul. mcell4 (V:real^3->bool) (ul:(real^3)list) =
77 then convex hull (set_of_list ul)
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`;;
84 let mcell_set = new_definition `mcell_set V =
85 { X | ?i ul. (X = mcell i V ul) /\ ul IN barV V 3 }`;;
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)`;;
91 let VX = new_definition
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)))`;;
100 let edgeX = new_definition `!V X. edgeX V X = { ({u,v}) | VX V X u /\ VX V X v /\ ~(u=v) }`;;
102 let total_solid = new_definition `!V X x. total_solid V X = sum ( VX V X ) (\(x:real^3). (sol x X))`;;
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).
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))`;;
116 (* The sum has a single term *)
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) ))`;;
124 (* The sum has two terms. Take the average *)
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) ))`;;
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)
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)`;;
144 let dihu3 = new_definition `!V ul. dihu3 V ul =
145 dihV (EL 0 ul) (EL 1 ul) (EL 2 ul) (mxi V ul)`;;
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)`;;
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)`;;
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
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`;;
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))`;;
175 let marchal = new_definition `marchal h =
176 (if (h <= sqrt(&2)) then marchal_quartic h else &0)`;;
178 (* changed March 16, 2012, following Ky's suggestion. *)
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)))`;;
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]))`;;
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)`;;
196 let h0 = new_definition `h0 = #1.26`;;
198 let lfun = new_definition `lfun h = (h0 - h)/(h0 - &1)`;;
200 let lmfun = new_definition `lmfun h = if (h<=h0) then (h0 - h)/(h0 - &1) else &0`;;
202 let hminus = new_definition `hminus = @x. #1.2 <= x /\ x < #1.3 /\ marchal_quartic x = lmfun x`;;
204 let critical_edgeX =new_definition
205 `critical_edgeX V X = { {u,v} | {u,v} IN edgeX V X /\ hminus <= hl [u;v] /\
208 let subcritical_edgeX =new_definition
209 `subcritical_edgeX V X = { {u,v} | {u,v} IN edgeX V X /\ hl [u;v] < hminus }`;;
211 let critical_weight = new_definition
212 `! V X. critical_weight V X = &1/ &(CARD (critical_edgeX V X))`;;
214 let bump = new_definition `!h. bump h = #0.005*(&1 - ((h- h0) pow 2)/((hplus - h0) pow 2))`;;
216 let critical_edge_y = new_definition `critical_edge_y y = ((&2*hminus <= y) /\ (y <= &2 *hplus))`;;
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))`;;
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) `;;
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`;;
237 let cell_cluster = new_definition
238 `!V e. cell_cluster V e = { X | e IN critical_edgeX V X /\ mcell_set V X }`;;
240 (* Next definitions deprecated, Dec 1, 2012.
241 Obsolete Jan 2, 2013. *)
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 ))`;;
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 )`;;
253 let cell_cluster_estimate = new_definition `!V. cell_cluster_estimate V = (!e.
254 (cluster_gammaX V e (cell_cluster V e) >= &0))`;;
256 (* average over all 4 = 2! x 2! possible representations *)
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 ))`;;
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 )`;;
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))`;;
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
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')
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 )`;;
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))`;;
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)`;;
292 let ball_annulus = new_definition
293 `ball_annulus = cball((vec 0:real^3) , &2 * h0) DIFF ball(vec 0, &2)`;;
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`;;
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 }`;;