(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Nonlinear *)
(* Author: Thomas C. Hales *)
(* Date: 2011-05-13 *)
(* ========================================================================== *)
(* TO DO XX
replace 0.696 -> 0.616 systematically in estimates.
(2013-05-05, changed 0.696->0.616 in 7697147739 and 4680581274)
*)
(* New test inequalities from May 2011. Redo all the tameTableD calculations,
together with associated nontriangular ad hoc LP estimates.
HEX (1 CASE):
tameTableD[6,0] has dropped to 0.712.
// old values: 0.7578, 0.723, ...
PENT (3 CASES):
tameTableD[4,1] = 0.616. This is AD HOC tauB5h in head.mod
tameTableD[5,0] = 0.4819. This is (standard) tau5 in head.mod
tau >= 0.616, diags >= sqrt8. This is AD HOC tau5h 9620775909-5 in head.mod
// old values: 0.696->0.616, 0.6548->0.616.
QUAD (2 CASES):
tau >= 0.477, diags >= sqrt8, 1edge [2.52,sqrt8]. This is AD HOC tauB4h 9620775909 in head.mod:
tau >= 0.467 diags >= 3. This is AD HOC 9563139965D in body.mod
+ standard B-series quad inequalities.
*)
(* This file does *not* treat the standard quad LP cases:
["3862621143";"4240815464";"6944699408";"7043724150"]
which are proved by usual quad methods *)
module Main_estimate_ineq = struct
let mk_tplate = Ineq.mk_tplate ;;
let all_forall = Sphere.all_forall;;
let add = Ineq.add;;
let skip = Ineq.skip;;
let addtex = Ineq.addtex;;
addtex(Section,"Main Estimate","Definitions");
(* for sphere.hl *)
add
{
idv = "1834976363";
doc = "replacement for 22065952723 A1";
tags=[Main_estimate;Flypaper["UPONLFY"];Tex];
ineq = all_forall `ineq
[
(&1 , x1, &1 + sol0/ pi);
(&1 , x2, &1 + sol0/ pi);
(&1 , x3, &1 + sol0/ pi);
((&2 / h0) pow 2, x4, #15.53);
((&2 / h0) pow 2, x5, &4 pow 2);
((&2 / h0) pow 2, x6, &4 pow 2)
]
(num1 x1 x2 x3 x4 x5 x6 > &0 \/
num1 x1 x2 x3 x4 x5 x6 < &0 \/
dnum1 x1 x2 x3 x4 x5 x6 < &0)`;
};;
add
{
idv="4828966562";
doc = "If minor diag >= 3, then 3/1.26 > 2.38 and we can contract.
15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
Added May 12, 2011.
c2 upper bound changed from 15.53 to 16.0 on May 23.";
tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];];
ineq = all_forall `ineq
[
(&1 , e1, &1 + sol0/ pi);
(&1 , e2, &1 + sol0/ pi);
(&1 , e3, &1 + sol0/ pi);
((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
((&2/ h0) pow 2, b2, #3.01 pow 2);
(#2.38 pow 2, c2,#16.0)
]
((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;
add
{
idv="6843920790";
doc = "In a pentagon with one long edge, we can contract the long edge to 2.52,
or even to 2, using 2 diags.
The constant 2.38 < 3.01/h0.";
tags=[Main_estimate;Cfsqp;Tex;Flypaper["UPONLFY"];];
ineq = all_forall `ineq
[
(&1 , e1, &1 + sol0/ pi);
(&1 , e2, &1 + sol0/ pi);
(&1 , e3, &1 + sol0/ pi);
((&2 / h0) pow 2, a2, #3.01 pow 2);
(#2.38 pow 2, b2, #15.53);
(#2.38 pow 2, c2, #15.53)
]
((num1 e1 e2 e3 a2 b2 c2 > &0) ) `;
};;
skip
{
idv="quadtest";
doc = "useful dimension reduction for quads. quadrilateral test";
tags=[Cfsqp;Tex];
ineq = all_forall `ineq
[
(&1 , e1, &1 + sol0/ pi);
(&1 , e2, &1 + sol0/ pi);
(&1 , e3, &1 + sol0/ pi);
((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
((&2/ h0) pow 2, b2, (&2 * h0) pow 2);
((#2.9/ h0) pow 2, c2,(#4.0) pow 2)
]
((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;
add
{
idv="1117202051";
doc="Used to maintain nonreflexivity when making num1-deformations.
The big angle on a skinny triangle (ear) is obtuse.
Case where 2 opposite edges equal 2.";
tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.0);
(#3.01,y4,#3.01);
(&2,y5,#2.52);
(&2,y6,&2)
]
(delta4_y y1 y2 y3 y4 y5 y6 < &0)`;
};;
add
{
idv="4559601669";
doc="Used to maintain nonreflexivity when making num1-deformations.
The big angle on a skinny triangle (ear) is obtuse.
Case where two adjacent edges equal 2 along y2 y3 y4";
tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,&2);
(&2,y3,&2);
(#3.01,y4,#3.915);
(&2,y5,#2.52);
(&2,y6,#2.52)
]
(delta4_y y1 y2 y3 y4 y5 y6 < &0)`;
};;
add
{
idv="4559601669b";
doc="Used to maintain nonreflexivity when making num1-deformations.
The big angle on a skinny triangle (ear) is obtuse.
Case where two adjacent edges equal 2 along face y1 y2 y6.
Added 5/2012.";
tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,&2);
(&2,y3,#2.52);
(#3.01,y4,#3.01);
(&2,y5,#2.52);
(&2,y6,&2)
]
(delta4_y y1 y2 y3 y4 y5 y6 < &0)`;
};;
add
{
idv="2485876245a";
doc="Used to justify matan approx in skinny triangles (ears).
This says that the skinny angle is acute.
y4 upper bound comes from the triangle inequality.
Revision a: May 20, 2012: changed lower bound on y5 from 3.01 to 3.0.
Note: this inequality is a consequence of 'JNTEFVP 1' and could be eliminated.";
tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(#3.0,y5, &2 * #2.52);
(&2,y6,#2.52)
]
(delta4_y y1 y2 y3 y4 y5 y6 > &0)`;
};;
add
{
idv="2485876245b";
doc="Used in some quad calculations to show that a node
is not straight (both halves are acute).
Added 2012-5-25.";
tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(#3.01,y5, &2 * #2.52);
(&2,y6,#3.01)
]
((delta4_y y1 y2 y3 y4 y5 y6 > &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0))`;
};;
(* PENT SECTION *)
addtex (Section,"Main Estimate","Local Fan/Main Estimate/Appendix/Terminal Pent");;
add
{
idv="7175074394";
doc="ear dih ineq when delta < 20.
Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
Adaptation of 9459075374.
(EAR) A bound on the delta of an ear in a pent,
The disjunct (dih_y y1 y2 y3 y4 y5 y6 < #0.3205 = (1.75-1.109)/2) has been 'linearized'.
Tan[0.3205]^2 = (>=) 0.110186
In more detail, this calc shows that delta > 20 or dih < 0.3205
By 4887115291, we know that the combined angle at the crowded node of a pent is
at least 1.75. If both ears have delta < 20, then combined angle
is at least 1.109 + 2 * 0.3205 = 1.75, so a cross diag <= 3.01.
Hence wlog one of the two ears has delta >= 20.
Added 2013-06-25. Replaces 3405144397 which has invalid domain constraints on y2,y5
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(&2,y6,&2)
]
(let tan2lower = #0.110186 in
(delta_y y1 y2 y3 y4 y5 y6 > &20) \/
(&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
)`;
};;
add
{
idv="4887115291";
doc="old name: angles pent*
Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.01);
(&2,y5,&2);
(&2,y6,&2)
]
( #1.75 < dih_y y1 y2 y3 y4 y5 y6
)`;
};;
add
{
idv="6789182745";
doc="old name: test A*
Local-fan/Main-estimate/Terminal-pent/both-ears-under-20.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = Sphere.all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
(dih_y y1 y2 y3 y4 y5 y6 < #1.109)
)`;
};;
add
{
idv="7796879304";
doc="old name: res1*
Local-fan/Main-estimate/terminal-pent/ear-tau-approximation
tau_residual. This restricts delta to [0,C]";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Cfsqp_branch 2];
ineq = all_forall `ineq [
(#2.0,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)
]
(
(delta_y y1 y2 y3 y4 y5 y6 < &0) \/
(delta_y y1 y2 y3 y4 y5 y6 > &80) \/
(y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.012 + #0.07 * (#2.52 - y1) + #0.01 * (#2.52 * &2 - y2 - y3 ))
)`;
};;
add
{
idv="2314572187";
doc="old name: res1*
Local-fan/Main-estimate/terminal-pent/ear-tau-approximation
tau_residual. This restricts delta above C";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(#2.0,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)
]
(
(taum y1 y2 y3 y4 y5 y6 > y_of_x taud_x y1 y2 y3 y4 y5 y6) \/
(delta_y y1 y2 y3 y4 y5 y6 < &80)
)`;
};;
add
{
idv="1347067436";
doc="old name: local max v4*, WNLKGOQ, 1671775772 (with #0.12->#0.1) 8146670324
better local max test.
This is the numerator of the 2nd derivative of the function taud.
Case delta > 20.";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.237);
(&2,y5,&2);
(&2,y6,&2)
]
(y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 > &0 \/
y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x taud_x y1 y2 y3 y4 y5 y6 > #0.12 \/
delta_y y1 y2 y3 y4 y5 y6 < &20)`;
};;
add
{
idv="3078028960";
doc="When delta <= 20, delta is monotonic decreasing in y1.
Hence smallest y1 on the comain delta <= 20 occurs when delta =20.
This gives a lower bound flat_term (y1 @ del20) <= taud on the domain delta <= 20.";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Tex;Xconvert;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)
]
(
y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0 \/
delta_y y1 y2 y3 y4 y5 y6 > &20
)`;
};;
add
{
idv="6601228004";
doc="old name: local max v4*
better local max test.
This is the numerator of the 2nd derivative of the function taud.";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.237);
(&2,y5,&2);
(&2,y6,&2)
]
(
y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
delta_y y1 y2 y3 y4 y5 y6 > &20 \/
delta_y y1 y2 y3 y4 y5 y6 < &0
)`;
};;
add
{
idv="3665919985";
doc=" 'A' piece lower bound for terminal pent.";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(taum y1 y2 y3 y4 y5 y6 > #0.541
)`;
};;
add
{
idv="7903347843";
doc="
local fan/main estimate/terminal pent
LHS(135,taum>=0.12) RHS(126,y1=2,delta>20)
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
(taum y1 y2 y3 y4 y5 y6 +
y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
#0.12
> #0.616)
)
`;
};;
add
{
idv="5546286427";
doc="
local fan/main estimate/terminal pent
LHS(135,taum>=0.12) RHS(126,delta=0 (reduced from 20))
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
let d = &0 in
((taum y1 y2 y3 y4 y5 y6 +
y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 +
#0.12
> #0.616) \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
`;
};;
add
{
idv="7997589055";
doc="
local fan/main estimate/terminal pent
LHS(135,y1=2) RHS(126,y1=2)
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
(taum y1 y2 y3 y4 y5 y6 +
y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
> #0.616)
)
`;
};;
add
{
idv="2320951108";
doc="
local fan/main estimate/terminal pent
LHS(135,y1=2) RHS(126,y1=2.52), extra implicit assumption delta > 20.
mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
(taum y1 y2 y3 y4 y5 y6 +
y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
+ #0.053
> #0.616)
)
`;
};;
add
{
idv="5429238960";
doc="
local fan/main estimate/terminal pent
LHS(135,y1=2) RHS(126,y1=2.52), extra assumption deltaRHS < 20.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
(taum y1 y2 y3 y4 y5 y6 +
y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
> #0.616))
`;
};;
add
{
idv="2565248885";
doc="
local fan/main estimate/terminal pent
LHS(135,y1=2) RHS(126,delta <= 20 (reduce to delta=0 or previous case))
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
let d = &0 in
((taum y1 y2 y3 y4 y5 y6 +
y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 +
y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
> #0.616) \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
`;
};;
add
{
idv="5708641738";
doc="
local fan/main estimate/terminal pent
LHS(135,y1=2.52) RHS(126,y1=2.52)
wlog. LHS delta on ears is >= 20,
mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053.
If RHS delta >= 20. get 0.541 + 2 (0.053) > 0.616.
so wlog. RHS delta on ear is <= 20.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(
let d = &20 in
((taum y1 y2 y3 y4 y5 y6 +
#0.053
> #0.616) \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
`;
};;
add
{
idv="1948775510";
doc="was test Q.
local fan/main estimate/terminal pent
LHS(135,y1=2.52,delta=>20) RHS(126,delta=0)
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(taum y1 y2 y3 y4 y5 y6 +
y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
y_of_x (mud_135_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6
> #0.616 \/
y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 // \/
// y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0
)`;
};;
add
{
idv="1586903463";
doc="
local fan/main estimate/terminal pent
LHS(135,delta=20) RHS(126,y1=2.52,delta<=20)
sqrt(20) .> 4.47.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(taum y1 y2 y3 y4 y5 y6 +
y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
(#0.012 + #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
&0
> #0.616 \/
// removed 2013-05-26 y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20
)`;
};;
add
{
idv="8875146520";
doc="
local fan/main estimate/terminal pent
LHS(135,delta=20) RHS(126,y1=2.52,delta>20)
sqrt(20) .> 4.47.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(taum y1 y2 y3 y4 y5 y6 +
y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
(#0.012 + #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
y_of_x (mud_126_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6
> #0.616 \/
// removed 2013-05-26: y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20
)`;
};;
add
{
idv="1008824382";
doc="
local fan/main estimate/terminal pent
LHS(135,delta=20) RHS(126,delta=0)
sqrt(20) .> 4.47.
0.705 comes by combining mu_y and flat_term2_x terms.
";
tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.237);
(#3.01,y6,#3.237)
]
(taum y1 y2 y3 y4 y5 y6 +
#0.705 * y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
(#0.012 + #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 +
y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
> #0.616 \/
y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &20 \/
y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0
)`;
};;
addtex (Section,"Main Estimate","Local Fan/Main Estimate/Appendix/Terminal Hex");;
(* START OF HEX SECTION *)
add
{
idv="6459846571";
doc="upper bound on minor diagonal is 3.915 when top edges are 2.
The bound on y4 comes from the triangle inequality.
This could be proved directly with monotonicity and delta, without interval arith.";
tags=[Flypaper["UPONLFY"];Main_estimate;Cfsqp;Xconvert;Tex];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#4.52);
(&2,y5,&2);
(&2,y6,&2)
]
((y4 < #3.915) \/
delta_y y1 y2 y3 y4 y5 y6 < &0
)`;
};;
add
{
idv="7439076204";
doc="local fan/main estimate/terminal hex.
This is used to remove the eulerA_x hypothesis.";
tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(#3.01,y5,#3.915);
(#3.01,y6,#3.915)
]
( y_of_x delta_x4 y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x eulerA_x y1 y2 y3 y4 y5 y6 > &0)
`;
};;
skip
{
idv="test-hex-numerical";
doc="For cfsqp only.
This is the numerator of the 2nd derivative of the function taud.";
tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)
]
(((y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6) pow 2 > &0) \/
(y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
taum y1 y2 y3 y4 y5 y6 > #0.0 \/ // can adjust this later.
delta_y y1 y2 y3 y4 y5 y6 < &15))`;
};;
add
{
idv="6877738680";
doc="local fan/main estimate/appendix/terminal hex
2nd derivative test for taud.
old version 4910585280. This uses taud.";
tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)
]
(y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 > &0 \/
y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 < &0 \/
(y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x taud_x y1 y2 y3 y4 y5 y6 > &0 \/
delta_y y1 y2 y3 y4 y5 y6 < &15))`;
};;
add
{
idv="9692636487";
doc="local fan/main estimate/appendix/terminal hex.
2nd derivative test for taud.";
tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)
]
(
(y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
delta_y y1 y2 y3 y4 y5 y6 < &0) \/
delta_y y1 y2 y3 y4 y5 y6 > &15
)`;
};;
let template_hex = `\ d234 d126 d135 c234 c126 c135 s45 s56 . ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(#3.01,y5,#3.915);
(#3.01,y6,#3.915)
]
(taum y1 y2 y3 y4 y5 y6 +
d234 +
d126 +
d135
> #0.712 \/
y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 \/
c234 \/
c126 \/
c135 \/
s45 \/
s56
)`;;
let mk_ineq_hex i234 i126 i135 =
let nth = List.nth in
let d234 = nth [` y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
`&0`;
`y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
`y_of_x (mudLs_234_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
`&0 - sol0`] i234 in
let d126 = nth [` y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
`&0`;
`y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
`y_of_x (mudLs_126_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
`&0 - sol0`] i126 in
let d135 = nth [` y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
`&0`;
`y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
`y_of_x (mudLs_135_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0`;
`&0 - sol0`] i135 in
let c234 = nth [`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
`F`;
`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i234 in
let c126 = nth [`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
`F`;
`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i126 in
let c135 = nth [`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
`F`;
`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i135 in
let s45 = if (i234= i126) then `y6 < y4` else `F` in
let s56 = if (i126= i135) then `y5 < y6` else `F` in
rhs(concl(REWRITE_CONV[] (Ineq.mk_tplate template_hex [d234;d126;d135;c234;c126;c135;s45;s56])));;
(* s45 correction svn 3246, 2013-05-28 *)
let make_hex_ear i234 i126 i135 =
{
idv = Printf.sprintf "7550003505 %d %d %d" i234 i126 i135;
ineq = mk_ineq_hex i234 i126 i135;
doc = "local fan/main estimate/terminal hex/body
cases: (0) delta=0; (1) taud>0; (2) y=2, 0<=delta<=16; (3) y=2, 16<=delta<=100; (4) y=2, 100<delta.";
tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Penalty(50.0,500.0)];
};;
for i1=0 to 4 do
for i2=i1 to 4 do
for i3=i2 to 4 do
add (make_hex_ear i1 i2 i3) done done done;;
(* HEXAGONS, SKINNY TRIANGLES *)
(* Now for the outer skinny triangle (ear) estimates used in hexagon triangulation *)
add{
idv = "6762190381";
doc="This reduces OWZLKVY to the case when delta_y < 200. Added 2013-4-18";
tags = [Cfsqp;Tablelp;Main_estimate;Xconvert;Tex];
ineq = all_forall `ineq
[
(&2 ,y1,&2 * h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)]
(
delta_y y1 y2 y3 y4 y5 y6 < &200 \/ taum y1 y2 y3 y4 y5 y6 > &0 )`;
};;
add{
idv = "8346775862";
doc="In OWZLKVY the angle at y1 is obtuse. Added 2013-4-18.";
tags = [Cfsqp;Tablelp;Xconvert;Main_estimate;Tex;Cfsqp_branch 1];
ineq = all_forall `ineq
[
(&2 ,y1,&2 * h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)]
(
delta_y y1 y2 y3 y4 y5 y6 > &200 \/ y_of_x delta_x4 y1 y2 y3 y4 y5 y6 < &0 ) `;
};;
add{
idv = "8631418063";
doc="In OWZLKVY the angle at y2,y3 is acute. Added 2013-4-18.";
tags = [Cfsqp;Tablelp;Xconvert;Main_estimate;Tex];
ineq = all_forall `ineq
[
(&2,y1,&2 * h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(&2,y4,&2);
(#3.01,y5,#3.915);
(&2,y6,&2)]
(y_of_x delta_x4 y1 y2 y3 y4 y5 y6 > &0)`;
};;
add{
idv = "4821120729";
doc="Used in the proof of OWZLKVY to show that sol>=0. Added 2013-04-17.";
tags = [Cfsqp;Tablelp;Xconvert;Main_estimate;Tex];
ineq = all_forall `ineq
[
(&2,y1,&2 * h0);
(#2.0,y2,&2 * h0);
(#2.0,y3,&2 * h0);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)]
(y_of_x eulerA_x y1 y2 y3 y4 y5 y6 > &0)`;
};;
add
{
idv="5202826650 a";
doc="
This is part of the proof of Lemma OWZLKVY in flypaper.pdf.
In the book this is called 'some analytic function f' and
doesn't give the idv of the calculation.
It shows that a
skinny triangle (ear) residual is positive, when y1=2.52,
We have tau = tau_residual * sqrt(delta), by definition.
This domain falls within the preconditions of the residual function because of
4559601669 and 2485876245
Domain generalized June 3 (2011?): y3 upperbound -> 2.52.
";
tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
ineq = all_forall `ineq [
(#2.52,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.915);
(&2,y5,&2);
(&2,y6,&2)
]
(
(y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > &0) \/
(delta_y y1 y2 y3 y4 y5 y6 < &0)
)`;
};;
addtex(Section,"Main Estimate","quadrilaterals");;
(* Here are some estimates for quad cases that were added late:
2013-08-07.
*)
add
{
idv="6184614449"; (* was "test gamma1"; *)
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2 * h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(#3.3,y4,&4 * h0);
(&2,y5,&2 * h0);
(&2,y6,&2 * h0)]
((delta4_y y1 y2 y3 y4 y5 y6 < &0) ) `;
};;
add
{
idv= "2073661826"; (* "test gamma"; *)
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.55,y4,&4 * h0);
(&2,y5,#2.52);
(#2.52,y6,#3.01)]
((delta4_y y1 y2 y3 y4 y5 y6 < &0) ) `;
};;
add
{
idv="1348932091"; (* was "testB"; *)
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.52,y4,#2.52);
(#3.01,y5,#3.3);
(&2,y6,#2.52)]
((dih_y y1 y2 y3 y4 y5 y6 < #1.4) ) `;
};;
add
{
idv="1348932091 delta";
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.52,y4,#2.52);
(#3.01,y5,#3.3);
(&2,y6,#2.52)]
((delta_y y1 y2 y3 y4 y5 y6 > &0) ) `;
};;
add
{
idv= "5557288534"; (* was "testC"; *)
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.01);
(#3.01,y5,#3.3);
(&2,y6,#2.52)]
((dih_y y1 y2 y3 y4 y5 y6 < #1.7) ) `;
};;
add
{
idv= "5557288534 delta";
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.01);
(#3.01,y5,#3.3);
(&2,y6,#2.52)]
((delta_y y1 y2 y3 y4 y5 y6 > &0) ) `;
};;
add
{
idv="9368433105";
doc = "Justify dih linearization in 8405387449";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.55);
(&2 * h0,y6,#3.01)]
((delta4_y y1 y2 y3 y4 y5 y6 > &0) ) `;
};;
add
{
idv="8405387449";
doc="
(EAR) A bound on the dih of an ear in a quad,
The disjunct (dih_y y1 y2 y3 y4 y5 y6 < #1.1 has been 'linearized'.
Tan[1.1]^2 = (>=) 3.86
In more detail, this calc shows that delta < 0 or dih < 1.1
";
tags=[Main_estimate;Cfsqp;Tex;Xconvert;];
ineq = Sphere.all_forall `ineq [
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,&2);
(#3.01,y5,#3.55);
(&2 * h0,y6,#3.01)]
(let tan2lower = #3.86 in
((&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
delta_y y1 y2 y3 y4 y5 y6 < &0))`;
};;
add
{
idv="5550839403"; (* was "test E"; *)
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.01);
(#3.01,y5,#3.55);
(&2,y6,&2 * h0)]
((dih_y y1 y2 y3 y4 y5 y6 < #2.0) ) `;
};;
add
{
idv="5550839403 delta";
doc = "";
tags=[Main_estimate;Cfsqp;Tex;Xconvert];
ineq = Sphere.all_forall `ineq
[
(&2,y1,&2);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.01);
(#3.01,y5,#3.55);
(&2,y6,&2 * h0)]
((delta_y y1 y2 y3 y4 y5 y6 > &0) ) `;
};;
addtex (Section,"Main Estimate","Ad hoc quadrilaterals");;
addtex(Comment,"",
"
Let's start with the ad hoc inequality: 9563139965D. (>= 0.467 )
By top edge contraction arguments, we may assume that
(0) all top edges have length 2, or
(1) both diagonals have length 3 (by contracting in different ways).
The first case (0) is impossible by geomeric considerations:
edges=2 ==> some diagonal <= sqrt8.
So both diagonals have length 3.
This has been completely solved in a series 9563139965D in ineq.hl.
");;
addtex(Comment,"",
"Next the ad hoc LP inequality in head.mod :
tauB4h 9620775909. tau >= 0.477, quad, diags >= sqrt8, one edge [2.52,sqrt8].
This comes from a pentagon that has a 'flat quarter'.
Case 1: a diagonal < 3.01. Here we make no deformations. We cut
the quad into two triangles.
Case 2: both diags > 3.01. In this case we bound the shorter diagonal.
Solve[Delta[x, 2, 2, x, 2, sqrt8] == 0, x] // N gives x <= 3.108
*)
");;
addtex(Comment,"",
"
Now third ad hoc LP inequality: Quad 0.696.
tau5h 9620775909-5 std5 INTER std56flatfree, tau >= 0.696, pent, diags >= sqrt8,
It drops to a quad case if some diag of pent has length <= 3.01 and a slice is made.
Contract top edges of quad until 3 have length 2.
Extremize the other long edge to 3.01 or sqrt8.
Short diag: Solve[Delta[x,2,2,x,2,3.01]==0,x]//N, gives x <= 3.166
");;
add
{
idv="4680581274 a";
doc="quad case both diags > 3.01, y9 long.
4559601669 gives the gratuitous delta4_y disjunct.
May 23, changed delta4 constant from -11.2 to 0.
2013-05-05, 0.696 -> 0.616.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 10000.0 (* was 0.001 *);
Xconvert;Tex;Penalty(50.0,5000.0)];
ineq = all_forall `ineq [
(#2.0,y1,&2 * h0);
(#2.0,y2,&2 * h0);
(#2.0,y3,&2 * h0);
(#3.01,y4,#3.166);
(#2.0,y5,&2);
(#2.0,y6,&2);
(#2.0,y7,&2 * h0);
(#2.0,y8,&2);
(#3.01,y9,#3.01)]
(
( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 > #0.513) \/
(delta_y y1 y2 y3 y4 y5 y6 < &10) \/
delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;
add
{
idv="4680581274 delta issue";
doc="quad case both diags > 3.01, y9 long.
This justifies the assumption the disjunct delta < 10 in the inequality.
4559601669 gives the gratuitous delta4_y disjunct.
May 23, changed delta4 constant from -11.2 to 0.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 10000.0 (* was 0.001 *);
Xconvert;Tex;Penalty(50.0,5000.0)];
ineq = all_forall `ineq [
(#2.0,y1,&2 * h0);
(#2.0,y2,&2 * h0);
(#2.0,y3,&2 * h0);
(#3.01,y4,#3.166);
(#2.0,y5,&2);
(#2.0,y6,&2);
(#2.0,y7,&2 * h0);
(#2.0,y8,&2);
(#3.01,y9,#3.01)]
(
(delta_y y1 y2 y3 y4 y5 y6 > &10) \/
delta4_y y1 y2 y3 y4 y5 y6 > &0 \/
( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;
add
{
idv="4680581274 delta top issue";
doc="quad case top neg delta.
Solve[Delta[x,2,2,x,2,3.01]==0,x] (*x < 3.166 *)
Added 2013-05-05.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert];
ineq = all_forall `ineq [
(#3.166,y1,&4);
(#3.01,y2,#3.01);
(&2,y3,&2);
(#3.166,y4,&4);
(&2,y5,&2);
(&2,y6,&2)]
(delta_y y1 y2 y3 y4 y5 y6 < &0)`;
};;
addtex (Section,"Main Estimate","Quadrilaterals (non ad hoc)");;
add
{
idv="2171548893";
doc=" Main estimate/quad case.
This justifies the upper bound of 3.62 on shortest diagonal when top edges are 2,cstab,2,cstab.
";
tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,&2);
(#3.01,y2,#3.01);
(#3.62,y3,&6);
(&2,y4,&2);
(#3.01,y5,#3.01);
(#3.62,y6,&6)
]
( delta_y y1 y2 y3 y4 y5 y6 < &0)`;
};;
add
{
idv="2468307358";
doc="Main estimate/quad/upper echelon.
tameTableD[2,2]
Triangulate quad with diagonal y4.
Use if some diag, 3.01 <= diag <= 3.62.
2013-06-13. Adapted from 9269152105. d and Lower bound on y4 changed ";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#3.01,y4,#3.62);
(#3.01,y5,#3.01);
(&2,y6,&2)
]
(
( taum y1 y2 y3 y4 y5 y6 > #0.2565 )
)`;
};;
(* now for the cases where the shorter diagonal does not separate long edges *)
add {
idv="9507202313";
doc="tameTableD[2,2].
Triangulate quad with diagonal y4.
Case both diags > 3.01, y6, y9 long (2.52 and 3.01),
short diagonal doesn't separate long edges.
Triangulate by long diagonal (at least 3.41 for otherwise it drops into case
where short diagonal separates long edges).
Solve[Delta[x, 2, 2, 3.01, 2.52, 3.01] == 0, x] (* x < 3.634 *)
";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Quad_cluster 10000.0 (* was 0.001 *);
Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(#2.0,y1,&2 * h0);
(#2.0,y2,&2 * h0);
(#2.0,y3,&2 * h0);
(#3.41,y4,#3.634);
(#2.0,y5,&2);
(#2.52,y6,#2.52);
(#2.0,y7,&2 * h0);
(#2.0,y8,&2);
(#3.01,y9,#3.01)]
(
delta_y y1 y2 y3 y4 y5 y6 > &30 \/
( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;
addtex (Section,"Main Estimate","Triangles");;
(* FIRST DEAL WITH AD HOC TRIANGLES *)
addtex(Comment,"",
"
If the sliced edge is between [sqrt8,3.01], the triangle (2,1) has tau < tame_table_d 2 1.
Nevertheless tau > 0.11
We must compensate by putting an extra penalty term (tame_table_d 2 1 - 0.11)
in the other pieces.
Ad hoc LP. The case.
tauB4h 9620775909 apex4 tau >= 0.477, quad, diags >= sqrt8, one edge [2.52,sqrt8]
This can break into a triangle (2,1) [2.52,sqrt8][sqrt8,3.01] and a triangle (1,2).
In this case we run one extra triangle calc,
replace tame_table_d entries with 0.477 - 0.11.
tau5h 9620775909-5 std5 INTER std56flatfree, tau >= 0.696, pent, diags >= sqrt8,
This will give an A-piece with [sqrt8,3.01][sqrt8,3.01]. need 0.696 - 2 0.11.
9563139965D, dart4_diag3_b, tau >= 0.467, quad, diags >= 3.
No triangle occurs here. No diagonal drawn.
");;
add
{
idv="3603097872";
doc="skinny clipped triangle (ear) inequality
In the application to tameTableD[4,1], we have y4=3.01, y6=2,
It is slightly generalized for later use.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(#2.0,y2,#2.52);
(&2,y3,#2.52);
(sqrt8,y4,#3.01);
(&2,y5,#2.52);
(&2,y6,#2.52)
]
(
( taum y1 y2 y3 y4 y5 y6 - #0.1 * (#3.01 - y4) > #0.11) \/
(delta_y y1 y2 y3 y4 y5 y6 < &0)
)`;
};;
add
{
idv="5405130650";
doc=" 0.477 estimate, clipped A-piece triangle.
Case 1.
We reuse the other cut triangle (bound 0.11) from above.
We have not done it here, but we could extremize edge y5, y6.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(#2.0,y2,#2.52);
(&2,y3,#2.52);
(sqrt8,y4,#3.01);
(#2.52,y5,sqrt8);
(&2,y6,#2.52)
]
(
( taum y1 y2 y3 y4 y5 y6 + #0.1 * (#3.01 - y4) > #0.477 - #0.11) \/
(delta_y y1 y2 y3 y4 y5 y6 < &0)
)`;
};;
add
{
idv="5026777310a";
doc="pentagon case, clipped A-piece triangle. Added 2013-4-20";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(#2.0,y2,#2.52);
(&2,y3,#2.52);
(sqrt8,y4,#3.01);
(sqrt8,y5,#3.01);
(&2,y6,#2.52)
]
(
( taum y1 y2 y3 y4 y5 y6 > tame_table_d 4 1 - &2 * #0.11) \/
(delta_y y1 y2 y3 y4 y5 y6 < &0)
)`;
};;
add
{
idv="7881254908";
doc="triangle 1,2, ad hoc 0.696 case LP";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(#2.0,y2,#2.52);
(&2,y3,#2.52);
(#2.52,y4,#2.52);
(sqrt8,y5,#3.01);
(sqrt8,y6,#3.01)
]
(
taum y1 y2 y3 y4 y5 y6 > #0.696 - &2 * #0.11
)`;
};;
addtex(Section,"Main Estimate","Triangle (non ad hoc)");;
add
{
idv="4010906068";
doc="main estimate/triangle 3 long edges. Added 2013-06-04.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = Sphere.all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(#2.52,y4,#3.01);
(#2.52,y5,#3.01);
(#2.52,y6,#3.01)
]
(
taum y1 y2 y3 y4 y5 y6 > #0.476
)`;
};;
add
{
idv="6833979866";
doc="main estimate A piece. Added 2013-06-04";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = Sphere.all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(#2.52,y5,#3.01);
(#2.52,y6,#3.01)
]
(
taum y1 y2 y3 y4 y5 y6 > #0.2759
)`;
};;
add
{
idv="5541487347";
doc="main estimate triangle short ear. Added 2013-06-04.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = Sphere.all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(&2,y5,#2.52);
(#2.52,y6,sqrt8)
]
(
taum y1 y2 y3 y4 y5 y6 > #0.103
)`;
};;
add{
idv = "OMKYNLT 3336871894";
tags = [Tex;Cfsqp;Eps 1.0e-8;Flypaper["OMKYNLT"];Main_estimate;Xconvert;Sharp];
doc = "This is the nonnegativity of $\\tau$ on triangles. It is a sharp inequality.";
ineq = all_forall `ineq
[
(#2.0,y1,#2.52);
(#2.0,y2,#2.52);
(#2.0,y3,#2.52);
(&2,y4,&2);
(&2,y5,&2);
(&2,y6,&2)
]
( taum y1 y2 y3 y4 y5 y6 >= #0.0)`;
};;
add
{
idv="8495326405";
doc=" Main estimate/quad case.
";
tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,&2);
(&2,y2,&2);
(#3.01,y3,&6);
(&2,y4,&2);
(&2 * h0,y5,&2 * h0);
(#3.01,y6,&6)
]
( delta_y y1 y2 y3 y4 y5 y6 < &0)`;
};;
add
{
idv="9096461391";
doc=" 0.513 estimate, A-piece triangle.
One diagonal exactly 3.01. Added 2013-06-13. replaces 8748498390";
tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(#2.52,y5,#3.01);
(#3.01,y6,#3.01)
]
( taum y1 y2 y3 y4 y5 y6 + #0.12 * (y1 - &2) > #0.403 )`;
};;
add
{
idv="2445657182";
doc=" 0.513 estimate. ear. Combine with 8748498390 along diagonal 3.01.
Added 2013-06-13.";
tags=[Flypaper["FHOLLLW"];Cfsqp;Main_estimate;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(&2,y5,#2.52);
(#3.01,y6,#3.01)
]
( taum y1 y2 y3 y4 y5 y6 > #0.11 + #0.12 * (y1 - &2) )`;
};;
add
{
idv="2125338128";
doc="Used to show that angle not straight in (3,3) diagonal main estimate.
Added 2013-06-13.";
tags=[Flypaper["FHOLLLW"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
ineq = all_forall `ineq [
(&2,y1,#2.52);
(&2,y2,#2.52);
(&2,y3,#2.52);
(&2,y4,#2.52);
(&2,y5,#2.52);
(&2,y6,#3.01)
]
( delta_y y1 y2 y3 y4 y5 y6 > &0 )`;
};;
end;;