(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Nonlinear *)
(* Author: Thomas C. Hales *)
(* Date: 2012-10-15 *)
(* ========================================================================== *)
(* This file is not used. I think it can be deleted. *)
(* This file connects inequalities from the book with the form in which
they appear in ineq.hl and main_estimate_ineq.hl
In the proofs of the conclusions, inequalities from ineq.hl and main_estimate_ineq.hl may
be used freely.
Here are the computer calculations mentioned by ID in Dense Sphere Packings
packing.tex:
TSKAJXY (Lemma 6.92, gamma(X,L) \ge 0).
OXLZLEZ (Lemma 6.93, Gamma(epsilon) \ge 0)
BIEFJHU (Lemma 6.110, card V = 13, 14, 15)
WAZLDCD (Lemma 6.112, saturation lemma)
UKBRPFE (Lemma 6.112, saturation lemma)
local.tex:
UPONLFY (tau* is increasing in y4)
5202826650 a (stability estimates, tautri-div-sqrt-delta \ge 0)
supplement_local.tex:
1117202051 (the solid angle at a pole is at least pi/2)
4559601669 (the solid angle at a pole is at least pi/2)
with $k(s)\le 4$, by a \cc{various inequalities}{}, (k<=4 implies tau*(s,v)>0).
tame.tex:
TVAWGDR (Delta >0 for certain simplex bounds)
KCBLRQC (b table estimates)
*)
(*
post form of "2065952723 A1"
4828966562, 8964099283,
6843920790, 5512912661,
main_estimate_ineq.hl
*)
module Post = struct
let post_206A1_concl = `!y1 y2 y3 y4 y5 y6 a b c.
(arclength (&2) (&2) a = arclength y2 y3 y4 /\
arclength (&2) (&2) b = arclength y1 y3 y5 /\
arclength (&2) (&2) c = arclength y1 y2 y6) /\
&0 < y1 /\ &0 < y2 /\ &0 < y3 /\ &0 < y4 /\ &0 < y5 /\ &0 < y6 /\
&0 < a /\ a < &4 /\ &0 < b /\ b < &4 /\ &0 < c /\ c < &4 ==>
(delta_y y1 y2 y3 y4 y5 y6 > &0 <=> delta_y (&2) (&2) (&2) a b c > &0)`;;
(* proof : if delta_y > 0, then ?v1 v2 v3 v4. deltaV v1 v2 v3 v4 = delta_y y1 y2 y3 y4 y5 y6
then let wi = 2* vi/|vi|,
then deltaV w1 w2 w3 w4 > 0,
also deltaV w1 w2 w3 w4 = delta_y (&2) (&2) (&2) a b c.
Conversely, given deltaV w1 w2 w3 w4 = delta_y ..... a b c > &0.
Let vi = (y1/2) * wi and repeat the process
*)
let post_206A1_concl2 = `!y1 y2 y3 y4 y5 y6 a b c e1 e2 e3 f'.
arclength (&2) (&2) a = arclength y2 y3 y4 /\
arclength (&2) (&2) b = arclength y1 y3 y5 /\
arclength (&2) (&2) c = arclength y1 y2 y6 /\
&2 <= y1 /\ y1 <= #2.52 /\
&2 <= y2 /\ y2 <= #2.52 /\
&2 <= y3 /\ y3 <= #2.52 /\
&0 < y4 /\ &0 < y5 /\ &0 < y6 /\
y4 < y2 + y3 /\ y5 < y1 + y3 /\ y6 < y1 + y2 /\
rho y1 = e1 /\
rho y2 = e2 /\
rho y3 = e3 /\
(&0 < delta_y y1 y2 y3 y4 y5 y6 ) /\
((has_real_derivative) (\y. taum y1 y2 y3 y y5 y6) f' (atreal y4)) ==>
(?r. &0 < r /\ (f' = r * num1 e1 e2 e3 (a pow 2) (b pow 2) (c pow 2)))`;;
(* proof:
Rewrite the variables y1...y6 in terms of variables a,b,c,e1,e2,e3.
Use calc_derivative.hl to calculate the y4 derivative of taum
and to simplify the rational expression.
num1 appears as the numerator in that expression.
See the mathematica notes in sphere.hl next to the definition of num1.
*)
let post_206A1_concl3 = `!y1 y2 y3 y4 y5 y6 a b c e1 e2 e3 f' f''.
arclength (&2) (&2) a = arclength y2 y3 y4 /\
arclength (&2) (&2) b = arclength y1 y3 y5 /\
arclength (&2) (&2) c = arclength y1 y2 y6 /\
&2 <= y1 /\ y1 <= #2.52 /\
&2 <= y2 /\ y2 <= #2.52 /\
&2 <= y3 /\ y3 <= #2.52 /\
&0 < y4 /\ &0 < y5 /\ &0 < y6 /\
y4 < y2 + y3 /\ y5 < y1 + y3 /\ y6 < y1 + y2 /\
rho y1 = e1 /\
rho y2 = e2 /\
rho y3 = e3 /\
(&0 < delta_y y1 y2 y3 y4 y5 y6 ) /\
(?eps. (&0 < eps) ==>
(!u. abs(u- y4) < eps ==> (has_real_derivative) (\y. taum y1 y2 y3 y y5 y6) (f' u) (atreal u))) /\
((has_real_derivative) f' f'' (atreal y4)) ==>
(?r. &0 < r /\ (f'' = r * num2 e1 e2 e3 (a pow 2) (b pow 2) (c pow 2)))`;;
(* proof:
Rewrite the variables y1...y6 in terms of variables a,b,c,e1,e2,e3.
Use calc_derivative.hl to calculate the y4 second derivative of taum
and to simplify the rational expression.
num2 appears as the numerator in that expression.
See the mathematica notes in sphere.hl next to the definition of num2.
*)
(* post form of 1117202051, 4559601669, 4559601669b, 2485876245a *)
let post_delta4_concl = `!y1 y2 y3 y4 y5 y6.
&0 < delta_y y1 y2 y3 y4 y5 y6 /\
&0 < y1 /\
delta4_y y1 y2 y3 y4 y5 y6 < &0 ==>
pi/ &2 < dih_y y1 y2 y3 y4 y5 y6`;;
let post_delta4_concl2 = `!y1 y2 y3 y4 y5 y6.
&0 < delta_y y1 y2 y3 y4 y5 y6 /\
&0 < y1 /\
&0 < delta4_y y1 y2 y3 y4 y5 y6 ==>
dih_y y1 y2 y3 y4 y5 y6 < pi/ &2 `;;
(* proof:
See Sphere.dih_x;;
*)
(* post form of 4322269127, 5556646409 *)
let post_mdtau_concl = `!y1 y2 y3 y4 y5 y6 f'.
&0 < delta_y y1 y2 y3 y4 y5 y6 /\
(has_real_derivative) (\y. taum y y2 y3 y4 y5 y6) f' (atreal y1) ==>
(?r. &0 < r /\ f' = r * mdtau_y y1 y2 y3 y4 y5 y6)`;;
let post_mdtau2_concl = `!y1 y2 y3 y4 y5 y6 f' f''.
&0 < delta_y y1 y2 y3 y4 y5 y6 /\
(?eps. (&0 < eps) /\ (!u. (has_real_derivative) (\y. taum y y2 y3 y4 y5 y6) (f' u) (atreal u))) /\
(has_real_derivative) f' f'' (atreal y1) ==>
(?r. &0 < r /\ f'' = r * mdtau2uf_y y1 y2 y3 y4 y5 y6)`;;
(* post form of hexagons SAUZWSD:
5338748573, 3306409086, 9075398267, 1324821088,
4108834026, 6388508112, 5493250206, 2283016857, 4872337467, 3615835903, 2535350075,
all top edges 2.
*)
(* `!V E FF. convex_local_fan (V,E,FF) /\
V HAS_SIZE 6 /\ (V SUBSET BB) /\
(!v1 v2. {v1,v2} IN E ==> dist (v1,v2) = &2) /\
(!w1 w2. ~({w1,w2} IN E) /\ (w1 IN V) /\ (w2 IN V) ==> (#3.01 <= dist(w1,w2))) /\
(?v1 v2 v3 v4 v5 v6.
V = {v1,v2,v3,v4,v5,v6} /\
E = {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v6},{v6,v1}} /\
(!w1 w2. {w1,w2} IN {{v1,v3},{v3,v5},{v5,v1}} ==> dist(w1,w2) <= #3.915)))
==> (tau_fun V E FF > #0.712)`;;
*)
(* better form of the preceding *)
let post_SAUZWSD_concl = `!v1 v2 v3 v4 v5 v6.
({v1,v2,v3,v4,v5,v6} SUBSET ball_annulus) /\
(!w1 w2. {w1,w2} IN {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v6},{v6,v1}}
==> dist(w1,w2)= &2) /\
(!w1 w2. {w1,w2} IN {{v1,v3},{v3,v5},{v5,v1}}
==> (#3.01 <= dist(w1,w2) /\ dist(w1,w2) <= #3.915)) /\
(!w w' w''. {w,w',w''} IN {{v2,v1,v3},{v4,v3,v5},{v6,v5,v1}} ==>
(norm w = &2 \/ norm w = #2.52 \/ w' IN aff_gt { vec 0 } {w',w''})) ==>
(tauV v1 v3 v5 +
tauV v1 v2 v3 + tauV v3 v4 v5 + tauV v5 v6 v1 > #0.712)`;;
(* post form of "5202826650 a" *)
(* See lemma OWZLKVY.
Some lemmas have already been proved about tau_residual_x in relation to taum. *)
(* post form of pentagons EDZEPIH:
7067938795, 9459075374, 2559885109, 9861833891, 8199484193, 3980286827,
"3221740746 a", 8520556953, 9977174768,
*)
let post_EDZEPIH_concl = `!v1 v2 v3 v4 v5.
{v1,v2,v3,v4,v5} SUBSET ball_annulus /\
(!w1 w2. {w1,w2} IN {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v1}} ==> dist(w1,w2)= &2) /\
(!w1 w2. {w1,w2} IN {{v1,v3},{v1,v4}}
==> (#3.01 <= dist(w1,w2) /\ (dist(w1,w2) <= #3.24))) /\
(pi/ &2 <= dihV (vec 0) v1 v2 v3 + dihV (vec 0) v2 v3 v4 + dihV (vec 0) v3 v4 v5) /\
(!w w' w''. {w,w',w''} IN {{v2,v1,v3},{v5,v4,v1}} ==>
(norm w = &2 \/ norm w = #2.52 \/ w' IN aff_gt { vec 0 } {w',w''})) ==>
(tauV v1 v3 v4 + tauV v1 v2 v3 + tauV v1 v4 v5 > #0.616)`;;
(* old form:
let post_EDZEPIH_concl = `!V E FF. convex_local_fan (V,E,FF) /\
V HAS_SIZE 5 /\ (V SUBSET BB) /\
(!v1 v2. {v1,v2} IN E ==> dist (v1,v2) = &2) /\
(!w1 w2. ~({w1,w2} IN E) /\ (w1 IN V) /\ (w2 IN V) ==> (#3.01 <= dist(w1,w2))) /\
(?v1 v2 v3 v4 v5.
V = {v1,v2,v3,v4,v5} /\
E = {{v1,v2},{v2,v3},{v3,v4},{v4,v5},{v5,v1}} /\
dist(v1,v3) <= #3.24 /\
dist(v1,v4) <= #3.24 /\
(norm v2 = &2 \/ norm v2 = #2.52 \/ azim (vec 0) v2 v3 v1 = pi) /\
(norm v5 = &2 \/ norm v5 = #2.52 \/ azim (vec 0) v5 v1 v4 = pi)
)
==> (tau_fun V E FF > #0.616)`;;
*)
end;;