1
$\begingroup$

I have the following code for simplifying an inequality:

glbcond =
  {0 < d1 < 1, d1 ∈ Reals, 0 < d2 < 1, d2 ∈ Reals, 
   0 < d3 < 1, d3 ∈ Reals, 0 < e1 < 1, e1 ∈ Reals, 
   0 < e2 < 1, e2 ∈ Reals, 0 < e3 < 1, e3 ∈ Reals, 
   0 < Hd < 1, Hd ∈ Reals, 0 < Hu < 1, Hu ∈ Reals, 
   0 < L1 < 1, L1 ∈ Reals, 0 < L2 < 1, L2 ∈ Reals, 
   0 < L3 < 1, L3 ∈ Reals, 0 < Q1 < 1, Q1 ∈ Reals, 
   0 < Q2 < 1, Q2 ∈ Reals, 0 < Q3 < 1, Q3 ∈ Reals, 
   0 < u1 < 1, u1 ∈ Reals, 0 < u2 < 1, u2 ∈ Reals, 
   0 < u3 < 1, u3 ∈ Reals};

z2cond = 
  Hd < Hu < L1 < L2 < L3 < Q1 < Q2 < Q3 < u1 < u2 < u3 < d1 < d2 < d3;

Simplify[Abs @ (Q1 u1)/(d2 Q3) < 1, (And @@ glbcond) && z2cond]

Q1 u1 < d2 Q3

However, if I turn up the SystemOptions as suggested by this related post here as

SetSystemOptions[
  "SimplificationOptions" -> "AssumptionsMaxNonlinearVariables" -> 14]

I get

Simplify[Abs[(Q1 u1)/(d2 Q3)] < 1, glbcond && z2cond]

True

So my question is, how exactly are the numbers of non-linear variables calculated? As far as I can see from my example, all the inequalities inside the argument for assumption are linear. Or does the calculation of number of non-linear variables involve both of the two arguments sitting inside Simplify?

This my first post on Mathematica.SE. I hope my post meets the site's posting conventions :)

$\endgroup$
  • $\begingroup$ The way I see it is that your rational/polynomial inequality is nonlinear and the 4 variables in it are related to each of the variables in z2cond. Thus {Abs[(Q1 u1)/(d2 Q3)] < 1, z2cond} form a nonlinear system, which has 14 variables. (The whole with glbcond has 17 variables, but the e1, e2, e3 components can be factored out as a direct product and treated as linear....But I don't know for sure that's how Mathematica approaches it.) $\endgroup$ – Michael E2 Jun 9 '17 at 18:31
  • $\begingroup$ Hi! I was wondering the same thing, but my question comes from these lines of codes In[43]:= SetSystemOptions["SimplificationOptions"->"AssumptionsMaxNonlinearVariables"->9]; ClearSystemCache[]; Simplify[Abs@((Hd Hu)/Q1)<1,glbcond&&z2cond] Out[45]= True, which now only requires "AssumptionsMaxNonlinearVariables"->9 $\endgroup$ – Y.X. Jun 10 '17 at 6:28
2
$\begingroup$

To simplify an inequality ineq to True using assumptions assum Simplify needs to prove that assum && Not[ineq] has no solutions. Hence non-linearity of both assum and ineq matter and all variables in assum and ineq are counted.

| improve this answer | |
$\endgroup$
  • $\begingroup$ Hi Adam, thank you for the answer! I see that both arguments of Simplify are counted for their non-linear variables. But in this particular case, why does it require 14 non-linear variables, since the rational function of ineq can always be converted a polynomial inequality, with all inequalities inside assum being linear? It would be helpful if some details can be given on this as I have quite a lot of similar inequalities that need similar simplification. :) $\endgroup$ – Y.X. Jun 9 '17 at 17:46
  • $\begingroup$ Simplify counts variables in the system for which it needs to decide the existence of solutions, that is assum && Not[ineq]. If the system is nonlinear (in any of the variables) then the number of all variables cannot exceed the value of "AssumptionsMaxNonlinearVariables". $\endgroup$ – Adam Strzebonski Jun 10 '17 at 1:26
  • $\begingroup$ So the non-linearity is introduced by the rational function (Q1 u1)/(d2 Q3) through substituting this into the inequalities in 14 variable expression of z2cond, as suggested by @Michael E2 in previous comments? If so, why is this particular codes requiring "AssumptionsMaxNonlinearVariables"->9:In[43]:= SetSystemOptions["SimplificationOptions"->"AssumptionsMaxNonlinearVariables"->9]; ClearSystemCache[]; Simplify[Abs@((Hd Hu)/Q1)<1,glbcond&&z2cond] Out[45]= True $\endgroup$ – Y.X. Jun 10 '17 at 6:24
  • $\begingroup$ Simplify splits z2cond into two-argument inequalities and it has a heuristic that attempts to select a subset of assumptions sufficient for the given simplification. In this case it must be finding a subset of assumptions that involves 9 variables and is sufficient to prove that ineq is true. $\endgroup$ – Adam Strzebonski Jun 11 '17 at 1:47

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.