(* Nguyen Quang Truong *)
needs "Multivariate/vectors.ml";; (* Eventually should load entire *)
needs "Examples/analysis.ml";; (* multivariate-complex theory. *)
needs "Examples/transc.ml";; (* Then it won't need these three. *)
needs "convex_header.ml";;
needs "definitions_kepler.ml";;
let ups_x = new_definition ` ups_x x1 x2 x6 =
--x1 * x1 - x2 * x2 - x6 * x6 +
&2 * x1 * x6 +
&2 * x1 * x2 +
&2 * x2 * x6 `;;let rho = new_definition ` rho (x12 :real) x13 x14 x23 x24 x34 =
--(x14 * x14 * x23 * x23) -
x13 * x13 * x24 * x24 -
x12 * x12 * x34 * x34 +
&2 *
(x12 * x14 * x23 * x34 +
x12 * x13 * x24 * x34 +
x13 * x14 * x23 * x24) `;;let chi = new_definition ` chi x12 x13 x14 x23 x24 x34 =
x13 * x23 * x24 +
x14 * x23 * x24 +
x12 * x23 * x34 +
x14 * x23 * x34 +
x12 * x24 * x34 +
x13 * x24 * x34 -
&2 * x23 * x24 * x34 -
x12 * x34 * x34 -
x14 * x23 * x23 -
x13 * x24 * x24 `;;let delta = new_definition ` delta x12 x13 x14 x23 x24 x34 =
--(x12 * x13 * x23) -
x12 * x14 * x24 -
x13 * x14 * x34 -
x23 * x24 * x34 +
x12 * x34 * (--x12 + x13 + x14 + x23 + x24 - x34) +
x13 * x24 * (x12 - x13 + x14 + x23 - x24 + x34 ) +
x14 * x23 * ( x12 + x13 - x14 - x23 + x24 + x34 ) `;;let eta_v = new_definition ` eta_v v1 v2 (v3: real^N) =
let e1 = dist (v2, v3) in
let e2 = dist (v1, v3) in
let e3 = dist (v2, v1) in
e1 * e2 * e3 / sqrt ( ups_x (e1 pow 2 ) ( e2 pow 2) ( e3 pow 2 ) ) `;;let delta_x12 = new_definition ` delta_x12 x12 x13 x14 x23 x24 x34 =
-- x13 * x23 + -- x14 * x24 + x34 * ( -- x12 + x13 + x14 + x23 + x24 + -- x34 )
+ -- x12 * x34 + x13 * x24 + x14 * x23 `;;
let delta_x13 = new_definition` delta_x13 x12 x13 x14 x23 x24 x34 =
-- x12 * x23 + -- x14 * x34 + x12 * x34 + x24 * ( x12 + -- x13 + x14 + x23 +
-- x24 + x34 ) + -- x13 * x24 + x14 * x23 `;;
let delta_x14 = new_definition`delta_x14 x12 x13 x14 x23 x24 x34 =
--x12 * x24 +
--x13 * x34 +
x12 * x34 +
x13 * x24 +
x23 * (x12 + x13 + --x14 + --x23 + x24 + x34) +
--x14 * x23`;;let delta_x34 = new_definition` delta_x34 x12 x13 x14 x23 x24 x34 =
-- &2 * x12 * x34 +
--x13 * x14 +
--x23 * x24 +
x13 * x24 +
x14 * x23 +
--x12 * x12 +
x12 * x14 +
x12 * x24 +
x12 * x13 +
x12 * x23`;;let delta_x23 = new_definition ` delta_x23 x12 x13 x14 x23 x24 x34 =
--x12 * x13 +
--x24 * x34 +
x12 * x34 +
x13 * x24 +
--x14 * x23 +
x14 * (x12 + x13 - x14 - x23 + x24 + x34) `;;let condA = new_definition `condA (v1:real^3) v2 v3 v4 x12 x13 x14 x23 x24 x34 =
( ~ ( v1 = v2 ) /\ coplanar {v1,v2,v3,v4} /\
( dist ( v1, v2) pow 2 ) = x12 /\
dist (v1,v3) pow 2 = x13 /\
dist (v1,v4) pow 2 = x14 /\
dist (v2,v3) pow 2 = x23 /\ dist (v2,v4) pow 2 = x24 )`;;let condC = new_definition ` condC M13 m12 m14 M24 m34 (m23:real) =
((! x. x IN {M13, m12, m14, M24, m34, m23 } ==> &0 <= x ) /\
M13 <= m12 + m23 /\
M13 <= m14 + m34 /\
M24 < m12 + m14 /\
M24 < m23 + m34 /\
&0 <= delta (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2 )
(m23 pow 2 ) )`;;let condF = new_definition` condF m14 m24 m34 M23 M13 M12 =
((!x. x IN {m14, m24, m34, M23, M13, M12} ==> &0 < x) /\
M12 < m14 + m24 /\
M13 < m14 + m34 /\
M23 < m24 + m34 /\
&0 <
delta (m14 pow 2) (m24 pow 2) (m34 pow 2) (M23 pow 2) (M13 pow 2)
(M12 pow 2)) `;;let condS = new_definition ` condS m m34 M13 M23 <=>
(!t. t IN {m, m34, M13, M23} ==> &0 < t) /\
M13 < m + m34 /\
M23 < m + m34 /\
M13 pow 2 < M23 pow 2 + &4 * m * m /\
M23 pow 2 < M13 pow 2 + &4 * m * m /\
(!r. delta (&4 * m * m) (M13 pow 2) (M23 pow 2) r (M13 pow 2) (M23 pow 2) = &0
==> r < &4 * m34 * m34) `;;let cos_arc = new_definition` cos_arc (a:real) b c =
( a pow 2 + b pow 2 - c pow 2 )/ ( &2 * a * b ) `;;
let muy_v = new_definition ` muy_v (x1: real^N ) (x2:real^N) (x3:real^N) (x4:real^N)
(x5:real^N) x45 =
(let x12 = dist (x1,x2) pow 2 in
let x13 = dist (x1,x3) pow 2 in
let x14 = dist (x1,x4) pow 2 in
let x15 = dist (x1,x5) pow 2 in
let x23 = dist (x2,x3) pow 2 in
let x24 = dist (x2,x4) pow 2 in
let x25 = dist (x2,x5) pow 2 in
let x34 = dist (x3,x4) pow 2 in
let x35 = dist (x3,x5) pow 2 in
cayleyR x12 x13 x14 x15 x23 x24 x25 x34 x35 x45) `;;let sqrt_of_ge_root = new_definition `
sqrt_of_ge_root y14 y24 y34 y12 y13 y23 y15 y25 y35 =
(@r. ?le ge a.
le <= ge /\
r = sqrt ge /\
(!x. cayleyR (y12 pow 2) (y13 pow 2) (y14 pow 2)
(y15 pow 2)
(y23 pow 2)
(y24 pow 2)
(y25 pow 2)
(y34 pow 2)
(y35 pow 2)
x =
a * (x - le) * (x - ge))) `;;let equivalent_lemma = prove(` (?t1 t2 t3.
!v1 v2 v3 (v:real^N).
v
IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
==> v =
t1 v1 v2 v3 v % v1 + t2 v1 v2 v3 v % v2 + t3 v1 v2 v3 v % v3 /\
t1 v1 v2 v3 v + t2 v1 v2 v3 v + t3 v1 v2 v3 v = &1 /\
(!ta tb tc.
v = ta % v1 + tb % v2 + tc % v3
==> ta =
t1 v1 v2 v3 v /\
tb = t2 v1 v2 v3 v /\
tc = t3 v1 v2 v3 v)) <=>
( !v1 v2 v3 (v:real^N).
v
IN affine hull {v1, v2, v3} /\ ~collinear {v1, v2, v3}
==> (?t1 t2 t3.
v =
t1 % v1 + t2 % v2 + t3 % v3 /\
t1 + t2 + t3 = &1 /\
(!ta tb tc.
v = ta % v1 + tb % v2 + tc % v3
==> ta =
t1 /\ tb = t2 /\ tc = t3))) `,
let plane_3p = new_definition `plane_3p (a:real^3) b c =
{x | ~collinear {a, b, c} /\
(?ta tb tc. ta + tb + tc = &1 /\ x = ta % a + tb % b + tc % c)}`;;let split = new_definition` split v0 v1 w u1 w' p =
( radV {v0, v1, w, u1} < eta_y (d3 w v0) (&2) #2.51 /\
u1 IN aff_ge {v0, v1, w} {p}
==> w' IN aff_gt {v0, v1} {w, u1} /\
radV {v0, v1, w, w'} >= eta_y (d3 v0 v1) (&2) #2.51 /\
d3 w' v1 <= #2.51 /\
d3 w' v0 <= #2.51 /\
#2.77 <= d3 w' w ) `;;let c_def38 = new_definition ` c_def38 S v' v1 v2 v3 v4 h1 h2 h3 h4 l k
= ( CARD ({v', v1, v2, v3, v4} UNION S) = 5 + CARD S /\
packing ({v', v1, v2, v3, v4} UNION S) /\
quadp v' v1 v2 v3 v4 /\
S SUBSET quadc0 v' v1 v2 v3 v4 /\
(!vi. vi IN {v1, v2, v3, v4} ==> &2 <= d3 vi v' /\ d3 vi v' <= k) /\
d3 v1 v2 <= k /\
d3 v2 v3 <= k /\
d3 v3 v4 <= k /\
d3 v4 v1 <= k /\
&2 <= d3 v1 v2 /\
&2 <= d3 v2 v3 /\
&2 <= d3 v3 v4 /\
&2 <= d3 v4 v1 /\
&2 <= d3 v1 v3 /\
&2 <= d3 v2 v4 /\
(!v. v IN S
==> &2 <= d3 v v' /\
d3 v v' <= l /\
h1 <= d3 v v1 /\
h2 <= d3 v v2 /\
h3 <= d3 v v3 /\
h4 <= d3 v v4) )`;;let small = new_definition ` small s =
( CARD s = 3 /\
packing s /\
(!x y. {(x:real^3) , y} SUBSET s ==> d3 x y < sqrt8) /\
(!x y z.
{x, y, z} = s /\ #2.51 < d3 x y /\ #2.51 < d3 y z
==> radV s < sqrt (&2)) ) `;;