legacy/oldnonlinear/post.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-10-15                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* This file is not used.  I think it can be deleted. *)
  10
  11 (* This file connects inequalities from the book with the form in which
  12 they appear in ineq.hl and main_estimate_ineq.hl
  13
  14 In the proofs of the conclusions, inequalities from ineq.hl and main_estimate_ineq.hl may
  15 be used freely.
  16
  17 Here are the computer calculations mentioned by ID in Dense Sphere Packings
  18
  19 packing.tex:
  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)
  25
  26 local.tex:
  27 UPONLFY (tau* is increasing in y4)
  28 5202826650 a (stability estimates, tautri-div-sqrt-delta \ge 0)
  29
  30 supplement_local.tex:
  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).
  34
  35 tame.tex:
  36 TVAWGDR (Delta >0 for certain simplex bounds)
  37 KCBLRQC (b table estimates)
  38
  39 *)
  40
  41 (*
  42 post form of "2065952723 A1"
  43 4828966562, 8964099283,
  44 6843920790, 5512912661,
  45  main_estimate_ineq.hl
  46 *)
  47
  48 module Post = struct
  49
  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)`;;
  57
  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.
  62
  63    Conversely, given deltaV w1 w2 w3 w4 = delta_y ..... a b c > &0.
  64    Let vi = (y1/2) * wi and repeat the process
  65 *)
  66
  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 /\
  76     rho y1 = e1 /\
  77     rho y2 = e2 /\
  78     rho y3 = e3 /\
  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)))`;;
  82
  83
  84 (* proof:
  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.
  90 *)
  91
  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 /\
 101     rho y1 = e1 /\
 102     rho y2 = e2 /\
 103     rho y3 = e3 /\
 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)))`;;
 109
 110 (* proof:
 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.
 116 *)
 117
 118 (* post form of 1117202051, 4559601669, 4559601669b, 2485876245a  *)
 119
 120 let post_delta4_concl = `!y1 y2 y3 y4 y5 y6.
 121    &0 < delta_y y1 y2 y3 y4  y5 y6  /\
 122     &0 < y1 /\
 123    delta4_y y1 y2 y3 y4 y5 y6 < &0 ==>
 124   pi/ &2 < dih_y y1 y2 y3 y4 y5 y6`;;
 125
 126 let post_delta4_concl2 = `!y1 y2 y3 y4 y5 y6.
 127    &0 < delta_y y1 y2 y3 y4  y5 y6  /\
 128     &0 < y1 /\
 129    &0 < delta4_y y1 y2 y3 y4 y5 y6  ==>
 130  dih_y y1 y2 y3 y4 y5 y6 <  pi/ &2 `;;
 131
 132 (* proof:
 133   See Sphere.dih_x;;
 134 *)
 135
 136 (* post form of 4322269127, 5556646409   *)
 137
 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)`;;
 142
 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)`;;
 148
 149 (* post form of hexagons SAUZWSD:
 150    5338748573, 3306409086, 9075398267, 1324821088,
 151    4108834026, 6388508112, 5493250206, 2283016857, 4872337467, 3615835903, 2535350075,
 152    all top edges 2.
 153   *)
 154
 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))) /\
 159   (?v1 v2 v3 v4 v5 v6.
 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)`;;
 164 *)
 165
 166 (* better form of the preceding *)
 167
 168
 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''})) ==>
 177  (tauV v1 v3 v5 +
 178   tauV v1 v2 v3 +  tauV v3 v4 v5 + tauV v5 v6 v1 > #0.712)`;;
 179
 180 (* post form of "5202826650 a" *)
 181
 182 (* See lemma OWZLKVY.
 183    Some lemmas have already been proved about tau_residual_x in relation to taum. *)
 184
 185 (* post form of pentagons  EDZEPIH:
 186   7067938795, 9459075374, 2559885109, 9861833891, 8199484193, 3980286827,
 187  "3221740746 a", 8520556953, 9977174768,
 188
 189 *)
 190
 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)`;;
 200
 201
 202 (* old form:
 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))) /\
 207   (?v1 v2 v3 v4 v5.
 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)
 214    )
 215    ==> (tau_fun V E FF > #0.616)`;;
 216 *)
 217
 218
 219
 220
 221 end;;