# Why does this boolean computation get stuck?

I want to build a boolean function which takes three one-parametric functions. I really don't know how to write a function for this, but this seems to be working for me as long as the parameter is t.

isCorrect[f1_, f2_, f3_] := Assuming[t >= 0, Refine[If[
1 + f1 + f2 + f3 >= 0 &&
1 + f1 - f2 - f3 >= 0 &&
1 - f1 + f2 - f3 >= 0 &&
1 - f1 - f2 + f3 >= 0, True, False]]]


For some functions it gives the correct value.

In[]:= isCorrect[Cos[t], Cos[t], 1]
Out[]= True


But for some examples like below it does not output anything.

In[]:= isCorrect[Exp[-t] Cos[t], Exp[-t], Exp[-t]]
Out[]= If[1 - 2 E^-t + E^-t Cos[t] >= 0, True, False]


But I know that Plot[1 - 2 E^-t + E^-t Cos[t], {t,0,10}] returns the following and is always non-negative for positive t. So I don't know why isCorrect does not output True then.

Any hints would be appreciated.

EDIT:

In[]:= Assuming[t >= 0, Reduce[1 - 2 E^-t + E^-t Cos[t] >= 0]]
Out[]:= Cos[t] \[Element] Reals && ((E^-t < 0 && Cos[t] <= E^t (-1 + 2 E^-t)) || E^-t == 0 || (E^-t > 0 && Cos[t] >= E^t (-1 + 2 E^-t)))


Why can't it figure out E^-t can't be negative ever. Also, Cos[t] is always real since t is explicitly assumed to be positive.

• I think Refine simply could not decide on the value of the expression. Reduce[1 - 2 E^-t + E^-t Cos[t] >= 0, t] can't also decide. So Refine returned the expression back. Help on Refine says gives the form of expr that would be obtained if symbols in it were replaced by explicit numerical expressions satisfying the assumptions assum – Nasser Mar 28 '20 at 7:09
• @Nasser So is there no function which would decide the value? – exp ikr Mar 28 '20 at 7:28
• I do not know. But for this one specific case, if you add one more conditions, then it can do it. Refine[If[1 - 2 E^-t + E^-t Cos[t] >= 0, True, False], t >= 0 && 1 >= 2 E^-t - E^-t Cos[t]] gives True. So I think your conditions you put there are not complete or may be need more refinement. I do not know why Reduce also can't do it. – Nasser Mar 28 '20 at 7:45
• Note that Assuming[] will not affect Reduce[], because Reduce[] does not have the Assumptions option. – J. M.'s torpor Mar 28 '20 at 12:12
• In:= Resolve[ ForAll[t, 0 <= t < 40 Pi, 1 - 2 E^-t + E^-t Cos[t] >= 0]] Out= True But if I replace 40Pi with Infinity then it returns unevaluated. Go figger. – Daniel Lichtblau Mar 28 '20 at 15:25

## 1 Answer

Clear["Global*"]


The If construct is unnecessary, and an optional variable designation can be included.

isCorrect[f1_, f2_, f3_, var : _Symbol : t] := Assuming[var >= 0,
Refine[1 + f1 + f2 + f3 >= 0 && 1 + f1 - f2 - f3 >= 0 &&
1 - f1 + f2 - f3 >= 0 && 1 - f1 - f2 + f3 >= 0]]

isCorrect[Cos[t], Cos[t], 1]

(* True *)


Using a different variable,

isCorrect[Cos[x], Cos[x], 1, x]

(* True *)


For the second example,

ex = isCorrect[Exp[-t] Cos[t], Exp[-t], Exp[-t]]

(* 1 - 2 E^-t + E^-t Cos[t] >= 0 *)


While neither Refine or Reduce resolves this expression, for this inequality you can use MinValue (Minimize).

MinValue[{ex[], t >= 0}, t] >= 0

(* True *)


Equivalently,

ex2 = ex // Simplify[#, t >= 0] &

(* E^t + Cos[t] >= 2 *)

MinValue[{ex2[], t >= 0}, t] >= 2

(* True *)

• Thanks. I rewrote the function isCorrect[f1_, f2_, f3_, var : _Symbol : t] := MinValue[{1 + f1 + f2 + f3, var >= 0}, var] >= 0 && MinValue[{1 + f1 - f2 - f3, var >= 0}, var] >= 0 && MinValue[{1 - f1 + f2 - f3, var >= 0}, var] >= 0 && MinValue[{1 - f1 - f2 + f3, var >= 0}, var] >= 0, (I don't know how to use MapThread for this). But, isCorrect[Exp[-t] Cos[t], Exp[-t], Exp[-t]] still does not resolve. Evaluating individually gives the correct answer. – exp ikr Mar 29 '20 at 5:58
• As you noted, If is not needed. Since >= will already return a Boolean value. – exp ikr Mar 29 '20 at 5:59