3
$\begingroup$

This question follows my last post.

I have a function $ \vec{f}: S^6 \times S^6 \rightarrow \mathbb{R}^{13} $ defined on two 6-dim hyperspheres. We will denote the function $ \vec{f}(\vec{x},\vec{y}) $, where $ \vec{x} $ and $ \vec{y} $ are points in the two spheres: so $ \vec{x} \cdot \vec{x} = 1 $ and $ \vec{y} \cdot \vec{y} = 1 $.

This function is saved in this file .wbx (download it) that you can import with the command

f= Uncompress @ Import["vector.wbx", "String"]

(If you have problems with the Import, you can copy the function here

The problem

This function appears in a infinite dimension system of strictly-positive inequalities

$$ \vec{f}(\vec{x},\vec{y}) \cdot \vec{\alpha}>0 $$ where $\vec{\alpha}$ is the vector of the unknowns. Each choice of $\vec{x},\vec{y}$ gives an inequality which must be consistent with all the possible inequalities you can get by varying the points $\vec{x},\vec{y}$.

If you import the function on your notebook, you see there are no consistent solutions for $\vec{X}=(X_1,X_2,0,0,0,0,0)$ and $\vec{Y}=(Y_1,Y_2,0,0,0,0,0)$, since these are zeros of the function $f(x,y)$. Indeed, if you find a zero, this contradicts the sign of the inequality (namely you get $0>0$).

Let us focus instead on points on the spheres which do not live on the space of zeros I have already found; that is, $ \vec{x}\neq \vec{X}$ and $\vec{y}\neq \vec{Y}$.

My aim is to show whether this system admits solutions or not for ANY choice of the points of the spheres $(\vec{x},\vec{y})\neq(\vec{X},\vec{Y})$

The strategy

  1. If there exist two points such that $\vec{f}(\vec{x}_i,\vec{y}_i)=-\vec{f}(\vec{x}_j,\vec{y}_j)$, then the system is impossible.
  2. However, it may not be possible two find such two points. Then, the system is impossible if, and only if, the convex-hull of the image of $\vec{f}(\vec{x},\vec{y})$ contains zero. This means that there is a set of points $\{x_n,y_n\}$ and positive coefficients $c_n>0$ such that

$$ \sum_n c_n\, \vec{f}(\vec{x}_n,\vec{y}_n) =0 $$

I want then to check if the convex-hull contains zero (notice the point 1 is a special case of the point 2).

I have tried following this post, which explains nicely how to compute the convex-hull in higher dimensions. However, their method takes a lot of time for a 15-dim vector.

So, this is my strategy I have thought to decrease the computational time: compute the convex-hull of all possible subvectors of $\vec{f}(\vec{x},\vec{y})$. If I find a convex-hull of these subvectors which does not include the zero, then the answer of my original question is negative.

Is there a better way to speed-up the computation?

Two possible scenarios

If the zero vector belongs to the convex-hull, then my problem is solved. If however this is not the case, then the system is consistent and may admit a solution. In this latter case, I want to get which are the values of $(\vec{x},\vec{y})$ such that the maximal numbers of zero appears in the entries of $\vec{f}(x,y)$. In this way, I can get simpler inequalities involving a less number (then 15) of unknowns. How can I do that with Mathematica?

My attempts

obj[x1_, x2_, x3_, x4_, x5_, x6_, x7_, y1_, y2_, y3_, y4_, y5_, y6_, y7_] := Uncompress@Import["vector.wdx", "String"];
SeedRandom[0];

listPoints = Table[Apply[obj, {Normalize@RandomReal[{-1, 1}, 7], Normalize@RandomReal[{-1, 1}, 7]} // Flatten], {i, 1, 1000}];
<< "https://gist.githubusercontent.com/jasondbiggs/c3d9410af3195da514a442be5b563ab8/raw/80ac5074077f0d4b1366540c8c710e35cb530ddd/NDConvexHull.m"
hull1 = CHNQuickHull[listPoints[[All, {1, 2, 3, 4, 5, 6, 7}]]];
hull2 = CHNQuickHull[Append[listPoints[[All, {1, 2, 3, 4, 5, 6, 7}]], {0, 0, 0, 0, 0, 0,0}]];

hull1 == hull2
(*False*)

As you see, the point {0, 0, 0, 0, 0, 0,0} does modify the convex-hull. This should mean that it does not belong to the convex-hull. Is this result robust? It may be that the zero belongs to a very narrow corner and the simulated points do not reach the corner. Any suggestion?

$\endgroup$
  • $\begingroup$ I get string errors when attempting that Import. $\endgroup$ – Daniel Lichtblau Nov 11 '18 at 16:42
  • $\begingroup$ @DanielLichtblau Which error? Michael E2 succeeded in importing the file (see the last question I am referring at the beginning of OP) $\endgroup$ – apt45 Nov 11 '18 at 16:45
  • $\begingroup$ Might be OS-dependent. You can make this process easier by putting the function right in the post. I managed to read it in by opening the file in Notepad, then cutting and pasting and using Uncompress. The result, when factored, has a leaf count around 7K, so not excessively large. $\endgroup$ – Daniel Lichtblau Nov 11 '18 at 16:52
  • $\begingroup$ Ok, so I try uploading the function on pastebin. Give me a second. $\endgroup$ – apt45 Nov 11 '18 at 16:54
  • $\begingroup$ @DanielLichtblau I have edited the question. Added the link pastebin.com/N6TetXtG $\endgroup$ – apt45 Nov 11 '18 at 16:56
2
$\begingroup$

Start with the definition (I use Together to make it somewhat shorter).

func = {1/225 (-15 x5^2 y1^2 - 15 x6^2 y1^2 - 15 x5^2 y2^2 - 15 x6^2 y2^2 - 
    5 Sqrt[15] x2 x5 y3^2 - 25 x5^2 y3^2 + 5 Sqrt[15] x1 x6 y3^2 - 
    25 x6^2 y3^2 + 30 x7^2 y3^2 - 10 Sqrt[15] x1 x5 y3 y4 - 
    10 Sqrt[15] x2 x6 y3 y4 + 5 Sqrt[15] x2 x5 y4^2 - 25 x5^2 y4^2 - 
    5 Sqrt[15] x1 x6 y4^2 - 25 x6^2 y4^2 + 30 x7^2 y4^2 - 
    10 Sqrt[15] x3 x4 y1 y5 + 90 x1 x5 y1 y5 + 30 x2 x6 y1 y5 - 
    45 x4 x7 y1 y5 - 5 Sqrt[15] x3^2 y2 y5 + 5 Sqrt[15] x4^2 y2 y5 - 
    90 x2 x5 y2 y5 + 30 x1 x6 y2 y5 - 45 x3 x7 y2 y5 - 15 x1^2 y5^2 - 
    15 x2^2 y5^2 - 25 x3^2 y5^2 - 25 x4^2 y5^2 - 56 x5^2 y5^2 + 
    4 x6^2 y5^2 - Sqrt[15] x3 x7 y5^2 + 6 x7^2 y5^2 + 
    5 Sqrt[15] x3^2 y1 y6 - 5 Sqrt[15] x4^2 y1 y6 + 30 x2 x5 y1 y6 - 
    90 x1 x6 y1 y6 - 45 x3 x7 y1 y6 - 10 Sqrt[15] x3 x4 y2 y6 + 
    30 x1 x5 y2 y6 + 90 x2 x6 y2 y6 + 45 x4 x7 y2 y6 + 
    120 x5 x6 y5 y6 - 2 Sqrt[15] x4 x7 y5 y6 - 15 x1^2 y6^2 - 
    15 x2^2 y6^2 - 25 x3^2 y6^2 - 25 x4^2 y6^2 + 4 x5^2 y6^2 - 
    56 x6^2 y6^2 + Sqrt[15] x3 x7 y6^2 + 6 x7^2 y6^2 - 
    45 x2 x5 y3 y7 - Sqrt[15] x5^2 y3 y7 - 45 x1 x6 y3 y7 + 
    Sqrt[15] x6^2 y3 y7 + 60 x3 x7 y3 y7 - 45 x1 x5 y4 y7 + 
    45 x2 x6 y4 y7 - 2 Sqrt[15] x5 x6 y4 y7 - 60 x4 x7 y4 y7 + 
    30 x3^2 y7^2 + 30 x4^2 y7^2 + 6 x5^2 y7^2 + 6 x6^2 y7^2), 
 1/450 (75 x3^2 y1^2 + 75 x4^2 y1^2 + 75 x3^2 y2^2 + 75 x4^2 y2^2 + 
    150 x1 x3 y1 y3 - 150 x2 x4 y1 y3 - 10 Sqrt[15] x4 x5 y1 y3 - 
    10 Sqrt[15] x3 x6 y1 y3 - 150 x2 x3 y2 y3 - 150 x1 x4 y2 y3 - 
    10 Sqrt[15] x3 x5 y2 y3 + 10 Sqrt[15] x4 x6 y2 y3 + 
    75 x1^2 y3^2 + 75 x2^2 y3^2 + 100 x3^2 y3^2 + 
    10 Sqrt[15] x2 x5 y3^2 - 75 x5^2 y3^2 - 10 Sqrt[15] x1 x6 y3^2 - 
    75 x6^2 y3^2 - 150 x2 x3 y1 y4 - 150 x1 x4 y1 y4 + 
    10 Sqrt[15] x3 x5 y1 y4 - 10 Sqrt[15] x4 x6 y1 y4 - 
    150 x1 x3 y2 y4 + 150 x2 x4 y2 y4 - 10 Sqrt[15] x4 x5 y2 y4 - 
    10 Sqrt[15] x3 x6 y2 y4 - 200 x3 x4 y3 y4 + 
    20 Sqrt[15] x1 x5 y3 y4 + 20 Sqrt[15] x2 x6 y3 y4 + 
    75 x1^2 y4^2 + 75 x2^2 y4^2 + 100 x4^2 y4^2 - 
    10 Sqrt[15] x2 x5 y4^2 - 75 x5^2 y4^2 + 10 Sqrt[15] x1 x6 y4^2 - 
    75 x6^2 y4^2 + 20 Sqrt[15] x3 x4 y1 y5 - 60 x4 x7 y1 y5 + 
    10 Sqrt[15] x3^2 y2 y5 - 10 Sqrt[15] x4^2 y2 y5 - 
    60 x3 x7 y2 y5 - 10 Sqrt[15] x2 x3 y3 y5 + 
    10 Sqrt[15] x1 x4 y3 y5 - 170 x3 x5 y3 y5 + 150 x4 x6 y3 y5 + 
    60 x2 x7 y3 y5 + 36 Sqrt[15] x5 x7 y3 y5 - 
    10 Sqrt[15] x1 x3 y4 y5 - 10 Sqrt[15] x2 x4 y4 y5 + 
    170 x4 x5 y4 y5 + 150 x3 x6 y4 y5 + 60 x1 x7 y4 y5 + 
    36 Sqrt[15] x6 x7 y4 y5 - 75 x3^2 y5^2 - 75 x4^2 y5^2 - 
    256 x5^2 y5^2 - 36 Sqrt[15] x3 x7 y5^2 - 84 x7^2 y5^2 - 
    10 Sqrt[15] x3^2 y1 y6 + 10 Sqrt[15] x4^2 y1 y6 - 
    60 x3 x7 y1 y6 + 20 Sqrt[15] x3 x4 y2 y6 + 60 x4 x7 y2 y6 - 
    10 Sqrt[15] x1 x3 y3 y6 - 10 Sqrt[15] x2 x4 y3 y6 + 
    150 x4 x5 y3 y6 + 170 x3 x6 y3 y6 - 60 x1 x7 y3 y6 + 
    36 Sqrt[15] x6 x7 y3 y6 + 10 Sqrt[15] x2 x3 y4 y6 - 
    10 Sqrt[15] x1 x4 y4 y6 + 150 x3 x5 y4 y6 - 170 x4 x6 y4 y6 + 
    60 x2 x7 y4 y6 - 36 Sqrt[15] x5 x7 y4 y6 + 512 x5 x6 y5 y6 - 
    72 Sqrt[15] x4 x7 y5 y6 - 75 x3^2 y6^2 - 75 x4^2 y6^2 - 
    256 x6^2 y6^2 + 36 Sqrt[15] x3 x7 y6^2 - 84 x7^2 y6^2 + 
    60 x4 x5 y1 y7 - 60 x3 x6 y1 y7 + 60 x3 x5 y2 y7 + 
    60 x4 x6 y2 y7 - 60 x2 x5 y3 y7 - 36 Sqrt[15] x5^2 y3 y7 - 
    60 x1 x6 y3 y7 + 36 Sqrt[15] x6^2 y3 y7 - 120 x3 x7 y3 y7 - 
    60 x1 x5 y4 y7 + 60 x2 x6 y4 y7 - 72 Sqrt[15] x5 x6 y4 y7 + 
    120 x4 x7 y4 y7 + 36 Sqrt[15] x3 x5 y5 y7 - 
    36 Sqrt[15] x4 x6 y5 y7 - 24 x5 x7 y5 y7 + 
    36 Sqrt[15] x4 x5 y6 y7 + 36 Sqrt[15] x3 x6 y6 y7 + 
    24 x6 x7 y6 y7 - 84 x5^2 y7^2 - 84 x6^2 y7^2 - 108 x7^2 y7^2), 
 8/25 (25 x1 x3 y1 y3 - 25 x2 x3 y2 y3 - 25 x1 x4 y1 y4 + 
    25 x2 x4 y2 y4 - 5 x3 x5 y3 y5 + 5 x4 x5 y4 y5 + 5 x3 x6 y3 y6 - 
    5 x4 x6 y4 y6 + 15 x1 x7 y1 y7 - 15 x2 x7 y2 y7 - 3 x5 x7 y5 y7 + 
    3 x6 x7 y6 y7), 
 1/450 (45 x7^2 y1^2 + 45 x7^2 y2^2 - 10 Sqrt[15] x4 x5 y1 y3 - 
    10 Sqrt[15] x3 x6 y1 y3 + 90 x6 x7 y1 y3 - 
    10 Sqrt[15] x3 x5 y2 y3 + 10 Sqrt[15] x4 x6 y2 y3 - 
    90 x5 x7 y2 y3 + 50 x3^2 y3^2 - 50 x4^2 y3^2 + 
    10 Sqrt[15] x2 x5 y3^2 - 30 x5^2 y3^2 - 10 Sqrt[15] x1 x6 y3^2 - 
    30 x6^2 y3^2 + 90 x7^2 y3^2 + 10 Sqrt[15] x3 x5 y1 y4 - 
    10 Sqrt[15] x4 x6 y1 y4 + 90 x5 x7 y1 y4 - 
    10 Sqrt[15] x4 x5 y2 y4 - 10 Sqrt[15] x3 x6 y2 y4 + 
    90 x6 x7 y2 y4 - 200 x3 x4 y3 y4 + 20 Sqrt[15] x1 x5 y3 y4 + 
    20 Sqrt[15] x2 x6 y3 y4 - 50 x3^2 y4^2 + 50 x4^2 y4^2 - 
    10 Sqrt[15] x2 x5 y4^2 - 30 x5^2 y4^2 + 10 Sqrt[15] x1 x6 y4^2 - 
    30 x6^2 y4^2 + 90 x7^2 y4^2 + 20 Sqrt[15] x3 x4 y1 y5 - 
    32 Sqrt[15] x5 x6 y1 y5 + 60 x4 x7 y1 y5 + 
    10 Sqrt[15] x3^2 y2 y5 - 10 Sqrt[15] x4^2 y2 y5 + 
    16 Sqrt[15] x5^2 y2 y5 - 16 Sqrt[15] x6^2 y2 y5 + 
    60 x3 x7 y2 y5 - 10 Sqrt[15] x2 x3 y3 y5 + 
    10 Sqrt[15] x1 x4 y3 y5 - 180 x3 x5 y3 y5 - 90 x2 x7 y3 y5 - 
    44 Sqrt[15] x5 x7 y3 y5 - 10 Sqrt[15] x1 x3 y4 y5 - 
    10 Sqrt[15] x2 x4 y4 y5 + 180 x4 x5 y4 y5 - 90 x1 x7 y4 y5 - 
    44 Sqrt[15] x6 x7 y4 y5 - 30 x3^2 y5^2 - 30 x4^2 y5^2 + 
    16 Sqrt[15] x2 x5 y5^2 - 32 x5^2 y5^2 + 16 Sqrt[15] x1 x6 y5^2 + 
    32 x6^2 y5^2 + 20 Sqrt[15] x3 x7 y5^2 + 81 x7^2 y5^2 - 
    10 Sqrt[15] x3^2 y1 y6 + 10 Sqrt[15] x4^2 y1 y6 + 
    16 Sqrt[15] x5^2 y1 y6 - 16 Sqrt[15] x6^2 y1 y6 + 
    60 x3 x7 y1 y6 + 20 Sqrt[15] x3 x4 y2 y6 + 
    32 Sqrt[15] x5 x6 y2 y6 - 60 x4 x7 y2 y6 - 
    10 Sqrt[15] x1 x3 y3 y6 - 10 Sqrt[15] x2 x4 y3 y6 + 
    180 x3 x6 y3 y6 + 90 x1 x7 y3 y6 - 44 Sqrt[15] x6 x7 y3 y6 + 
    10 Sqrt[15] x2 x3 y4 y6 - 10 Sqrt[15] x1 x4 y4 y6 - 
    180 x4 x6 y4 y6 - 90 x2 x7 y4 y6 + 44 Sqrt[15] x5 x7 y4 y6 - 
    32 Sqrt[15] x1 x5 y5 y6 + 32 Sqrt[15] x2 x6 y5 y6 + 
    128 x5 x6 y5 y6 + 40 Sqrt[15] x4 x7 y5 y6 - 30 x3^2 y6^2 - 
    30 x4^2 y6^2 - 16 Sqrt[15] x2 x5 y6^2 + 32 x5^2 y6^2 - 
    16 Sqrt[15] x1 x6 y6^2 - 32 x6^2 y6^2 - 20 Sqrt[15] x3 x7 y6^2 + 
    81 x7^2 y6^2 - 90 x4 x5 y1 y7 + 90 x3 x6 y1 y7 + 90 x1 x7 y1 y7 - 
    90 x3 x5 y2 y7 - 90 x4 x6 y2 y7 - 90 x2 x7 y2 y7 + 
    60 x2 x5 y3 y7 + 20 Sqrt[15] x5^2 y3 y7 + 60 x1 x6 y3 y7 - 
    20 Sqrt[15] x6^2 y3 y7 + 360 x3 x7 y3 y7 + 60 x1 x5 y4 y7 - 
    60 x2 x6 y4 y7 + 40 Sqrt[15] x5 x6 y4 y7 - 360 x4 x7 y4 y7 - 
    90 x2 x3 y5 y7 + 90 x1 x4 y5 y7 - 44 Sqrt[15] x3 x5 y5 y7 + 
    44 Sqrt[15] x4 x6 y5 y7 - 306 x5 x7 y5 y7 + 90 x1 x3 y6 y7 + 
    90 x2 x4 y6 y7 - 44 Sqrt[15] x4 x5 y6 y7 - 
    44 Sqrt[15] x3 x6 y6 y7 + 306 x6 x7 y6 y7 + 45 x1^2 y7^2 + 
    45 x2^2 y7^2 + 90 x3^2 y7^2 + 90 x4^2 y7^2 + 81 x5^2 y7^2 + 
    81 x6^2 y7^2 + 90 x7^2 y7^2), 
 1/225 (5 Sqrt[15] x4 x5 y1 y3 + 5 Sqrt[15] x3 x6 y1 y3 - 
    45 x6 x7 y1 y3 + 5 Sqrt[15] x3 x5 y2 y3 - 
    5 Sqrt[15] x4 x6 y2 y3 + 45 x5 x7 y2 y3 - 
    5 Sqrt[15] x3 x5 y1 y4 + 5 Sqrt[15] x4 x6 y1 y4 - 
    45 x5 x7 y1 y4 + 5 Sqrt[15] x4 x5 y2 y4 + 
    5 Sqrt[15] x3 x6 y2 y4 - 45 x6 x7 y2 y4 + 
    5 Sqrt[15] x2 x3 y3 y5 - 5 Sqrt[15] x1 x4 y3 y5 + 
    90 x3 x5 y3 y5 + 45 x2 x7 y3 y5 + 22 Sqrt[15] x5 x7 y3 y5 + 
    5 Sqrt[15] x1 x3 y4 y5 + 5 Sqrt[15] x2 x4 y4 y5 - 
    90 x4 x5 y4 y5 + 45 x1 x7 y4 y5 + 22 Sqrt[15] x6 x7 y4 y5 + 
    5 Sqrt[15] x1 x3 y3 y6 + 5 Sqrt[15] x2 x4 y3 y6 - 
    90 x3 x6 y3 y6 - 45 x1 x7 y3 y6 + 22 Sqrt[15] x6 x7 y3 y6 - 
    5 Sqrt[15] x2 x3 y4 y6 + 5 Sqrt[15] x1 x4 y4 y6 + 
    90 x4 x6 y4 y6 + 45 x2 x7 y4 y6 - 22 Sqrt[15] x5 x7 y4 y6 + 
    45 x4 x5 y1 y7 - 45 x3 x6 y1 y7 - 45 x1 x7 y1 y7 + 
    45 x3 x5 y2 y7 + 45 x4 x6 y2 y7 + 45 x2 x7 y2 y7 + 
    45 x2 x3 y5 y7 - 45 x1 x4 y5 y7 + 22 Sqrt[15] x3 x5 y5 y7 - 
    22 Sqrt[15] x4 x6 y5 y7 + 153 x5 x7 y5 y7 - 45 x1 x3 y6 y7 - 
    45 x2 x4 y6 y7 + 22 Sqrt[15] x4 x5 y6 y7 + 
    22 Sqrt[15] x3 x6 y6 y7 - 153 x6 x7 y6 y7), 
 4/225 (75 x2 x4 y1 y3 - 15 Sqrt[15] x4 x5 y1 y3 - 
    15 Sqrt[15] x3 x6 y1 y3 + 60 x6 x7 y1 y3 + 75 x1 x4 y2 y3 - 
    15 Sqrt[15] x3 x5 y2 y3 + 15 Sqrt[15] x4 x6 y2 y3 - 
    60 x5 x7 y2 y3 - 25 x3^2 y3^2 - 25 x4^2 y3^2 - 20 x5^2 y3^2 - 
    20 x6^2 y3^2 - 15 x7^2 y3^2 + 75 x2 x3 y1 y4 + 
    15 Sqrt[15] x3 x5 y1 y4 - 15 Sqrt[15] x4 x6 y1 y4 + 
    60 x5 x7 y1 y4 + 75 x1 x3 y2 y4 - 15 Sqrt[15] x4 x5 y2 y4 - 
    15 Sqrt[15] x3 x6 y2 y4 + 60 x6 x7 y2 y4 - 25 x3^2 y4^2 - 
    25 x4^2 y4^2 - 20 x5^2 y4^2 - 20 x6^2 y4^2 - 15 x7^2 y4^2 + 
    30 x1 x5 y1 y5 - 30 x2 x6 y1 y5 + 4 Sqrt[15] x5 x6 y1 y5 - 
    30 x4 x7 y1 y5 - 30 x2 x5 y2 y5 - 2 Sqrt[15] x5^2 y2 y5 - 
    30 x1 x6 y2 y5 + 2 Sqrt[15] x6^2 y2 y5 - 30 x3 x7 y2 y5 - 
    15 Sqrt[15] x2 x3 y3 y5 + 15 Sqrt[15] x1 x4 y3 y5 - 
    50 x3 x5 y3 y5 + 65 x4 x6 y3 y5 - 24 Sqrt[15] x5 x7 y3 y5 - 
    15 Sqrt[15] x1 x3 y4 y5 - 15 Sqrt[15] x2 x4 y4 y5 + 
    50 x4 x5 y4 y5 + 65 x3 x6 y4 y5 - 24 Sqrt[15] x6 x7 y4 y5 - 
    20 x3^2 y5^2 - 20 x4^2 y5^2 - 2 Sqrt[15] x2 x5 y5^2 - 
    42 x5^2 y5^2 - 2 Sqrt[15] x1 x6 y5^2 - 6 x6^2 y5^2 - 
    10 Sqrt[15] x3 x7 y5^2 - 24 x7^2 y5^2 - 30 x2 x5 y1 y6 - 
    2 Sqrt[15] x5^2 y1 y6 - 30 x1 x6 y1 y6 + 2 Sqrt[15] x6^2 y1 y6 - 
    30 x3 x7 y1 y6 - 30 x1 x5 y2 y6 + 30 x2 x6 y2 y6 - 
    4 Sqrt[15] x5 x6 y2 y6 + 30 x4 x7 y2 y6 - 
    15 Sqrt[15] x1 x3 y3 y6 - 15 Sqrt[15] x2 x4 y3 y6 + 
    65 x4 x5 y3 y6 + 50 x3 x6 y3 y6 - 24 Sqrt[15] x6 x7 y3 y6 + 
    15 Sqrt[15] x2 x3 y4 y6 - 15 Sqrt[15] x1 x4 y4 y6 + 
    65 x3 x5 y4 y6 - 50 x4 x6 y4 y6 + 24 Sqrt[15] x5 x7 y4 y6 + 
    4 Sqrt[15] x1 x5 y5 y6 - 4 Sqrt[15] x2 x6 y5 y6 + 
    72 x5 x6 y5 y6 - 20 Sqrt[15] x4 x7 y5 y6 - 20 x3^2 y6^2 - 
    20 x4^2 y6^2 + 2 Sqrt[15] x2 x5 y6^2 - 6 x5^2 y6^2 + 
    2 Sqrt[15] x1 x6 y6^2 - 42 x6^2 y6^2 + 10 Sqrt[15] x3 x7 y6^2 - 
    24 x7^2 y6^2 - 45 x1 x7 y1 y7 + 45 x2 x7 y2 y7 - 30 x2 x5 y3 y7 - 
    10 Sqrt[15] x5^2 y3 y7 - 30 x1 x6 y3 y7 + 
    10 Sqrt[15] x6^2 y3 y7 - 90 x3 x7 y3 y7 - 30 x1 x5 y4 y7 + 
    30 x2 x6 y4 y7 - 20 Sqrt[15] x5 x6 y4 y7 + 90 x4 x7 y4 y7 - 
    60 x2 x3 y5 y7 + 60 x1 x4 y5 y7 - 24 Sqrt[15] x3 x5 y5 y7 + 
    24 Sqrt[15] x4 x6 y5 y7 - 147 x5 x7 y5 y7 + 60 x1 x3 y6 y7 + 
    60 x2 x4 y6 y7 - 24 Sqrt[15] x4 x5 y6 y7 - 
    24 Sqrt[15] x3 x6 y6 y7 + 147 x6 x7 y6 y7 - 15 x3^2 y7^2 - 
    15 x4^2 y7^2 - 24 x5^2 y7^2 - 24 x6^2 y7^2 - 27 x7^2 y7^2), -(2/
   225) (25 x3^2 y3^2 + 25 x4^2 y3^2 - 15 x7^2 y3^2 + 25 x3^2 y4^2 + 
    25 x4^2 y4^2 - 15 x7^2 y4^2 + 16 Sqrt[15] x5 x6 y1 y5 - 
    60 x4 x7 y1 y5 - 8 Sqrt[15] x5^2 y2 y5 + 8 Sqrt[15] x6^2 y2 y5 - 
    60 x3 x7 y2 y5 - 8 Sqrt[15] x2 x5 y5^2 - 16 x5^2 y5^2 - 
    8 Sqrt[15] x1 x6 y5^2 - 16 x6^2 y5^2 - 4 Sqrt[15] x3 x7 y5^2 - 
    24 x7^2 y5^2 - 8 Sqrt[15] x5^2 y1 y6 + 8 Sqrt[15] x6^2 y1 y6 - 
    60 x3 x7 y1 y6 - 16 Sqrt[15] x5 x6 y2 y6 + 60 x4 x7 y2 y6 + 
    16 Sqrt[15] x1 x5 y5 y6 - 16 Sqrt[15] x2 x6 y5 y6 - 
    8 Sqrt[15] x4 x7 y5 y6 + 8 Sqrt[15] x2 x5 y6^2 - 16 x5^2 y6^2 + 
    8 Sqrt[15] x1 x6 y6^2 - 16 x6^2 y6^2 + 4 Sqrt[15] x3 x7 y6^2 - 
    24 x7^2 y6^2 - 60 x2 x5 y3 y7 - 4 Sqrt[15] x5^2 y3 y7 - 
    60 x1 x6 y3 y7 + 4 Sqrt[15] x6^2 y3 y7 - 60 x3 x7 y3 y7 - 
    60 x1 x5 y4 y7 + 60 x2 x6 y4 y7 - 8 Sqrt[15] x5 x6 y4 y7 + 
    60 x4 x7 y4 y7 - 15 x3^2 y7^2 - 15 x4^2 y7^2 - 24 x5^2 y7^2 - 
    24 x6^2 y7^2 - 27 x7^2 y7^2), 
 1/225 (75 x3^2 y3^2 - 25 x4^2 y3^2 + 20 Sqrt[15] x2 x5 y3^2 - 
    20 x5^2 y3^2 - 20 Sqrt[15] x1 x6 y3^2 - 20 x6^2 y3^2 - 
    45 x7^2 y3^2 - 200 x3 x4 y3 y4 + 40 Sqrt[15] x1 x5 y3 y4 + 
    40 Sqrt[15] x2 x6 y3 y4 - 25 x3^2 y4^2 + 75 x4^2 y4^2 - 
    20 Sqrt[15] x2 x5 y4^2 - 20 x5^2 y4^2 + 20 Sqrt[15] x1 x6 y4^2 - 
    20 x6^2 y4^2 - 45 x7^2 y4^2 + 40 Sqrt[15] x3 x4 y1 y5 - 
    120 x1 x5 y1 y5 - 120 x2 x6 y1 y5 + 20 Sqrt[15] x3^2 y2 y5 - 
    20 Sqrt[15] x4^2 y2 y5 + 120 x2 x5 y2 y5 - 120 x1 x6 y2 y5 - 
    20 x3^2 y5^2 - 20 x4^2 y5^2 - 40 x5^2 y5^2 - 72 x6^2 y5^2 + 
    8 Sqrt[15] x3 x7 y5^2 - 72 x7^2 y5^2 - 20 Sqrt[15] x3^2 y1 y6 + 
    20 Sqrt[15] x4^2 y1 y6 - 120 x2 x5 y1 y6 + 120 x1 x6 y1 y6 + 
    40 Sqrt[15] x3 x4 y2 y6 - 120 x1 x5 y2 y6 - 120 x2 x6 y2 y6 - 
    64 x5 x6 y5 y6 + 16 Sqrt[15] x4 x7 y5 y6 - 20 x3^2 y6^2 - 
    20 x4^2 y6^2 - 72 x5^2 y6^2 - 40 x6^2 y6^2 - 
    8 Sqrt[15] x3 x7 y6^2 - 72 x7^2 y6^2 + 8 Sqrt[15] x5^2 y3 y7 - 
    8 Sqrt[15] x6^2 y3 y7 + 60 x3 x7 y3 y7 + 
    16 Sqrt[15] x5 x6 y4 y7 - 60 x4 x7 y4 y7 - 45 x3^2 y7^2 - 
    45 x4^2 y7^2 - 72 x5^2 y7^2 - 72 x6^2 y7^2 - 81 x7^2 y7^2), -(2/
   225) (-30 x6 x7 y1 y3 + 30 x5 x7 y2 y3 + 25 x3^2 y3^2 - 
    25 x4^2 y3^2 + 10 Sqrt[15] x2 x5 y3^2 - 10 x5^2 y3^2 - 
    10 Sqrt[15] x1 x6 y3^2 - 10 x6^2 y3^2 - 15 x7^2 y3^2 - 
    30 x5 x7 y1 y4 - 30 x6 x7 y2 y4 - 100 x3 x4 y3 y4 + 
    20 Sqrt[15] x1 x5 y3 y4 + 20 Sqrt[15] x2 x6 y3 y4 - 
    25 x3^2 y4^2 + 25 x4^2 y4^2 - 10 Sqrt[15] x2 x5 y4^2 - 
    10 x5^2 y4^2 + 10 Sqrt[15] x1 x6 y4^2 - 10 x6^2 y4^2 - 
    15 x7^2 y4^2 + 20 Sqrt[15] x3 x4 y1 y5 - 90 x1 x5 y1 y5 - 
    30 x2 x6 y1 y5 + 4 Sqrt[15] x5 x6 y1 y5 + 
    10 Sqrt[15] x3^2 y2 y5 - 10 Sqrt[15] x4^2 y2 y5 + 
    90 x2 x5 y2 y5 - 2 Sqrt[15] x5^2 y2 y5 - 30 x1 x6 y2 y5 + 
    2 Sqrt[15] x6^2 y2 y5 + 50 x4 x6 y3 y5 + 75 x2 x7 y3 y5 + 
    25 Sqrt[15] x5 x7 y3 y5 + 50 x3 x6 y4 y5 + 75 x1 x7 y4 y5 + 
    25 Sqrt[15] x6 x7 y4 y5 - 10 x3^2 y5^2 - 10 x4^2 y5^2 - 
    2 Sqrt[15] x2 x5 y5^2 - 18 x5^2 y5^2 - 2 Sqrt[15] x1 x6 y5^2 + 
    26 x6^2 y5^2 - 12 Sqrt[15] x3 x7 y5^2 + 12 x7^2 y5^2 - 
    10 Sqrt[15] x3^2 y1 y6 + 10 Sqrt[15] x4^2 y1 y6 - 
    30 x2 x5 y1 y6 - 2 Sqrt[15] x5^2 y1 y6 + 90 x1 x6 y1 y6 + 
    2 Sqrt[15] x6^2 y1 y6 + 20 Sqrt[15] x3 x4 y2 y6 - 
    30 x1 x5 y2 y6 - 90 x2 x6 y2 y6 - 4 Sqrt[15] x5 x6 y2 y6 + 
    50 x4 x5 y3 y6 - 75 x1 x7 y3 y6 + 25 Sqrt[15] x6 x7 y3 y6 + 
    50 x3 x5 y4 y6 + 75 x2 x7 y4 y6 - 25 Sqrt[15] x5 x7 y4 y6 + 
    4 Sqrt[15] x1 x5 y5 y6 - 4 Sqrt[15] x2 x6 y5 y6 + 
    88 x5 x6 y5 y6 - 24 Sqrt[15] x4 x7 y5 y6 - 10 x3^2 y6^2 - 
    10 x4^2 y6^2 + 2 Sqrt[15] x2 x5 y6^2 + 26 x5^2 y6^2 + 
    2 Sqrt[15] x1 x6 y6^2 - 18 x6^2 y6^2 + 12 Sqrt[15] x3 x7 y6^2 + 
    12 x7^2 y6^2 + 75 x4 x5 y1 y7 - 75 x3 x6 y1 y7 - 45 x1 x7 y1 y7 + 
    75 x3 x5 y2 y7 + 75 x4 x6 y2 y7 + 45 x2 x7 y2 y7 - 
    12 Sqrt[15] x5^2 y3 y7 + 12 Sqrt[15] x6^2 y3 y7 - 
    90 x3 x7 y3 y7 - 24 Sqrt[15] x5 x6 y4 y7 + 90 x4 x7 y4 y7 + 
    30 x2 x3 y5 y7 - 30 x1 x4 y5 y7 + 25 Sqrt[15] x3 x5 y5 y7 - 
    25 Sqrt[15] x4 x6 y5 y7 + 93 x5 x7 y5 y7 - 30 x1 x3 y6 y7 - 
    30 x2 x4 y6 y7 + 25 Sqrt[15] x4 x5 y6 y7 + 
    25 Sqrt[15] x3 x6 y6 y7 - 93 x6 x7 y6 y7 - 15 x3^2 y7^2 - 
    15 x4^2 y7^2 + 12 x5^2 y7^2 + 12 x6^2 y7^2 + 27 x7^2 y7^2), 
 8/25 (10 x3 x5 y3 y5 - 10 x4 x5 y4 y5 - 10 x3 x6 y3 y6 + 
    10 x4 x6 y4 y6 - 5 x1 x7 y1 y7 + 5 x2 x7 y2 y7 + 7 x5 x7 y5 y7 - 
    7 x6 x7 y6 y7), 
 1/450 (-125 x3^2 y3^2 - 25 x4^2 y3^2 - 20 Sqrt[15] x2 x5 y3^2 + 
    260 x5^2 y3^2 + 20 Sqrt[15] x1 x6 y3^2 + 260 x6^2 y3^2 + 
    435 x7^2 y3^2 + 200 x3 x4 y3 y4 - 40 Sqrt[15] x1 x5 y3 y4 - 
    40 Sqrt[15] x2 x6 y3 y4 - 25 x3^2 y4^2 - 125 x4^2 y4^2 + 
    20 Sqrt[15] x2 x5 y4^2 + 260 x5^2 y4^2 - 20 Sqrt[15] x1 x6 y4^2 + 
    260 x6^2 y4^2 + 435 x7^2 y4^2 - 40 Sqrt[15] x3 x4 y1 y5 + 
    240 x2 x6 y1 y5 + 16 Sqrt[15] x5 x6 y1 y5 - 
    20 Sqrt[15] x3^2 y2 y5 + 20 Sqrt[15] x4^2 y2 y5 - 
    8 Sqrt[15] x5^2 y2 y5 + 240 x1 x6 y2 y5 + 8 Sqrt[15] x6^2 y2 y5 - 
    240 x3 x5 y3 y5 + 240 x4 x6 y3 y5 + 360 x2 x7 y3 y5 + 
    72 Sqrt[15] x5 x7 y3 y5 + 240 x4 x5 y4 y5 + 240 x3 x6 y4 y5 + 
    360 x1 x7 y4 y5 + 72 Sqrt[15] x6 x7 y4 y5 + 260 x3^2 y5^2 + 
    260 x4^2 y5^2 - 8 Sqrt[15] x2 x5 y5^2 + 432 x5^2 y5^2 - 
    8 Sqrt[15] x1 x6 y5^2 + 1088 x6^2 y5^2 - 
    168 Sqrt[15] x3 x7 y5^2 + 984 x7^2 y5^2 + 
    20 Sqrt[15] x3^2 y1 y6 - 20 Sqrt[15] x4^2 y1 y6 + 
    240 x2 x5 y1 y6 - 8 Sqrt[15] x5^2 y1 y6 + 8 Sqrt[15] x6^2 y1 y6 - 
    40 Sqrt[15] x3 x4 y2 y6 + 240 x1 x5 y2 y6 - 
    16 Sqrt[15] x5 x6 y2 y6 + 240 x4 x5 y3 y6 + 240 x3 x6 y3 y6 - 
    360 x1 x7 y3 y6 + 72 Sqrt[15] x6 x7 y3 y6 + 240 x3 x5 y4 y6 - 
    240 x4 x6 y4 y6 + 360 x2 x7 y4 y6 - 72 Sqrt[15] x5 x7 y4 y6 + 
    16 Sqrt[15] x1 x5 y5 y6 - 16 Sqrt[15] x2 x6 y5 y6 + 
    1312 x5 x6 y5 y6 - 336 Sqrt[15] x4 x7 y5 y6 + 260 x3^2 y6^2 + 
    260 x4^2 y6^2 + 8 Sqrt[15] x2 x5 y6^2 + 1088 x5^2 y6^2 + 
    8 Sqrt[15] x1 x6 y6^2 + 432 x6^2 y6^2 + 168 Sqrt[15] x3 x7 y6^2 + 
    984 x7^2 y6^2 + 360 x4 x5 y1 y7 - 360 x3 x6 y1 y7 + 
    360 x3 x5 y2 y7 + 360 x4 x6 y2 y7 - 168 Sqrt[15] x5^2 y3 y7 + 
    168 Sqrt[15] x6^2 y3 y7 - 1260 x3 x7 y3 y7 - 
    336 Sqrt[15] x5 x6 y4 y7 + 1260 x4 x7 y4 y7 + 
    72 Sqrt[15] x3 x5 y5 y7 - 72 Sqrt[15] x4 x6 y5 y7 + 
    144 x5 x7 y5 y7 + 72 Sqrt[15] x4 x5 y6 y7 + 
    72 Sqrt[15] x3 x6 y6 y7 - 144 x6 x7 y6 y7 + 435 x3^2 y7^2 + 
    435 x4^2 y7^2 + 984 x5^2 y7^2 + 984 x6^2 y7^2 + 1215 x7^2 y7^2), 
 4/225 (25 x3^2 y3^2 + 25 x4^2 y3^2 - 50 x5^2 y3^2 - 50 x6^2 y3^2 - 
    90 x7^2 y3^2 + 25 x3^2 y4^2 + 25 x4^2 y4^2 - 50 x5^2 y4^2 - 
    50 x6^2 y4^2 - 90 x7^2 y4^2 + 80 x3 x5 y3 y5 - 80 x4 x6 y3 y5 - 
    90 x2 x7 y3 y5 - 6 Sqrt[15] x5 x7 y3 y5 - 80 x4 x5 y4 y5 - 
    80 x3 x6 y4 y5 - 90 x1 x7 y4 y5 - 6 Sqrt[15] x6 x7 y4 y5 - 
    50 x3^2 y5^2 - 50 x4^2 y5^2 - 80 x5^2 y5^2 - 224 x6^2 y5^2 + 
    36 Sqrt[15] x3 x7 y5^2 - 198 x7^2 y5^2 - 80 x4 x5 y3 y6 - 
    80 x3 x6 y3 y6 + 90 x1 x7 y3 y6 - 6 Sqrt[15] x6 x7 y3 y6 - 
    80 x3 x5 y4 y6 + 80 x4 x6 y4 y6 - 90 x2 x7 y4 y6 + 
    6 Sqrt[15] x5 x7 y4 y6 - 288 x5 x6 y5 y6 + 
    72 Sqrt[15] x4 x7 y5 y6 - 50 x3^2 y6^2 - 50 x4^2 y6^2 - 
    224 x5^2 y6^2 - 80 x6^2 y6^2 - 36 Sqrt[15] x3 x7 y6^2 - 
    198 x7^2 y6^2 - 90 x4 x5 y1 y7 + 90 x3 x6 y1 y7 - 
    90 x3 x5 y2 y7 - 90 x4 x6 y2 y7 + 36 Sqrt[15] x5^2 y3 y7 - 
    36 Sqrt[15] x6^2 y3 y7 + 270 x3 x7 y3 y7 + 
    72 Sqrt[15] x5 x6 y4 y7 - 270 x4 x7 y4 y7 - 
    6 Sqrt[15] x3 x5 y5 y7 + 6 Sqrt[15] x4 x6 y5 y7 + 
    72 x5 x7 y5 y7 - 6 Sqrt[15] x4 x5 y6 y7 - 
    6 Sqrt[15] x3 x6 y6 y7 - 72 x6 x7 y6 y7 - 90 x3^2 y7^2 - 
    90 x4^2 y7^2 - 198 x5^2 y7^2 - 198 x6^2 y7^2 - 243 x7^2 y7^2), -(
   2/225) (25 x3^2 y3^2 + 25 x4^2 y3^2 + 40 x5^2 y3^2 + 
    40 x6^2 y3^2 + 45 x7^2 y3^2 + 25 x3^2 y4^2 + 25 x4^2 y4^2 + 
    40 x5^2 y4^2 + 40 x6^2 y4^2 + 45 x7^2 y4^2 + 40 x3 x5 y3 y5 - 
    40 x4 x6 y3 y5 + 24 Sqrt[15] x5 x7 y3 y5 - 40 x4 x5 y4 y5 - 
    40 x3 x6 y4 y5 + 24 Sqrt[15] x6 x7 y4 y5 + 40 x3^2 y5^2 + 
    40 x4^2 y5^2 + 64 x5^2 y5^2 + 64 x6^2 y5^2 + 72 x7^2 y5^2 - 
    40 x4 x5 y3 y6 - 40 x3 x6 y3 y6 + 24 Sqrt[15] x6 x7 y3 y6 - 
    40 x3 x5 y4 y6 + 40 x4 x6 y4 y6 - 24 Sqrt[15] x5 x7 y4 y6 + 
    40 x3^2 y6^2 + 40 x4^2 y6^2 + 64 x5^2 y6^2 + 64 x6^2 y6^2 + 
    72 x7^2 y6^2 + 24 Sqrt[15] x3 x5 y5 y7 - 
    24 Sqrt[15] x4 x6 y5 y7 + 216 x5 x7 y5 y7 + 
    24 Sqrt[15] x4 x5 y6 y7 + 24 Sqrt[15] x3 x6 y6 y7 - 
    216 x6 x7 y6 y7 + 45 x3^2 y7^2 + 45 x4^2 y7^2 + 72 x5^2 y7^2 + 
    72 x6^2 y7^2 + 81 x7^2 y7^2)};

Now we use quantifier elimination on an appropriate quantified formula to see if restrictions apply. We allow for equality to zero.

vars = Variables[func];
avars = Array[a, Length[func]];

Timing[
 result = Resolve[
   Exists[Evaluate@avars, ForAll[vars, func.avars >= 0]]]]

(* Out[354]= {51.4219, (x1 | x2 | x3 | x4 | x5 | x6 | x7 | y1 | y2 | y3 |
     y4 | y5 | y6 | y7) \[Element] Reals} *)

So the weak inequality can always be satisfied. (But don't ask me why Evaluate was needed, I have no idea.)

We can try to remove the weak inequalities, by specifying that one component of the function have absolute value at least unity. I was not able to make this work in one fell swoop so instead broke into all possible cases. It turns out that the first twelve can be handled but not the thirteenth.

Timing[result = 
  Table[{Resolve[
     Exists[Evaluate@avars, 
      ForAll[vars, func[[j]] >= 1, func.avars > 0]]],
    Resolve[
     Exists[Evaluate@avars, 
      ForAll[vars, func[[j]] <= -1, func.avars > 0]]]}, {j, 
    Length[func]}];]

(* Out[68]={385.352, Null} *)

Union[result[[1 ;; 12]]]

(* Out[76]= {{(x1 | x2 | x3 | x4 | x5 | x6 | x7 | y1 | y2 | y3 | y4 | 
     y5 | y6 | y7) \[Element] 
   Reals, (x1 | x2 | x3 | x4 | x5 | x6 | x7 | y1 | y2 | y3 | y4 | y5 |
      y6 | y7) \[Element] Reals}} *)

The last one returns essentially unevaluated. I do not know what is the issue there.

$\endgroup$
  • $\begingroup$ Thank you very much for this post. I have learnt commands that I didn't know. I have to think about what you have done. Just one question. The command Resolve[Exists[Evaluate@avars, ForAll[vars, func.avars >= 0]]] checks if there exists values of avars such that the inequalities are satisfied for any value of vars? $\endgroup$ – apt45 Nov 11 '18 at 22:21
  • $\begingroup$ BTW the command Timing[result = Resolve[Exists[Evaluate@avars, ForAll[vars, func.avars > 0]]]] with the strong inequality gives me back a result. Does this mean that there are indeed solutions? $\endgroup$ – apt45 Nov 11 '18 at 22:28
  • $\begingroup$ Yes to the question about resolve[Exists[...]]. As for the second, based on the conditions I am seeing, it appears that there are always solutions off a proper subvariety. If those conditions enforce that the function is not zero, then that means solutions always exist in the region of interest. $\endgroup$ – Daniel Lichtblau Nov 11 '18 at 23:13
  • $\begingroup$ What is the meaning of the output , say Out[76], in your post? $\endgroup$ – apt45 Nov 18 '18 at 14:19
  • 1
    $\begingroup$ I don't know, and I agree it is confusing. $\endgroup$ – Daniel Lichtblau Nov 18 '18 at 15:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.