Let 
![A (x) = \left[\begin{array}{ccc} 1 & x_1 & x_2\\ x_1 & 1 & x_3\\ x_2 & x_3 & 1\end{array}\right]](http://s0.wp.com/latex.php?latex=A+%28x%29+%3D+%5Cleft%5B%5Cbegin%7Barray%7D%7Bccc%7D+1+%26+x_1+%26+x_2%5C%5C+x_1+%26+1+%26+x_3%5C%5C+x_2+%26+x_3+%26+1%5Cend%7Barray%7D%5Cright%5D&bg=ffffff&fg=333333&s=0 "A (x) = \left[\begin{array}{ccc} 1 & x_1 & x_2\\ x_1 & 1 & x_3\\ x_2 & x_3 & 1\end{array}\right]")
The elliptope 
where 
The
[ source ]
__________
Saying that 
which we can discard. The three 2nd order principal minors (determinants of 
from sympy import *
# symbolic variables
x1 = Symbol('x1')
x2 = Symbol('x2')
x3 = Symbol('x3')
# build matrix A(x)
A = Matrix([[1,x1,x2],
[x1,1,x3],
[x2,x3,1]])
print "\nMatrix A(x):"
print A
print "\n2nd order principal minors:"
print A.extract([0,1],[0,1]).det()
print A.extract([0,2],[0,2]).det()
print A.extract([1,2],[1,2]).det()
print "\n3rd order principal minor:"
print A.det()
which produces the following output:
Matrix A(x): [ 1, x1, x2] [x1, 1, x3] [x2, x3, 1] 2nd order principal minors: -x1**2 + 1 -x2**2 + 1 -x3**2 + 1 3rd order principal minor: -x1**2 + 2*x1*x2*x3 - x2**2 - x3**2 + 1
Hence, the 2nd order principal minors yield the following inequalities
which define the 
![[-1,1]^3 \subset \mathbb{R}^3](http://s0.wp.com/latex.php?latex=%5B-1%2C1%5D%5E3+%5Csubset+%5Cmathbb%7BR%7D%5E3&bg=ffffff&fg=333333&s=0 "[-1,1]^3 \subset \mathbb{R}^3")
We can thus conclude that
__________
Deciding the convexity of
In my last post, I used quantifier elimination to decide the convexity of two semialgebraic sets in 
Based on the scripts in my previous post, we write the following REDUCE + REDLOG script to decide the convexity of
% decide the convexity of the elliptope E3
load_package redlog;
rlset ofsf;
% define predicates in antecedent
p1 := (1-x1^2>=0) and (1-x2^2>=0) and (1-x3^2>=0) and
(1-x1^2-x2^2-x3^2+2*x1*x2*x3>=0);
p2 := (1-y1^2>=0) and (1-y2^2>=0) and (1-y3^2>=0) and
(1-y1^2-y2^2-y3^2+2*y1*y2*y3>=0);
p3 := (theta>=0) and (theta<=1);
% define predicate in the consequent
z1 := theta*x1+(1-theta)*y1;
z2 := theta*x2+(1-theta)*y2;
q := (1-z1^2>=0) and (1-z2^2>=0) and (1-z3^2>=0) and
(1-z1^2-z2^2-z3^2+2*z1*z2*z3>=0);
% define universal formula
phi := all({x1,x2,x3,y1,y2,y3,theta}, (p1 and p2 and p3) impl q);
% perform quantifier elimination
rlqe phi;
end;
After 30 minutes (!!!) waiting for the decision procedure to terminate, I killed the reduce.exe process (which was eating all my machine’s CPU cycles and RAM memory). This is disappointing…
, defined by
and ![g_1, \dots, g_m \in \mathbb{R}[x]](http://s0.wp.com/latex.php?latex=g_1%2C+%5Cdots%2C+g_m+%5Cin+%5Cmathbb%7BR%7D%5Bx%5D&bg=ffffff&fg=333333&s=0 "g_1, \dots, g_m \in \mathbb{R}[x]")
, how can one decide if set 
is 
and any 
with 
, we have 
.
, defined by
.
is equivalent to asserting that 
. From the definition above, it follows that set ![\forall x \, \forall y \, \forall \theta \, \left[ \, p(x) \land p(y) \land (\theta \geq 0 \land \theta \leq 1) \implies p (\theta x + (1-\theta) y) \, \right]](http://s0.wp.com/latex.php?latex=%5Cforall+x+%5C%2C+%5Cforall+y+%5C%2C+%5Cforall+%5Ctheta+%5C%2C+%5Cleft%5B+%5C%2C+p%28x%29+%5Cland+p%28y%29+%5Cland+%28%5Ctheta+%5Cgeq+0+%5Cland+%5Ctheta+%5Cleq+1%29+%5Cimplies+p+%28%5Ctheta+x+%2B+%281-%5Ctheta%29+y%29+%5C%2C+%5Cright%5D&bg=ffffff&fg=333333&s=0 "\forall x \, \forall y \, \forall \theta \, \left[ \, p(x) \land p(y) \land (\theta \geq 0 \land \theta \leq 1) \implies p (\theta x + (1-\theta) y) \, \right]")
range over 
and 
, evaluates to 
. Since 
are polynomials, the formula above can be decided using quantifier elimination software like 
is convex. However, relying on the human visual system is extremely limiting. Therefore, we would like to automate the decision. We decide the convexity of 
is not convex. We decide the convexity of 
and, hence, 
. We say that 
is 
there exists a 
with 
. More formally, 
and 
range over sets 
and 
, respectively. Equivalently, 
is surjective.
and 
range over set 
and 
are equivalent to 
and 
, respectively. The 
.
is the state trajectory, and 
is a known 
is an 
at some time 
implies that the state will remain at 
for all 
. In other words, an equilibrium point 
.
. However, suppose that we are not interested in computing the equilibrium points; instead, all we would like to know is whether any such points exist. Thus, we arrive at the following 
, where 
.
are 
-dimensional vectors, 
and 
, we can rewrite the 
.
. Note also that we have a free parameter 
.
. We thus obtain 
and 
. For 
, we have two equilibrium points at 
and 
. For 
, we have one equilibrium point at 
. Finally, for 
, we have no equilibrium points, as the equation 
. Stating that this dynamical system has at least one equilibrium point is the same as saying that the following existentially-quantified formula
. Let us confirm this using the following 
