Why does this boolean computation get stuck?

Question

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.

Answer 1

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[[1]], t >= 0}, t] >= 0

(* True *)

Equivalently,

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

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

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

(* True *)