1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Nonlinear *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
9 (* This file is not used. I think it can be deleted. *)
11 (* This file connects inequalities from the book with the form in which
12 they appear in ineq.hl and main_estimate_ineq.hl
14 In the proofs of the conclusions, inequalities from ineq.hl and main_estimate_ineq.hl may
17 Here are the computer calculations mentioned by ID in Dense Sphere Packings
20 TSKAJXY (Lemma 6.92, gamma(X,L) \ge 0).
21 OXLZLEZ (Lemma 6.93, Gamma(epsilon) \ge 0)
22 BIEFJHU (Lemma 6.110, card V = 13, 14, 15)
23 WAZLDCD (Lemma 6.112, saturation lemma)
24 UKBRPFE (Lemma 6.112, saturation lemma)
27 UPONLFY (tau* is increasing in y4)
28 5202826650 a (stability estimates, tautri-div-sqrt-delta \ge 0)
31 1117202051 (the solid angle at a pole is at least pi/2)
32 4559601669 (the solid angle at a pole is at least pi/2)
33 with $k(s)\le 4$, by a \cc{various inequalities}{}, (k<=4 implies tau*(s,v)>0).
36 TVAWGDR (Delta >0 for certain simplex bounds)
37 KCBLRQC (b table estimates)
42 post form of "2065952723 A1"
43 4828966562, 8964099283,
44 6843920790, 5512912661,
50 let post_206A1_concl = `!y1 y2 y3 y4 y5 y6 a b c.
51 (arclength (&2) (&2) a = arclength y2 y3 y4 /\
52 arclength (&2) (&2) b = arclength y1 y3 y5 /\
53 arclength (&2) (&2) c = arclength y1 y2 y6) /\
54 &0 < y1 /\ &0 < y2 /\ &0 < y3 /\ &0 < y4 /\ &0 < y5 /\ &0 < y6 /\
55 &0 < a /\ a < &4 /\ &0 < b /\ b < &4 /\ &0 < c /\ c < &4 ==>
56 (delta_y y1 y2 y3 y4 y5 y6 > &0 <=> delta_y (&2) (&2) (&2) a b c > &0)`;;
58 (* proof : if delta_y > 0, then ?v1 v2 v3 v4. deltaV v1 v2 v3 v4 = delta_y y1 y2 y3 y4 y5 y6
59 then let wi = 2* vi/|vi|,
60 then deltaV w1 w2 w3 w4 > 0,
61 also deltaV w1 w2 w3 w4 = delta_y (&2) (&2) (&2) a b c.
63 Conversely, given deltaV w1 w2 w3 w4 = delta_y ..... a b c > &0.
64 Let vi = (y1/2) * wi and repeat the process
67 let post_206A1_concl2 = `!y1 y2 y3 y4 y5 y6 a b c e1 e2 e3 f'.
68 arclength (&2) (&2) a = arclength y2 y3 y4 /\
69 arclength (&2) (&2) b = arclength y1 y3 y5 /\
70 arclength (&2) (&2) c = arclength y1 y2 y6 /\
71 &2 <= y1 /\ y1 <= #2.52 /\
72 &2 <= y2 /\ y2 <= #2.52 /\
73 &2 <= y3 /\ y3 <= #2.52 /\
74 &0 < y4 /\ &0 < y5 /\ &0 < y6 /\
75 y4 < y2 + y3 /\ y5 < y1 + y3 /\ y6 < y1 + y2 /\
79 (&0 < delta_y y1 y2 y3 y4 y5 y6 ) /\
80 ((has_real_derivative) (\y. taum y1 y2 y3 y y5 y6) f' (atreal y4)) ==>
81 (?r. &0 < r /\ (f' = r * num1 e1 e2 e3 (a pow 2) (b pow 2) (c pow 2)))`;;
85 Rewrite the variables y1...y6 in terms of variables a,b,c,e1,e2,e3.
86 Use calc_derivative.hl to calculate the y4 derivative of taum
87 and to simplify the rational expression.
88 num1 appears as the numerator in that expression.
89 See the mathematica notes in sphere.hl next to the definition of num1.
92 let post_206A1_concl3 = `!y1 y2 y3 y4 y5 y6 a b c e1 e2 e3 f' f''.
93 arclength (&2) (&2) a = arclength y2 y3 y4 /\
94 arclength (&2) (&2) b = arclength y1 y3 y5 /\
95 arclength (&2) (&2) c = arclength y1 y2 y6 /\
96 &2 <= y1 /\ y1 <= #2.52 /\
97 &2 <= y2 /\ y2 <= #2.52 /\
98 &2 <= y3 /\ y3 <= #2.52 /\
99 &0 < y4 /\ &0 < y5 /\ &0 < y6 /\
100 y4 < y2 + y3 /\ y5 < y1 + y3 /\ y6 < y1 + y2 /\
104 (&0 < delta_y y1 y2 y3 y4 y5 y6 ) /\
105 (?eps. (&0 < eps) ==>
106 (!u. abs(u- y4) < eps ==> (has_real_derivative) (\y. taum y1 y2 y3 y y5 y6) (f' u) (atreal u))) /\
107 ((has_real_derivative) f' f'' (atreal y4)) ==>
108 (?r. &0 < r /\ (f'' = r * num2 e1 e2 e3 (a pow 2) (b pow 2) (c pow 2)))`;;
111 Rewrite the variables y1...y6 in terms of variables a,b,c,e1,e2,e3.
112 Use calc_derivative.hl to calculate the y4 second derivative of taum
113 and to simplify the rational expression.
114 num2 appears as the numerator in that expression.
115 See the mathematica notes in sphere.hl next to the definition of num2.
118 (* post form of 1117202051, 4559601669, 4559601669b, 2485876245a *)
120 let post_delta4_concl = `!y1 y2 y3 y4 y5 y6.
121 &0 < delta_y y1 y2 y3 y4 y5 y6 /\
123 delta4_y y1 y2 y3 y4 y5 y6 < &0 ==>
124 pi/ &2 < dih_y y1 y2 y3 y4 y5 y6`;;
126 let post_delta4_concl2 = `!y1 y2 y3 y4 y5 y6.
127 &0 < delta_y y1 y2 y3 y4 y5 y6 /\
129 &0 < delta4_y y1 y2 y3 y4 y5 y6 ==>
130 dih_y y1 y2 y3 y4 y5 y6 < pi/ &2 `;;
136 (* post form of 4322269127, 5556646409 *)
138 let post_mdtau_concl = `!y1 y2 y3 y4 y5 y6 f'.
139 &0 < delta_y y1 y2 y3 y4 y5 y6 /\
140 (has_real_derivative) (\y. taum y y2 y3 y4 y5 y6) f' (atreal y1) ==>
141 (?r. &0 < r /\ f' = r * mdtau_y y1 y2 y3 y4 y5 y6)`;;
143 let post_mdtau2_concl = `!y1 y2 y3 y4 y5 y6 f' f''.
144 &0 < delta_y y1 y2 y3 y4 y5 y6 /\
145 (?eps. (&0 < eps) /\ (!u. (has_real_derivative) (\y. taum y y2 y3 y4 y5 y6) (f' u) (atreal u))) /\
146 (has_real_derivative) f' f'' (atreal y1) ==>
147 (?r. &0 < r /\ f'' = r * mdtau2uf_y y1 y2 y3 y4 y5 y6)`;;
149 (* post form of hexagons SAUZWSD:
150 5338748573, 3306409086, 9075398267, 1324821088,
151 4108834026, 6388508112, 5493250206, 2283016857, 4872337467, 3615835903, 2535350075,
155 (* `!V E FF. convex_local_fan (V,E,FF) /\
156 V HAS_SIZE 6 /\ (V SUBSET BB) /\
157 (!v1 v2. {v1,v2} IN E ==> dist (v1,v2) = &2) /\
158 (!w1 w2. ~({w1,w2} IN E) /\ (w1 IN V) /\ (w2 IN V) ==> (#3.01 <= dist(w1,w2))) /\
160 V = {v1,v2,v3,v4,v5,v6} /\
161 E = {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v6},{v6,v1}} /\
162 (!w1 w2. {w1,w2} IN {{v1,v3},{v3,v5},{v5,v1}} ==> dist(w1,w2) <= #3.915)))
163 ==> (tau_fun V E FF > #0.712)`;;
166 (* better form of the preceding *)
169 let post_SAUZWSD_concl = `!v1 v2 v3 v4 v5 v6.
170 ({v1,v2,v3,v4,v5,v6} SUBSET ball_annulus) /\
171 (!w1 w2. {w1,w2} IN {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v6},{v6,v1}}
172 ==> dist(w1,w2)= &2) /\
173 (!w1 w2. {w1,w2} IN {{v1,v3},{v3,v5},{v5,v1}}
174 ==> (#3.01 <= dist(w1,w2) /\ dist(w1,w2) <= #3.915)) /\
175 (!w w' w''. {w,w',w''} IN {{v2,v1,v3},{v4,v3,v5},{v6,v5,v1}} ==>
176 (norm w = &2 \/ norm w = #2.52 \/ w' IN aff_gt { vec 0 } {w',w''})) ==>
178 tauV v1 v2 v3 + tauV v3 v4 v5 + tauV v5 v6 v1 > #0.712)`;;
180 (* post form of "5202826650 a" *)
182 (* See lemma OWZLKVY.
183 Some lemmas have already been proved about tau_residual_x in relation to taum. *)
185 (* post form of pentagons EDZEPIH:
186 7067938795, 9459075374, 2559885109, 9861833891, 8199484193, 3980286827,
187 "3221740746 a", 8520556953, 9977174768,
191 let post_EDZEPIH_concl = `!v1 v2 v3 v4 v5.
192 {v1,v2,v3,v4,v5} SUBSET ball_annulus /\
193 (!w1 w2. {w1,w2} IN {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v1}} ==> dist(w1,w2)= &2) /\
194 (!w1 w2. {w1,w2} IN {{v1,v3},{v1,v4}}
195 ==> (#3.01 <= dist(w1,w2) /\ (dist(w1,w2) <= #3.24))) /\
196 (pi/ &2 <= dihV (vec 0) v1 v2 v3 + dihV (vec 0) v2 v3 v4 + dihV (vec 0) v3 v4 v5) /\
197 (!w w' w''. {w,w',w''} IN {{v2,v1,v3},{v5,v4,v1}} ==>
198 (norm w = &2 \/ norm w = #2.52 \/ w' IN aff_gt { vec 0 } {w',w''})) ==>
199 (tauV v1 v3 v4 + tauV v1 v2 v3 + tauV v1 v4 v5 > #0.616)`;;
203 let post_EDZEPIH_concl = `!V E FF. convex_local_fan (V,E,FF) /\
204 V HAS_SIZE 5 /\ (V SUBSET BB) /\
205 (!v1 v2. {v1,v2} IN E ==> dist (v1,v2) = &2) /\
206 (!w1 w2. ~({w1,w2} IN E) /\ (w1 IN V) /\ (w2 IN V) ==> (#3.01 <= dist(w1,w2))) /\
208 V = {v1,v2,v3,v4,v5} /\
209 E = {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v1}} /\
210 dist(v1,v3) <= #3.24 /\
211 dist(v1,v4) <= #3.24 /\
212 (norm v2 = &2 \/ norm v2 = #2.52 \/ azim (vec 0) v2 v3 v1 = pi) /\
213 (norm v5 = &2 \/ norm v5 = #2.52 \/ azim (vec 0) v5 v1 v4 = pi)
215 ==> (tau_fun V E FF > #0.616)`;;