4
$\begingroup$

I have the following:

$Assumptions = {0 < Ijm1 < Ij < Ijp1 < 1, bpjm1 < 0, bpj < 0, 
bpjp1 < 0, Ijm1 \[Element] Reals, Ij \[Element] Reals, 
Ijp1 \[Element] Reals, bpjm1 \[Element] Reals, bjp \[Element] Reals,
bpjp1 \[Element] Reals};

x = (1 - bpjp1 Ijp1 + bpjp1 Ijp1^2) ;
y = bpj (Ij - Ijm1) (-1 + Ij (1 + bpjp1 (-1 + Ijp1)) - 
bpjp1 (-1 + Ijp1) Ijp1);

When checking inequalities I get

In[243]:= Simplify[x > 0]
Out[243]= True

In[244]:= Simplify[y > 0]
Out[244]= True

but

In[245]:= Simplify[x + y > 0]  
Out[245]= 
1 + bpjp1 (-1 + Ijp1) Ijp1 + 
bpj (Ij - Ijm1) (-1 + Ij (1 + bpjp1 (-1 + Ijp1)) - 
bpjp1 (-1 + Ijp1) Ijp1) > 0

Why?

$\endgroup$
  • 1
    $\begingroup$ Can you tell us your precise version of Mathematica and try again after restarting the kernel (Quit)? I get this. $\endgroup$ – Szabolcs Jun 15 '16 at 15:52
  • $\begingroup$ Aside from this: Simplify is not guaranteed to be able to perform the simplification. It uses heuristics to try to arrive to a simpler result. It may not be able to do it. If Simplify[expr > 0] returns as expr > 0, it does not mean that expr is not always positive. Usually, when Mathematica returns your input as-is, it means "I don't know". $\endgroup$ – Szabolcs Jun 15 '16 at 15:53
  • 1
    $\begingroup$ Mathematica version: 10.0.1.0, Student Edition, Linux x86. Restarting the kernel did not help. In my original post I had a wrong definition of y to which your computation refers, sorry about that. $\endgroup$ – U.T. Jun 15 '16 at 15:57
  • $\begingroup$ It won't fix this, but you should upgrade to at least 10.0.2, which fixed many bugs in 10.0.1. $\endgroup$ – Szabolcs Jun 15 '16 at 16:00
9
$\begingroup$

The assumptions mechanism used by Simplify has a bound on the number of variables in a system of nonlinear inequalities. If the number of variables exceeds the bound, the assumption mechanism does not attempt to decide whether the system has solutions. (Simplify proves that an inequality follows from the assumptions by showing that assumptions && Not[inequality] has no solutions.) The default value of the bound is 4, but it can be changed using a system option.

SetSystemOptions["SimplificationOptions"->{"AssumptionsMaxNonlinearVariables"->5}];

Simplify[x + y > 0]
True
$\endgroup$
  • $\begingroup$ Is that documented (other than here)? If so, where? If not, why not? $\endgroup$ – murray Jun 15 '16 at 21:57
  • $\begingroup$ Thanks! This works, but I noticed that the order in which one sets the system options and evaluates Simplify[x+y>0] matters. If I first evaluate Simplify[x+y>0], get the indeterminate result, then set the system options and try Simplify[x+y>0] again, I get x+z>0. If instead I set the system options before calling Simplify[x+y>0] for the first time, I get True. $\endgroup$ – U.T. Jun 16 '16 at 12:27
  • 1
    $\begingroup$ That would be a caching effect. Many internal uses of caching do not record the state of system options. ClearSystemCache[] and variants thereof will flush the earlier computed result(s) so you can redo the computation after altering the system option. $\endgroup$ – Daniel Lichtblau Jun 16 '16 at 15:14
2
$\begingroup$

This is not an answer, but here's some analysis of the issue which didn't fit in a comment.

First, let us rewrite your assumptions in a slightly different form:

asmp = And @@ {0 < Ijm1 < Ij < Ijp1 < 1, bpjm1 < 0, bpj < 0, 
    bpjp1 < 0, Ijm1 ∈ Reals, Ij ∈ Reals, 
    Ijp1 ∈ Reals, bpjm1 ∈ Reals, 
    bjp ∈ Reals, bpjp1 ∈ Reals};

Now let's play with Reduce:

Reduce[Implies[asmp, x > 0], Reals]
(* True *)

Reduce[Implies[asmp, y > 0], Reals]
(* True *)

All good so far. But what about this?

res = Reduce[Implies[asmp, x + y > 0], Reals]
(* Ij < 
  1 || (Ij == 
    1 && (Ijm1 <= 
      0 || (0 < Ijm1 < 1 && (Ijp1 < 1 || Ijp1 == 1 || Ijp1 > 1)) || 
     Ijm1 >= 1)) || Ij > 1 *)

What is strange about this result is that:

Reduce[Implies[asmp, res], Reals]
(* True *)

And also that

Reduce[Implies[Reduce[asmp], x + y > 0], Reals]
(* True *)

Also that it contains things like Ijp1 < 1 || Ijp1 == 1 || Ijp1 > 1, which are obviously True and that it contains Ijm1 <= 0 and Ij > 1, which contradict asmp so should be dropped.

Somehow Reduce doesn't seem to finish its job.

$\endgroup$

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.