How to figure out whether a nonlinear inequality holds or not

Question

I have an inequality consisted only of seven parameters as follows:

$(1 + g)^{-(m+w)}\big[\big\{a+(1-a)(1 + g)^m\big\}(1 + p q)Q - (1 + g)^w \big\{(1 + g)^m (1 + q)-(1-p)q\big\} Q\big] < 0$

Parameters, $g$, $w$, and $m$, are subject to the following restrictions:

$0<g$, $0<w$, $0<m$, $0<Q$

That is, these four parameters are all positive.

Now, we can manually verify that this inequality holds under the above parameter restrictions. And I would like to confirm this with Mathematica.

My codes for the assumptions:

$Assumptions = 0 < g && 0 < w && 0 < m && 0 < Q

And as for checking if the inequality holds, I used Refine and If as follows:

Refine[If[(1 + g)^(-m - w) ((a - (-1 + a) (1 + g)^m) (1 + p q) Q - (1 + g)^w ((-1 + p) q + (1 + g)^m (1 + q)) Q)<0, Print[True], Print[False]]]

Since the condition is true, the result I expect is True. But what I get is a simple repetition of the If bracket:

If[(1 + g)^(-m - w) ((a - (-1 + a) (1 + g)^m) (1 + p q) Q - (1 + g)^w ((-1 + p) q + (1 + g)^m (1 + q)) Q) < 0, Print[Yes], Print[No]]

When I use a little simpler, but similar, type of inequality, it gives me either True or False depending on the specific form of inequality I use. But it seems Mathematica is not able to figure out whether the above inequality, which is too complex (maybe?), is true or false.

Or am I missing something? Can anyone help? Thank you so much.

Answer 1

I would recommend using Reduce instead of Refine. Also, you might as well cancel the factors (1+g)^(-m-w) and Q which are positive. Then, since g > 0 and m and w are independent positive real numbers, we may as well replace

{(1 + g)^m -> u, (1 + g)^w -> v}

to simplify its human readability. The conditions translate to u > 1 and v > 1. The inequality becomes

expr = ((a - (-1 + a) (1 + g)^m) (1 + p q) - (1 + g)^w ((-1 + p) q + (1 + g)^m (1 + q)))  /.
  {(1 + g)^m -> u, (1 + g)^w -> v}
(* (1 + p q) (a - (-1 + a) u) - ((-1 + p) q + (1 + q) u) v *)

Then we can use Reduce, with or without specifying the order of the variables.

Assuming[a > 0 && p > 0 && q > 0 && u > 1 && v > 1,
 Reduce[$Assumptions && expr < 0]
 ]
(*
  v > 1 && (
    (0 < a < 1 && (
       (1 < u <= (a - v)/(-1 + a) && p > 0 && q > 0) ||
       (u > (a - v)/(-1 + a) && (
          (0 < p <= (v - u v)/(-a - u + a u + v) && q > 0) ||
          (p > (v - u v)/(-a - u + a u + v) && 
             0 < q < (a + u - a u - u v)/(-a p - p u + a p u - v + p v + u v)))))
     ) ||
    (a >= 1 && u > 1 && p > 0 && q > 0))
*)

The order of the variables matters (because Reduce will return a cylindrical decomposition). You can play with it to see if one makes the problem clearer.

Assuming[a > 0 && p > 0 && q > 0 && u > 1 && v > 1,
 Reduce[$Assumptions && expr < 0, {p, q, a, u, v}]
 ]
(*
  (0 < p <= 1 && q > 0 && a > 0 && u > 1 && v > 1) ||
  (p > 1 && q > 0 && (
     (0 < a < (-q + p q)/(1 + p q) && u > 1 &&
          v > (a + a p q + u - a u + p q u - a p q u)/(-q + p q + u + q u)) ||
     (a >= (-q + p q)/(1 + p q) && u > 1 && v > 1)))
*)

One can also play with the alternative inequality to understand why it is not simply true or false.

Assuming[a > 0 && p > 0 && q > 0 && u > 1 && v > 1,
 red = Reduce[$Assumptions && expr > 0]
 ]
(*
  v > 1 && 0 < a < 1 && u > (a - v)/(-1 + a) && 
    p > (v - u v)/(-a - u + a u + v) && 
    q > (a + u - a u - u v)/(-a p - p u + a p u - v + p v + u v)
*)

Interpreting this, it says we can pick any v > 1 and 0 < a < 1. Let's do this and examine red:

red /. {v -> 2, a -> 1/2} // Simplify
(* u > 3 && 4 + p (-3 + u) > 4 u && 1 + q (4 + p (-3 + u) - 4 u) > 3 u *)

Now we can pick any u > 3:

red /. {v -> 2, a -> 1/2, u -> 4} // Simplify
(* p > 12 && q > 11/(-12 + p) *)

Next, pick p > 12:

red /. {v -> 2, a -> 1/2, u -> 4, p -> 13} // Simplify
(* q > 11 *)

And finally pick q > 12:

red /. {v -> 2, a -> 1/2, u -> 4, p -> 13, q -> 12} // Simplify
(* True *)

So the settings {v -> 2, a -> 1/2, u -> 4, p -> 13, q -> 12} make the expression positive:

expr /. {v -> 2, a -> 1/2, u -> 4, p -> 13, q -> 12}
(* 1/2 *)

Similarly one can find numbers that make the expression negative. @evanb has pointed some of this out in comments.