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$
    – Feyre
    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$
    – bdecaf
    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$
    – Musang
    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$
    – Daniel Lichtblau
    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$
    – bdecaf
    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$
    – bdecaf
    Dec 25, 2016 at 21:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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