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.

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ Note that #>0 implies Reals $\endgroup$ Commented Dec 19, 2016 at 13:44
  • $\begingroup$ Thanks that will shorten my code - I just wanted to assure I had all conditions spelled out. $\endgroup$ Commented Dec 19, 2016 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$ Commented Dec 19, 2016 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$ Commented Dec 23, 2016 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$ Commented Dec 25, 2016 at 21:45

1 Answer 1

Reset to default
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 *)
Improve this answer
$\endgroup$
1
  • $\begingroup$ Interesting. I didn't know about resolve. I will try it when i get back to the lab. $\endgroup$ Commented Dec 25, 2016 at 21:51

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.