3
$\begingroup$

Trying to create a simple example I find I need a number of variables.

All my variables are Reals and greater 0. So I use

$Assumptions = Element[lab, Reals] && Element[q, Reals] && 
  Element[r, Reals] && Element[s, Reals] && Element[t, Reals] && 
  Element[u, Reals] &&  Element[v, Reals] && 
  lab > 0 && q > 0 && r > 0 && s > 0 && t > 0 &&  u > 0 && v > 0 && q < 1 

From an equation system I get lengthy solutions having terms like following and I am interested whether they are smaller 0.

My problem is to weed out the parts that are "obviously" true. So I actually obtain the following expressions as part of a larger expression.

(s (-1 + q - q u)) < 0 // Refine
lab (-1 + q) q u v < 0 // Refine

They instantly evaluate to True

But as things get more complex (here just summing the two expressions) - Simplify (or Refine) fail to find the simplification instantly (in the sense that they immediately give up).

(s (-1 + q - q u)) + lab (-1 + q) q u v < 0 // Refine

I found just if would delete the lab it would evaluate nicely. But since I have many much longer expressions this is not really an option to weed through the sub expressions manually.

All this calculations happen instantaneously and I could definitely live with Mathematica spending some minutes searching for this simplifications. So I am very open to any suggestions even if they strain my machine a bit.

Update

After a few days I also wrote to community.wolfram.com.

A user there suggested to use Simplify[Equivalent[$Assumptions, Reduce[$Assumptions && (s (-1 + q - q u)) + lab (-1 + q) q u v < 0]]] - which seems to do what I want.

I am not putting it as answer yet as I still am curious why Simplify doesn't catch this trivial case.

$\endgroup$
  • 3
    $\begingroup$ Note that #>0 implies Reals $\endgroup$ – Feyre Dec 19 '16 at 13:44
  • $\begingroup$ Thanks that will shorten my code - I just wanted to assure I had all conditions spelled out. $\endgroup$ – bdecaf Dec 19 '16 at 13:46
  • 3
    $\begingroup$ For those looking at this question, there are definitely some weird things going on here... Looking at the last code line provided in the OP, there's aq*u*v in the right term. If you take away u the Refine doesn't transform the expression, but if you remove the v instead it does: Refine[(s (-1 + q - q u)) + lab (-1 + q) q v < 0] gives True. More generally, you can remove the letter if it doesn't appear in the left term, so Refine[(s (-1 + q - q v)) + lab (-1 + q) q v < 0] does compute. Thus Mathematica seems to need some sort of factorization to be able to transform it. $\endgroup$ – Musang Dec 19 '16 at 15:36
  • $\begingroup$ Can use FindInstance on the reversed inequality to show it cannot be satisfied: FindInstance[(s (-1 + q - q u)) + lab (-1 + q) q u v >= 0 && lab > 0 && q > 0 && r > 0 && s > 0 && t > 0 && u > 0 && v > 0 && q < 1, {s, q, u, lab, v, r, s, t}] Out[464]= {}` $\endgroup$ – Daniel Lichtblau Dec 23 '16 at 18:45
  • $\begingroup$ It seems i didn't clearly explain - i'm having a more complex expression - imagine (u-v) multiplied with one of the terms above. And I am after a simplification to (u-v)>0 - if there is any. $\endgroup$ – bdecaf Dec 25 '16 at 21:45
4
$\begingroup$

To show this, cast it as a quantifier elimination problem and let Resolve do what its name implies.

Resolve[
 Exists[{s, q, u, lab, v, r, s, t}, 
  lab > 0 && q > 0 && r > 0 && s > 0 && t > 0 && u > 0 && v > 0 && 
   q < 1, (s (-1 + q - q u)) + lab (-1 + q) q u v < 0]]

(* Out[466]= True *)
$\endgroup$
  • $\begingroup$ Interesting. I didn't know about resolve. I will try it when i get back to the lab. $\endgroup$ – bdecaf Dec 25 '16 at 21:51

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.