# Simplify terms with delayed and immediate function definitions

Say I want to define a function fwith input x but also involving parameter p not yet specified:

f[x_] := p^x


Now I want to verify some inequalities with additional assumptions. A (hopefully) minimal example, showing my problem:

If, for some for input y in the function and for some paremeter value q>0, it holds that f[y] >= 2 q, then I would expect f[y] >= q to yield True.

However,

FullSimplify[f[y] >= q, {f[y] >= 2 q, q > 0}]


yields p^y >= q instead. Even if I add q \[Element] Reals as an assumption.

Do I overlook an obvious mathematical (non-Mathematica) issue, or how I can get Mathematica to "fully" simplify the expression? I have also looked at this issue with FullSimplify, but the solution provided did not help.

• Have you tried the functions ForAll and Resolve? May 13 '20 at 10:56
• I rather seek to verify whether for some specific (not all/arbitrary) values of the parameters certain statements hold true. So as in the example, I have a general function f, "local" assumption f[y]>=2q with q>0 and the statement I want to verify, f[y] >= q, which I expected to turn into True. ForAll and Resolve don't seem to fare any bettr. I hoped my example was minimalistic enough, I can add more if required. May 13 '20 at 11:21
• I am not sure how capable Mathematica is in solving these kind of analytical questions. It might also be due to the complexity of your function f. Try using f[x_] := Hold[E^(Log[p] x)] as your equation, this seems to give the desired result. May 13 '20 at 12:07

I am not certain that this is what you are looking for?

f[x_] := p^x
Reduce[f[x] > q && q > 0, p, Reals]


Visual:

With[
{f = p^x},
Manipulate[
Plot[{f, q}, {x, 0, 2}, Filling -> {1 -> {{2}, {Orange, Blue}}}],
{{p, 1/2}, -1, 1},
{{q, 1/2}, -4, 4}
]
]

• I am not so much interested in the requirements/ranges for the parameters for certain (in)equalities to be true (which, I presume, Reduce would give me to some extend), but rather in having local restrictions/assumptions on certain values, then trying to check how these simplify my computations. I.e. "if some statement x holds, can I then infer y"? So I would want to "reduce" w.r.t. all parameters, i.e. some sort of "simplifying". May 13 '20 at 10:28