Say I want to define a function f
with 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.
ForAll
andResolve
? $\endgroup$f
, "local" assumptionf[y]>=2q
withq>0
and the statement I want to verify,f[y] >= q
, which I expected to turn intoTrue
.ForAll
andResolve
don't seem to fare any bettr. I hoped my example was minimalistic enough, I can add more if required. $\endgroup$f[x_] := Hold[E^(Log[p] x)]
as your equation, this seems to give the desired result. $\endgroup$