Defining relations between functions in Mathematica

Question

I would like to find a way to implement the following in Mathematica:

---

Let $F$ be the set of real functions $f_1,f_2,\ldots f_n$. The function $\min$ is defined as follows...

$$\min F=f_i\iff \forall j.\lim_{x\to\infty}[f_i(x)-f_j(x)]\le0$$

Let $h:\Bbb{R}^2\to\Bbb{R}$ and $f,g:\Bbb{R}\to\Bbb{R}$. The relation $R_h$ is defined as follows...

$$R_h(f,g)\iff\exists x,y.\forall z>y. h(\min\{f,g\}(z),x)>\max\{f,g\}(z)$$

---

For the first of these, I've opted to define a binary operator FuncLess which behaves for functions much the same way as <= for numbers:

FuncLess[f_,g_]:=Limit[f[x]-g[x],x->Infinity]<=0

This seemed more practical to me since the minimum and maximum can be found using a loop, and I don't need to deal with the 'forall'. Still, if there's a more efficient way to do this, I would like to know.

For the second relation, $R_h$, I'm not sure what to do. I tried inputting the expression as-is:

FuncR[h_][f_,g_]:=
    If[
        FuncLess[f,g],
        Exists[{x,y},ForAll[z,z>y,h[f[z],x]>g[z]]],
        Exists[{x,y},ForAll[z,z>y,h[g[z],x]>f[z]]]
    ]

but this proved ineffective. I'm not sure how Mathematica evaluates quantifiers, but I imagine that I'm not using them correctly.

Example

In[31]:= f[x_]:=x^2

In[32]:= g[x_]:=x^3

In[33]:= h[x_,y_]:=x^y

In[34]:= FuncLess[f,g]

Out[34]= True

Ideally, I want FuncR[h,f,g] to return True, but it only returns the expression. I've tried using Reduce[FuncR[h,f,g],{x,y,z},Reals], but this returns the message:

Reduce: This system cannot be solved with the methods available to Reduce

Answer 1

Maybe you can use AsymptoticGreater/AsymptoticLess:

FuncR[h_][f_,g_] := Switch[AsymptoticLess[f[x],g[x],x->Infinity],
    True,
    AsymptoticGreater[h[f[z],x], g[z],z->Infinity],

    False,
    AsymptoticGreater[h[g[z],x], f[z],z->Infinity],

    _,
    Indeterminate
]

For your example:

f[x_] := x^2
g[x_] := x^3
h[x_,y_] := x^y

FuncR[h][f, g]

ConditionalExpression[True, x > 3/2]